TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?

Le papier présente TaoBench, une nouvelle norme d'évaluation démontrant que les prouveurs de théorèmes automatisés actuels peinent à généraliser au-delà du cadre MathLib, leur performance chutant de 26 % face à des constructions mathématiques personnalisées issues de l'analyse de Terence Tao.

L'essentiel

🧠 Le Problème : Les Robots qui ne savent pas parler "Autre Langue"

Imaginez que vous avez formé un super-étudiant (une Intelligence Artificielle) pour résoudre des problèmes de mathématiques. Pour l'entraîner, vous lui avez donné des milliers d'exercices écrits dans un carnet de notes très spécifique (appelé MathLib).

Dans ce carnet, tout est codifié :

• Le mot "ensemble" est écrit d'une certaine façon.
• Le mot "nombre réel" est défini avec une règle précise.
• Tout le monde utilise le même dictionnaire.

Grâce à cet entraînement, l'IA devient un champion. Elle résout 70 % des problèmes de ce carnet. On pense alors : "Super ! Elle est prête à faire des maths partout !"

Mais voici le piège :
Dans la vraie vie, les mathématiciens (comme Terence Tao, un génie vivant) ne travaillent pas toujours avec ce carnet officiel. Parfois, ils créent leurs propres règles, leurs propres définitions, et leurs propres façons d'écrire les choses pour explorer de nouvelles idées. C'est comme si un architecte dessinait une maison en utilisant ses propres symboles au lieu du plan standard de l'urbanisme.

La question de l'article est simple : Si on donne à notre super-étudiant un problème écrit dans le "carnet de Tao" (avec ses propres règles), va-t-il réussir à le résoudre, ou va-t-il paniquer ?

🧪 L'Expérience : TAOBENCH

Les chercheurs ont créé un nouveau test, qu'ils ont appelé TAOBENCH.

1. Le Défi : Ils ont pris 150 exercices du livre Analysis I de Terence Tao. Ce livre est célèbre car il construit les mathématiques "de zéro", sans utiliser les raccourcis du carnet officiel (MathLib).
2. La Comparaison : Pour être sûrs que le problème n'est pas plus difficile, ils ont traduit chaque exercice de Tao en utilisant le langage officiel de MathLib.
   • Version A (Tao) : Le problème dans le style "maison", avec les définitions originales.
   • Version B (MathLib) : Le même problème, mais traduit dans le langage standard que l'IA connaît par cœur.

C'est comme donner à un joueur de football un match où l'arbitre siffle avec un sifflet différent et où les lignes de but sont dessinées légèrement différemment, mais la règle du jeu (marquer un but) reste la même.

📉 Les Résultats : Le Choc de la Réalité

Les résultats sont surprenants et un peu inquiétants :

• Sur la Version B (MathLib) : L'IA fonctionne très bien. Elle résout environ 70 % des problèmes. Elle est un champion dans son environnement habituel.
• Sur la Version A (Tao) : Dès qu'on change le "vocabulaire" et les règles de base, la performance de l'IA s'effondre. Elle ne résout plus que 40 à 50 % des problèmes.

La chute est d'environ 26 %.

C'est comme si un traducteur expert en français pouvait parfaitement lire un livre écrit en français, mais dès qu'on lui donne le même livre écrit en "français avec un accent très fort" ou avec quelques mots inventés, il ne comprend plus rien, même si le sens des phrases est identique.

🔍 Pourquoi cela arrive-t-il ? (L'Analogie du Lego)

Imaginez que l'IA a appris à construire des châteaux avec des briques Lego rouges (le standard MathLib). Elle sait exactement comment elles s'emboîtent.

Dans le livre de Tao, les mathématiciens utilisent des briques bleues qu'ils ont fabriquées eux-mêmes.

• La forme est presque la même.
• La fonction est la même.
• Mais la couleur et le petit crochet de connexion sont différents.

L'IA, qui a été entraînée uniquement avec des briques rouges, regarde les briques bleues et se dit : "Je ne connais pas cette pièce. Je ne sais pas comment l'assembler. Je vais abandonner."

L'article montre que le problème n'est pas que les maths sont plus difficiles. Le problème, c'est que l'IA n'a pas appris à s'adapter. Elle a appris par cœur le manuel, mais elle n'a pas appris à penser de manière flexible.

💡 Ce que cela signifie pour l'avenir

Cet article nous donne un avertissement important :

1. Les benchmarks actuels sont biaisés : Si on teste les IA uniquement sur des problèmes standards (MathLib), on a l'impression qu'elles sont géniales. Mais c'est une illusion.
2. Le vrai travail est ailleurs : La recherche mathématique réelle se fait souvent dans des environnements nouveaux, avec des définitions sur mesure. Si les IA ne peuvent pas s'adapter à ces nouveaux environnements, elles ne seront jamais de véritables assistants pour les chercheurs de pointe.
3. La solution : Il faut entraîner les IA à comprendre le sens des mathématiques, et non pas juste à mémoriser un dictionnaire spécifique. Il faut qu'elles apprennent à lire n'importe quel "dialecte" mathématique, pas seulement le standard.

En résumé

TAOBENCH est un test de vérité. Il révèle que nos meilleures IA de mathématiques sont comme des étudiants qui ont appris par cœur un seul manuel scolaire. Ils sont excellents pour passer l'examen de ce manuel, mais s'ils doivent résoudre un problème écrit par un professeur qui utilise un style différent, ils perdent leurs moyens.

Pour que l'IA devienne un véritable partenaire de la science, elle doit apprendre à être flexible, pas juste à répéter ce qu'elle a vu.

Résumé technique

1. Problématique

Les benchmarks actuels pour la preuve de théorèmes automatisée (ATP) reposent presque exclusivement sur MathLib, la bibliothèque standard de Lean 4. Cela crée un biais majeur : les modèles d'IA sont entraînés et évalués dans un cadre définitionnel spécifique. Or, la recherche mathématique de pointe est souvent exploratoire et repose sur des constructions sur mesure (bespoke constructions) qui s'écartent des bibliothèques standard.

Le problème central soulevé par les auteurs est le suivant : Les modèles ATP actuels sont-ils capables de généraliser leur capacité de raisonnement à des cadres définitionnels nouveaux et différents de MathLib, même lorsque les problèmes mathématiques sous-jacents sont équivalents ? Les benchmarks existants ne permettent pas de distinguer la difficulté mathématique réelle de la familiarité avec une syntaxe ou des définitions spécifiques.

2. Méthodologie : TAOBENCH et TAOBENCHMATHLIB

Pour répondre à cette question, les auteurs ont développé une infrastructure expérimentale rigoureuse basée sur le livre Analysis I de Terence Tao, formalisé en Lean.

A. Construction du Benchmark (TAOBENCH)

• Source : 150 exercices extraits de la formalisation Lean de Terence Tao.
• Caractéristique clé : Tao construit les concepts fondamentaux de l'analyse (nombres naturels, ensembles, réels, limites) à partir de zéro (from scratch), en utilisant des types inductifs personnalisés et des notations qui divergent significativement de MathLib.
• Pipeline Agentique : Pour garantir une évaluation équitable, les auteurs ont créé un pipeline automatisé utilisant des agents (basés sur GPT-5 et des outils statiques comme JiXia) pour extraire un environnement local compilable et autonome pour chaque problème. Ce contexte inclut uniquement les définitions et lemmes strictement nécessaires, évitant ainsi les échecs de compilation dus à un manque de contexte ou à des importations excessives.

B. Le Contrôle Apparié (TAOBENCHMATHLIB)

• Pour isoler l'effet du cadre définitionnel de la difficulté mathématique, chaque problème de TAOBENCH a été traduit automatiquement en une formulation équivalente utilisant MathLib.
• Pipeline de Traduction :
  1. Réécriture : Un agent réécrit l'énoncé en utilisant les définitions canoniques de MathLib, avec recherche web pour s'assurer de l'exactitude syntaxique.
  2. Vérification d'Équivalence : Un agent vérifie que les états de preuve (goal states) des deux versions sont mathématiquement équivalents.
  3. Validation Humaine : Des experts en analyse et en Lean ont vérifié manuellement les traductions pour corriger les subtilités sémantiques.
• Cela crée des paires de problèmes identiques mathématiquement mais différents syntaxiquement (Tao vs MathLib).

3. Contributions Principales

1. TAOBENCH : Le premier benchmark Lean conçu spécifiquement pour tester la robustesse des modèles ATP au-delà de MathLib, en utilisant un cadre définitionnel pédagogique mais non standard.
2. TAOBENCHMATHLIB : Un ensemble de données apparié contenant les traductions MathLib des problèmes, permettant une évaluation in-distribution pour isoler la variable "cadre définitionnel".
3. Pipeline d'Extraction Agentique : Une méthode innovante pour extraire automatiquement des contextes compilables et auto-contenus à partir de projets formels massifs, résolvant le problème de la longueur de contexte et de la fidélité des énoncés.
4. Analyse de la Généralisation : Une démonstration empirique que la performance des modèles chute drastiquement hors du cadre MathLib, révélant une limite fondamentale de l'entraînement actuel.

4. Résultats Expérimentaux

Les auteurs ont évalué plusieurs modèles d'État de l'Art (SOTA) comme DeepSeek-Prover-V2, Goedel-Prover-V2 et Kimina-Prover.

• Chute de Performance : Bien que les modèles obtiennent de bons résultats sur TAOBENCHMATHLIB (souvent > 65-70 % de réussite), leur performance chute d'environ 26 % en moyenne sur TAOBENCH (les mêmes problèmes dans le cadre de Tao).
  • Exemple : Le meilleur modèle (Goedel-Prover-V2-32B) passe de 72,67 % sur MathLib à 49,33 % sur Tao.
• Impact de la Longueur de Contexte : L'analyse montre que la performance sur TAOBENCH s'effondre à mesure que le nombre de définitions locales dans le contexte augmente. Pour les problèmes avec 10+ définitions locales, le taux de réussite chute à ~6 %, tandis qu'il reste élevé sur la version MathLib. Cela indique une incapacité à intégrer et raisonner sur des définitions inconnues, même lorsqu'elles sont fournies.
• Modèles de Fondation (Frontier Models) : Les modèles de base (comme GPT-5.1) montrent une meilleure capacité d'adaptation aux définitions de Tao que les modèles spécialisés ATP, suggérant que la spécialisation excessive sur MathLib nuit à la flexibilité.
• Études de Cas :
  • Induction arrière sur les naturels : Les modèles échouent sur la version Tao car ils doivent reconstruire les propriétés arithmétiques de zéro, alors que MathLib fournit ces lemmes nativement.
  • Théorème de la compression (Squeeze Theorem) : La différence réside dans la définition de la convergence (définition explicite $\epsilon$-$\delta$ chez Tao vs filtres dans MathLib). Les modèles préfèrent souvent la formulation explicite locale, mais échouent à traduire cela vers les abstractions de filtres de MathLib, ou vice-versa selon le modèle.

5. Signification et Implications

• Limitation de la Généralisation : Les résultats démontrent que les modèles ATP actuels ne généralisent pas bien au-delà de leur distribution d'entraînement (MathLib). Ils sont "fragiles" face aux changements de formalismes, même lorsque la difficulté mathématique est identique.
• Écart entre Benchmark et Réalité : Il existe un fossé entre la performance sur les benchmarks standards et l'applicabilité réelle en recherche mathématique, où les définitions sont souvent personnalisées.
• Nécessité de Nouveaux Entraînements : Pour que les IA soient utiles aux mathématiciens de recherche, les futurs modèles doivent être entraînés sur des ensembles de données diversifiés incluant des cadres définitionnels variés, et non seulement sur MathLib.
• Outil pour la Recherche : TAOBENCH fournit une base concrète pour développer et tester des prouveurs plus robustes, capables de s'adapter à de nouveaux environnements formels sans nécessiter un réentraînement complet.

En conclusion, cet article met en lumière que la maîtrise des outils de preuve actuels est largement une question de familiarité avec un écosystème spécifique (MathLib) plutôt que d'une véritable compréhension universelle des mathématiques formelles.