IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch

Ce papier présente IndiMathBench, un benchmark de 312 théorèmes Lean 4 vérifiés par des experts et issus des Olympiades indiennes de mathématiques, conçu pour évaluer les défis persistants de l'autoformalisation et de la preuve de théorèmes par les modèles de langage actuels.

L'essentiel

🧠 Le Défi : Transformer la Magie des Maths en Code Robotique

Imaginez que les mathématiques sont comme un langage de conte de fées, rempli d'histoires, de dessins et d'intuitions. D'un autre côté, les ordinateurs (et les robots mathématiciens) parlent un langage très strict, sans aucune ambiguïté, comme du code informatique pur et dur.

Le problème ? Les humains sont excellents pour raconter l'histoire, mais les ordinateurs ont du mal à la comprendre. C'est ce qu'on appelle l'autoformalisation : transformer un énoncé mathématique "en langage humain" en un théorème vérifiable par un ordinateur.

Jusqu'à présent, c'était comme essayer de traduire un poème en code binaire sans dictionnaire : les robots faisaient beaucoup d'erreurs, inventaient des mots qui n'existent pas, ou comprenaient mal le sens profond. De plus, il n'y avait pas assez de "livres de référence" (données d'entraînement) de haute qualité pour les entraîner.

🇮🇳 La Solution : INDIMATHBENCH (Le Nouveau Terrain de Jeu)

Les auteurs de cet article, travaillant chez Microsoft, ont créé un nouveau défi appelé INDIMATHBENCH.

Imaginez que vous voulez tester la force de nouveaux athlètes (les intelligences artificielles). Au lieu de les faire courir sur une piste usée et connue de tous (les anciens examens de mathématiques), vous leur donnez un nouveau parcours, basé sur les Olympiades Mathématiques Indiennes.

Pourquoi l'Inde ? Parce que leurs problèmes sont célèbres pour être très créatifs, surtout en géométrie (dessiner des formes) et en combinatoire (combiner des éléments), des domaines où les robots actuels sont souvent perdus.

Ce nouveau défi contient 312 problèmes soigneusement choisis. Mais le vrai secret, ce n'est pas juste les problèmes, c'est comment ils ont été préparés.

🤝 La Méthode : Le Duo Humain-Robot (L'Atelier de Traduction)

Traduire ces problèmes manuellement prendrait des années. Traduire uniquement par ordinateur donne des résultats faux. Alors, ils ont inventé une méthode hybride, un peu comme un atelier de traduction assisté par la magie.

Voici comment ça marche, étape par étape :

1. Le Robot Scribe (L'IA) : On donne le problème à une intelligence artificielle. Elle essaie de l'écrire en "Lean" (le langage des robots mathématiciens).
2. Le Contrôleur de Qualité (Le Compilateur) : Le code est immédiatement testé. Si le robot a fait une faute de grammaire ou de logique, le système lui renvoie un message d'erreur : "Non, tu as oublié de définir ce point !".
3. La Boucle de Réflexion : Le robot corrige, réessaie, et se fait corriger jusqu'à 6 fois. C'est comme un élève qui fait des brouillons jusqu'à ce que son professeur valide l'exercice.
4. L'Ensemble des Robots (Le Conseil) : Au lieu de faire confiance à un seul robot, ils utilisent 12 robots différents (comme GPT-5, Claude, etc.) pour traduire le même problème. Ils comparent leurs versions.
5. Le Maître d'Œuvre Humain : C'est ici que l'humain intervient. Il regarde un tableau de bord spécial (une sorte de cockpit) qui résume les meilleures tentatives des robots. Il ne doit pas tout écrire de zéro, mais juste vérifier, ajuster et valider.

L'analogie : Imaginez que vous voulez construire un château de cartes parfait. Les robots sont des machines qui lancent des cartes très vite, mais elles tombent souvent. L'humain est l'architecte qui regarde les chutes, dit "Non, cette carte est mal placée", et aide à stabiliser la tour. Grâce à cette aide, la construction est 3,5 fois plus rapide que si l'humain avait tout fait seul !

📉 Les Résultats : Les Robots Ont Encore du Pain sur la Planche

Une fois le défi prêt, ils ont testé les meilleurs robots du monde (les "modèles de pointe") pour voir s'ils pouvaient résoudre ces problèmes.

Les résultats sont sans appel :

• Syntaxe vs Sens : Les robots sont devenus très forts pour écrire le code correctement (pas de fautes de frappe), mais ils échouent souvent à comprendre le sens profond du problème. C'est comme écrire une phrase parfaite en français, mais qui ne veut rien dire.
• Le Mur de la Géométrie : Les robots ont énormément de mal avec la géométrie. Sur les 312 problèmes, très peu de géométrie ont été résolus. C'est comme si les robots avaient du mal à visualiser l'espace.
• Le Score Final : Même avec 10 tentatives et beaucoup d'aide, le meilleur robot (GPT-5) n'a réussi à prouver que 11 % des problèmes. C'est un score très bas, ce qui montre que la "compréhension mathématique" est encore un défi immense pour l'IA.

🚀 Conclusion : Pourquoi c'est important ?

Ce papier nous dit deux choses essentielles :

1. L'IA ne remplace pas encore l'expert humain pour les mathématiques complexes. Elle est un excellent assistant, mais pas un maître.
2. La collaboration est la clé. En créant des outils qui permettent aux humains et aux robots de travailler ensemble (comme leur tableau de bord), on peut produire des données de haute qualité beaucoup plus vite.

En résumé, INDIMATHBENCH est une nouvelle carte au trésor pour les chercheurs. Elle montre que le chemin vers des robots capables de faire des maths de niveau olympique est encore long, mais que grâce à l'aide humaine intelligente, on avance plus vite que jamais.

Et le meilleur ? Tout est gratuit ! Leurs problèmes et leurs outils sont ouverts à tous pour que tout le monde puisse continuer à apprendre et à améliorer ces robots.

Résumé technique

Voici un résumé technique détaillé du papier de recherche INDIMATHBENCH, rédigé en français.

1. Problématique et Contexte

L'autoformalisation (la traduction automatique de problèmes mathématiques informels en logique formelle vérifiable par machine, comme Lean) reste un défi majeur, même à l'ère des grands modèles de langage (LLM). Le principal goulot d'étranglement est le manque de données d'entraînement de haute qualité, appariées (énoncé informel / preuve formelle).

Les benchmarks existants (comme MINIF2F ou PutnamBench) souffrent de plusieurs limitations :

• Échelle et diversité limitées : Ils couvrent une fraction minime des problèmes de compétition mathématique (environ 1000 problèmes au total).
• Biais culturel et thématique : Ils reflètent principalement les curricula occidentaux, avec une sous-représentation marquée de la géométrie et de la combinatoire, domaines pourtant cruciaux dans les olympiades.
• Contamination des données : De nombreux problèmes populaires apparaissent déjà dans les corpus de pré-entraînement des LLM, faussant l'évaluation des capacités de raisonnement réel.
• Coût humain : La création de benchmarks nécessite une annotation manuelle experte, longue et coûteuse.

De plus, bien que les LLM améliorent la fidélité syntaxique, leur alignement sémantique avec l'intention mathématique reste faible, créant un fossé entre la validité syntaxique du code et sa correction logique.

2. Méthodologie : INDIMATHBENCH et le Pipeline Hybride

Les auteurs introduisent INDIMATHBENCH, un benchmark de 312 problèmes mathématiques de niveau olympiade (issus des Olympiades Mathématiques Régionales et Nationales de l'Inde - RMO et INMO), entièrement vérifiés par des humains et formalisés en Lean 4.

Le benchmark couvre quatre domaines : Géométrie (98), Algèbre (92), Théorie des Nombres (77) et Théorie des Ensembles/Combinatoire (45).

Pour créer ce jeu de données, l'équipe a développé un pipeline d'autoformalisation assisté par l'IA et supervisé par l'humain, composé de trois étapes clés :

1. Récupération basée sur les catégories (Category-based Retrieval) :

   • Chaque problème est classé dans une catégorie (ex: Géométrie).
   • Un agent IA explore la bibliothèque Mathlib de Lean pour extraire les définitions, théorèmes et notations pertinents à cette catégorie.
   • Ce contexte statique est injecté dans les prompts des LLM pour réduire les hallucinations et les erreurs de syntaxe (notamment pour les constructions géométriques complexes).

2. Raffinement itératif avec retour du compilateur (Iterative Refinement) :

   • Les LLM génèrent des théorèmes Lean.
   • Le code est compilé via Lean 4. Si des erreurs de syntaxe ou de type apparaissent, elles sont analysées et renvoyées au modèle pour correction.
   • Ce processus se répète jusqu'à 6 itérations, permettant d'obtenir des formalisations syntaxiquement valides pour 95,3 % des problèmes.

3. Ensemble multi-modèles et analyse comparative :

   • 12 modèles de pointe (GPT-5, Claude Opus 4, Gemini 2.5 Pro, etc.) génèrent des candidats pour chaque problème.
   • Un modèle "summarizer" (GPT-5) agrège ces sorties, identifie les erreurs communes et classe les candidats par fiabilité.
   • Cela permet de créer un espace de travail interactif où les experts humains peuvent comparer, fusionner et corriger les propositions.

Outil d'annotation : Les auteurs ont développé une extension VS Code (Dashboard) qui intègre la compilation Lean, l'affichage des erreurs, et les résumés générés par l'IA pour optimiser le travail des annotateurs humains.

3. Contributions Clés

• INDIMATHBENCH : Un nouveau benchmark de 312 théorèmes Lean 4 vérifiés par l'homme, spécifiquement conçu pour tester les limites du raisonnement formel sur des problèmes d'olympiades indiennes, comblant le vide en géométrie et combinatoire.
• Pipeline d'annotation hybride : Une méthodologie systématique combinant récupération de connaissances, boucle de débogage automatique et ensembles de modèles, validée par une étude contrôlée montrant une réduction significative du temps d'annotation (de 2h52 à 4 minutes par problème avec le système complet).
• Extension VS Code : Un outil open-source facilitant la collaboration humain-IA pour l'annotation de théorèmes Lean.
• Évaluation rigoureuse : Une analyse approfondie des capacités d'autoformalisation et de preuve automatique des modèles de pointe actuels.

4. Résultats Expérimentaux

A. Évaluation de l'Autoformalisation

Les modèles ont été évalués sur deux métriques :

• BEq (Bidirectional Equivalence) : Vérifie l'équivalence logique (sémantique) en tentant de prouver un théorème à partir de l'autre.
• GTED (Generalized Tree Edit Distance) : Mesure la similarité structurelle syntaxique.

Résultats notables :

• Performance globale : Même les meilleurs modèles (Claude Opus 4, GPT-5) n'atteignent qu'une équivalence sémantique (BEq) d'environ 17-21 % (54/312 pour Opus 4).
• Écart Syntaxique/Sémantique : Les taux de compilation réussie sont élevés (jusqu'à 77,9 % pour Claude Opus 4), mais la majorité de ces codes compilés sont sémantiquement incorrects.
• Difficulté de la Géométrie : Les modèles échouent massivement sur les problèmes de géométrie (seulement 12 succès BEq sur 108 réussites globales pour les trois meilleurs modèles), soulignant le manque de support de Mathlib pour ce domaine.
• Impact du contexte : L'utilisation de la documentation et du feedback d'erreur améliore drastiquement le taux de compilation (ex: Claude Opus 4 passe de 4,1 % à 77,9 %).

B. Évaluation de la Preuve Automatique (ATP)

Les modèles ont tenté de compléter les preuves (remplacer sorry par une preuve valide) :

• Mode Single-Turn : Très faible performance. Seuls 3 modèles ont résolu un seul problème chacun (sur 312), souvent grâce à l'appel de lemmes existants dans Mathlib.
• Mode Multi-Turn (10 itérations) : GPT-5 atteint un taux de réussite de 11,5 % (36/312) sur INDIMATHBENCH et 4 % sur PutnamBench.
• Aucune géométrie résolue : Aucun modèle n'a réussi à prouver un problème de géométrie, même avec itération.

5. Signification et Conclusion

INDIMATHBENCH démontre que, malgré les progrès des LLM, l'autoformalisation et la preuve automatique de théorèmes mathématiques complexes restent extrêmement difficiles.

• Le fossé persiste : Il existe un écart significatif entre la capacité des modèles à générer du code syntaxiquement valide et leur capacité à capturer la sémantique mathématique profonde.
• La nécessité de l'humain : L'approche "Humain-AI" s'avère indispensable. Le pipeline proposé réduit le coût d'annotation tout en garantissant une qualité de vérité terrain (ground truth) élevée, ce qui est essentiel pour entraîner les futurs systèmes.
• Limites actuelles : Les modèles peinent particulièrement avec la géométrie et les raisonnements nécessitant des constructions auxiliaires non triviales.
• Ressource ouverte : La publication du benchmark et de l'outil d'annotation vise à accélérer la recherche en preuve de théorèmes neuronale et en autoformalisation, en fournissant un testbed non contaminé et diversifié.

En résumé, ce travail met en lumière les limites actuelles des LLM pour le raisonnement formel strict et propose une voie pragmatique (collaboration humain-IA) pour construire les données nécessaires à leur amélioration future.