Selon 1M AI News , l'équipe LongCat de Meituan a open-sourcé LongCat-Flash-Prover, un modèle MoE de 560 milliards de paramètres dédié aux tâches de raisonnement mathématique dans le langage de preuve formelle Lean4. Les poids du modèle sont publiés sous licence MIT et sont désormais disponibles sur GitHub, Hugging Face et ModelScope.
Le modèle décompose le raisonnement formel en trois capacités indépendantes : la formalisation automatique (conversion des problèmes mathématiques en langage naturel en énoncés formels Lean4), la génération de croquis (production d’un cadre de preuve au style de lemme) et la génération de preuves complètes. Ces trois capacités sont vérifiées en temps réel grâce à l’intégration d’outils d’agent pour le raisonnement (TIR) et l’interactivité avec le compilateur Lean4.
En ce qui concerne l'entraînement, l'équipe a proposé le cadre d'itération Hybrid-Experts pour générer des données de démarrage à froid, introduit l'algorithme HisPO lors de la phase d'apprentissage par renforcement pour stabiliser l'entraînement à long terme du modèle MoE, et a intégré des mécanismes de vérification de la cohérence et de la légalité des théorèmes pour prévenir le reward hacking.
Les tests de référence montrent que LongCat-Flash-Prover a établi de nouveaux résultats d'état de l'art dans la formalisation automatique et la preuve de théorèmes parmi les modèles à poids ouverts. Il atteint un taux de réussite de 97,1 % en seulement 72 inférences sur MiniF2F-Test, et 70,8 % et 41,5 % sur ProverBench et PutnamBench respectivement, avec au plus 220 inférences par problème.