DeepSeek Prover-V2: Model AI Baru Ahli Matematika
infokilasan.com – Startup AI yang berbasis di Hangzhou, China, merilis versi terbaru dari model Prover mereka pada Rabu, 30 April 2025. Model ini, yang dinamakan DeepSeek-Prover-V2, dirancang secara khusus untuk menangani pembuktian teorema matematika formal dengan akurasi tinggi.
DeepSeek-Prover-V2 merupakan model bahasa besar (LLM) yang mengandalkan bahasa pemrograman Lean 4. Lean 4 memungkinkan model ini memeriksa logika dari setiap langkah pembuktian secara terpisah, memastikan konsistensi dan validitas hasil akhir.
Dengan pendekatan ini, Prover-V2 tidak hanya cocok untuk menyusun pembuktian, tetapi juga sangat efektif dalam mendeteksi kesalahan logis. Ini menjadikannya alat yang berguna bagi peneliti, pendidik, dan mahasiswa yang fokus pada bidang matematika formal.
Model ini merupakan bagian dari komitmen DeepSeek terhadap keterbukaan teknologi. Seperti versi sebelumnya, DeepSeek-Prover-V2 dirilis sebagai model sumber terbuka. Publik dapat mengunduh dan menggunakan model ini melalui dua platform utama: GitHub dan Hugging Face.
Dengan merilis Prover-V2, DeepSeek memperkuat posisinya dalam pengembangan LLM yang terspesialisasi. Fokus perusahaan pada aplikasi matematika membedakannya dari banyak pengembang AI lain yang menargetkan kasus penggunaan umum.
Langkah ini juga menegaskan bahwa model AI khusus memiliki potensi besar untuk mendukung kemajuan ilmu pengetahuan melalui otomatisasi penalaran logis dan pembuktian matematis.
“Baca Juga: Slow Fade dalam Hubungan: Tanda dan Cara Menghadapinya“
DeepSeek mempublikasikan detail Prover-V2, model AI terbaru yang dirancang khusus untuk matematika, melalui laman GitHub mereka. Model ini dibangun dengan pendekatan penalaran chain of thought (CoT) dan dikembangkan dari DeepSeek-V3, yang dirilis pada Desember 2024.
Prover-V2 berfokus pada pemecahan masalah matematika dari tingkat sekolah menengah hingga perguruan tinggi. Model ini juga mampu mendeteksi serta memperbaiki kesalahan dalam pembuktian teorema. Selain itu, ia dapat digunakan untuk membuat penjelasan langkah demi langkah dan membantu matematikawan menyusun serta menguji teorema baru.
Model ini tersedia dalam dua ukuran parameter. Versi ringan memiliki 7 miliar parameter dan dibangun di atas DeepSeek-Prover-V1.5-Base. Sementara versi lebih besar, dengan 671 miliar parameter, dilatih di atas DeepSeek-V3-Base. Keduanya memiliki panjang konteks hingga 32.000 token, mendukung pembuktian yang memerlukan konteks panjang.
Dalam pelatihannya, DeepSeek menerapkan pendekatan cold-start. Peneliti memaksa model dasar mengurai masalah kompleks menjadi sub-tujuan. Setelah berhasil diselesaikan, bukti dari sub-tujuan ini digabungkan ke dalam CoT untuk memperkuat pembelajaran berbasis penguatan.
Prover-V2 tersedia secara terbuka di GitHub dan Hugging Face. Meski begitu, DeepSeek tidak mengungkap detail teknis lengkap seperti arsitektur inti atau dataset pelatihan yang digunakan.
Model ini menunjukkan bagaimana iterasi dalam metode. pelatihan dapat menghasilkan peningkatan signifikan dalam kemampuan AI yang sangat terspesialisasi.
“Baca Juga: Rilis GTA VI Diundur, Rockstar Targetkan Mei 2026“
