Résumé technique : Pseudo-formalisation pour la vérification automatique de preuves

Énoncé du problème

La vérification automatique fiable des preuves mathématiques reste un goulot d'étranglement critique pour l'entraînement et l'évaluation des systèmes d'IA sur le raisonnement mathématique complexe. Bien que les preuves entièrement formelles (par exemple, en Lean ou Isabelle) soient faciles à vérifier en raison de leur précision sémantique et de leur modularité, la plupart des preuves — en particulier celles générées par l'IA ou rédigées par des humains en langage naturel — ne possèdent pas ces propriétés. La traduction des preuves en langage naturel vers des langages entièrement formels est souvent irréalisable pour les mathématiques de pointe en raison de bibliothèques formelles incomplètes et de l'effort d'expert immense requis. Par conséquent, les méthodes de vérification actuelles, telles que « LLM-as-judge » (évaluation directe de preuves en langage naturel), peinent en termes de précision et de rappel, échouant souvent à identifier des erreurs spécifiques dans des arguments longs et complexes.

Méthodologie : Pseudo-formalisation et vérification par blocs

Les auteurs proposent la Pseudo-formalisation (PF) combinée à la Vérification par blocs (BV) comme cadre pour combler le fossé entre la flexibilité du langage naturel et la vérifiabilité des preuves formelles.

1. Format de preuve pseudo-formel

Une preuve pseudo-formelle décompose un argument en langage naturel en une séquence de modules autonomes (lemmes, propositions, affirmations). Chaque module est un tuple $(P, c, \pi)$ représentant :

• Prémisses ($P$) : Hypothèses explicitement énoncées et contexte hérité.
• Conclusion ($c$) : L'affirmation spécifique à prouver.
• Preuve ($\pi$) : L'argument en langage naturel établissant $c$ à partir de $P$.

La structure est régie par deux graphes :

• Graphe de dépendance ($G$) : Un graphe orienté acyclique (DAG) où une arête existe si un module invoque la conclusion d'un autre. Cela empêche le raisonnement circulaire.
• Forêt d'héritage de portée ($T$) : Une structure en forêt organisant les modules hiérarchiquement (par exemple, des lemmes au sein d'une proposition), permettant l'héritage du contexte (définitions, hypothèses) sans réénonciation.

Les auteurs définissent les « Bonnes preuves pseudo-formelles » comme celles adhérant à deux desiderata : la concision (preuves courtes invoquant peu d'autres nœuds) et la profondeur de portée bornée (arbres d'héritage peu profonds). Théoriquement, vérifier de telles preuves permet de maintenir la longueur de contexte requise pour chaque étape de vérification indépendante de la taille totale de la preuve, atténuant ainsi la « pourriture du contexte » (la dégradation des performances des LLM avec l'augmentation de la longueur d'entrée).

2. Le pipeline de vérification (PF+BV)

Le processus de vérification comporte quatre étapes, utilisant toutes des LLM prêts à l'emploi sans fine-tuning :

1. Traduction : Un LLM traduit la preuve originale en langage naturel $\Pi$ en une preuve pseudo-formelle $\hat{\Pi}$. Une boucle d'auto-réparation optionnelle vérifie $\hat{\Pi}$ par rapport à $\Pi$ pour assurer la fidélité.
2. Vérification par blocs : Un LLM vérificateur examine chaque module de $\hat{\Pi}$ indépendamment. Il reçoit les prémisses complètes du module (y compris le contexte hérité), la conclusion, la preuve, et les conclusions vérifiées de tous les modules enfants invoqués. Il émet un verdict d'acceptation ou une description spécifique de l'erreur.
3. Calibration : Un LLM calibrateur agrège les rapports d'erreur par module en un verdict final. Il peut appliquer des seuils de rigueur configurables et mapper les erreurs au niveau des blocs vers la structure de la preuve originale (par exemple, identifier des étapes ou des lemmes spécifiques).
4. Mise à l'échelle parallèle : L'ensemble du pipeline est exécuté $k$ fois indépendamment. Une preuve n'est acceptée que si toutes les $k$ exécutions l'acceptent (agrégation pessimiste). Cela permet d'arbitrer entre précision et rappel en variant $k$.

Contributions clés

1. Pseudo-formalisation (PF) : Un nouveau format de preuve qui conserve la flexibilité du langage naturel tout en imposant la modularité et la structure explicite prémisse-conclusion nécessaires à une vérification fiable.
2. Vérification par blocs (BV) : Un algorithme qui vérifie les preuves en les décomposant en blocs indépendants, réduisant théoriquement les exigences de contexte et améliorant empiriquement la détection d'erreurs.
3. ArxivMathGradingBench : Un nouveau benchmark comprenant 35 articles de mathématiques de niveau recherche provenant d'arXiv contenant des erreurs connues et corrigées par les auteurs. Cet ensemble de données comble une lacune dans les benchmarks existants en testant la vérification sur des preuves de recherche réelles plutôt que sur des problèmes de niveau compétition.
4. Justification théorique : Les auteurs fournissent un théorème (Théorème 1) démontrant que pour les preuves pseudo-formelles « Bonnes », la vérification par blocs peut être simulée par un Transformer de taille fixe avec une longueur de contexte indépendante de la taille de la preuve, contrairement à la croissance linéaire du contexte requise pour la vérification de la preuve entière.

Résultats expérimentaux

La méthode a été évaluée sur deux benchmarks : Hard2Verify (problèmes de niveau Olympiades/Putnam) et ArxivMathGradingBench (articles de niveau recherche).

• Performance par rapport aux bases de référence : Sur les deux benchmarks, PF+BV domine au sens de Pareto la base de référence « LLM-as-judge ». Cela signifie que pour tout niveau donné de rappel (capacité à trouver des erreurs), PF+BV atteint une précision plus élevée (moins de fausses alarmes), et inversement.
• Hard2Verify : PF+BV a égalé la base de référence en rappel (~90 %) mais a considérablement réduit le nombre de fausses erreurs signalées par preuve (plus de 40 % de faux positifs en moins pour $k=8$).
• ArxivMathGradingBench : Le benchmark s'est révélé difficile, les deux méthodes laissant ~50 % des erreurs annotées non détectées pour $k=8$. Cependant, PF+BV a constamment surpassé la base de référence en rappel, en taux de fausses alarmes et en fraction d'articles où toutes les erreurs annotées ont été détectées.
• Analyse qualitative : Des études de cas (par exemple, IMO 2024 P6) illustrent que PF+BV réussit en isolant les sauts logiques dans des blocs locaux. Cela permet au vérificateur de détecter lorsqu'une preuve renforce incorrectement une prémisse (par exemple, inférer « même signe » à partir de « pas de $d$ et $-d$ ») sans avoir besoin de réévaluer l'argument global entier.

Signification et affirmations

L'article affirme que la pseudo-formalisation offre une alternative pratique à l'auto-formalisation (traduction vers Lean/Isabelle) pour la vérification de la recherche mathématique moderne. Bien que l'auto-formalisation fournisse des garanties de correction plus fortes, elle est souvent intraitable pour la recherche actuelle en raison de l'incomplétude des bibliothèques. PF+BV sacrifie la certitude absolue de la vérification formelle au profit de l'applicabilité à un éventail plus large de domaines mathématiques, exploitant le vocabulaire riche et les techniques standard du langage naturel tout en imposant une structure qui rend les erreurs plus faciles à localiser.

Les auteurs positionnent ce travail comme une étape vers une surveillance évolutive du raisonnement de l'IA, fournissant un mécanisme pour générer des signaux de récompense fiables pour l'entraînement des LLM sur des mathématiques difficiles et aidant les mathématiciens humains à réviser des preuves. Ils reconnaissent les limites, notant que produire une réécriture fidèle en pseudo-formel n'est pas trivial et que des travaux futurs pourraient impliquer l'entraînement de modèles pour générer des preuves directement dans ce format.