Meituan merilis model pembuktian teorema dengan parameter 560B secara open source, dengan tingkat keberhasilan 97,1% dalam 72 kali inferensi, menyegarkan posisi SOTA open source

Berita Gate, 21 Maret, tim LongCat dari Meituan merilis open source LongCat-Flash-Prover, sebuah model MoE dengan 560 miliar parameter yang fokus pada tugas penalaran matematika dalam bahasa pembuktian formal Lean4. Bobot model dirilis di bawah lisensi MIT dan sudah tersedia di GitHub, Hugging Face, serta ModelScope.

Model ini memecah penalaran formal menjadi tiga kemampuan independen: formal otomatis (mengubah masalah matematika bahasa alami menjadi pernyataan formal Lean4), pembuatan sketsa (menghasilkan kerangka pembuktian bergaya lemma), dan pembuatan pembuktian lengkap. Ketiga kemampuan ini diintegrasikan melalui alat Agent yang melakukan penalaran (TIR) dan berinteraksi secara real-time dengan compiler Lean4 untuk verifikasi.

Dalam pelatihan, tim mengusulkan Hybrid-Experts Iteration Framework untuk menghasilkan data inisialisasi dingin, dan selama tahap pembelajaran penguatan, memperkenalkan algoritma HisPO untuk menstabilkan pelatihan tugas jangka panjang model MoE, serta menambahkan mekanisme deteksi konsistensi dan legalitas teorema untuk mencegah reward hacking.

Pengujian benchmark menunjukkan bahwa LongCat-Flash-Prover memecahkan rekor SOTA dalam otomatisasi formal dan pembuktian teorema di model bobot open source. Pada MiniF2F-Test, hanya membutuhkan 72 inference untuk mencapai tingkat keberhasilan 97,1%, dan di ProverBench serta PutnamBench mencapai 70,8% dan 41,5%, dengan jumlah inference per soal tidak lebih dari 220 kali.