Résumé Technique : Formaliser une fois, éditer le reste (BASE)

1. Énoncé du problème

Alors que les modèles de langage de grande taille (LLM) sont de plus en plus appliqués au raisonnement mathématique, ils génèrent souvent de multiples chemins de raisonnement distincts et des réponses candidates pour un même problème. Un défi critique apparaît lors de la sélection de la réponse : comment vérifier quel candidat est correct sans avoir accès aux étiquettes de vérité terrain (ground-truth) lors de l'augmentation de l'échelle au moment du test (test-time scaling).

Bien que les approches existantes, telles que le vote majoritaire ou les modèles de récompense appris, offrent des signaux statistiques, elles manquent de garanties formelles. Des travaux récents ont exploité les assistants de preuve formelle (spécifiquement Lean 4) pour vérifier les candidats. Dans ce paradigme, un « autoformaliseur » traduit un problème et une réponse candidate en un énoncé de théorème Lean affirmant la correction de la réponse. Un prouveur tente ensuite de vérifier cet énoncé.

Cependant, un goulot d'étranglement important subsiste : pour vérifier $K$ réponses candidates, l'autoformaliseur doit être invoqué $K$ fois de manière indépendante. Cela induit un coût computationnel de $\Theta(K)$, qui croît linéairement avec le nombre d'échantillons. Les auteurs observent que pour un même problème, les $K$ énoncés formels sont presque identiques, partageant la même structure de problème et ne différant que par l'expression de la réponse. Le problème central est de savoir comment exploiter cette structure partagée pour réduire les coûts de formalisation de $\Theta(K)$ à $\Theta(1)$ sans sacrifier la précision de la sélection.

2. Méthodologie : Le pipeline BASE

Les auteurs proposent BASE (Base-and-Substitute-Edit), un pipeline conçu pour formaliser un candidat « de base » unique et dériver les $K-1$ énoncés restants par une édition localisée.

2.1 Découverte de la base

Le pipeline commence par un solveur en amont générant une liste classée de $K$ réponses candidates, $S(x) = (a_1, \dots, a_K)$, ordonnée selon la confiance du solveur.

• Le système itère à travers les candidats par ordre de rang.
• Pour chaque candidat $a_i$, il tente de formaliser la paire problème-réponse $(x, a_i)$ en un énoncé Lean $F_i$.
• Le processus s'arrête au premier candidat $a_b$ dont la formalisation $F_b$ parvient à vérifier son type (type-check) dans Lean.
• $F_b$ devient la formalisation de base, et $a_b$ est la réponse de base.
• Si aucun candidat ne vérifie son type, le système revient au candidat le mieux classé $a_1$.

2.2 Cascade de substitution

Une fois une base valide $F_b$ établie, le système génère les $K-1$ énoncés restants en éditant $F_b$ sur place pour refléter les autres candidats. Cela est géré par une cascade à deux niveaux :

1. Niveau 1 (R1) : Localisation directe basée sur des règles

   • Le système tente de localiser l'expression de la réponse dans $F_b$ via une correspondance de chaînes exacte au sein d'une « région de garde » (le corps du théorème, excluant les commentaires/en-têtes).
   • Si une correspondance unique est trouvée, le système effectue une substitution directe de la chaîne de la réponse.
   • Si plusieurs correspondances apparaissent, un petit modèle de désambiguïsation sélectionne le slot correct.
   • Ce niveau est efficace mais échoue lorsque l'autoformaliseur encode la réponse sous une forme syntaxiquement diverse (par exemple, un tuple (3, 5) encodé comme des liaisons séparées ou une valeur Prod) plutôt que sous une chaîne de caractères verbatim.

2. Niveau 2 (R2) : LEANSCRIBE (Réécrivain appris)

   • Pour les cas où R1 échoue, le système invoque LEANSCRIBE, un LLM spécialisé et affiné (fine-tuned).
   • Entrée : Le problème $x$, la formalisation de base $F_b$, et la réponse de base $a_b$.
   • Sortie :
     • Un bloc local $s$ : Un segment contigu de $F_b$ contenant l'expression dépendante de la réponse.
     • Une fonction de remplissage $f$ : Une fonction Python légère qui mappe toute réponse informelle $a_i$ vers l'expression Lean correspondante remplaçant $s$.
   • Exécution : LEANSCRIBE s'exécute une seule fois par problème. La fonction $née$ $f$ est ensuite appliquée à tous les candidats restants $a_i$ pour produire leurs énoncés formels $F_i = f(a_i)$. Cela amortit le coût de l'appel au modèle sur l'ensemble des $K-1$ candidats.

2.3 Vérification et Sélection

Le pipeline repose sur la vérification du type de l'énoncé comme signal de sélection principal.

• Un candidat est considéré comme « vérifié » si son énoncé formel $F_i$ vérifie son type dans Lean (c'est-à-dire s'il s'agit d'une proposition bien formée).
• Le système sélectionne le candidat le mieux classé $a_j$ tel que $F_j$ vérifie son type.
• Si aucun candidat ne vérifie son type, il revient au premier candidat classé $a_1$.
• Les auteurs notent que bien que la vérification au niveau de la preuve (exécution d'un prouveur) soit plus rigoureuse, les prouveurs actuels ont des taux pass@1 faibles, faisant de la vérification du type de l'énoncé un signal plus pratique pour la sélection dans ce contexte de budget contraint.

3. Contributions clés

1. Pipeline BASE : Le premier travail qui amortit les coûts de formalisation en partageant un énoncé de base vérifié unique entre plusieurs candidats, réduisant les appels à l'autoformaliseur de $\Theta(K)$ à $\Theta(1)$.
2. Modèle LEANSCRIBE : Un réécrivain appris entraîné pour localiser des blocs dépendants de la réponse et générer des fonctions d'édition réutilisables, gérant les variations syntaxiques que la substitution par règles ne peut traiter.
3. Amélioration de Pareto : La méthode atteint une précision de sélection plus élevée tout en réduisant considérablement le coût computationnel à travers toutes les configurations testées.

4. Résultats expérimentaux

Les auteurs ont évalué BASE sur quatre benchmarks (MATH-500, OlympiadBench, AMC-AIMO, AIME 2024) en utilisant trois solveurs en amont différents (Gemini 3 Pro, Qwen3-8B, DeepSeek-R1-Qwen3-8B) avec $K=8$ candidats.

• Précision : BASE a amélioré la précision de sélection (Acc) dans les 12 configurations (jeu de données, solveur) par rapport à une formalisation indépendante, avec des gains allant de +0,7 à +23,3 points de pourcentage.
• Robustesse : Le taux de « passage de la réponse d'or » (GT-pass) — la fraction des problèmes où l'énoncé de la réponse correcte vérifie son type — a augmenté de manière significative (jusqu'à +33,3 points), atteignant 96–100 % dans de nombreux cas. Cela indique que le partage d'une base vérifiée rend la formalisation de la réponse correcte plus robuste.
• Efficacité des coûts : À $K=8$, BASE a réduit le nombre d'appels à l'autoformaliseur d'environ 5,4× (réduction moyenne de 4,7–6,5×). Le coût suit une échelle de $\Theta(1)$ plutôt que $\Theta(K)$.
• Ablation : Le retrait du réécrivain appris (LEANSCRIBE) et le recours exclusif à la substitution par règles (R1) ont entraîné une chute significative de la couverture des candidats (8–22 points de pourcentage), démontrant la nécessité de la composante apprise pour gérer les divers encodages syntaxiques.
• Analyse au niveau de la preuve : Même en utilisant un prouveur (DeepSeek-Prover-V2) avec une seule tentative par candidat, BASE a amélioré la précision au niveau de la preuve dans 11 des 12 configurations, suggérant que des énoncés formels mieux structurés aident les prouveurs en aval.

5. Signification et Revendications

L'article affirme que BASE représente une amélioration de Pareto pour la sélection de réponses basée sur Lean. En formalisant une fois et en éditant le reste, la méthode permet simultanément de :

• Réduire les coûts : Diminue drastiquement le coût d'inférence de la vérification formelle, rendant l'augmentation de l'échelle au moment du test avec un grand $K$ plus réalisable.
• Améliorer la précision : Renforce la fiabilité de la sélection de la réponse correcte, probablement parce que la structure de base partagée réduit la variance et le taux d'échec de l'autoformaliseur pour le candidat correct.

Les auteurs soulignent que cette approche est un « remplacement direct » (drop-in replacement) pour l'étape de formalisation dans les pipelines existants (démontré par son intégration dans le pipeline FANS), et que les gains sont portés par la capacité du vérificateur à conserver plus efficacement les bonnes réponses lorsqu'un échafaudage partagé et vérifié est utilisé, plutôt que par des changements dans la génération du solveur en amont.

Le travail reconnaît des limites, notant qu'il se concentre sur la vérification du type de l'énoncé en raison des limitations actuelles des prouveurs et suppose que les réponses candidates partagent une structure côté problème. Il ne prétend pas résoudre la fidélité de l'autoformalisation (où une réponse incorrecte pourrait toujours vérifier son type), mais suggère que la combinaison de signaux formels avec les classements des solveurs atténue ce risque.