Menurut pemantauan 1M AI News , tim LongCat dari Meituan mengopen-source LongCat-Flash-Prover, sebuah model MoE dengan 560 miliar parameter yang dirancang khusus untuk tugas penalaran matematis dalam bahasa pembuktian formal Lean4. Bobot model dirilis di bawah lisensi MIT dan telah tersedia di GitHub, Hugging Face, dan ModelScope.
Model memecah penalaran formal menjadi tiga kemampuan independen: formalisasi otomatis (mengubah masalah matematika dalam bahasa alami menjadi pernyataan formal Lean4), generasi sketsa (menghasilkan kerangka bukti bergaya lemma), dan generasi bukti lengkap. Ketiga kemampuan tersebut diverifikasi secara real-time melalui integrasi alat Agent dengan penalaran TIR dan compiler Lean4.
Dalam hal pelatihan, tim mengusulkan Hybrid-Experts Iteration Framework untuk menghasilkan data cold start, serta memperkenalkan algoritma HisPO pada tahap reinforcement learning untuk menstabilkan pelatihan jangka panjang model MoE, sekaligus menambahkan mekanisme pemeriksaan konsistensi teorema dan legalitas untuk mencegah reward hacking.
Hasil benchmark menunjukkan bahwa LongCat-Flash-Prover memperbarui dua SOTA dalam formalisasi otomatis dan pembuktian teorema pada model dengan bobot open-source. Dengan hanya 72 inferensi di MiniF2F-Test, mencapai tingkat kelulusan 97,1%, sementara ProverBench dan PutnamBench masing-masing mencapai 70,8% dan 41,5%, dengan tidak lebih dari 220 inferensi per soal.