🤖 AI

Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization

Cet article soutient que s'appuyer uniquement sur les taux de compilation Lean pour évaluer la formalisation du langage naturel vers Lean est trompeur en raison d'un écart significatif entre la validité syntaxique et la fidélité sémantique, proposant une métrique de consensus rigoureuse calibrée par l'humain et identifiant le retour d'élaboration comme l'intervention la plus critique pour améliorer l'exactitude des énoncés formels.

Auteurs originaux : Ke Zhang, Patricio Gallardo Candela, Sudhir Murthy, Yi Xie, Zhi Wang, Maziar Raissi

Publié 2026-07-01

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Ke Zhang, Patricio Gallardo Candela, Sudhir Murthy, Yi Xie, Zhi Wang, Maziar Raissi

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

La vue d'ensemble : Traduire, pas seulement vérifier

Imaginez que vous possédez une bibliothèque de problèmes mathématiques complexes écrits en anglais courant (comme un manuel scolaire). Vous voulez traduire ces problèmes dans un langage strict et lisible par ordinateur appelé Lean.

Par le passé, les chercheurs se concentraient principalement sur la deuxième étape : donner à l'ordinateur une traduction parfaite et lui demander : « Peux-tu prouver que ceci est vrai ? »
Ce papier se concentre sur la première étape : « Peux-tu traduire correctement la phrase en anglais en Lean ? »

Les auteurs soutiennent que le simple fait qu'une traduction « fonctionne » (l'ordinateur l'accepte sans erreur) ne signifie pas qu'elle dit réellement la même chose que la phrase anglause originale. C'est comme un traducteur qui rédigerait une phrase grammaticalement parfaite, mais qui changerait accidentellement tout le sens.

Le problème central : « Compiler » vs « Être fidèle »

Le papier introduit une distinction cruciale entre deux choses :

La Compilation (La vérification de la grammaire) : L'ordinateur vérifie si le code Lean respecte les règles de syntaxe. Si c'est le cas, le code « compile ».
- Analogie : Imaginez un étudiant écrivant une dissertation. Le professeur vérifie s'il a utilisé l'orthographe et la ponctuation correctes. S'il l'a fait, la dissertation « passe ».
La Fidélité (La vérification du sens) : Le code exprime-t-il réellement ce que le problème mathématique original voulait dire ?
- Analogie : L'étudiant peut avoir une orthographe parfaite, mais il a écrit un texte sur les « chats » alors que le sujet portait sur les « chiens ». La dissertation a réussi le test de grammaire, mais a échoué au test de sens.

La grande découverte :
Les auteurs ont découvert un écart massif entre ces deux éléments.

Leur meilleur système d'IA a réussi à faire « compiler » (passer le test de grammaire) 89,5 % des traductions.
Cependant, seules 60,5 % de ces traductions étaient réellement « fidèles » (elles signifiaient la même chose).
L'écart : Environ 29 % du temps, l'IA produisait un code qui semblait parfait pour l'ordinateur, mais qui était en réalité faux dans son sens. Elle pouvait oublier une condition, changer un nombre ou rendre l'énoncé trop facile (ou trop difficile).

Comment ils ont mesuré cela

Puisque les ordinateurs ne peuvent pas toujours déterminer si une traduction est « significative », les auteurs ont créé un nouveau protocole de test :

Le Benchmark : Ils ont rassemblé 400 problèmes mathématiques difficiles provenant de manuels de niveau master (Analyse réelle, Analyse complexe, Topologie et Algèbre).
Le panel de « Juges » : Au lieu d'un seul ordinateur, ils ont utilisé deux modèles d'IA avancés pour agir en tant que juges. Ils ont demandé à ces juges : « Ce code Lean signifie-t-il la même chose que la phrase en anglais ? »
La règle du consensus : Pour qu'une traduction soit comptabilisée comme « Fidèle », les deux juges IA devaient être d'accord sur sa qualité.
Les audits humains : Pour s'assurer que les juges IA n'étaient pas déraisonnables, des experts mathématiques humains ont vérifié aléatoirement les résultats. Ils ont confirmé que lorsque les juges IA disaient « Non, c'est faux », ils avaient généralement raison.

La boîte à outils : Comment corriger les traductions

Les auteurs ont testé un « agent augmenté par des outils » (un assistant IA intelligent) capable d'utiliser trois outils spécifiques pour corriger ses erreurs. Ils ont traité cela comme une expérience scientifique, activant et désactivant les outils pour voir lequel aidait le plus.

Considérez l'IA comme un étudiant essayant de rédiger une traduction mathématique. Les outils sont :

Rédaction experte (T) : L'IA demande à un « robot traducteur » spécialisé de rédiger un premier jet.
- Analogie : Demander à un traducteur professionnel de fournir un brouillon avant de procéder à l'édition.
Recherche (S) : L'IA cherche des définitions et des symboles dans la bibliothèque mathématique (Mathlib) ou sur le web.
- Analogie : Chercher un mot dans le dictionnaire pour s'assurer d'utiliser le bon terme.
Feedback (F) : L'IA tente de compiler le code. Si elle échoue, l'ordinateur renvoie un message d'erreur, et l'IA tente de corriger l'erreur.
- Analogie : Le professeur corrige la dissertation et dit : « Il vous manque une virgule ici » ou « Cette phrase ne fait pas de sens ».

Les résultats de la boîte à outils :

Le Feedback (F) est le MVP (le plus précieux) : C'était l'outil le plus puissant. Il a corrigé le plus grand nombre d'« erreurs de grammaire » (problèmes de compilation). Cependant, il a aussi révélé un problème : en corrigeant la grammaire de manière trop agressive, il a parfois créé un code qui était grammaticalement parfait mais qui avait toujours un mauvais sens.
La Recherche (S) aide à l'ancrage : Elle a aidé l'IA à choisir les bons mots, mais elle n'était pas aussi puissante que le Feedback.
La Rédaction experte (T) est devenue moins importante : Une fois que l'IA disposait du Feedback et de la Recherche, le « premier jet » du robot expert n'apportait plus beaucoup de valeur. L'IA pouvait faire aussi bien seule si elle disposait des autres outils.

La conclusion principale

Le papier conclut que nous devons cesser de célébrer l'IA simplement parce qu'elle peut « compiler » du code.

Ancienne méthode : « Regardez ! L'IA a écrit un code que l'ordinateur a accepté ! »
Nouvelle méthode : « Regardez ! L'IA a écrit un code que l'ordinateur a accepté ET qui signifie réellement ce que nous avons demandé ! »

Les auteurs montrent que si l'IA devient très douée pour la « grammaire » du code mathématique, elle peine encore à préserver l'intégrité du « sens ». Ils fournissent une nouvelle façon de mesurer cet écart et démontent que l'utilisation d'une combinaison d'outils (particulièrement le feedback et la recherche) est le meilleur moyen de combler ce fossé, même si, malgré cela, une partie importante des traductions perd encore son sens originel.

En résumé : Ce n'est pas parce que l'ordinateur dit « Bon travail » que l'IA a réellement compris les mathématiques. Nous devons vérifier si le sens est préservé, et non pas seulement si le code s'exécute.

Résumé technique : Au-delà de la compilation : Évaluer la fidélité de la formalisation de déclarations du langage naturel vers Lean

1. Énoncé du problème

L'article traite de la tâche de formalisation de déclarations du langage naturel vers Lean : traduire automatiquement des énoncés mathématiques informels en déclarations de théorèmes valides en Lean 4. Cette tâche est distincte de la démonstration de théorèmes. Dans les benchmarks de démonstration (ex. MiniF2F, LeanDojo), l'énoncé formel est fixe et fiable ; le but du système est de générer une preuve acceptée par le vérificateur. En formalisation d'énoncés, le système doit générer l'énoncé lui-même.

Le défi central est que la compilation est une condition nécessaire mais insuffisante pour la réussite. Une déclaration Lean peut être typée (compiler) tout en :

Omettant des hypothèses critiques.
Modifiant le domaine de discours.
Renforçant ou affaiblissant l'affirmation.
Encodant une version vacue du résultat.

Les travaux antérieurs se sont souvent appuyés sur les taux de compilation ou sur des métriques d'équivalence basées sur des références (ex. BEq, rétro-traduction). Cet article soutient que la compilation seule crée un « écart de passage de la compilation » où les systèmes semblent réussir mais échouent à préserver le sens mathématique voulu. Les auteurs définissent le problème central comme l'évaluation de la formalisation fidèle d'énoncés : générer des déclarations qui compilent ET préservent l'intention sémantique de l'entrée en langage naturel.

2. Méthodologie

2.1 Construction du benchmark

Les auteurs ont constitué un benchmark de niveau master/doctorat composé de 400 énoncés en langage naturel dérivés de notes de cours et de manuels LaTeX en open-source. Le jeu de données est équilibré entre quatre domaines :

Analyse réelle (100 entrées)
Analyse complexe (100 entrées)
Topologie (100 entrées)
Algèbre (100 entrées)

Crucialement, ces énoncés n'ont aucune déclaration Lean de référence associée, garantissant que la tâche représente une véritable traduction plutôt qu'une simple récupération.

2.2 Protocole d'évaluation

L'article propose une métrique de Consensus LLM-as-Judge (LLM comme juge), calibrée par des experts humains, pour évaluer la fidélité. Le protocole comprend deux étapes :

Vérification par le compilateur : Tout code échouant à compiler est immédiatement jugé infidèle.
Consensus sémantique : Pour le code compilé, deux juges LLM indépendants (GPT-5.2 et Gemini-2.5-Pro) comparent la déclaration Lean générée avec l'énoncé original en langage naturel. Ils attribuent un score de fidélité (0–10).
- Métrique de succès : Une traduction est considérée comme Fidèle si et seulement si elle compile ET que les deux juges lui attribuent un score $\ge 9$ .
- Cette approche de consensus strict est conçue comme un point de fonctionnement conservateur pour la comparaison de systèmes, et non comme une preuve formelle d'équivalence.

2.3 Calibration humaine

Pour valider la métrique automatisée, les auteurs ont mené des audits humains :

Consensus-Positif : 96,0 % des sorties étiquetées fidèles par le consensus strict ont été confirmées fidèles par les réviseurs humains.
Consensus-Négatif (Passage de la compilation) : 82,4 % des sorties qui ont compilé mais ont été rejetées par le consensus ont été confirmées comme de véritables échecs sémantiques par les humains.
Cela confirme que la métrique est un filtre de haute précision et conservateur qui identifie efficacement la dérive sémantique.

2.4 Configuration expérimentale : Plan factoriel

Les auteurs ont évalué divers systèmes (LLM généralistes, formalisateurs spécialisés, modèles orientés preuve, et agents augmentés par des outils) en utilisant un plan factoriel $2^3$ pour décomposer les effets de trois interventions courantes :

Rédaction d'expert paramétrée (T) : Utiliser un modèle affiné (Herald) pour générer un premier jet.
Recherche de connaissances (S) : Utiliser des outils pour interroger Mathlib (recherche de symboles, résolution d'espaces de noms) et effectuer des recherches web pour l'ancrage (grounding).
Retour d'élaboration de Lean (F) : Utiliser un REPL pour compiler le code de manière itérative et recevoir des messages d'erreur pour la réparation.

L'architecture de l'agent utilise un orchestrateur central (GPT-5.2) qui maintient l'état et décide quels outils invoquer en fonction de la configuration.

3. Résultats clés

3.1 L'écart de passage de la compilation

La découverte empirique la plus significative est la divergence entre les taux de compilation et la fidélité sémantique :

Un agent complet augmenté d'outils a atteint un taux de compilation de 89,5 %.
Cependant, sous la métrique de consensus strict, seulement 60,5 % des sorties ont été jugées fidèles.
Cela laisse un écart de 29,0 points où les sorties compilent mais échouent aux tests sémantiques. Les audits humains ont confirmé que la majorité de ces cas « compilation réussie, consensus négatif » sont de réels échecs sémantiques (ex. hypothèses manquantes, affirmations vacues).

3.2 Performance des modèles

Formalisateurs spécialisés & Modèles de preuve : Les formalisateurs d'énoncés dédiés (ex. Herald, Kimina-Autoformalizer) et les modèles orientés preuve (ex. Goedel-Prover, Kimina-Prover) ont mal performé sur la génération d'énoncés lorsque la cible formelle n'était pas fournie. Leurs taux de fidélité variaient de 4,0 % à 12,3 %.
LLM généralistes : Les LLM généralistes en "one-shot" ont atteint 19,8–28,0 % de fidélité.
Agents augmentés par des outils : Le cadre d'agent complet a nettement surpassé les bases en "one-shot", atteignant 60,5 % de fidélité. Cependant, différents orchestrateurs (Sonnet 4.5, Gemini-2.5-Pro) convergent vers des niveaux de performance similaires (60–65 %) malgré des bases différentes, suggérant que les gains sont structurels à l'approche augmentée par des outils plutôt qu'au modèle d'orchestrateur spécifique.

3.3 Décomposition factorielle des interventions

L'étude a isolé l'impact des trois outils :

Retour d'élaboration (F) : C'était le principal moteur de la validité (compilation), augmentant considérablement le taux de compilation. Cependant, cela a également élargi le compartiment « compilation réussie mais infidèle », car cela a permis à davantage d'énoncés syntaxiquement corrects mais sémantiquement dérives de passer.
Recherche (S) : La recherche a principalement amélioré l'ancrage et la sélectivité. Elle a réduit l'écart de passage de la compilation (c'est-à-dire qu'elle a aidé à filtrer les énoncés sémantiquement incorrects qui parvenaient à compiler) et a amélioré l'efficacité en réduisant le nombre d'itérations REPL nécessaires. Son bénéfice marginal était le plus élevé en l'absence de feedback.
Rédaction d'expert (T) : Le préalable de rédaction affiné était largement substituable une fois que le feedback et l'ancrage étaient disponibles. En fait, avec un feedback complet, le préalable de rédaction a légèrement nui à la performance, suggérant qu'un orchestrateur fort avec un feedback du compilateur peut surpasser un jet spécialisé dans ce stack d'outils spécifique.

3.4 Variations spécifiques aux domaines

L'analyse complexe a montré les gains les plus élevés grâce au retour du compilateur (+54,2 points en fidélité), probablement en raison d'une couverture mature de Mathlib.
L'analyse réelle et l'algèbre ont montré des gains plus faibles, indiquant soit un support de bibliothèque limité, soit une difficulté intrinsèque de formalisation plus élevée.
La topologie a présenté des défis spécifiques avec des concepts avancés (ex. espaces recouvrants), où le feedback a souvent conduit à des énoncés valides mais sémantiquement décalés.

4. Signification et revendications

L'article soutient que la formalisation d'énoncés doit être évaluée comme une préservation du sens, et non simplement comme une acceptation par Lean. Les principales contributions sont :

Une nouvelle métrique : Une métrique basée sur le consensus et calibrée par l'humain, qui expose l'« écart de passage de la compilation », révélant que de nombreux systèmes génèrent des énoncés syntaxiquement valides mais sémantiquement incorrects.
Décomposition diagnostique : Une analyse factorielle montrant que les outils ne sont pas des ajouts monotones. Si le feedback corrige la syntaxe, il peut occulter les erreurs sémantiques ; la recherche améliore l'ancrage mais présente des rendements décroissants en présence de feedback ; et la rédaction spécialisée n'est pas toujours nécessaire dans une boucle riche en feedback.
Comparaison de systèmes : La preuve que les modèles actuels orientés preuve et les formalisateurs spécialisés ne transfèrent pas automatiquement leurs capacités de preuve à la génération d'énoncés sémantiquement fidèles sans un entraînement explicite centré sur l'énoncé ou des protocoles augmentés par des outils.

Les auteurs concluent que les futurs systèmes devraient coupler un fort feedback de Lean avec une évaluation sémantique et des politiques décidant quand chercher, réparer ou s'arrêter, plutôt que de se fier uniquement aux gains de précision moyenne. L'article évite explicitement de prétendre que leur métrique est une preuve formelle d'équivalence, se positionnant plutôt comme une frontière de décision conservatrice et scalable pour la comparaison de systèmes.