DeepSeek Prover V2, model AI yang berfokus pada matematika sumber terbuka, dirilis

DeepSeek, perusahaan kecerdasan buatan (AI) yang berbasis di Hangzhou, China, merilis versi terbaru dari model Prover-nya pada hari Rabu. Dijuluki DeepSeek-Prover-V2, ini adalah model yang sangat khusus yang berfokus pada pembuktian teorema matematika formal. Model bahasa besar (LLM) menggunakan bahasa pemrograman Lean 4 untuk memeriksa apakah bukti matematis konsisten secara logis dengan menganalisis setiap langkah secara independen. Mirip dengan rilis perusahaan China sebelumnya, DeepSeek-Prover-V2 adalah model open-source dan dapat diunduh dari repositori populer seperti GitHub dan Hugging Face.

Model AI Baru DeepSeek yang Berfokus pada Matematika Ada di Sini

Perusahaan AI merinci model baru di halaman daftar GitHub-nya. Ini pada dasarnya adalah model yang berfokus pada penalaran dengan rantai pemikiran yang terlihat (CoT), yang berfungsi dalam domain matematika. Ini dibangun dan disuling dari model AI DeepSeek-V3, yang dirilis pada Desember 2024.

DeepSeek-Prover-V2 dapat digunakan dalam berbagai cara. Ini dapat memecahkan masalah matematika tingkat sekolah menengah hingga perguruan tinggi dan menemukan dan memperbaiki kesalahan dalam bukti teorema matematika. Ini juga dapat digunakan sebagai alat bantu mengajar dan menghasilkan penjelasan langkah demi langkah untuk pembuktian, dan dapat membantu matematikawan dan peneliti dalam mengeksplorasi teorema baru dan membuktikan validitasnya.

Ini tersedia dalam dua ukuran model – ukuran tujuh miliar parameter dan ukuran parameter 671 miliar yang lebih besar. Sementara yang terakhir dilatih di atas DeepSeek-V3-Base, yang pertama dibangun di atas DeepSeek-Prover-V1.5-Base dan hadir dengan panjang konteks hingga 32.000 token.

Datang ke proses pra-pelatihan, para peneliti menerapkan sistem pelatihan cold-start dengan mendorong model dasar untuk menguraikan masalah yang kompleks. Masalah-masalah ini berfungsi sebagai serangkaian subtujuan. Kemudian, bukti subtujuan yang diselesaikan ditambahkan ke CoT dan dikombinasikan dengan penalaran model dasar untuk menciptakan awal awal yang dingin untuk pembelajaran penguatan.

Khususnya, selain GitHub, model AI juga dapat diunduh dari daftar Hugging Face DeepSeek. Model Prover-V2 menyoroti bagaimana perubahan berulang pada proses pelatihan model AI dapat menghasilkan peningkatan kemampuan khusus mereka secara signifikan. Mirip dengan rilis model sumber terbuka lainnya, detail tentang arsitektur inti atau himpunan data yang lebih besar tidak diketahui.