💻 computer science

ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers

Cet article introduit ITPEval, le premier benchmark et l'infrastructure unifiée pour évaluer la traduction automatisée de preuves formelles à travers quatre prouveurs de théorèmes interactifs majeurs, révélant que les modèles de langage de grande taille actuels éprouvent des difficultés significatives en matière de traduction de preuves en raison de décalages de bibliothèques et que le simple typage natif surestime souvent la fidélité sémantique.

Auteurs originaux : Jiayi Wu, Robert Joseph George, Anima Anandkumar

Publié 2026-07-23

📖 4 min de lecture☕ Lecture pause café

CC BY 4.0

Auteurs originaux : Jiayi Wu, Robert Joseph George, Anima Anandkumar

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

Imaginez un monde où les mathématiciens parlent quatre langues différentes, mais où ils essaient tous de résoudre exactement les mêmes énigmes. Dans l'arène de haut niveau de la « preuve formelle de théorèmes », les ordinateurs agissent comme les arbitres ultimes, vérifiant chaque étape d'une preuve mathématique pour s'assurer qu'elle est correcte à 100 %. Cependant, tout comme les humains qui parlent français, japonais, swahili et arabe, ces systèmes informatiques (appelés Prouveurs de Théorèmes Interactifs, ou ITP) possèdent leur propre grammaire, leur vocabulaire et leurs bibliothèques de faits pré-approuvés. Une preuve écrite parfaitement dans un système est souvent du charabia pour les autres. Cela crée un problème de solitude : si une preuve brillante est écrite dans une langue, elle ne peut pas être facilement utilisée ou vérifiée par les autres. Les scientifiques ont tenté de construire des « traducteurs universels » pour combler ce fossé, espérant que l'Intelligence Artificielle (IA) pourrait apprendre à traduire automatiquement ces preuves mathématiques, permettant ainsi à toute la communauté de partager son travail.

Entrez dans ITPEVAL, une nouvelle étude qui agit comme un examen de langue massif et rigoureux pour l'IA. Les chercheurs ont voulu voir si les modèles d'IA les plus intelligents d'aujourd'hui pouvaient réellement traduire des preuves mathématiques formelles entre quatre systèmes majeurs : Lean 4, Rocq, Isabelle et HOL Light. Ils ne se sont pas contentés de demander à l'IA de deviner ; ils ont construit un terrain d'essai spécialisé avec plus de 1 500 fichiers sources et près de 7 000 théorèmes. Ils ont divisé le test en deux niveaux : un niveau « Contrôlé » avec des problèmes mathématiques simples et autonomes (comme un quiz de vocabulaire sans références extérieures), et un niveau « Écosystème » utilisant du code de bibliothèque réel et complexe qui repose sur des règles spécifiques au système (comme une conversation complète avec de l'argot et des références culturelles).

Les résultats sont un mélange de « pas mal » et de « encore très difficile ». Lorsque l'IA a tenté de traduire uniquement les énoncés des théorèmes (le « quoi »), les meilleurs modèles ont réussi environ 29,1 % du temps. Mais lorsqu'on lui a demandé de traduire les preuves elles-mêmes (le « comment »), le taux de réussite a chuté à seulement 10,5 %. L'étude a révélé que le plus grand obstacle n'était pas les mathématiques elles-mêmes ou les différentes fondations logiques, mais l'« écosystème ». L'IA a le plus lutté lorsqu'elle devait naviguer dans les bibliothèques spécifiques, les conventions de nommage et les styles d'automatisation du système cible. C'est comme si l'IA pouvait comprendre la phrase « Le chat est assis sur le tapis », mais échouait lorsqu'on lui demandait de la traduire dans un dialecte spécifique qui exigeait l'utilisation d'une marque de tapis particulière et d'un type de chat spécifique.

De plus, les chercheurs ont découvert que le simple fait de faire dire à un ordinateur « Cela semble correct » (un contrôle de type) ne suffit pas. Ils ont effectué une « vérification de sens » plus approfondie et ont constaté que même lorsque la traduction de l'IA passait le test de base de l'ordinateur, elle était souvent mathématiquement plus faible ou légèrement différente de l'original dans 46 % des cas. L'étude suggère que, bien que l'IA s'améliore sur les bases, elle doit encore apprendre à s'adapter à la « culture » unique de chaque système mathématique avant de pouvoir véritablement devenir un traducteur universel. Les auteurs ont également exploré un test de « l'aller-retour », où ils ont traduit des mathématiques en langage naturel et inversement, constatant que les résultats variaient considérablement selon le système utilisé, ce qui laisse entendre que l'utilisation de plusieurs systèmes ensemble pourrait aider, mais que ce n'est pas encore une solution miracle.

Résumé technique : ITPEVAL – Évaluation comparative de la traduction formelle entre les prouveurs de théorèmes interactifs

1. Énoncé du problème

L'écosystème de la preuve formelle est actuellement fragmenté. Bien que les grands modèles de langage (LLM) aient connu un succès significatif dans la preuve de théorèmes automatisée et l'autoformalisation, les résultats vérifiés restent isolés au sein de prouveurs de théorèmes interactifs (ITP) incompatibles. Chaque système (par exemple, Lean 4, Rocq, Isabelle, HOL Light) implémente sa propre fondation logique, son propre langage de tactiques et ses propres bibliothèques mathématiques. Par conséquent, un théorème prouvé dans un système ne peut pas être directement invoqué dans un autre, ce qui entraîne une duplication des efforts de formalisation et limite les données d'entraînement disponibles pour les prouveurs basés sur l'apprentissage.

La traduction inter-ITP — la tâche consistant à convertir des preuves formelles entre systèmes tout en préservant la correction — a fait l'objet de peu d'études systématiques. Les efforts existants, tels que les catalogues « Formalizing 100 Theorems » ou les cadres d'interopérabilité comme Dedukti, se concentrent sur le suivi de la couverture ou sur l'activation de l'échange de preuves via des représentations intermédiaires, mais manquent de benchmarks standardisés pour évaluer la qualité de la traduction. De plus, les méthodologies d'évaluation existantes sont insuffisantes ; la simple vérification de type produit souvent des taux élevés de faux positifs pour la correction sémantique, et les benchmarks de traduction de code ne tiennent pas compte des différences profondes de fondation logique inhérentes aux ITP.

2. Méthodologie et conception du benchmark

Les auteurs présentent ITPEVAL, le premier benchmark conçu pour évaluer la traduction automatisée de preuves formelles entre quatre ITP majeurs : Lean 4, Rocq (anciennement Coq), Isabelle et HOL Light. Le benchmark couvre deux fondations logiques distinctes : le Calcul des Constructions Inductives (CIC) et la Logique d'Ordre Supérieur (HOL).

2.1. Structure des données

Le benchmark comprend 1 560 fichiers sources et 6 848 théorèmes, organisés en deux niveaux distincts pour isoler les sources de difficulté :

Niveau A (Contrôlé) : Contient 64 fichiers auto-contenus et axiomatisés (660 lemmes) dérivés du benchmark Babel-formal. Ces fichiers incluent leurs propres définitions et hypothèses, évitant la dépendance aux bibliothèques spécifiques aux prouveurs. Ce niveau isole les problèmes de traduction fondamentale (ex: théorie des types, niveaux d'univers, arguments implicites).
Niveau B (Écosystème) : Contient des formalisations tirées de véritables bibliothèques communautaires, exposant les décalages d'API, les conventions de nommage et les différences de style de preuve. Ce niveau inclut :
- 232 fichiers de Formalizing 100 Theorems (4 924 lemmes), alignés sur les quatre systèmes.
- 1 264 fichiers à théorème unique issus de miniF2F (énoncés uniquement), offrant un contenu mathématique de compétition diversifié.

La conception impose une exigence d'intersection quadruple : chaque fichier doit être formalisé dans les quatre ITP pour garantir des comparaisons directionnelles propres sans biais liés aux données manquantes.

2.2. Tâches de traduction

ITPEVAL évalue deux tâches principales :

Traduction d'énoncé : Générer du code ITP cible où les corps de preuve sont remplacés par des marqueurs (ex: sorry). La vérification exige que le fichier généré soit vérifiable par le type dans le système cible.
Traduction de preuve : Générer des fichiers de preuve complets et compilables sans marqueurs. La vérification exige que l'intégralité du fichier compile avec succès dans le prouveur cible.

2.3. Infrastructure de vérification

Un composant critique de la méthodologie est itpeval, une infrastructure de vérification multi-ITP unifiée. Pour répondre à l'hétérogénéité des modèles d'exécution des ITP (ex: coûts de démarrage élevés pour Isabelle et HOL Light), le système utilise :

Des backends chauds isolés par état : Garantissant que chaque vérification est observationnellement équivalente à la vérification d'un artefact dans un environnement neuf, évitant ainsi les fuites de déclarations.
Une vérification par le prouveur cible natif : Tous les labels sont produits par les ITP cibles réels, et non par des heuristiques de surface.
Une planification adaptative : Utilisation de workers persistants, de mise en lots de sessions et de serveurs de fork pour gérer le débit tout en présant la sémantique de vérification par fichier.

2.4. Vérification de l'équivalence sémantique

Reconnaissant que la vérification de type est nécessaire mais insuffisante pour la fidélité sémantique, les auteurs implémentent une vérification de Équivalence Définitionnelle Étendue Bidirectionnelle (BEq) pour les cibles Lean 4. Cette vérification déterministe vérifie si un énoncé généré $G$ et un énoncé de référence $R$ s'impliquent mutuellement ( $G \vdash R$ et $R \vdash G$ ) en utilisant une recherche de preuve restreinte, évitant ainsi toute variance supplémentaire dépendante du modèle.

3. Contributions clés

Benchmark aligné sur quatre voies : Un ensemble de données de 1 560 fichiers et 6 848 théorèmes à travers Lean 4, Rocq, Isabelle et HOL Light, structuré en niveaux contrôlés et écosystémiques pour quantifier le coût des dépendances de bibliothèque.
Infrastructure de vérification unifiée : Un client à état isolé (itpeval) qui permet une évaluation scalable et reproductible à travers des prouveurs hétérogènes avec des sémantiques de vérification natives.
Évaluation systématique des LLM : Une évaluation de cinq modèles de pointe et à poids ouverts (GPT-5.5, Claude Sonnet 4.6, Gemini 3.1 Pro, DeepSeek-V4-Pro, Qwen3-235B-A22B) sur 12 paires de traduction dirigées.
Analyse de la fidélité sémantique : L'application de BEq pour démontrer que la vérification de type native seule peut surestimer considérablement la correction sémantique.
Étude exploratoire de l'aller-retour (Round-Trip) : Une investigation des boucles d'autoformalisation et d'auto-informalisation pour évaluer les modèles de vérification dépendants de la cible et les bénéfices potentiels du contexte multi-ITP.

4. Résultats

4.1. Performance de la traduction

Traduction d'énoncé : Le meilleur modèle, GPT-5.5, a atteint un taux pass@1 de 29,1 % globalement. DeepSeek-V4-Pro suit avec 27,1 %. La performance chute significativement pour les autres modèles (Gemini à 14,0 %, Qwen et Claude en dessous de 10 %).
Traduction de preuve : La performance est nettement inférieure, GPT-5.5 n'atteignant que 10,5 % de pass@1 globalement.
Écart entre les niveaux : Le niveau contrôlé (Niveau A) était systématiquement plus facile que le niveau écosystémique (Niveau B). Pour la traduction de preuve, GPT-5.5 atteint 29,7 % sur les fichiers contrôlés mais seulement 5,2 % sur les fichiers écosystémiques. Cela indique que le décalage de bibliothèque (APIs, nommage, automatisation) est la plus grande source de défaillance observée, plutôt que les différences de fondation logique.
Asymétrie directionnelle : La difficulté de traduction varie considérablement selon la cible. Isabelle et HOL Light sont de solides cibles pour la traduction d'énoncés, mais Isabelle devient la cible la plus difficile pour la traduction de preuves. La similitude de la fondation logique (ex: CIC vers CIC) ne garantit pas un taux de réussite plus élevé ; les conventions de l'écosystème cible jouent un rôle plus important.

4.2. Équivalence sémantique (BEq)

Lors de l'application de la vérification BEq aux traductions d'énoncés Lean 4 vérifiées de miniF2F :

Seulement 54,0 % des traductions vérifiées ont passé le test d'équivalence.
Claude Sonnet 4.6 a montré le taux de réussite BEq le plus élevé (83,8 %) parmi les traductions vérifiées, tandis que les autres oscillaient entre 34,5 % et 48,4 %.
Ce résultat démontre qu'un énoncé peut être syntaxiquement valide (vérification de type) tout en étant sémantiquement plus faible ou décalé par rapport au théorème original.

4.3. Aller-retour et autoformalisation

Dans une étude d'aller-retour multi-ITP (NL $\to$ Formel $\to$ NL $\to$ Formel), Rocq et HOL Light ont vérifié environ un tiers des sorties aux deux étapes de formalisation, tandis que Lean 4 tournait autour de 11 % et Isabelle tombait à 4,3 % à l'étape finale. Le contexte multi-ITP a montré des bénéfices potentiels pour certaines combinaisons modèle-cible (ex: améliorant les taux de réussite de l'étape 1 de Lean 4 de 4,8 % à 10,6 %), mais les résultats n'étaient pas uniformes pour tous les systèmes.

5. Signification et affirmations

L'article affirme qu'ITPEVAL fournit le premier benchmark systématique à quatre voies pour la traduction formelle, révélant que la barrière principale à la traduction inter-ITP n'est pas la fondation logique elle-même, mais les dépendances au niveau de l'écosystème (bibliothèques, APIs et idiomes de preuve).

Les auteurs soulignent que :

La vérification native est essentielle : Les heuristiques de surface ou la simple vérification de type sont insuffisantes pour évaluer la fidélité sémantique.
L'infrastructure compte : Une évaluation inter-ITP fiable nécessite une vérification isolée par état pour éviter les facteurs de confusion comme la fuite de déclaration.
Directions futures : Le domaine doit prioriser la récupération, la cartographie des bibliothèques et l'alignement des API plutôt que la pure traduction fondamentale. L'article note également des limites, notamment le cadre d'évaluation zero-shot, la restriction de BEq aux cibles Lean 4, et le potentiel de contamination des données d'entraînement dans les jeux de données publics comme miniF2F.

Ce travail établit une base pour mesurer les progrès de la traduction formelle, suggérant que les futurs systèmes devront traiter le problème du « décalage de bibliothèque » pour parvenir à une interopérabilité robuste entre les écosystèmes de preuves formelles.