Résumé technique : Optimiser le compromis coût-qualité des prouveurs de théorèmes agentiques dans Lean

Énoncé du problème

Les grands modèles de langage (LLM) ont réalisé des progrès significatifs dans la preuve automatique de théorèmes au sein de l'assistant de preuve Lean en employant des flux de travail agentiques. Ces flux de travail décomposent généralement des problèmes complexes en de plus petits lemmes, génèrent de nombreuses tentatives de preuve et utilisent le retour d'information du compilateur pour guider la recherche. Bien que cette approche permette d'obtenir des performances élevées sur des benchmarks exigeants comme PutnamBench, elle souffre de coûts computationnels prohibitifs. Les systèmes actuels allouent souvent des budgets fixes, pré-spécifiés, pour la décomposition et la génération de preuves à chaque problème, indépendamment de sa difficulté. Cette politique de « pas fixe » entraîne un gaspillage substantiel, car les agents consacrent fréquemment un calcul important à des problèmes infaisables ou à des énoncés mal formalisés qui ont peu de chances de réussir. Le défi central abordé est l'absence de conscience dynamique du coût dans les agents existants, ce qui échoue à optimiser le compromis entre la dépense de calcul et les taux de succès des preuves.

Méthodologie

Les auteurs proposent une nouvelle architecture d'Agent de Routage d'Action conçue pour remplacer les politiques statiques par des décisions de routage dynamiques et fondées sur les données. Le système est conceptuellement divisé en deux plans :

1. Plan de Données (Génération de Preuves)

Inspiré par des travaux antérieurs (ex. : Chen et al., 2025c ; Varambally et al., 2025), le plan de données gère la génération effective des preuves. Il opère via quatre modules :

• Module de Décomposition (Breakdown Module) : Un modèle polyvalent (GPT-OSS-20B) décompose le problème original en lemmes en langage naturel et en esquisses de preuves.
• Formalisateur (Formalizer) : L'agent formalise ces lemmes en code Lean en utilisant GOEDEL-FORMALIZER-V2-8B, sélectionnant le meilleur candidat qui compile sans erreurs de syntaxe ou de type.
• Prouveur de Décomposition Formelle (Formal Breakdown Prover) : Le système tente de prouver le théorème de haut niveau en utilisant les lemmes formalisés comme axiomes, guidé par l'esquisse en langage naturel.
• Prouveur de Lemmes (Lemma Prover) : Une fois la décomposition prouvée, l'agent tente de manière récursive de prouver les lemmes individuels requis par la preuve, en ajoutant de nouvelles dépendances sur une pile.

2. Plan de Contrôle (Routage Coût-Qualité)

Le plan de contrôle observe la trajectoire des tentatives de preuve échouées et décide de poursuivre la tentative sur la cible actuelle ou de terminer la trajectoire pour redémarrer avec une nouvelle décomposition. Il utilise une politique de routage légère basée sur un compromis coût-qualité :

• État ($s$) : Résume l'historique des tentatives échouées, incluant les tentatives de preuve, les résultats de compilation, les messages d'erreur et les longueurs de sortie.
• Espace d'Action : $\{ \text{TENTER (ATTEMPT)}, \text{TERMINER (TERMINATE)} \}$. L'agent échantillonne soit une autre preuve pour la cible actuelle, soit rejette la décomposition actuelle.
• Fonction d'Utilité : Le routeur calcule un score d'utilité $\tau(s) = \hat{q}(s) - \lambda\hat{c}(s)$, où :
  • $\hat{q}(s)$ est la probabilité prédite de succès pour la prochaine tentative (Qualité).
  • $\hat{c}(s)$ est le coût prédit de la prochaine tentative (mesuré en tokens de génération LLM/SFLOPs).
  • $\lambda$ est un hyperparamètre contrôlant la pénalité pour le coût de calcul.
• Règle de Décision : Si $\tau(s) > 0$, l'agent continue ; sinon, il termine la trajectoire actuelle.

Estimateurs :

• Estimateur de Coût : Suppose que les coûts de tentative sont indépendants et identiquement distribués, en utilisant le coût moyen des tentatives précédentes dans la trajectoire.
• Estimateur de Qualité : Un modèle de régression logistique entraîné pour prédire la probabilité de succès sur la base des caractéristiques de la trajectoire, spécifiquement :
  • Similarité de Preuve : Le ratio de similarité floue (fuzzy string ratio) moyen par paire des preuves normalisées (une faible similarité suggère une confusion).
  • Diversité d'Erreur : Le ratio des erreurs de compilation uniques par rapport au nombre total d'erreurs (une faible diversité suggère un mode d'échec persistant).
  • Nombre de Tentatives : Le nombre de tentatives précédentes.

Contributions Clés

1. Identification de l'Inefficacité : Le papier identifie que le passage à l'échelle à pas fixe dans les agents Lean est extrêmement inefficace et que la réduction des tentatives inutiles est essentielle pour un meilleur compromment coût-qualité.
2. Nouvelle Architecture : Le développement d'un prouveur Lean de type "lemme" équipé d'un routeur coût-qualité adaptatif en ligne qui évalue dynamiquement la valeur marginale de l'ajout de calcul.
3. Validation Empirique : La démonstration que le routeur proposé réduit considérablement le calcul gaspillé tout en maintenant une précision compétitive, prouvant que les trajectoires échouées contiennent des signaux exploitables pour l'allocation des ressources.

Résultats Expérimentaux

Le système a été évalué sur un sous-ensemble de 85 problèmes de PutnamBench, comparant l'agent de routage dynamique à une ligne de base à pas fixe et à un agent "oracle" ayant accès aux probabilités de succès de vérité terrain.

• Réduction des Coûts : À précision égale, l'agent proposé a réduit le budget requis de 25,8 % en moyenne par rapport à la ligne de base à pas fixe.
• Amélioration de la Précision : À coût égal, l'agent a obtenu une amélioration de 7,8 % du taux de résolution.
• Compromis Spécifiques :
  • Pour atteindre un taux de résolution d'environ 43,6 %, la ligne de base à pas fixe nécessitait 31,6 M de SFLOPs, tandis que l'agent de routage n'en nécessitait que 22,6 M (une réduction de coût de 28,4 %).
  • Dans un régime de budget moyen (~41,6 % de taux de résolution), l'agent a réduit les coûts de 29,6 % (17,5 M contre 24,9 M de SFLOPs).
• Études d'Ablation :
  • Importance des Caractéristiques : La « diversité d'erreur » a été identifiée comme la caractéristique la plus critique pour l'estimation de la qualité.
  • Impact du Plan de Données : L'architecture de décomposition de type lemme elle-même a amélioré le taux de résolution de près de 100 % par rapport à une approche de génération de preuve complète utilisant le même modèle 8B, approchant les performances d'un modèle 32B.
  • Écart avec l'Oracle : Bien que l'agent de routage surpasse significativement la ligne de base fixe, un écart subsiste par rapport à l'agent oracle (qui a atteint une réduction de coût de 59,9 %), suggérant une marge de progression pour l'ingénierie des caractéristiques et l'architecture des estimateurs.

Signification et Revendications

Le papier affirme que les trajectoires Lean échouées fournissent des signaux exploitables pour une allocation de ressources sensible au coût dans la preuve de théorèmes agentique. En s'éloignant des politiques statiques à pas fixe vers un routage dynamique, les agents peuvent réduire considérablement le gaspillage de calcul sans sacrifier la performance. Les auteurs positionnent ce travail comme une étape fondamentale vers un « contrôle sensible au coût » pour la preuve mathématique formelle, suggant que les futurs agents devraient allouer dynamiquement le calcul en fonction des progrès observés et des schémas d'échec plutôt qu'en assignant des budgets d'inférence de manière statique. Les résultats indiquent que les politiques à pas fixe laissent une marge substantielle pour des améliorations d'efficacité, et que les stratégies de routage peuvent efficacement atténuer les coûts inutiles.