DeepSeek. (Foto: DeepSeek)
JAKARTA - DeepSeek, start up kecerdasan buatan (AI) yang berpusat di Hangzhou, China, merilis versi terbaru model Provernya pada Rabu, (30/4/2025). Model yang disebut sebagai DeepSeek-Prover-V2, ini adalah model yang sangat terspesialisasi yang berfokus pada pembuktian teorema matematika formal.
Model bahasa besar (LLM) menggunakan bahasa pemrograman Lean 4 untuk memeriksa apakah pembuktian matematika konsisten secara logis dengan menganalisis setiap langkah secara independen. Mirip dengan rilisan perusahaan China sebelumnya, DeepSeek-Prover-V2 adalah model sumber terbuka dan dapat diunduh dari repositori populer seperti GitHub dan Hugging Face.
Model AI yang Berfokus pada Matematika
DeepSeek merinci model baru itu di halaman daftar GitHub-nya. Ini pada dasarnya adalah model yang berfokus pada penalaran dengan rantai pemikiran yang terlihat (chain of though/CoT), yang berfungsi dalam domain matematika. Ia dibangun dan disuling dari model AI DeepSeek-V3, yang dirilis pada Desember 2024.
DeepSeek-Prover-V2 dapat digunakan dalam berbagai cara. Ia dapat memecahkan masalah matematika tingkat sekolah menengah hingga perguruan tinggi dan menemukan serta memperbaiki kesalahan dalam pembuktian teorema matematika. Ini juga dapat digunakan sebagai alat bantu pengajaran dan menghasilkan penjelasan langkah demi langkah untuk pembuktian, dan dapat membantu matematikawan dan peneliti dalam mengeksplorasi teorema baru dan membuktikan validitasnya.
Dilansir Gadgets 360, Prover-V2 tersedia dalam dua ukuran model — ukuran tujuh miliar parameter dan ukuran 671 miliar parameter yang lebih besar. Sementara yang terakhir dilatih di atas DeepSeek-V3-Base, yang pertama dibangun di atas DeepSeek-Prover-V1.5-Base dan memiliki panjang konteks hingga 32.000 token.
