Le modèle de preuve de théorème open-source de Meituan avec 560 milliards de paramètres, atteignant un taux de réussite de 97,1 % après 72 inférences, établit un nouveau record open-source SOTA.

Gate News, le 21 mars, l'équipe LongCat de Meituan a publié en open source LongCat-Flash-Prover, un modèle MoE de 560 milliards de paramètres, spécialisé dans les tâches de raisonnement mathématique en langage de preuve formelle Lean4. Les poids du modèle sont distribués sous licence MIT et sont disponibles sur GitHub, Hugging Face et ModelScope.

Ce modèle décompose le raisonnement formel en trois capacités indépendantes : la formalisation automatique (convertir un problème mathématique en langage naturel en une déclaration formelle Lean4), la génération de brouillons (produire un cadre de preuve de style lemme) et la génération de preuves complètes. Ces trois capacités intègrent le raisonnement via un ensemble d'outils Agent (TIR) qui interagissent en temps réel avec le compilateur Lean4 pour vérification.

Concernant 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, et durant la phase d'apprentissage par renforcement, elle a introduit l'algorithme HisPO pour stabiliser l'entraînement à long terme du modèle MoE. Elle a également intégré des mécanismes de vérification de la cohérence et de la légalité des théorèmes afin de prévenir le hacking de récompenses.

Les tests de référence montrent que LongCat-Flash-Prover établit de nouveaux records SOTA pour la formalisation automatique et la preuve de théorèmes parmi les modèles open source. Sur le MiniF2F-Test, il atteint un taux de réussite de 97,1 % après seulement 72 raisonnements, tandis que ProverBench et PutnamBench atteignent respectivement 70,8 % et 41,5 %, avec un nombre de raisonnements par problème ne dépassant pas 220.