FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?

Le papier présente FormalProofBench, un benchmark privé évaluant la capacité des modèles d'IA à générer des preuves mathématiques de niveau universitaire vérifiables formellement en Lean 4, révélant que le meilleur modèle atteint une précision de 33,5 %.

L'essentiel

🧠 Le Grand Défi des Mathématiques : Les IA peuvent-elles prouver leurs dires ?

Imaginez que vous êtes un professeur de mathématiques très exigeant. Vous avez un élève (une Intelligence Artificielle) qui vous explique comment résoudre un problème complexe. L'élève écrit une réponse très convaincante, avec de beaux mots et une logique qui semble parfaite.

Le problème ? En mathématiques, on ne peut pas se fier aux apparences. Une petite erreur de logique, un cas oublié, ou une règle inventée de toutes pièces, et toute la démonstration s'effondre. C'est comme construire un gratte-ciel sur des fondations en mousse : ça a l'air beau, mais ça va s'écrouler.

C'est là qu'intervient FormalProofBench, le nouveau "terrain de jeu" créé par les chercheurs pour tester les IA.

🏗️ L'Analogie du "Juge Robot" (Lean 4)

Dans le monde réel, un humain peut relire un devoir et dire : "C'est plausible". Mais en mathématiques de haut niveau (niveau master ou doctorat), le "plausible" ne suffit pas.

Les chercheurs ont créé un juge robotique infaillible appelé Lean 4.

• L'IA doit écrire sa preuve non pas en français ou en anglais, mais dans un langage informatique très strict (le langage Lean).
• Le Juge ne lit pas les mots. Il vérifie chaque brique de la preuve. Si une seule brique est mal posée, le bâtiment s'effondre et le juge dit : "Échec".
• Si tout est parfait, le juge dit : "Validé".

Il n'y a pas de demi-mesure. Soit la preuve passe le test, soit elle échoue. C'est comme un code informatique : ça compile ou ça ne compile pas.

🎓 Le Niveau du Test : "Le Doctorat"

La plupart des tests d'IA actuels demandent de résoudre des problèmes de type "olympiade" (niveau lycée) ou des énigmes logiques simples. C'est comme demander à un élève de faire des calculs de base.

FormalProofBench, lui, demande aux IA de résoudre des problèmes de niveau universitaire avancé (analyse, algèbre, probabilités, logique).

• C'est comme demander à un élève de lycée de résoudre les équations d'un physicien Nobel.
• Les problèmes viennent de vrais examens de fin d'études et de manuels universitaires.

🤖 Le Résultat : Qui est le meilleur ?

Les chercheurs ont mis en compétition les IA les plus puissantes du monde (comme Claude, GPT-5, Gemini, etc.). Elles avaient le droit d'utiliser des outils pour les aider :

1. Une bibliothèque de référence (pour chercher des théorèmes existants).
2. Un laboratoire d'essai (pour écrire du code, tester leur preuve, voir où ça coince, et réessayer).

Le verdict est sans appel :

• Même la meilleure IA du moment (Claude Opus 4.5) n'a réussi qu'33,5 % des problèmes.
• C'est-à-dire qu'elle a échoué sur deux tiers des exercices, même avec beaucoup de temps et d'outils à sa disposition.
• Les autres modèles ont fait beaucoup moins bien, certains réussissant moins de 5 % des cas.

L'analogie du coureur : Imaginez une course de 100 mètres. Les IA actuelles sont capables de courir très vite sur les 10 premiers mètres (les problèmes faciles), mais dès qu'elles doivent gérer la complexité et la précision requises pour le reste du parcours, elles trébuchent.

🔍 Ce que nous avons appris (Les leçons)

1. L'importance de l'essai-erreur : Les IA qui réussissent le mieux sont celles qui n'essaient pas de tout deviner d'un coup. Elles écrivent un bout de code, le testent, voient l'erreur, corrigent, et réessaient. C'est comme un artisan qui teste son marteau avant de frapper le clou.
2. Le piège de la recherche : Certaines IA passent trop de temps à chercher des informations dans la bibliothèque sans jamais essayer de construire la preuve. C'est comme un étudiant qui lit tout le dictionnaire au lieu de rédiger son devoir.
3. L'écart entre "dire" et "faire" : Une IA peut expliquer une solution en langage naturel de manière brillante, mais dès qu'elle doit la formaliser rigoureusement, ses erreurs cachées apparaissent.

🚀 Pourquoi c'est important pour le futur ?

Ce test est une étape cruciale. Aujourd'hui, les mathématiciens doivent vérifier manuellement chaque preuve, ce qui prend du temps et est sujet aux erreurs humaines.

Si un jour une IA peut passer ce test avec succès (100 % de réussite), cela signifiera qu'elle peut devenir un assistant de recherche réel. Elle pourrait aider les humains à :

• Découvrir de nouveaux théorèmes.
• Vérifier des preuves complexes en quelques secondes.
• Démocratiser l'accès aux mathématiques de pointe.

Pour l'instant, nous sommes encore à l'aube de cette révolution. Les IA sont brillantes, mais elles ne sont pas encore prêtes à remplacer les mathématiciens. Elles doivent encore apprendre à être aussi rigoureuses que le juge robotique.

Résumé technique

1. Problématique et Contexte

Les modèles de langage (LLM) ont montré des progrès significatifs en raisonnement mathématique sur des benchmarks informels (comme MATH ou GSM8K). Cependant, ces évaluations reposent sur des solutions en langage naturel, qui peuvent masquer des erreurs logiques subtiles, des cas omis ou des lemmes inexistants, difficiles à détecter même par des experts humains.

Le papier identifie le besoin crucial d'une méthode d'évaluation déterministe et vérifiable formellement. L'objectif est de déterminer si les modèles d'IA peuvent non seulement générer des arguments plausibles, mais produire des preuves mathématiques rigoureuses au niveau graduate (master/doctorat) qui passent la vérification d'un assistant de preuve.

2. Méthodologie : FormalProofBench

A. Construction du Benchmark

• Nature des tâches : Chaque tâche associe un énoncé de problème en langage naturel à sa formalisation correspondante en Lean 4 (un assistant de preuve interactif).
• Contenu : Le benchmark comprend 200 problèmes issus d'examens de qualification (qualifying exams) et de manuels standards. Les domaines couverts incluent l'analyse réelle et fonctionnelle, l'algèbre, la théorie des probabilités, la géométrie algébrique, la théorie des nombres et la logique.
• Qualité des données : Les problèmes ont été formalisés par des doctorants et experts en Lean 4, puis soumis à une révision secondaire rigoureuse pour éviter les erreurs de formalisation (misformalization), un problème courant dans les benchmarks existants.
• Critère de réussite : Une preuve est considérée correcte uniquement si elle est acceptée par le noyau (kernel) de Lean 4. C'est un signal binaire (succès/échec) totalement automatisé.

B. Environnement d'Évaluation (Agentic Harness)
Contrairement aux évaluations en "un seul passage" (one-shot), les modèles opèrent dans un environnement agentique avec un budget de 40 tours d'interaction par problème.

• Outils fournis :
  • lean_loogle : Un moteur de recherche pour interroger la bibliothèque Mathlib (théorèmes et définitions).
  • lean_run_code : Un exécuteur de code Lean permettant de compiler des fragments de preuve, d'obtenir des retours d'erreurs, de vérifier les types et d'itérer sur la solution.
  • submit_proof : L'outil final pour soumettre la preuve complète.
• Prompting : Les modèles reçoivent l'énoncé informel, la formalisation Lean, et des instructions spécifiques sur la syntaxe Lean 4 (naming convention, tactiques, etc.).

3. Contributions Clés

1. Nouveau Benchmark Rigoureux : Présentation de FormalProofBench, un benchmark privé, non contaminé (les formalisations spécifiques sont peu susceptibles d'être dans les données d'entraînement), et déterministe pour évaluer les capacités de preuve formelle au niveau supérieur.
2. Évaluation des Modèles de Pointe : Évaluation comparative de modèles fondationnels (OpenAI, Anthropic, Google, DeepSeek, etc.) sur des problèmes de niveau graduate, dépassant les niveaux olympiades habituels.
3. Analyse des Coûts et Latences : Fourniture de métriques détaillées sur le coût financier et le temps de latence nécessaires pour résoudre ces problèmes complexes dans un cadre agentique.
4. Analyse des Patterns d'Utilisation des Outils : Mise en évidence du lien entre l'itération via l'exécution de code et la réussite, contrastant avec l'usage excessif de la recherche.

4. Résultats Principaux

Performance des Modèles

• Le modèle le plus performant est Claude Opus 4.5 (Thinking) avec une précision de 33,5 %.
• Une chute rapide des performances est observée ensuite :
  • Gemini 3 Pro : 18,5 %
  • Claude Sonnet 4.5 : 18,0 %
  • GPT-5 : 17,0 %
  • Les modèles les plus faibles (ex: Grok 4.1, DeepSeek V3.2 Thinking) tombent en dessous de 5 %.
• Cela indique que même les modèles les plus avancés peinent encore à maîtriser la preuve formelle complexe au niveau graduate.

Analyse des Outils et Échecs

• Corrélation Exécution-Code : Les modèles performants utilisent fréquemment lean_run_code pour obtenir des retours d'erreur immédiats et itérer vers la solution.
• Piège de la Recherche : Un mode d'échec courant consiste à effectuer une recherche excessive (lean_loogle) pour trouver des lemmes inexistants ou inadaptés, sans valider par l'exécution.
• Latence et Coût : La résolution d'un problème prend en moyenne plus d'une heure (latence murale) et coûte entre 0,10 $ et 1,34 $ par test, soulignant la complexité computationnelle de la tâche.

Exemples d'Échec vs Succès
L'annexe illustre que même lorsque la stratégie de preuve est correcte (ex: décomposition d'une somme infinie), les modèles échouent souvent à la gestion fine des classes de types (type classes) de Lean ou à la résolution d'instances, là où les modèles réussissants construisent explicitement les instances nécessaires.

5. Signification et Perspectives

Impact sur la Pratique Mathématique
Le papier suggère que l'écart entre la compétence mathématique informelle et formelle reste un goulot d'étranglement majeur. Cependant, la progression rapide des modèles (33,5 % de réussite sur des problèmes graduate est un signal fort) indique que nous nous approchons d'un seuil où l'IA pourrait devenir un outil pratique pour les mathématiciens, permettant une exploration rapide de stratégies de preuve avec un retour de vérification immédiat.

Futur de la Recherche

• Évolution des Outils : L'interface de recherche actuelle (Loogle) semble être un goulot d'étranglement ; des alternatives comme la recherche sémantique ou le greppage de code local pourraient améliorer les performances.
• Niveau Recherche : Le benchmark actuel est limité par la couverture de Mathlib. Les futures versions pourraient cibler des théorèmes de recherche pure non encore formalisés.
• Démocratisation : L'amélioration de ces capacités pourrait démocratiser l'accès aux méthodes formelles, au-delà de la petite communauté d'experts en assistants de preuve.

En conclusion, FormalProofBench établit une nouvelle norme pour l'évaluation de l'IA en mathématiques, passant de la génération de texte plausible à la production de preuves vérifiables par machine, tout en révélant les limites actuelles et les leviers d'amélioration (itération par code) des systèmes d'IA.