DeepSeek telah memperkenalkan DeepSeek-Prover-V2, model bahasa besar (LLM) sumber terbuka yang inovatif dan direka teliti untuk domain yang rumit iaitu pembuktian teorem formal dalam rangka kerja Lean 4. Model baharu ini memanfaatkan saluran pembuktian teorem rekursif, yang memanfaatkan kuasa model asas DeepSeek-V3 DeepSeek yang canggih. Lean 4, lelaran terbaru pembukti teorem Lean, adalah pembantu bukti interaktif yang dibangunkan oleh Microsoft Research. Bahasa pengaturcaraan berfungsi yang canggih ini dan sistem pembuktian teorem interaktif memperkasakan ahli matematik dan saintis komputer untuk membina bukti formal dengan pengesahan diperiksa mesin yang tiada tandingannya.
Projek ini menandakan langkah besar ke arah merapatkan jurang antara penaakulan matematik formal dan tidak formal. Dengan memanfaatkan keupayaan intrinsik LLM tujuan umum, ia bertujuan untuk menangani dengan berkesan domain pembuktian teorem formal yang sangat berstruktur. Pasukan penyelidik DeepSeek mengemukakan bahawa pendekatan inovatif mereka mencerminkan proses kognitif yang digunakan oleh ahli matematik manusia apabila membina bukti, dengan teliti membedah teorem kompleks kepada komponen yang lebih terkawal dan mudah difahami.
Memperluaskan Rangka Kerja Penilaian: Memperkenalkan ProverBench
Dalam langkah penting untuk meningkatkan ketelitian penyelidikan mereka, pasukan DeepSeek telah memperluaskan rangka kerja penilaian mereka dengan ketara dengan pengenalan ProverBench, koleksi penanda aras baharu yang direka khusus untuk penilaian komprehensif keupayaan pembuktian teorem formal. Koleksi komprehensif ini berfungsi sebagai sumber yang berharga untuk menilai prestasi LLM dalam konteks matematik formal.
"Di luar penanda aras konvensional, kami dengan bangga memperkenalkan ProverBench, koleksi 325 masalah formal yang disusun dengan teliti, untuk memperkaya proses penilaian kami. Koleksi ini merangkumi 15 masalah yang dipilih dengan teliti yang diperoleh terus daripada pertandingan Peperiksaan Matematik Jemputan Amerika (AIME) baru-baru ini, khususnya dari tahun 24-25," jelas para penyelidik.
Penyertaan masalah AIME dalam set data ProverBench amat ketara, kerana ia memperkenalkan satu set masalah matematik yang mencabar dan mantap yang diiktiraf secara meluas dalam komuniti matematik. Ini menyediakan asas yang standard dan teliti untuk menilai prestasi DeepSeek-Prover-V2 dan membandingkannya dengan pendekatan lain.
Hasil Awal yang Memberangsangkan: Menangani Masalah AIME
Hasil awal yang berpunca daripada ujian yang ketat ke atas masalah AIME yang mencabar ini telah mendedahkan prestasi yang sangat menjanjikan daripada model pembuktian teorem khusus mereka yang direka dengan teliti. Pasukan DeepSeek dengan bangganya melaporkan bahawa DeepSeek-Prover-V2 menunjukkan kehebatannya dengan berjaya menyelesaikan 6 daripada 15 masalah AIME yang dibentangkan kepadanya. Sebagai perbandingan, model DeepSeek-V3 tujuan umum, apabila menggunakan teknik pengundian majoriti, berjaya menyelesaikan 8 masalah.
Penemuan ini menyoroti potensi kedua-dua LLM khusus dan tujuan umum dalam menangani masalah matematik yang kompleks. Walaupun model tujuan umum mempamerkan kadar kejayaan yang sedikit lebih tinggi dalam penanda aras tertentu ini, model pembuktian teorem khusus menunjukkan kecekapan dalam penaakulan matematik formal.
Meniru Pembinaan Bukti Manusia: Pendekatan Rantaian Pemikiran
"Memandangkan cabaran yang didokumentasikan dengan baik yang sering dihadapi oleh model tujuan umum apabila cuba menghasilkan bukti Lean yang lengkap, kami secara strategik mengarahkan DeepSeek-V3 untuk menjana hanya lakaran bukti peringkat tinggi, dengan sengaja meninggalkan butiran rumit. Rantaian pemikiran yang terhasil memuncak dalam teorem Lean yang terdiri daripada urutan penyataan have, setiap satu disimpulkan dengan teliti dengan pemegang tempat sorry, yang secara berkesan menunjukkan submatlamat yang perlu diselesaikan. Pendekatan inovatif ini mencerminkan dengan elegan gaya pembinaan bukti manusia, di mana teorem kompleks dikurangkan secara berperingkat kepada urutan lema yang lebih mudah diurus," jelas pasukan DeepSeek.
Pendekatan inovatif penjanaan lakaran bukti peringkat tinggi ini sejajar dengan cara ahli matematik sering mendekati bukti yang kompleks. Dengan memfokuskan pada struktur keseluruhan dan langkah-langkah utama, model itu boleh membimbing dengan berkesan penghalusan dan penyelesaian bukti seterusnya.
Strategi Berkaedah: Menangani Setiap Komponen Bukti Secara Individu
Sistem ini kemudiannya menggunakan dengan teliti strategi berkaedah dan berstruktur untuk menangani setiap komponen bukti individu. Pendekatan sistematik ini memastikan setiap aspek bukti dipertimbangkan dengan teliti dan ditangani secara logik dan koheren. Sistem ini mewujudkan pendekatan yang sangat berstruktur untuk pembuktian teorem, membina hasil yang telah ditetapkan sebelum ini untuk memastikan asas yang kukuh untuk setiap langkah seterusnya.
"Dengan memanfaatkan submatlamat yang dijana oleh DeepSeek-V3, kami menggunakan strategi penyelesaian rekursif untuk menyelesaikan setiap langkah bukti perantaraan secara sistematik. Kami mengekstrak ungkapan submatlamat daripada penyataan have untuk menggantikannya dengan matlamat asal dalam masalah yang diberikan dan kemudian memasukkan submatlamat sebelumnya sebagai premis. Pembinaan ini membolehkan submatlamat berikutnya diselesaikan menggunakan hasil perantaraan langkah sebelumnya, dengan itu menggalakkan struktur pergantungan yang lebih setempat dan memudahkan pembangunan lema yang lebih mudah," jelas para penyelidik.
Strategi penyelesaian rekursif ialah aspek utama keupayaan sistem untuk mengendalikan bukti yang kompleks. Dengan memecahkan masalah kepada submatlamat yang lebih kecil dan lebih mudah diurus, sistem boleh menggunakan keupayaan penaakulannya dengan berkesan pada setiap komponen individu.
Mengoptimumkan Sumber Pengiraan: Model Parameter 7B Khusus
Untuk mengoptimumkan sumber pengiraan dengan berkesan dan memastikan pemprosesan yang cekap, sistem ini secara strategik menggunakan model parameter 7B yang lebih kecil dan sangat khusus untuk memproses lema yang diuraikan. Pendekatan ini adalah penting untuk menguruskan dengan berkesan permintaan pengiraan yang berkaitan dengan carian bukti yang meluas, memastikan sistem boleh beroperasi dengan cekap tanpa dibebani dengan kerumitan ruang carian. Pendekatan itu akhirnya memuncak dalam bukti lengkap yang diperolehi secara automatik apabila semua langkah yang diuraikan berjaya diselesaikan.
"Rangka kerja algoritma beroperasi dalam dua peringkat yang berbeza, memanfaatkan dua model pelengkap: DeepSeek-V3 untuk penguraian lema dan model pembukti 7B untuk melengkapkan butiran bukti formal yang sepadan," jelas para penyelidik.
Pendekatan dua peringkat ini membolehkan sistem memanfaatkan kekuatan kedua-dua model tujuan umum yang besar dan model khusus yang lebih kecil. Model besar digunakan untuk menjana lakaran bukti peringkat tinggi, manakala model yang lebih kecil digunakan untuk mengisi butiran dan melengkapkan bukti formal.
Mensintesis Data Penaakulan Formal: Laluan Semula Jadi
Seni bina yang direka dengan teliti ini mewujudkan dengan berkesan laluan semula jadi dan intuitif untuk mensintesis data penaakulan formal, dengan lancar menggabungkan penaakulan matematik peringkat tinggi dengan keperluan ketat dan ketat pengesahan formal. Penyepaduan ini adalah penting untuk memastikan kebolehpercayaan dan kebolehpercayaan hasil sistem.
"Kami menyusun subset masalah yang mencabar yang kekal tidak diselesaikan oleh model pembukti 7B secara menyeluruh, tetapi yang mana semua submatlamat yang diuraikan telah berjaya diselesaikan. Dengan mengarang bukti semua submatlamat, kami membina bukti formal lengkap untuk masalah asal," jelas para penyelidik.
Pendekatan ini membolehkan sistem belajar daripada kesilapannya dan meningkatkan keupayaannya untuk menyelesaikan masalah yang kompleks. Dengan mengenal pasti submatlamat tertentu yang menyebabkan kesukaran, sistem boleh menumpukan usahanya untuk meningkatkan prestasinya dalam bidang tersebut.
Kebimbangan dan Cabaran: Butiran Pelaksanaan Di Bawah Penelitian
Walaupun terdapat pencapaian teknikal yang tidak dapat dinafikan yang ditunjukkan oleh DeepSeek-Prover-V2, beberapa pakar dalam bidang ini telah menimbulkan kebimbangan yang berkaitan mengenai butiran pelaksanaan tertentu. Elliot Glazer, seorang ahli matematik Utama yang sangat dihormati di Epoch AI, telah menunjukkan potensi isu yang memerlukan siasatan lanjut.
Beberapa kebimbangan mengenai kertas DeepSeek-Prover-V2. Contoh yang mungkin diformalkan secara salah, dan perbincangan mengenai Lean zulip mencadangkan bukti PutnamBench adalah tidak masuk akal dan menggunakan sorry tersirat (kemungkinan tersembunyi dalam taktik apply?) yang tidak dilaporkan dalam gelung read-eval-print mereka.
Kebimbangan ini dengan jelas menyoroti cabaran berterusan yang wujud dalam ruang pengesahan formal, di mana walaupun butiran pelaksanaan yang paling kecil dan kelihatan tidak penting boleh memberi kesan yang tidak seimbang besar terhadap kesahihan dan kebolehpercayaan keseluruhan hasil. Proses pengesahan formal memerlukan perhatian yang tidak berbelah bahagi terhadap perincian dan pematuhan teliti terhadap piawaian yang ditetapkan.
Potensi contoh yang salah diformalkan dan kemungkinan taktik "sorry" tersembunyi dalam bukti PutnamBench menimbulkan soalan penting tentang ketelitian dan kesempurnaan proses pengesahan. Kebimbangan ini menggariskan keperluan untuk penelitian berterusan dan pengesahan bebas terhadap keputusan.
Ketersediaan dan Sumber: Mendemokrasikan Akses kepada Pembuktian Teorem Formal
DeepSeek telah menyediakan Prover-V2nya dalam dua saiz model yang berbeza, memenuhi pelbagai sumber pengiraan dan objektif penyelidikan. Versi pertama ialah model parameter 7B yang dibina berdasarkan Prover-V1.5-Base mereka sebelum ini, yang menampilkan panjang konteks yang dilanjutkan sehingga 32K token. Versi kedua ialah model parameter 671B yang jauh lebih besar yang dilatih pada DeepSeek-V3-Base. Kedua-dua model kini mudah diakses di HuggingFace, platform terkemuka untuk berkongsi dan bekerjasama dalam model pembelajaran mesin.
Selain model itu sendiri, DeepSeek juga telah menyediakan set data ProverBench penuh, yang mengandungi 325 masalah formal yang direka dengan teliti untuk tujuan penilaian, tersedia di HuggingFace. Set data komprehensif ini menyediakan penyelidik dan pembangun dengan sumber yang berharga untuk menilai prestasi model mereka dan membandingkannya dengan DeepSeek-Prover-V2.
Dengan menyediakan sumber ini secara percuma, DeepSeek sedang mendemokrasikan akses kepada teknologi pembuktian teorem formal dan memupuk kerjasama dalam komuniti penyelidikan. Pendekatan sumber terbuka ini berkemungkinan mempercepatkan kemajuan dalam bidang ini dan membawa kepada penemuan baharu dalam penaakulan dan pengesahan automatik.
Siaran ini memperkasakan penyelidik dan pembangun dengan sumber yang diperlukan untuk menyelidiki keupayaan dan batasan teknologi ini. Dengan menyediakan akses terbuka kepada model dan set data ProverBench, DeepSeek menggalakkan penerokaan lanjut dan usaha sama untuk menangani kebimbangan yang dibangkitkan oleh pakar dalam bidang ini. Pendekatan kerjasama ini memegang kunci untuk merungkai kerumitan pembuktian teorem formal dan mengukuhkan kebolehpercayaan kemajuan terobosan ini.