🤖 machine learning

VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving

Le papier introduit VERITAS, un cadre zero-shot qui améliore la preuve de théorèmes formels en réinjectant des signaux de vérification riches dans le processus de recherche via un protocole en deux phases de Best-of-N et de MCTS guidé par un critique, atteignant des performances de pointe sur des benchmarks comme miniF2F et un nouveau jeu de données de combinatoire.

Auteurs originaux : Manish Acharya, Zhenyu Liao, Yueke Zhang, Kevin Leach, Yu Huang, Yifan Zhang

Publié 2026-06-19

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Manish Acharya, Zhenyu Liao, Yueke Zhang, Kevin Leach, Yu Huang, Yifan Zhang

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous essayez de résoudre un casse-tête très difficile, comme un problème de mathématiques complexe, mais que vous le faites avec une équipe d'assistants IA. Habituellement, lorsque ces assistants IA tentent de résoudre un problème, ils proposent une solution, vérifient si elle fonctionne et, si elle échoue, ils reçoivent simplement un signal simple du type « Non, réessayez ». Ils jettent ainsi toutes les détails sur la raison de l'échec.

VERITAS est un nouveau système qui change la donne. Au lieu de simplement dire « Non », il écoute les raisons spécifiques de l'échec de la preuve et utilise ces raisons pour guider la tentative suivante. Considérez cela comme un détective qui ne se contente pas de dire « Le suspect est innocent », mais qui dit : « Le suspect est innocent parce qu'il était au magasin à 17h, donc cherchons quelqu'un d'autre qui était au magasin ».

Voici comment fonctionne VERITAS, décomposé en parties simples :

1. L'équipe de quatre spécialistes

VERITAS ne repose pas sur un seul cerveau IA. Il utilise une équipe de quatre agents spécialisés qui communiquent entre eux :

Le Stratège : Avant de tenter de résoudre le problème, cet agent décide d'un plan de haut niveau (par exemple, « Essayons de diviser cela par cas » ou « Essayons de prouver cela par l'absurde »). Il réduit ainsi la recherche pour que l'équipe ne perde pas de temps avec de mauvaises idées.
Le Chercheur : Cet agent est comme un bibliothécaire. Il trouve rapidement les livres de référence appropriés (règles mathématiques et lemmes) qui pourraient aider à résoudre l'étape actuelle.
Le Tacticien : C'est le travailleur principal. Il tente d'écrire les étapes réelles de la preuve. Crucialement, il consulte une liste des tentatives échouées précédentes. Si une tentative antérieure a échoué parce qu'elle a utilisé le mauvais nom pour une règle, le Tacticien est informé : « N'utilisez plus ce nom ; voici le message d'erreur ».
Le Critique : Cet agent agit comme un entraîneur. Il surveille la progression et dit : « Vous vous rapprochez » ou « Vous vous engagez dans une impasse », en se basant sur le retour spécifique de l'ordinateur qui vérifie les mathématiques.

2. Le plan de jeu en deux phases

Le système joue le jeu en deux tours distincts pour être efficace :

Phase 1 : Le « Balayage Rapide » (Best-of-N)
L'équipe fait 5 tentatives rapides et indépendantes de la solution. Si l'une d'elles fonctionne, tant mieux ! Ils s'arrêtent immédiatement. C'est rapide et cela gère les problèmes « faciles ».
Phase 2 : L'« Immersion Profonde » (Recherche guidée par le Critique)
Si le balayage rapide échoue, le système passe à un mode plus méticuleux. Il prend toutes les erreurs de la Phase 1 et les réinjecte dans le Tacticien sous forme d'« exemples négatifs ».
- Analogie : Imaginez que vous essayez d'ouvrir une porte verrouillée. En Phase 1, vous essayez 5 clés différentes rapidement. Aucune ne fonctionne. En Phase 2, au lieu d'essayer des clés au hasard, vous examinez les 5 clés qui ont coincé la serrure, notez précisément comment elles ont coincé, et utilisez ces informations pour fabriquer une nouvelle clé qui s'adapte à la forme spécifique de la serrure.

3. Pourquoi cela importe : Le problème de la « Combinatoire »

L'article a testé cela sur deux types de problèmes mathématiques.

Problèmes mathématiques standards : VERITAS en a résolu plus que les méthodes précédentes (40,6 % contre 36,9 %).
Combinatoire (problèmes de dénombrement) : C'est ici que VERITAS s'est vraiment illustré. Dans ces problèmes, il faut souvent utiliser des noms très spécifiques et exacts pour les règles mathématiques.
- Le Problème : L'IA de devinette standard a souvent tendance à « halluciner » (inventer) des noms de règles qui n'existent pas. Si une IA propose un faux nom de règle, un système standard dira simplement « Échec » et passera à la suite.
- La Solution VERITAS : Parce que VERITAS lit le message d'erreur spécifique (« Constante inconnue 'X' »), il apprend en temps réel que « X » n'existe pas. Il corrige de manière itérative le nom jusqu'à trouver le vrai.
- Résultat : Sur ces problèmes de dénombrement difficiles, le devinage standard devient en fait pire à mesure qu'il essaie (car il continue d'inventer de faux noms). VERITAS, lui, devient meilleur car il apprend de ses erreurs.

4. La garantie de « Monotonie »

Les auteurs se sont assurés que VERITAS ne perd jamais une solution qu'il a déjà trouvée.

La Garantie : Si le « Balayage Rapide » (Phase 1) résout un problème, VERITAS conserve cette solution et n'y touche plus. L'« Immersion Profonde » (Phase 2) ne travaille que sur les problèmes que la première phase n'a pas pu résoudre.
Pourquoi c'est important : Cela prouve que tout succès supplémentaire réalisé par VERITAS provient spécifiquement de la recherche intelligente pilotée par le feedback, et non pas simplement du fait d'essayer plus de devinettes aléatoires.

5. L'astuce du « Batch » (Lot)

L'une des astuces d'ingénierie ingénieuses de l'article concerne la façon dont ils vérifient les réponses.

L'ancienne méthode : Vérifier une supposition, attendre que l'ordinateur dise « Non », vérifier la suivante, attendre, vérifier la suivante... C'est lent.
La méthode VERITAS : Ils regroupent 6 suppositions dans un seul fichier et demandent à l'ordinateur de toutes les vérifier en même temps. Cela rend le système environ 10 à 20 fois plus rapide, économisant ainsi beaucoup de temps et d'argent.

Résumé

VERITAS est un système qui traite les messages d'erreur de l'ordinateur non pas comme un « panneau stop », mais comme une carte. En lisant les raisons spécifiques pour lesquelles une preuve a échoué (erreurs de syntaxe, types erronés, étapes manquantes) et en réinjectant ces informations dans la tentative suivante de l'IA, il peut résoudre des problèmes mathématiques difficiles auxquels les autres systèmes renoncent. Il combine une approche rapide de « essai et erreur » avec une approche intelligente de « apprentissage par l'échec » pour obtenir les meilleurs résultats.

Résumé Technique : VERITAS : Recherche de Preuves Guidée par le Vérificateur pour la Preuve Formelle Zero-Shot

Énoncé du Problème

Les prouveurs de théorèmes formels actuels basés sur les modèles de langage de grande taille (LLM) réduisent généralement les signaux riches et structurés des vérificateurs formels (tels que Lean 4) en un résultat binaire de type succès/échec. Les vérificateurs fournissent des retours granulaires incluant des erreurs de syntaxe, des incompatibilités de types, une progression partielle des objectifs et le statut d'achèvement de la preuve. Cependant, les pipelines standards rejettent ces artefacts intermédiaires, les résumant en récompenses scalaires ou les ignorant totalement. Cela force l'algorithme de recherche à « réapprendre » des informations que le vérificateur a déjà explicitement fournies, une limitation qui devient particulièrement coûteuse dans les preuves nécessitant des chaînes de tactiques dépendantes où la correction de chaque étape dépend de l'effet de l'étape précédente sur l'objectif.

Méthodologie : Le Cadre VERITAS

VERITAS est un cadre zero-shot conçu pour rediriger chaque signal du vérificateur vers le processus de génération de preuve. Il emploie une architecture à quatre agents coordonnée par un état de preuve partagé et un protocole de recherche en deux phases.

1. Quatre Agents Spécialisés

Tous les agents opèrent sur un ProofState partagé contenant le théorème, l'objectif actuel, les hypothèses, l'historique des tactiques et quatre signaux structurés provenant de Lean :

Stratège (Strategist) : Mappe l'état de la preuve à l'une des six stratégies de haut niveau (directe, induction, contradiction, cas, réécriture, apply_lemma) et estime la profondeur, restreignant ainsi la recherche à un sous-espace pertinent.
Récupérateur (Retriever) : Fait remonter les prémisses pertinentes de Mathlib en évaluant le chevauchement de mots-clés avec les jetons de l'objectif, les noms de lemmes et les signatures.
Critique (Critic) : Un modèle léger qui évalue les états de preuve partiels, suggérant les prochaines tactiques et des recommandations d'élagage. Il remplace les rollouts aléatoires dans MCTS par une estimation de valeur intégrant le feedback à quatre voies de Lean.
Tacticien (Tactician) : Génère $K$ candidats de tactiques conditionnés par la stratégie, les prémisses récupérées, le guidage du Critique, et crucialement, une liste des tactiques précédemment échouées avec leurs messages d'erreur Lean spécifiques injectés comme exemples négatifs.

2. Protocole en Deux Phases avec Garantie de Monotonie

Le cadre utilise un protocole conservateur en deux phases pour garantir que les gains sont attribuables au processus de recherche piloté par le feedback :

Phase 1 (Best-of-N) : Un balayage standard Best-of-N (par exemple, $N=5$ ) génère des tactiques en un seul lot. Si l'une d'elles réussit, le théorème est résolu immédiatement.
Phase 2 (Critic-Guided MCTS) : Activée uniquement si la Phase 1 échoue. L'ensemble des échecs de la Phase 1 (tactiques et leurs erreurs) est injecté dans le prompt système du Tacticien en tant qu'exemples négatifs. Le Critique guide un arbre de recherche de Monte Carlo (MCTS) où :
- Sélection : Utilise une formule UCB étendue incorporant la valeur du Critique et l'alignement stratégique.
- Expansion : Les agents s'exécutent séquentiellement ; les candidats sont validés via une astuce de Validation Lean par Lot (Batched Lean Validation).
- Simulation : Remplace les rollouts aléatoires par la valeur du Critique augmentée de signaux structurés ( $\sigma_A$ syntaxe, $\sigma_B$ type, $\sigma_C$ progression, $\sigma_D$ achèvement).
- Rétropropagation : Transporte les signaux structurés vers le haut plutôt que de les réduire à un succès/échec binaire, préservant ainsi le crédit pour la progression partielle.

Validation Lean par Lot (Batched Lean Validation) : Au lieu d'invoquer Lean $K$ fois par expansion, les candidats sont compilés dans un seul fichier .lean en tant que théorèmes privés et validés en un seul appel. Cela réduit le coût de vérification de $O(K)$ à $O(1)$ , offrant une accélération d'environ $\sim10\times$ .

Monotonie : Le protocole garantit que l'ensemble final de théorèmes résolus est un surensemble de ceux résolus par la Phase 1 seule ( $S \supseteq S_1$ ). Cela isole la contribution de la Phase 2, assurant que toute résolution supplémentaire est strictement due au MCTS guidé par le vérificateur.

Contributions Clés

Cadre à Quatre Agents Zero-Shot : Un système qui redirige le feedback structuré de Lean (syntaxe, type, progression, achèvement) dans chaque décision de génération sans fine-tuning de trace.
Protocole en Deux Phases : Une conception Best-of-N $\to$ Critic-MCTS avec une garantie interne de monotonie permettant une attribution claire des contributions de la recherche.
Optimisation de l'Efficacité : Une astuce de validation Lean par lot qui réduit le surcoût de vérification d'environ $10\times$ .
VERITAS-CombiBench : Un nouveau benchmark de 55 théorèmes de combinatoire difficiles, vérifiés par auteur, en Lean 4, publié pour exposer les limites de l'échantillonnage non guidé.
Analyse d'Attribution : Preuve empirique montrant que 11 théorèmes de miniF2F étaient uniquement solubles par la phase MCTS, ce que l'échantillonnage plat ne pouvait atteindre.

Résultats Expérimentaux

Les expériences ont été menées sur miniF2F (244 théorèmes) et VERITAS-CombiBench (55 théorèmes).

Performance miniF2F : VERITAS a atteint un taux de résolution de 40,6 % (99/244), surpassant une ligne de base Best-of-5 indépendante (36,9 %) et un Portfolio fait main (26,2 %).
- La Phase 2 a contribué à 11 résolutions uniques que l'échantillonnage plat n'avait pas pu atteindre, principalement sur des problèmes nécessitant 2 à 4 tactiques dépendantes.
- Sur les problèmes "difficiles" sans 'sorry', VERITAS a atteint 28,9 % contre 25,9 % pour Best-of-5.
Performance VERITAS-CombiBench : Ce benchmark a mis en évidence l'échec de l'échantillonnage non guidé. Le Best-of-5 n'a obtenu que 1,8 %, tombant sous le Portfolio (3,6 %) car les LLM hallucinaient des noms de lemmes Mathlib incorrects. VERITAS a atteint 7,3 % en corrigeant de manière itérative ces noms grâce au feedback d'erreur de Lean.
Efficacité : VERITAS domine la frontière de Pareto pour les méthodes d'inférence seule, atteignant un taux de résolution de 40,6 % avec environ 27 appels Lean par théorème pour un coût d'API d'environ 150 $ par balayage.
Modes d'Échec : L'analyse a montré que 32 % des échecs étaient de niveau syntaxique (hallucination de noms), 17 % étaient corrects sur le type mais erronés, et 10 % étaient des « quasi-réussites » (progression partielle de l'objectif) où le Critique pouvait fournir un guidage à haute valeur.

Signification et Revendications

L'article pose un principe de conception général : lorsqu'un vérificateur déterministe émet des signaux intermédiaires structurés, les réinjecter dans la génération amplifie les LLM de manière bien plus substantielle qu'un simple échantillonnage supplémentaire.

VERITAS démontre que :

Signaux du Vérificateur comme État : Les signaux déterminists du vérificateur peuvent servir d'état d'inférence, et non de simples vérifications finales.
Synergie des Composants : Coupler étroitement le vérificateur avec la génération est plus efficace que de passer à l'échelle soit le LLM, soit la recherche de manière isolée.
Correction Itérative : Pour les domaines nécessitant une récupération précise de lemmes (comme la combinatoire), la correction itérative à partir des erreurs du vérificateur est supérieure à l'échantillonnage plat, qui tend à halluciner des noms lexicalement incorrects.

Les auteurs concluent que, bien que VERITAS ne soit pas un remède à la créativité de niveau IMO ou à la latence interactive, sa contribution principale est le routage : collecter efficacement les preuves faciles en Phase 1 et consacrer le budget de calcul en Phase 2 uniquement là où les échecs du vérificateur peuvent guider la tactique suivante. Des travaux futurs sont identifiés pour améliorer la récupération, créer des critiques moins coûteux et distiller les traces de la Phase 2 pour étendre ce principe à la queue de problèmes difficiles restants.