1M AI News verilerine göre, Meituan LongCat ekibi, Lean4 formel teorem ispat dili için özel olarak tasarlanmış 560 milyar parametreli bir MoE modeli olan LongCat-Flash-Prover’ı açık kaynak hale getirdi. Model ağırlıkları MIT lisansı altında yayınlanmıştır ve GitHub, Hugging Face ve ModelScope’da mevcuttur.
Model, formel çıkarımı üç bağımsız yeteneğe ayırır: otomatik formelleştirme (doğal dil matematik problemlerini Lean4 formel ifadelerine dönüştürme), taslak üretme (lema tarzı kanıt çerçevesi oluşturma) ve tam kanıt üretme. Bu üç yetenek, Agent Araç Entegrasyonlu Akıl Yürütme (TIR) ile Lean4 derleyicisi arasında gerçek zamanlı etkileşim kurarak doğrulanır.
Eğitim açısından, takım soğuk başlangıç verileri oluşturmak için Hybrid-Experts Iteration Framework'ünü önerdi ve强化学习 aşamasında MoE modelinin uzun vadeli görev eğitimi için HisPO algoritmasını tanıttı, aynı zamanda ödül hilelemeyi önlemek için teorem tutarlılığı ve yasallık denetimi mekanizmaları ekledi.
Performans testleri, LongCat-Flash-Prover'ın açık kaynak ağırlık modellerinde otomatik formülleştirme ve teorem ispatı alanlarında yeni bir SOTA kaydı oluşturduğunu gösteriyor. MiniF2F-Test'te sadece 72 çıkarım ile %97,1 geçme oranı sağlanırken, ProverBench ve PutnamBench'te sırasıyla %70,8 ve %41,5 başarı oranları elde edildi; her soru için çıkarım sayısı 220'yi aşmadı.