Résumé technique : Visored : Un prouveur de langage naturel contrôlé pour les mathématiques générées par LLM

Énoncé du problème

Les grands modèles de langage (LLM) ont démontré une capacité croissante en raisonnement mathématique, pourtant ils restent sujets aux hallucinations. Par conséquent, la fiabilité des preuves générées par l'IA dépend entièrement du processus de vérification. Bien que les prouveurs de théorèmes automatisés (ATP) et les modèles de preuve complète (visant par exemple Lean ou Rocq) aient atteint des taux de réussite élevés sur des benchmarks comme miniF2F, ils nécessitent généralement un énoncé déjà formalisé en entrée. Le goulot d'étranglement critique réside dans l'autoformalisation : la traduction de la prose mathématique informelle en une forme vérifiable par machine.

Cette traduction est non triviale car les mathématiques informelles reposent sur un contexte partagé, des conditions de bord implicites (ex: $x \neq 0$) et des abus de notation que le lecteur interprète automatiquement. Une traduction directe vers un langage formel nécessite de s'engager sur des lemmes de bibliothèque spécifiques, des sous-types, des conventions de cas limites et des coercitions (ex: $\mathbb{N}$ vs $\mathbb{Z}$ vs $\mathbb{R}$) qui ne laissent aucune trace dans le texte source. Les erreurs liées à ces décisions se manifestent rarement sous forme d'erreurs de compilation, mais plutôt comme une « dérive sémantique silencieuse », où un énoncé compile mais ne reflète plus l'intention originale.

Méthodologie

Visored est un prototype de recherche conçu pour combler le fossé entre l'écriture mathématique informelle et la vérification formelle en introduisant une représentation intermédiaire (IR) à types dépendants qui se situe entre le LaTeX et les prouveurs de bas niveau comme Lean.

Architecture centrale

Le système fonctionne selon un pipeline (Figure 2 de l'article) composé des étapes suivantes :

1. Entrée en Langage Naturel Contrôlé (CNL) : Visored accepte un sous-ensemble contrôlé de l'anglais mathématique intégré dans le LaTeX. Le vocabulaire (modèles de phrases comme "Let...", "Assume...", "Then..." et commandes LaTeX) est défini par des fichiers de spécification .lpcsv externes, permettant d'étendre le langage de surface sans modifier le parseur.
2. Syntaxe et Sémantique : L'entrée est analysée en un arbre syntaxique puis élaborée en un AST typé (sem AST). Cette étape résout les noms, assigne les types et les genres, et impose la définissabilité lors de la vérification de type. Suivant la tradition de PVS, les fonctions partielles (ex: $1/x$, $\sqrt{x}$, $\log x$) portent des arguments d'hypothèse implicites (ex: $x \neq 0$, $x \ge 0$) qui doivent être levés avant que l'expression ne soit acceptée.
3. IR de niveau intermédiaire (MIR) : L'AST typé est abaissé vers le Visored MIR, le substrat du solveur.
4. Solveur à coût limité : Le solveur lève les obligations "Then..." et les conditions de définition via un moteur piloté par des règles et à coût limité (nommé "Miracle"). Il emploie une base de données de règles de rétro-propagation et de progression (inspirée de ProofGrader) ainsi que des tactiques spécialisées (ex: normalisateurs algébriques, solveurs de chaînes) pour clore les étapes routinières que les mathématiciens omettent habituellement.
5. Émission Lean optionnelle : Les preuves acceptées peuvent être transpiler vers Lean 4. La transpilation est une étape descendante optionnelle pour la vérification par un noyau externe. Le processus de transpilation implique de rejouer l'historique de normalisation et de gérer les témoins de coercition entre les systèmes numériques.

Philosophie de conception

Visored repose sur deux observations primordiales :

1. Fluidité des LLM : Les LLM sont entraînés massivement sur les mathématiques informelles. Un CNL de surface reste proche du domaine où les LLM sont déjà fluents, évitant ainsi au modèle d'apprendre de zéro la syntaxe de bas niveau des prouveurs (tactiques, noms de lemmes de bibliothèque).
2. Tractabilité : Combler le fossé entre le raisonnement naturel et formel est plus traitable que la preuve de théorèmes entièrement automatisée. En demandant au LLM de fournir le contour de la preuve en CNL, le solveur n'a plus qu'à clore de petites étapes évidentes, une tâche tout à fait à la portée de l'ingénierie agentique moderne.

Le système traite la tâche de parsing sémantique ascendant (LaTeX $\to$ Visored) comme le problème difficile, géré par le LLM, tandis que la projection descendante (Visored $\to$ Lean) est un processus déterministe et mécanique.

Contributions clés

• IR à types dépendants pour l'autoformalisation : Visored introduit une IR sémantiquement riche où chaque décision sans trace de surface dans le LaTeX (sous-types, lemmes de bibliothèque, conventions de cas limites, casts) est rendue explicite.
• Extensibilité pilotée par spécification : La surface CNL est définie par des fichiers de configuration externes plutôt que par des parseurs codés en dur, permettant d'ajuster le vocabulaire aux conventions mathématiques spécifiques (manuels, compétitions, recherche) sans recompiler le système.
• Diagnostics localisés : Contrairement aux systèmes qui fournissent un simple verdict d'acceptation/rejet après une compilation complète de Lean, Visored fournit des diagnostics localisés lors de l'étape d'élaboration ou de résolution. Cela permet une boucle "vérifier et réviser" où un LLM peut identifier et corriger des erreurs spécifiques.
• Application de la définition (Well-Definedness) : Le système impose la définition (ex: s'assurer que $x \neq 0$ avant $1/x$) via des arguments d'hypothèse implicites levés par le solveur, plutôt que de compter sur les conventions de totalisation du prouveur cible.
• Synthèse d'écoles existantes : Visored synthétise des éléments de Mizar/Naproche (surface CNL), PVS (définissabilité au moment de la vérification de type), Lean/Rocq (types dépendants) et ProofGrader (résolution par règles à budget de coût) dans un pipeline unique orienté vers le LLM.

Résultats expérimentaux

Les auteurs rapportent une étude de couverture sur le split miniF2F-valid (244 problèmes), qui a servi à la fois de set de développement et d'évaluation.

• Performance : Un agent de codage LLM (Claude), guidé par un document de compétences décrivant la surface CNL, a produit des preuves vérifiées par Visored pour 222 des 244 problèmes (91%).
• Répartition :
  • Induction : 100% (8/8)
  • Algèbre : 98% (86/88)
  • Théorie des nombres : 97% (66/68)
  • AMC/AIME : 93% / 87%
  • IMO (Olympiades) : 35% (7/20)
• Analyse d'échec : Les problèmes non résolus ont été attribués à des lacunes dans la base de règles de Visored (ex: absence de l'inégalité AM-GM, manque de types de corps finis, identités trigonométriques) ou à des régressions du prototype, plutôt qu'à l'incapacité du LLM à trouver la stratégie de preuve. Les auteurs affirment explicitement que l'agent a échoué car la "machinerie" nécessaire n'était pas encore implémentée dans le système.
• Coût de transpilation : Le schéma d'émission actuel, assez parcimonieux, entraîne une sortie Lean très verbeuse, avec un ratio médian de lignes de $\approx 250\times$ par rapport aux preuves Lean écrites à la main, atteignant parfois $\approx 25\,000\times$. Ceci est dû au rejeu des étapes de normalisation et des témoins de coercition.

Signification et affirmations

L'article positionne Visored non pas comme un prouveur de théorèmes automatisé compétitif, mais comme une preuve de concept pour une nouvelle infrastructure de vérification et d'organisation des mathématiques informelles produites par l'IA.

• Revendications modestes : Les auteurs déclarent explicitement qu'ils ne prétendent pas être un prouveur de théorèmes automatisé compétitif, ni n'extrapolent les résultats à des partitions de test non vues. Les 91 % de couverture sont présentés comme une limite inférieure de ce que la conception peut exprimer, et non comme un taux de réussite optimisé.
• Changement de goulot d'étranglement : Ce travail soutient l'idée que la contrainte de liaison dans les mathématiques par IA se déplace de la "génération d'idées" vers la "vérification et l'organisation de ces idées à grande échelle".
• Modes d'utilité : Visored est conçu pour fonctionner selon quatre modes :
  1. Vérificateur au moment de l'inférence : Un vérificateur en temps réel pour les sorties de LLM.
  2. Boucle d'autoformalisation : Un mécanisme permettant aux LLM de réécrire des preuves basées sur des diagnostics localisés.
  3. Signal de récompense dense : Fournir un feedback par étape pour l'apprentissage par renforcement (RL).
  4. Générateur de données CNL : Créer un corpus renouvelable de preuves lues naturellement et formellement vérifiées.

L'article conclut que la combinaison d'une surface CNL, d'une IR à types dépendants et d'un solveur piloté par des règles crée un pipeline où les échecs sont localisés et exploitables, offrant une voie plus fiable de la prose informelle vers les preuves vérifiées par le noyau que les approches actuelles d'autoformalisation directe. Les problèmes non résolus représentent un arriéré de règles et de machinerie manquantes, et non une limitation fondamentale de la conception.