SorryDB: Can AI Provers Complete Real-World Lean Theorems?

Cette présentation de SorryDB, une nouvelle base de référence dynamique pour les tâches Lean issues de projets réels, révèle que les approches actuelles de preuve assistée par IA sont complémentaires et que les modèles d'agents les plus performants ne surpassent pas systématiquement les autres méthodes existantes.

L'essentiel

🧱 Le Grand Jeu du "Trou à Combler" : Pourquoi les IA ont du mal avec les vrais maths

Imaginez que vous êtes un architecte qui construit une cathédrale géante (la mathématique moderne). Pour que l'édifice soit solide, chaque pierre doit être parfaitement taillée et posée. Mais parfois, les architectes sont pressés ou bloqués. Ils posent donc une pierre provisoire, un peu comme un panneau "Travaux en cours" ou un trou béant qu'ils disent : "Je reviendrai plus tard pour finir ça."

Dans le monde des mathématiques informatisées (avec un outil appelé Lean), ce panneau s'appelle un "sorry" (qui signifie "désolé" en anglais). C'est un mot-clé qui dit au logiciel : "Je sais que cette partie devrait être prouvée, mais pour l'instant, fais comme si c'était vrai."

L'article que nous allons explorer s'intitule SORRYDB. C'est une nouvelle façon de tester les intelligences artificielles (IA) pour voir si elles peuvent vraiment aider les mathématiciens à combler ces trous.

1. Le Problème : Les IA s'entraînent sur des "Jeux Vidéo"

Jusqu'à présent, pour tester si une IA est bonne en maths, on lui donnait des problèmes de concours (comme les Olympiades Internationales).

• L'analogie : C'est comme entraîner un pilote de Formule 1 uniquement sur un circuit de karting virtuel. Il est très rapide, mais il ne sait pas conduire dans la boue, sous la pluie, ou réparer une panne sur une vraie route de campagne.
• La réalité : Les vrais projets mathématiques sur GitHub (le "GitHub" des maths) sont des chantiers en cours, désordonnés, avec des dépendances complexes. Les benchmarks actuels sont saturés (les IA ont déjà appris les réponses par cœur) et ne reflètent pas la vraie vie.

2. La Solution : SORRYDB, le "Vrai Chantier"

Les auteurs ont créé SORRYDB (la base de données des "Désolés").

• Comment ça marche ? Ils ont scanné 78 projets mathématiques réels et actifs sur GitHub. Au lieu de prendre des problèmes finis, ils ont repéré tous les endroits où les humains avaient laissé un "sorry".
• L'analogie : Au lieu de donner à l'IA un puzzle terminé à recopier, on lui donne une boîte de Legos avec un trou précis et on lui dit : "Voici la pièce manquante, assemble-la pour que tout tienne ensemble."
• Le point fort : C'est un benchmark dynamique. Dès qu'une IA résout un "trou", les humains le comblent, et de nouveaux "trous" apparaissent dans les projets. C'est comme un jeu vidéo qui se met à jour tout seul pour rester difficile.

3. L'Expérience : Qui gagne le concours ?

Les chercheurs ont testé différentes "équipes" d'IA sur 1000 de ces trous, en demandant : "Peux-tu écrire le code pour remplacer ce 'sorry' ?"

Voici les résultats, expliqués simplement :

• Les "Marteaux" (Les tactiques classiques) : Ce sont des outils automatiques simples. Ils sont rapides mais ne peuvent résoudre que des problèmes très faciles (comme serrer un écrou).
• Les "Génies Solitaires" (Les gros modèles d'IA) : Des modèles comme GPT-5 ou Claude. Ils sont intelligents, mais s'ils essaient de deviner la solution d'un coup sans vérifier, ils échouent souvent. C'est comme un étudiant qui écrit une dissertation sans la relire : il fait des erreurs de logique.
• Les "Chercheurs Actifs" (Les agents IA) : C'est la grande surprise. Ces IA ne se contentent pas de répondre. Elles agissent comme un détective :
  1. Elles proposent une solution.
  2. Elles la testent dans le vrai logiciel (Lean).
  3. Si ça plante (erreur de compilation), elles lisent le message d'erreur, comprennent leur bêtise, et réessaient.
  • Résultat : C'est la méthode la plus efficace. L'IA qui apprend de ses erreurs (boucle de rétroaction) gagne largement sur celle qui essaie juste de "deviner" une fois.

4. La Leçon : La Complémentarité est la clé

Le résultat le plus important n'est pas qu'une IA a gagné, mais qu'aucune n'a tout gagné.

• Certaines IA sont bonnes pour les exercices de cours (pédagogie).
• D'autres sont bonnes pour les problèmes de recherche pure.
• D'autres encore sont bonnes pour trouver des outils dans la bibliothèque de maths.

L'analogie finale : Imaginez une équipe de sauvetage. Vous n'avez pas besoin d'un seul super-héros qui fait tout. Vous avez besoin d'un pompier, d'un médecin et d'un ingénieur. Chacun résout un type de problème différent. SORRYDB nous montre que pour avancer en mathématiques, il faut combiner plusieurs IA, et surtout, leur donner la capacité de tester et corriger leurs propres erreurs.

En résumé

SORRYDB est un nouveau terrain de jeu pour les IA, basé sur les vrais problèmes non résolus des mathématiciens. Il prouve que pour réussir dans le monde réel, une IA ne doit pas seulement être "intelligente", elle doit être curieuse, capable de se tromper, et surtout, capable d'apprendre de ses échecs en testant ses solutions dans un environnement réel. C'est un pas de géant vers des assistants mathématiques qui nous aideront vraiment à construire la cathédrale du futur.

Résumé technique

1. Problématique et Contexte

Le domaine de la preuve de théorèmes assistée par ordinateur (ATP) a connu des progrès significatifs, notamment avec des modèles capables de résoudre des problèmes de mathématiques compétitives (Olympiades Internationales, Putnam). Cependant, les benchmarks existants (comme miniF2F ou PutnamBench) présentent plusieurs limitations majeures pour évaluer l'utilité pratique des agents IA :

• Manque de réalisme : Ils se concentrent sur des problèmes isolés et compétitifs, ne reflétant pas la complexité des projets de formalisation réels qui impliquent des dépendances complexes, un contexte local spécifique et une collaboration asynchrone.
• Saturation et contamination : Ces datasets sont souvent saturés, et les solutions peuvent avoir fuité dans les données d'entraînement des modèles commerciaux, faussant les résultats (mémoire vs raisonnement).
• Évaluation statique : Les benchmarks fixes ne permettent pas de suivre l'évolution rapide des capacités des agents face à de nouveaux défis mathématiques.

L'objectif de cet article est de combler ce fossé en proposant un environnement d'évaluation dynamique, aligné sur les besoins réels de la communauté des utilisateurs de Lean (un assistant de preuve interactif), où les tâches consistent à compléter des preuves partielles marquées par des espaces réservés (sorry).

2. Méthodologie : Le Benchmark SorryDB

Les auteurs proposent SorryDB, un benchmark dynamique et évolutif extrait de projets de formalisation actifs sur GitHub.

A. Construction du Dataset

• Source : Le dataset est généré à partir de 78 dépôts GitHub actifs hébergés dans le registre de packages Lean (Reservoir).
• Critères de sélection : Les projets doivent être sous licence open-source, actifs (au moins un commit dans les 3 derniers mois) et publics.
• Extraction des tâches : Le pipeline identifie tous les mots-clés sorry (placeholders pour des preuves non encore écrites) dans les fichiers .lean. Une tâche est définie comme le remplissage d'un sorry spécifique pour qu'il soit remplacé par une preuve valide, sans nécessairement prouver tout le théorème.
• Catégories : Les tâches proviennent de diverses catégories : pédagogiques, outils, benchmarks, bibliothèques mathématiques, et projets de formalisation de théorèmes majeurs (ex: Théorème de Fermat, Théorème de Carleson).
• Dynamisme : Contrairement aux benchmarks statiques, SorryDB se met à jour continuellement. À mesure que les preuves sont complétées par la communauté, de nouveaux sorry apparaissent, empêchant la saturation du benchmark.

B. Infrastructure de Validation

Pour évaluer une solution proposée par un modèle, le système :

1. Clone le dépôt spécifique et la branche concernée.
2. Remplace le sorry cible par la proposition du modèle.
3. Utilise l'outil LeanInteract pour compiler le projet et vérifier l'état de la preuve.
4. Valide la réussite uniquement si le projet compile sans erreur et si le sorry a été effectivement éliminé (et non simplement masqué par un autre sorry ou une astuce syntaxique).

3. Contributions Clés

1. Le Dataset SorryDB : Une procédure automatisée pour extraire et structurer des obligations de preuve réelles (sorry) issues de projets en cours, créant un dataset évolutif aligné sur l'usage quotidien des développeurs Lean.
2. Framework de Benchmarking : Un pipeline de validation automatisé capable de tester la validité des preuves dans leur contexte réel (dépendances, imports, versions de Lean), sans nécessiter d'étiquettes manuelles.
3. Évaluation Comparative : Une analyse approfondie de 1000 tâches (snapshot de janvier 2026) mettant en lumière la complémentarité des approches et l'importance des boucles de rétroaction.

4. Résultats Expérimentaux

Les auteurs ont évalué une variété d'approches sur un échantillon de 1000 tâches :

• Tactiques déterministes : (ex: trivial, grind, linarith).
• LLMs Généralistes : (GPT-5.2, Claude Opus 4.5, Gemini Flash/Pro 3, Qwen 3).
• Modèles Spécialisés : (Kimina Prover, Goedel Prover V2).
• Approches Agentic et Auto-Correctives : Modèles itératifs avec rétroaction d'erreurs (Self-Correction - SC) ou agents utilisant des outils de recherche (ReAct).

Principaux constats :

• Supériorité des approches itératives : Les méthodes itératives (Self-Correction et Agentic) surpassent massivement les approches "one-shot" (pass@1 ou pass@32). Avec 16 itérations, Gemini Flash 3 (Agentic) atteint un taux de réussite de 30,3%, contre 10,8% pour une seule tentative. La rétroaction des erreurs de compilation est cruciale.
• Complémentarité des modèles : Aucun modèle ne résout tous les problèmes. L'agrégation des résultats de tous les modèles (Combined) atteint 35,7%, montrant que chaque approche excelle sur un sous-ensemble différent de problèmes. Les tactiques déterministes résolvent des tâches que les LLMs ne peuvent pas résoudre, et vice-versa.
• Limites des modèles spécialisés : Les modèles entraînés spécifiquement pour les mathématiques compétitives (comme Goedel Prover) performent bien sur les benchmarks classiques mais moins bien sur les projets de formalisation réels, probablement en raison d'un décalage de version de Lean et d'un manque de généralisation aux contextes complexes.
• Rôle des outils : L'utilisation d'outils de recherche de bibliothèque (comme LeanSearch) aide pour certaines tâches mais peut parfois distraire le modèle (sur-reliance sur la recherche au lieu de la construction de preuve), comme illustré par des cas d'échec où un modèle plus simple sans outil a réussi.

5. Signification et Impact

• Alignement avec la communauté : SorryDB évalue les outils non pas sur leur capacité à gagner des compétitions, mais sur leur utilité réelle pour les mathématiciens et les formalisateurs qui travaillent sur des projets en cours.
• Évolutivité et robustesse : En étant dynamique, le benchmark résiste à la contamination des données d'entraînement et offre une métrique fiable pour mesurer les progrès futurs des agents IA.
• Nécessité de l'itération : L'étude démontre que pour la preuve de théorèmes dans des contextes réels, la capacité à itérer, à lire les messages d'erreur et à se corriger est plus importante que la simple puissance de génération d'un seul jet.
• Futur : Les auteurs prévoient de maintenir un classement (leaderboard) et de publier des snapshots mensuels pour suivre l'évolution de l'état de l'art.

En conclusion, SorryDB marque un tournant dans l'évaluation des prouveurs de théorèmes, passant d'une logique de compétition statique à une évaluation pratique, dynamique et centrée sur la résolution de problèmes réels dans l'écosystème Lean.