Résumé Technique : Ax-Prover

Énoncé du Problème

Le développement de Modèles de Langage à Grande Échelle (LLM) capables d'un raisonnement formel fiable à travers divers domaines scientifiques reste un défi majeur. Les approches actuelles font face à une dichotomie :

1. Proveurs Spécialisés : Des modèles comme DeepSeek-Prover, Kimina-Prover et Goedel-Prover sont entraînés spécifiquement sur la preuve de théorèmes en Lean. Bien qu'ils obtiennent des résultats de pointe sur les benchmarks de compétitions mathématiques (par exemple, MiniF2F, PutnamBench), ils souffrent d'une généralisation limitée. Ils peinent à s'adapter à des domaines extérieurs à leurs données d'entraînement (par exemple, la physique quantique ou l'algèbre abstraite) et sont fragiles face aux mises à jour de la bibliothèque Mathlib en évolution, nécessitant souvent un réentraînement fréquent. De plus, ils manquent de la capacité d'utiliser des outils externes ou de collaborer de manière interactive avec des experts humains.
2. LLM à Usage Général : Des modèles comme Claude et GPT possèdent une connaissance étendue et de fortes capacités de raisonnement, mais manquent d'intégration native avec les assistants de preuve formelle. Ils ne peuvent pas interagir nativement avec l'environnement Lean, ce qui entraîne une division nette où ils sont accessibles mais incapables de produire des preuves rigoureuses et vérifiées par machine.

Ce fossé nécessite un système qui combine les capacités de raisonnement étendu et d'utilisation d'outils des LLM à usage général avec le rigorisme syntaxique strict et la puissance de vérification de Lean, sans nécessiter de réentraînement spécifique à un domaine ni une infrastructure lourde.

Méthodologie

Les auteurs présentent Ax-Prover, un cadre multi-agents conçu pour automatiser la preuve de théorèmes en Lean. Le système exploite le Protocole de Contexte de Modèle (MCP) pour équiper les LLM à usage général d'une suite d'outils Lean, leur permettant d'interagir dynamiquement avec l'environnement formel.

Architecture du Système

Ax-Prover emploie un flux de travail en trois agents, où chaque agent est un LLM avec des invites spécifiques :

1. Orchestrateur : Agit comme un planificateur. Il reçoit le théorème non prouvé, attribue des tâches au Proveur, gère le routage des retours du Vérificateur et détermine quand terminer la boucle d'affinement.
2. Proveur : Le cœur constructif. Il transforme itérativement les théorèmes non prouvés en preuves complètes. Le Proveur suit un processus incrémental :
   • Identifie les théorèmes cibles (marqués par sorry).
   • Génère un croquis de preuve en langage naturel.
   • Formalise le croquis en énoncés Lean (en utilisant have et sorry).
   • Propose des tactiques pour remplacer sorry.
   • Utilise les outils MCP pour inspecter les objectifs, rechercher des lemmes et diagnostiquer les erreurs avant de passer à l'étape suivante.
3. Vérificateur : Un gardien final qui compile indépendamment le fichier Lean généré en utilisant lean diagnostic messages. Il signale les erreurs et s'assure qu'aucun sorry ni erreur de niveau 1 ne subsiste avant de certifier la preuve.

Intégration des Outils

Un composant critique d'Ax-Prover est son accès aux outils Lean via le dépôt lean-lsp-mcp. Ces outils permettent au LLM de :

• Gestion de Fichiers : Lire, écrire et éditer des fichiers .lean.
• Diagnostics : Compiler le code et récupérer les messages de diagnostic pour identifier les erreurs de syntaxe ou de type.
• Inspection du Contexte : Interroger l'objectif de preuve actuel (lean goal) et les informations de survol.
• Recherche : Rechercher dans la bibliothèque Mathlib des théorèmes pertinents (lean leansearch) et des déclarations par signature de type (lean loogle).
• Exécution : Exécuter du code et tenter plusieurs stratégies de preuve.

Ce raisonnement enrichi par les outils permet au Proveur de fonctionner comme un « mathématicien prudent », élaborant des plans, explorant progressivement des idées et vérifiant la correction à chaque étape.

Contributions Clés

L'article expose trois contributions principales :

1. Cadre Ax-Prover : Un flux de travail léger et agentic reliant les LLM à usage général aux outils Lean via MCP. Il démontre des performances équivalentes ou supérieures à la fois aux LLM à usage général et aux proveurs spécialisés en mathématiques et en physique, sans nécessiter d'entraînement ni de réglage fin spécifique à un domaine.
2. Nouveaux Benchmarks : L'introduction de deux nouveaux jeux de données pour évaluer le raisonnement formel dans des domaines sous-représentés :
   • AbstractAlgebra : 100 problèmes tirés du manuel de Dummit & Foote, se concentrant sur des concepts de recherche de niveau master (groupes, anneaux, corps) plutôt que sur des énigmes de style compétition.
   • QuantumTheorems : 134 problèmes couvrant les fondements de la mécanique quantique (matrices de densité, observables, bornes d'entropie), faisant le pont entre la physique théorique et la vérification formelle.
3. Vérification Conviviale pour les Chercheurs : Une démonstration d'Ax-Prover en tant qu'assistant interactif. À travers des études de cas en cryptographie classique et quantique, le système collabore avec des experts du domaine pour formaliser et vérifier des garanties de sécurité complexes, abaissant la barrière à l'entrée pour les chercheurs sans expertise en Lean.

Résultats

Les auteurs ont évalué Ax-Prover (alimenté par Claude Sonnet 4) face à des proveurs spécialisés (DeepSeek-Prover-V2-671B, Kimina-Prover-72B) et des LLM à usage général (Sonnet) sur plusieurs benchmarks.

• Nouveaux Benchmarks (AbstractAlgebra & QuantumTheorems) :

  • AbstractAlgebra : Ax-Prover a atteint une précision de 64 %, surpassant significativement DeepSeek-Prover (24 %) et Kimina (13 %). Les modèles spécialisés ont peiné en raison du caractère hors distribution des concepts algébriques de niveau recherche.
  • QuantumTheorems : Ax-Prover a atteint une précision globale de 96 % (100 % sur les faciles, 92 % sur les intermédiaires), contre 61 % pour DeepSeek-Prover et 57 % pour Kimina. Les modèles spécialisés ont échoué à se généraliser à des définitions physiques personnalisées (par exemple, bra/ket, matrices de densité) absentes de Mathlib standard.
  • NuminaMath-LEAN : Ax-Prover a obtenu 51 % au total, surpassant DeepSeek-Prover (28 %) et Kimina (31 %), tandis que le LLM de base (Sonnet) n'a obtenu que 5 %.

• PutnamBench :

  • Sur ce benchmark exigeant de compétitions universitaires, Ax-Prover a atteint une précision de 14 %, se classant comme le modèle open-source le mieux classé et troisième au total. Il a résolu 92 problèmes, dépassant d'autres modèles open-source comme Goedel-Prover-V2 (13 %) et DeepSeek-Prover-V2 (7 %).
  • Notamment, Ax-Prover a atteint ce résultat avec un budget de calcul significativement inférieur (pass@1 avec un délai d'attente de 25 minutes) par rapport aux modèles spécialisés qui reposent souvent sur des tentatives massives en parallèle (par exemple, pass@1024).

• Analyse de l'Utilisation des Outils :

  • Le Proveur a effectué en moyenne environ 100 appels d'outils par exécution, avec des taux de réussite élevés (>99 %).
  • Ax-Prover a utilisé un ensemble plus large de tactiques (incluant change, suffices, norm_cast) par rapport aux modèles spécialisés, qui comptaient lourdement sur le réécriture locale. Cela suggère que l'intégration d'outils améliore l'exploration créative et la capacité de gérer des définitions personnalisées.

• Déploiement et Coût :

  • Ax-Prover ne nécessite que l'accès à une API, tandis que les modèles spécialisés exigent des clusters GPU haut de gamme (par exemple, H200/A100) et une expertise en MLOps.
  • Bien que les coûts API d'Ax-Prover aient été plus élevés que l'exécution de modèles spécialisés sur une seule tentative pass@1, l'écart de coût se réduit considérablement lorsque les modèles spécialisés sont exécutés avec les valeurs élevées de pass@n requises pour des performances compétitives (par exemple, DeepSeek-Prover à pass@1024 coûterait environ 307 000 $ pour 1000 points de données contre environ 4 000 $ pour Ax-Prover).

Importance et Revendications

L'article affirme qu'Ax-Prover offre une méthodologie généralisable pour la vérification formelle à travers divers domaines scientifiques, répondant aux limitations des systèmes spécialisés qui peinent à se généraliser au-delà de leurs données d'entraînement.

• Généralisation : Contrairement aux proveurs spécialisés qui sont fragiles face aux changements de bibliothèque et aux décalages de domaine, l'approche basée sur les outils d'Ax-Prover lui permet de s'adapter à de nouvelles définitions (par exemple, en physique quantique) et aux versions évolutives de Mathlib sans réentraînement.
• Collaboration : Le système comble le fossé entre l'IA et les chercheurs humains. En agissant comme un assistant interactif, il permet aux experts du domaine de s'engager dans la vérification formelle sans avoir besoin d'une expertise profonde en Lean, comme démontré dans les études de cas en cryptographie où il a aidé à identifier des lacunes subtiles dans des arguments informels.
• Efficacité : Le cadre atteint des performances compétitives ou supérieures avec un budget de calcul « plus léger », évitant le besoin d'une infrastructure spécialisée coûteuse.

Les auteurs concluent qu'Ax-Prover représente une étape vers une intelligence artificielle scientifique vérifiable, où les systèmes d'IA peuvent contribuer à la découverte scientifique grâce à un raisonnement validé formellement, soutenant à la fois la preuve de théorèmes autonome et la recherche collaborative humain-IA.