A Minimal Agent for Automated Theorem Proving

Les auteurs proposent une baseline minimale d'agent pour la preuve de théorèmes, intégrant les fonctionnalités essentielles des systèmes de pointe, qui démontre des performances compétitives avec une architecture plus simple et une meilleure efficacité d'échantillonnage grâce à une approche itérative, tout en étant disponible en open source.

L'essentiel

Voici une explication simple et imagée de l'article, comme si on en parlait autour d'un café.

🧠 Le Problème : L'Architecte qui oublie ses plans

Imaginez que vous essayez de construire une maison (c'est la preuve mathématique) avec un architecte très intelligent mais un peu distrait (c'est l'Intelligence Artificielle).

Dans le passé, pour prouver des théorèmes complexes, les chercheurs ont construit des usines gigantesques et coûteuses. Ils ont entraîné des robots sur des millions de plans, leur ont donné des outils ultra-complexes et ont dépensé des fortunes en électricité. C'est comme si on utilisait un robot de 10 tonnes pour assembler un Lego : ça marche, mais c'est cher, lent et compliqué à installer chez soi.

De plus, ces robots avaient tendance à tourner en rond. Si l'architecte se trompait de brique, il recommençait la même erreur encore et encore, sans jamais se rendre compte qu'il fallait changer de stratégie.

🚀 La Solution : "AxProverBase", le Petit Apprenti Intelligents

Les auteurs de cet article (de l'entreprise Axiomatic AI à Barcelone) ont dit : "Et si on simplifiait tout ?"

Ils ont créé un système minimaliste, qu'ils appellent AxProverBase. Au lieu d'une usine, c'est un petit atelier bien organisé avec trois règles d'or. Imaginez un apprenti architecte qui a trois super-pouvoirs :

1. Le Cycle de "Brouillon-Feedback" (L'Art de l'Essai-Erreur)

C'est le cœur du système.

• L'ancien système : L'IA essayait de construire la maison d'un seul coup. Si elle se trompait, c'était perdu.
• Leur système : L'IA propose un plan (un brouillon). Un inspecteur (le compilateur) vérifie si ça tient debout.
  • Si ça s'effondre, l'inspecteur ne dit pas juste "C'est nul". Il donne un rapport précis : "Attention, le mur du salon est mal posé, la fondation glisse."
  • L'apprenti lit le rapport, corrige le plan, et réessaie.
  • L'analogie : C'est comme apprendre à faire du vélo. On tombe, on se relève, on ajuste l'équilibre, et on réessaie. On n'essaie pas de faire le Tour de France dès la première seconde.

2. Le "Carnet de Notes" (La Mémoire)

C'est ici que la magie opère pour éviter de tourner en rond.

• Souvent, l'IA oublie qu'elle a déjà fait cette erreur il y a 5 minutes. Elle recommence la même bêtise.
• AxProverBase a un carnet de notes intelligent. À chaque échec, l'IA écrit dans son carnet : "Aujourd'hui, j'ai appris que le mur du salon ne peut pas être en bois, il faut du béton."
• Au prochain essai, elle lit son carnet avant de commencer. Elle ne refait plus l'erreur. C'est comme un détective qui consulte son dossier avant de retourner sur les lieux du crime.

3. La Bibliothèque et Google (Les Outils)

Parfois, l'apprenti ne connaît pas la bonne technique.

• Le système lui permet de consulter la bibliothèque des mathématiques (Mathlib) pour trouver des théorèmes existants, ou même de faire une recherche sur Google pour trouver une stratégie.
• La surprise : Les auteurs ont découvert que c'est le moins important des trois ! Avoir un bon carnet de notes et savoir corriger ses erreurs est beaucoup plus puissant que d'avoir accès à toute la bibliothèque du monde.

🏆 Les Résultats : Simple mais Efficace

Quand ils ont testé leur "petit apprenti" contre les "géants" (les systèmes complexes et coûteux) sur des concours de maths difficiles (comme le Putnam, l'équivalent des Olympiades pour les étudiants américains), le résultat a été bluffant :

• Performance : Leur système simple a obtenu des résultats aussi bons, voire meilleurs, que les systèmes ultra-complexes.
• Coût : C'est beaucoup moins cher. Là où les autres dépensent des milliers de dollars par problème, leur système en coûte quelques centimes.
• Vitesse : C'est beaucoup plus rapide à mettre en place. Pas besoin de construire une usine, juste d'ouvrir un logiciel.

💡 La Leçon à retenir

L'article nous dit quelque chose de très important pour l'avenir de l'IA : On n'a pas besoin de robots de plus en plus gros et complexes pour tout résoudre.

Parfois, ce dont on a besoin, c'est juste d'une méthode de travail intelligente :

1. Essayer.
2. Écouter les critiques.
3. Se souvenir de ses erreurs.
4. Réessayer.

C'est comme si on avait découvert que pour gagner une course, il ne faut pas nécessairement une Ferrari (le modèle IA le plus puissant), mais un bon conducteur qui sait corriger sa trajectoire à chaque virage (l'agent itératif).

En résumé, AxProverBase est une boîte à outils simple, gratuite et ouverte à tous, qui permet à n'importe qui de prouver des théorèmes mathématiques complexes sans avoir besoin d'être un expert en ingénierie ou d'avoir un budget de milliardaire. C'est une victoire de la sagesse sur la force brute.

Résumé technique

Voici un résumé technique détaillé de l'article « A Minimal Agent for Automated Theorem Proving » (Un agent minimal pour la preuve de théorèmes automatisée), rédigé en français.

1. Problématique et Contexte

La preuve de théorèmes automatisée (ATP) représente un défi majeur pour le raisonnement scientifique vérifiable en intelligence artificielle. Bien que des outils interactifs comme Lean (et sa bibliothèque Mathlib) soient puissants, leur adoption par la communauté scientifique reste limitée en raison de la complexité des systèmes existants.

Les approches actuelles (comme AlphaProof, Hilbert, Seed-Prover) reposent souvent sur des architectures complexes impliquant :

• Des boucles de rétroaction par renforcement (RL) sur de vastes ensembles de données synthétiques.
• Des mécanismes de recherche d'arbres (Tree-Search) coûteux en calcul.
• Des infrastructures lourdes difficiles à déployer.

De plus, la rapidité d'évolution des modèles de langage (LLM) et des bibliothèques formelles (Mathlib) rend difficile l'isolation des sources de performance : une amélioration provient-elle d'une innovation architecturale ou simplement d'un LLM plus puissant ? L'objectif est de créer une approche simple, abordable et efficace qui puisse servir de référence (baseline) tout en étant compétitive.

2. Méthodologie : AxProverBase

Les auteurs proposent AxProverBase, un agent minimaliste conçu pour décomposer les éléments essentiels du succès des systèmes actuels. L'architecture est modulaire et repose sur trois piliers principaux, illustrés dans une boucle itérative :

A. Architecture Modulaire

L'agent se compose de trois modules interconnectés :

1. L'Agent Propositeur (Proposer) : Un LLM généraliste (ou spécialisé) chargé d'écrire du code Lean pour prouver un théorème. Il peut utiliser des outils (recherche de bibliothèque, recherche web) avant de générer une proposition.
2. Le Système de Révision (Review System) :
   • Compilateur : Vérifie si le code compile. Si ce n'est pas le cas, il renvoie les erreurs de compilation. Si le code compile mais contient des sorry (placeholders), il renvoie l'état des objectifs restants.
   • Agent Réviseur : Vérifie que l'énoncé du théorème n'a pas été modifié et qu'aucun "truc" (comme l'utilisation de tactiques incomplètes qui compileraient mais ne prouveraient rien) n'a été utilisé.
3. Le Système de Mémoire : Gère le contexte entre les itérations pour éviter que l'agent ne tourne en rond.

B. Stratégies Clés

• Raffinement Itératif : Contrairement à la génération "one-shot" (tentative unique), l'agent utilise les retours du compilateur pour corriger et améliorer sa preuve étape par étape.
• Gestion de la Mémoire (Self-Managed Context) : Au lieu de garder tout l'historique (ce qui gonfle le contexte et coûte cher), l'agent maintient un "cahier de laboratoire" synthétisé. Il réfléchit sur ses échecs passés pour extraire des leçons clés et éviter de répéter les mêmes erreurs.
• Outils de Recherche : Intégration de LeanSearch (pour trouver des lemmes dans Mathlib) et de Tavily (recherche web pour des stratégies), utilisés de manière limitée avant la génération.

3. Contributions Principales

1. Démystification des facteurs de performance : L'étude montre que la capacité à effectuer un raffinement itératif est le facteur le plus déterminant pour la réussite, surpassant de loin la complexité architecturale.
2. Efficacité de la mémoire : Un mécanisme de mémoire auto-géré (réflexion) est supérieur à un simple historique de tentatives. Il permet d'éviter les cycles d'erreurs répétitives, augmentant la performance de 7 % tout en réduisant les coûts de 20 %.
3. Architecture Minimaliste et Compétitive : AxProverBase démontre qu'une architecture simple, sans fine-tuning spécifique ni entraînement par renforcement complexe, peut rivaliser avec des systèmes d'état de l'art (SOTA) beaucoup plus lourds.
4. Base de référence Open Source : Le code est publié pour servir de baseline évolutive, capable de s'améliorer naturellement avec les progrès des LLMs sans nécessiter de réentraînement.

4. Résultats Expérimentaux

Les expériences ont été menées sur plusieurs benchmarks, notamment PutnamBench (mathématiques de niveau undergraduate), FATE (algèbre abstraite) et LeanCat (théorie des catégories).

• Performance vs Complexité :

  • Sur PutnamBench, AxProverBase (utilisant Claude Opus 4.5) atteint 54,7 % de réussite en une seule tentative (pass@1), surpassant des systèmes complexes comme Hilbert (qui nécessite 1840 tentatives pour atteindre ~70 %) et DeepSeek-Prover-V2 (7,1 % en pass@1).
  • Sur FATE-M (algèbre abstraite), il atteint 98 % de réussite, contre ~62 % pour les meilleurs systèmes existants.
  • Sur LeanCat, il obtient 59 %, démontrant une capacité à gérer des domaines de recherche avancés.

• Analyse des Composants (Ablation Study) :

  • La génération "one-shot" (sans itération) est inefficace (< 5 % de réussite).
  • L'ajout de la rétroaction itérative double la performance.
  • L'ajout de la mémoire améliore encore significativement les résultats et la stabilité.
  • Les outils de recherche apportent une amélioration marginale mais utile.

• Coût-Efficacité :

  • Le coût moyen par échantillon est d'environ 12,6 $, avec un temps d'exécution un ordre de grandeur inférieur à celui de Hilbert.
  • Les modèles "plus intelligents" (comme Claude Opus) bénéficient davantage de l'architecture agentic que les modèles plus légers, suggérant que le cadre permet d'exploiter pleinement les capacités des LLMs de pointe.

5. Signification et Impact

Ce travail démontre que la course à la complexité architecturale n'est pas toujours nécessaire pour atteindre des performances élevées en preuve de théorèmes.

• Accessibilité : En réduisant la barrière à l'entrée (pas de fine-tuning massif, infrastructure simple), cela rend la preuve formelle accessible à une communauté plus large de chercheurs et d'ingénieurs.
• Évolutivité : Le système est conçu pour s'améliorer automatiquement à mesure que les LLMs sous-jacents progressent, offrant une baseline robuste pour la recherche future.
• Pragmatisme : La réussite sur des benchmarks de recherche (FATE, LeanCat) indique que cette approche simple est déjà applicable dans des scénarios réels de projets mathématiques complexes, permettant de prouver rapidement une grande partie des théorèmes nécessaires.

En conclusion, AxProverBase prouve qu'un agent minimal, centré sur l'itération, la mémoire contextuelle intelligente et l'utilisation judicieuse des outils, constitue une alternative puissante et économique aux systèmes de preuve automatisée surdimensionnés.