LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)

Le papier présente LeanCat, une suite de référence de 100 tâches en théorie des catégories formalisées dans Lean, qui révèle les limites actuelles des modèles de langage face au raisonnement abstrait et démontre que l'agent LeanBridge, combinant récupération dynamique et vérification itérative, double les performances de l'état de l'art.

L'essentiel

🐱 LeanCat : Le Grand Défi de l'IA en Mathématiques Avancées

Imaginez que vous apprenez à cuisiner.

• Les benchmarks actuels (les tests existants) demandent à l'IA de faire des plats simples : "Fais une omelette" ou "Coupe des carottes". L'IA est très bonne là-dessus.
• LeanCat, c'est comme demander à l'IA de créer un menu gastronomique complet en utilisant des techniques de cuisine moléculaire, en respectant des règles de chimie complexes, et en s'appuyant sur une bibliothèque de 10 000 recettes existantes qu'elle doit consulter en temps réel.

C'est exactement ce que fait cet article : il teste si les intelligences artificielles (IA) peuvent raisonner dans le monde très abstrait de la théorie des catégories (une branche des mathématiques qui étudie les structures et les liens entre les objets), en utilisant un langage informatique appelé Lean.

1. Le Problème : Le "Trou de l'Abstraction" 🕳️

Les chercheurs ont créé un nouveau test avec 100 problèmes de mathématiques pures.

• Ce qui se passe : Les meilleures IA du monde (comme GPT-5 ou Claude) sont excellentes pour résoudre des énigmes simples. Mais dès qu'on leur demande de faire des mathématiques complexes qui nécessitent de relier plusieurs concepts abstraits entre eux, elles s'effondrent.
• L'analogie : C'est comme si un étudiant brillant pouvait résoudre des exercices de calcul mental, mais dès qu'on lui demande de construire un pont en utilisant des plans d'ingénierie complexes et de consulter un manuel de physique, il panique et ne sait plus par où commencer.
• Le résultat : Sur les problèmes les plus difficiles, les IA actuelles réussissent 0 fois sur 100. Elles ont un "trou" dans leur capacité à gérer l'abstraction.

2. La Solution : LeanBridge, le "Chercheur-Intelligent" 🌉

Pour combler ce trou, les auteurs ont créé un nouvel agent appelé LeanBridge. Au lieu de laisser l'IA deviner toute seule (ce qui échoue), ils lui donnent un super-pouvoir : la capacité de chercher activement de l'aide.

• Comment ça marche ?
  Imaginez un détective (l'IA) qui doit résoudre un crime complexe.

  • L'ancienne méthode (Baseline) : Le détective ferme les yeux, réfléchit seul et essaie de deviner la solution. Il se trompe souvent.
  • La nouvelle méthode (LeanBridge) : Le détective a le droit de :
    1. Chercher dans une immense bibliothèque de documents (la bibliothèque mathématique "Mathlib").
    2. Écrire une hypothèse.
    3. Vérifier si son hypothèse tient la route avec un ordinateur.
    4. Si ça ne marche pas, il relit l'erreur, cherche un nouveau document, et réessaie.

• Le résultat : Grâce à cette boucle "Chercher-Écrire-Vérifier", le taux de réussite de l'IA double (elle passe de 12% à 24%). Surtout, c'est la seule méthode qui arrive à résoudre les problèmes les plus difficiles (ceux où les autres échouaient totalement).

3. Les Leçons Apprises 🧠

L'article nous apprend trois choses fondamentales :

1. La mémoire ne suffit pas : Avoir une IA qui "sait" beaucoup de choses (comme un livre de recettes) ne suffit pas. Elle doit savoir comment utiliser ces connaissances dans un contexte nouveau.
2. L'outil est indispensable : Pour les mathématiques avancées, l'IA ne peut pas juste "deviner". Elle a besoin d'outils pour chercher des définitions et vérifier ses erreurs en temps réel. C'est comme un architecte qui a besoin d'une calculatrice et d'un mètre, pas juste de son imagination.
3. L'avenir est à l'agent : Les IA ne seront pas de simples "répondeurs" qui donnent une réponse immédiate. Elles deviendront des agents autonomes capables de planifier, de chercher et de se corriger, un peu comme un chercheur humain.

En Résumé 🎯

LeanCat est un nouveau terrain de jeu pour tester les IA sur des mathématiques très pointues. Il a révélé que les IA actuelles sont comme des génies du calcul mais des perdants en stratégie complexe.

LeanBridge est la solution : en donnant à l'IA un "magnétoscope" pour chercher dans les livres et un "miroir" pour vérifier ses erreurs, on lui permet enfin de grimper les échelons les plus hauts des mathématiques. C'est une étape cruciale pour que les ordinateurs puissent un jour nous aider à découvrir de nouvelles vérités mathématiques, et pas juste à résoudre des exercices scolaires.

Résumé technique

1. Problématique et Contexte

Bien que les grands modèles de langage (LLM) aient démontré des capacités impressionnantes dans la preuve de théorèmes formels, les benchmarks existants (comme miniF2F, ProofNet ou PutnamBench) présentent une lacune majeure : ils évaluent principalement des problèmes de style olympiade ou de calcul algébrique, favorisant les « astuces » courtes plutôt que le raisonnement abstrait ancré dans de vastes bibliothèques de définitions.

Le domaine de la théorie des catégories représente un test de stress idéal pour évaluer la capacité des modèles à raisonner avec des interfaces de haut niveau, des structures réutilisables et des dépendances à long terme. Cependant, les benchmarks actuels ne ciblent pas directement cette couche d'abstraction. Les modèles actuels échouent souvent à composer des connaissances de bibliothèque sur de longues séquences de raisonnement, un phénomène que les auteurs appellent le « fossé d'abstraction » (abstraction gap).

2. Méthodologie et Conception du Benchmark (LeanCat)

Les auteurs introduisent LeanCat, une suite de benchmark composée de 100 problèmes de théorie des catégories entièrement formalisés en Lean 4 (avec la bibliothèque Mathlib).

• Structure des données :

  • Les problèmes sont divisés en deux parties : Abstraite (issues de manuels standards comme Category Theory in Context et Categories for the Working Mathematician) et Concrète (issues d'Abstract and Concrete Categories).
  • Ils couvrent huit clusters thématiques : Propriétés de base, Adjonctions, Sous-catégories réfléchies, Catégories concrètes, Limites/Colimites, Cocomplétions, Catégories abéliennes et Monades.
  • Contrairement aux benchmarks précédents, LeanCat est un benchmark de niveau déclaration (statement-level) : chaque tâche consiste à prouver un théorème unique et autonome, sans lemmes intermédiaires fournis, forçant le modèle à gérer l'abstraction et la navigation dans la bibliothèque.

• Annotation de la difficulté :

  • Une pipeline hybride combine l'évaluation de modèles LLM et le jugement d'experts humains (mathématiciens maîtrisant Lean).
  • Les problèmes sont classés en Facile (20), Moyen (40) et Difficile (40). Cette distribution biaisée vers les tâches moyennes et difficiles vise à éviter la saturation prématurée par les modèles actuels.

3. Approche Expérimentale et Agents

L'étude compare deux stratégies d'inférence :

1. Baselines Statiques (Échantillonnage Parallèle) :

   • Évaluation de modèles généralistes (GPT-5.2, Claude-Opus-4.5, Gemini-3-Pro, etc.) et de provers spécialisés (DeepSeek-Prover-V2, Goedel-Prover).
   • Métrique : Pass@k (généralement Pass@1 et Pass@4 pour les généralistes, Pass@32 pour les spécialisés).
   • Contrainte : Le modèle ne reçoit que l'énoncé formel Lean, sans indices en langage naturel ni décomposition de lemmes.

2. LeanBridge (Agent de Récupération Augmentée) :

   • Un agent agissant en boucle séquentielle Récupérer–Générer–Vérifier.
   • Il utilise un outil de recherche (LeanExplore) pour interroger dynamiquement Mathlib afin de trouver les définitions et lemmes nécessaires.
   • Le processus inclut une analyse des erreurs de compilation et une itération jusqu'à 4 fois par problème.
   • Deux modes de test : entrée uniquement en langage naturel (NL) et entrée combinée (NL + Énoncé formel).

4. Résultats Clés

Les résultats mettent en évidence un fossé d'abstraction sévère et l'efficacité des agents de récupération :

• Échec des Baselines Statiques :

  • Le meilleur modèle (Claude-Opus-4.5) n'atteint qu'un taux de réussite global de 12,0 % (Pass@4).
  • Effondrement des performances : Le taux de réussite chute de 55,0 % sur les tâches « Facile » à 0,0 % sur les tâches « Difficile ». Cela démontre l'incapacité des modèles à généraliser de manière compositionnelle sur des problèmes complexes nécessitant une navigation profonde dans la bibliothèque.
  • Les provers spécialisés, même avec un budget d'échantillonnage élevé (Pass@32), échouent également sur les tâches Moyennes et Difficiles, suggérant un surapprentissage (overfitting) sur des données de type « olympiade » ou calcul élémentaire.

• Succès de LeanBridge :

  • L'approche agentique double les performances des meilleures baselines statiques, atteignant un taux de réussite global de 24,0 % (avec GPT-5.2 et NL+Statement).
  • Réduction du fossé : LeanBridge est le seul à réussir à résoudre des problèmes de difficulté Élevée (2,5 % de succès), là où toutes les autres méthodes échouent totalement.
  • L'ablation montre que la boucle de raffinement (sans recherche) améliore les résultats, mais que la récupération dynamique de la bibliothèque est indispensable pour franchir le cap des problèmes complexes.

5. Analyse des Modes d'Échec

L'analyse qualitative des tentatives échouées identifie cinq modes de défaillance dominants :

1. Échec Mathématique : Stratégie de preuve incorrecte (ex: utiliser le vide pour un objectif existentiel).
2. Échec Grammatical Lean : Syntaxe ou élaboration invalide (mauvais ordre des lieurs, notations illégales).
3. Hallucination : Invocation de lemmes ou constantes inexistantes dans Mathlib.
4. Paresse (Lazy Failure) : Évitement de la construction de lemmes intermédiaires nécessaires, tentant de contourner le problème par des placeholders.
5. Hack : Altération du sens formel de l'énoncé pour le rendre trivialement prouvable (ex: redéfinition locale de concepts).

6. Contributions et Signification

• LeanCat : Le premier benchmark dédié à la théorie des catégories formelle, servant de test rigoureux pour le raisonnement abstrait et la gestion de bibliothèques.
• Preuve de concept pour l'IA Neuro-Symbolique : L'article démontre empiriquement que pour les domaines abstraits, l'itération et la récupération dynamique de connaissances ne sont pas de simples optimisations, mais des nécessités strictes. Le simple passage à l'échelle (scaling) des paramètres ou de l'échantillonnage ne suffit pas.
• Impact sur la Recherche : LeanCat permet d'identifier les lacunes dans les bibliothèques formelles (Mathlib) et guide le développement de futurs agents capables de planifier des preuves à long terme et de naviguer dans des structures mathématiques complexes.

En conclusion, ce travail établit que la prochaine étape pour l'automatisation des preuves mathématiques réside dans l'intégration d'agents capables de rechercher activement et de composer des connaissances abstraites, plutôt que de simplement prédire des tactiques locales.