DeepSeek telah merilis model khusus bernama Prover-V2 di bidang pembuktian teorema matematika, yang bertujuan untuk membuktikan teorema matematika secara otomatis dalam sistem verifikasi formal Lean 4 menggunakan AI.
Mengapa arah ini penting?
Pembuktian teorema matematika adalah medan uji ekstrem bagi kemampuan AI. Matematika tidak menerima "hampir benar" — sebuah bukti harus sepenuhnya benar atau salah. Tidak ada yang namanya "bukti yang 95% benar."
Sistem verifikasi formal (seperti Lean 4) akan memeriksa setiap langkah penalaran logis seperti kompiler memeriksa sintaksis. Jika satu langkah salah, seluruh bukti akan gagal. Ini adalah ujian paling ketat bagi kemampuan penalaran logis AI.
Kinerja Prover-V2
Pada tolok ukur miniF2F, Prover-V2 mencapai hasil yang mendekati atau setara dengan yang terbaik saat ini. Metode yang digunakannya adalah dekomposisi sub-tujuan — memecah bukti kompleks menjadi serangkaian sub-tujuan yang lebih kecil dan menaklukkannya satu per satu.
Ini mirip dengan cara berpikir matematikawan manusia: ketika menghadapi masalah sulit, pertama-tama pikirkan "untuk membuktikan A, saya perlu membuktikan B dan C terlebih dahulu, dan untuk membuktikan B saya perlu memastikan D terlebih dahulu..."
Perbedaan dengan model penalaran umum
Model umum (GPT, Claude, Gemini) mengandalkan Chain-of-Thought untuk penalaran matematika — pada dasarnya "bernalar langkah demi langkah dalam bahasa alami." Cara ini efektif untuk masalah sederhana, tetapi bukti kompleks dapat dengan mudah mengalami celah logis di beberapa langkah.
Prover-V2 mengambil jalur formal, dengan setiap langkah diverifikasi oleh Lean 4. Keuntungannya adalah tidak ada "halusinasi"; kerugiannya adalah cakupan aplikasinya sangat sempit — hanya dapat bekerja dalam sistem formal.
Signifikansi
Pembuktian teorema matematika adalah arah yang tampaknya niche tetapi memiliki implikasi yang luas. Jika AI benar-benar dapat membuktikan teorema kompleks secara andal dalam sistem formal, maka AI dapat diterapkan ke serangkaian bidang kritis seperti verifikasi perangkat lunak, verifikasi perangkat keras, dan pembuktian kriptografi.
Investasi DeepSeek dalam arah ini menunjukkan bahwa mereka tidak hanya bersaing dalam tolok ukur model besar umum — tetapi juga serius membangun alat sains fundamental.
Sumber: CocoLoop, makalah DeepSeek Prover-V2