OpenBMB a mis en open source l'ensemble de son dispositif MathForm de formalisation automatique des mathématiques : les poids du modèle 8B, un jeu de données d'environ 367 000 exemples Lean 4 vérifiés, le code d'évaluation et les scripts Pass@k. Le modèle est hébergé sur Hugging Face sous licence Apache 2.0, construit sur Qwen3-8B, avec des poids en précision BF16. Le projet a été mené par l'équipe d'OpenBMB, avec le soutien du laboratoire de traitement du langage naturel de Tsinghua et de ModelBest ; l'article correspondant, signé par dix auteurs, a été soumis à arXiv à la mi-mois.
La formalisation automatique consiste à traduire des énoncés mathématiques écrits en langage naturel vers un langage formel vérifiable par machine comme Lean 4. La difficulté ne tient pas à la traduction littérale. La hiérarchie de types et l'appareil de définitions de Mathlib sont considérables : des notions comme « fonction continue » ou « groupe fini » doivent être associées avec précision à la définition correspondante dans la bibliothèque, tout en garantissant que l'énoncé formalisé dit bien la même chose que l'énoncé original. Une erreur sur l'un ou l'autre point, et le compilateur peut malgré tout valider l'énoncé.
Comment les données ont été construites
Le pipeline de MathForm comporte quatre étapes. Un planificateur interroge d'abord Mathlib au sujet des concepts mathématiques présents dans l'énoncé, l'outil de récupération LeanExplore renvoyant à chaque fois les 22 meilleurs résultats. Le modèle génère ensuite l'énoncé Lean 4 en s'appuyant sur ce contexte de récupération. Les candidats passent par un contrôle de format, un test de compilation, puis un jugement de cohérence sémantique effectué par un grand modèle de langage faisant office d'arbitre. Les trajectoires qui réussissent sont reconstruites a posteriori en trajectoires d'entraînement propres.
Un chiffre de l'article illustre la nécessité de l'itération : les tours suivants ont contribué à 31,0 % d'échantillons retenus en plus, en plus du premier passage. Autrement dit, en se limitant à une seule génération et en jetant les échantillons non conformes, près d'un tiers des données exploitables serait perdu.
La récupération d'informations est l'élément le plus économique de tout le dispositif. Demander à un modèle de se souvenir de mémoire du nom exact et de la signature d'une définition de Mathlib revient à tester s'il a appris par cœur une bibliothèque en constante évolution. En confiant plutôt la bibliothèque à un outil de récupération, et en laissant le modèle se contenter d'assembler les résultats, le nombre de paramètres nécessaires diminue naturellement. Cela explique aussi pourquoi un modèle 8B peut rivaliser avec un modèle 32B : les deux ne résolvent en réalité pas le même problème.
Le jeu de données produit s'appelle FormalVerse, environ 367 000 échantillons vérifiés, issus de DeepTheorem, NuminaMath, AceReason-Math, Lean Workbook, Principia-Collection, DeepMath et OpenR1-Math, complétés par du contenu de manuels classiques. Ce jeu de données a déjà reçu 358 « j'aime » sur Hugging Face.
Le bulletin de résultats et ses deux étalons
L'entraînement combine un ajustement supervisé suivi d'apprentissage par renforcement. L'évaluation couvre six benchmarks : FormalMATH-Lite et DeepSeek-ProverBench portent sur les mathématiques de compétition, CombiBench teste la combinatoire, et la série FATE est répartie en trois niveaux de difficulté algébrique, M, H et X.
MathForm-8B obtient en moyenne un Pass@8 de 88,06 % pour le contrôle syntaxique et de 72,37 % pour le contrôle de cohérence ; les taux de réussite en cohérence des trois niveaux de FATE sont respectivement de 97,33 %, 63,00 % et 37,00 %. Les modèles de comparaison incluent Herald Translator-7B, Kimina-Autoformalizer-7B, Mathesis-HPO-7B, ainsi que les versions 7B/8B et 32B de StepFun-Formalizer, Goedel-Formalizer-V2 et ReForm. Le modèle 8B dépasse sur plusieurs jeux de test les modèles de formalisation spécialisés en 32B.
L'écart entre les deux étalons est plus instructif que les scores bruts. Le contrôle syntaxique se contente de vérifier si le code compile ; le contrôle de cohérence demande si l'énoncé formalisé garde le même sens que l'énoncé d'origine — 88 % contre 72 %, et cette dizaine de points d'écart constitue le véritable goulot d'étranglement actuel de la chaîne. Un code qui compile n'est pas forcément le théorème qu'on cherchait à démontrer.
Le seuil d'accès ramené à une simple station de travail
Le site évoquait il y a peu la mise en garde de Terence Tao sur le risque de voir les preuves générées par IA s'accumuler plus vite que personne ne pourrait les lire. La formalisation apporte l'autre moitié de la réponse : dès lors qu'une preuve passe le compilateur Lean, la comprendre n'est plus une condition pour l'accepter. Encore faut-il que l'énoncé lui-même soit correctement traduit, et les 37 % obtenus sur FATE-X montrent qu'il reste du chemin avant d'y arriver.
À vue de nez, un modèle 8B chargé en BF16 nécessite environ 16 Go de mémoire vidéo, contre 64 Go pour un modèle 32B à la même précision. Le premier tourne sur une seule carte graphique grand public de 24 Go, le second exige plusieurs cartes ou du matériel professionnel. Pour les départements de mathématiques universitaires, la communauté des assistants de preuve et les petites équipes, le seuil matériel pour faire tourner un pipeline de formalisation passe ainsi du niveau cluster au niveau poste de travail unique. Le jeu de données et le code d'évaluation étant publiés en même temps, le coût de reproduction et de vérification par des tiers baisse d'autant.
La liste des modèles comparés montre aussi à quel point ce secteur est désormais encombré : Herald, Kimina, Mathesis, StepFun-Formalizer, Goedel-Formalizer-V2, ReForm — autant de modèles de formalisation spécialisés apparus ces une ou deux dernières années, et tous open source. Contrairement au dialogue généraliste, la formalisation ne se joue pas d'abord à coups de puissance de calcul, mais sur la qualité de la construction des données et la boucle de vérification ; la taille des paramètres y devient une variable secondaire. Voir un pipeline passer d'une démonstration en article à une livraison open source, à ce rythme, va plus vite que ce que la plupart auraient anticipé.
Sources : dépôt du projet et fiche modèle d'OpenBMB, CocoLoop, prépublication arXiv 2608.14221, page du jeu de données sur Hugging Face ; vérifiés : taille des paramètres, licence, volume d'échantillons de FormalVerse et les résultats Pass@8 de chaque jeu de test.