Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs

1. Problématique

La preuve de théorèmes formels assistée par des modèles de langage (LLM) souffre d'un goulot d'étranglement majeur en matière d'évolutivité. Les approches actuelles (comme le Chain-of-Thought ou les méthodes par renforcement) nécessitent souvent des ressources de calcul prohibitives au moment du test (test-time compute), soit via des déployements massifs (massive roll-outs), soit via des fenêtres de contexte extrêmement longues pour accumuler l'historique des tentatives de preuve.

Les méthodes existantes traitent souvent les retours du compilateur (comme Lean) de manière simpliste (indicateurs binaires de succès/échec ou messages d'erreur en texte brut), ignorant la richesse structurelle de ces signaux. Cela force les modèles à s'appuyer sur des historiques d'interaction longs et coûteux pour corriger leurs erreurs, limitant ainsi la profondeur de l'exploration dans un budget de calcul fixe.

2. Méthodologie : Le Cadre "Learning-to-Refine"

Les auteurs proposent un nouveau paradigme basé sur l'observation que le compilateur Lean agit comme un compresseur de dimension. Bien que l'espace des programmes Lean soit combinatoirement vaste, le compilateur projette une multitude de tentatives de preuve incorrectes sur un ensemble compact et structuré de modes d'échec (messages d'erreur).

A. Compression par le Compilateur

L'idée centrale est que des programmes syntaxiquement différents mais sémantiquement défectueux produisent souvent les mêmes messages d'erreur. Le compilateur filtre le bruit syntaxique pour révéler les défauts sémantiques sous-jacents. Cela permet de regrouper les échecs par "modes d'échec" (failure modes) plutôt que par problème spécifique.

B. Chaîne de Distributions (Chain of Distributions - CoD)

Au lieu de générer des preuves à partir d'une distribution fixe (génération directe), le modèle apprend à naviguer dans l'espace des preuves via une chaîne de distributions conditionnelles.

• Chaque étape de raffinement (refinement) dépend uniquement de l'état actuel (la preuve échouée + le message d'erreur + le problème), rendant le processus Markovien.
• Cela élimine la nécessité de maintenir un long historique de contexte, réduisant drastiquement les coûts de calcul et de mémoire.
• Le modèle apprend à corriger localement les erreurs basées sur le feedback explicite du vérificateur, permettant de sortir des distributions initiales (OOD - Out-of-Distribution) vers des solutions correctes.

C. Pipeline d'Entraînement

1. Synthèse de données à froid (Cold-Start) : Utilisation d'un modèle plus puissant (Claude-3.7-Sonnet) pour analyser les erreurs de compilation et générer des plans de correction ("thoughts") et des solutions correctes à partir des échecs du modèle de base.
2. Itération d'Expert (Expert Iteration) : Le modèle est entraîné de manière itérative. Il tente de résoudre des problèmes, et lorsqu'il échoue, il utilise ses propres capacités de raffinement pour corriger l'échec. Les trajectoires réussies sont converties en données de supervision pour améliorer la politique de raffinement.
3. Apprentissage Supervisé (SFT) : Le modèle est affiné sur un mélange équilibré de données de génération directe et de données de raffinement.

D. Stratégies de Recherche au Moment du Test

Le cadre permet de choisir dynamiquement entre deux stratégies :

• Recherche en largeur (BFS) : Générer de nouvelles preuves à partir de zéro.
• Recherche en profondeur (DFS) / Raffinement : Corriger une preuve échouée précédente.
• Recherche Arborescente Guidée par la Valeur : Un modèle de valeur (Value Function) est entraîné pour estimer le potentiel de chaque nœud dans l'arbre de recherche (soit une nouvelle tentative, soit une correction). Cette fonction guide l'allocation du budget de calcul vers les branches les plus prometteuses, optimisant l'exploration.

3. Contributions Clés

1. Théorie de la Compression : Identification et formalisation du compilateur Lean comme un compresseur de dimension efficace, transformant un espace de preuves infini en un espace de modes d'échec structuré et fini.
2. Cadre "Learning-to-Refine" : Introduction d'une méthode qui internalise les trajectoires de correction d'erreurs, permettant au modèle d'apprendre des stratégies de réparation généralisables basées sur les types d'erreurs plutôt que sur la syntaxe brute.
3. Processus Markovien : Démonstration que la correction d'erreurs peut être traitée comme un processus décisionnel de Markov (dépendant uniquement de l'état actuel), éliminant la dépendance aux longs contextes historiques.
4. Stratégie de Recherche Adaptative : Développement d'une stratégie de recherche arborescente guidée par la valeur qui équilibre dynamiquement la génération directe et le raffinement itératif.

4. Résultats Expérimentaux

Les expériences ont été menées sur deux modèles de base : Kimina-Prover-Distill-8B et Goedel-Prover-V2-32B, évalués sur plusieurs benchmarks (MiniF2F, ProofNet, MathOlympiadBench, PutnamBench).

• Performance Globale : La méthode améliore systématiquement les capacités de raisonnement des modèles de base. Sur PutnamBench (un benchmark très difficile de mathématiques de niveau compétition), la méthode atteint des performances de pointe (State-of-the-Art) pour les modèles de taille ~8B et ~32B sous des budgets de calcul comparables.
  • Exemple : Goedel-32B raffiné résout 110 problèmes sur PutnamBench (contre 86 pour la version originale en mode auto-correction et 91 pour Ax-Prover).
  • Exemple : Kimina-8B raffiné résout 25 problèmes, se classant premier parmi les modèles de taille similaire.
• Efficacité du Raffinement : L'analyse montre que le raffinement est particulièrement efficace pour les problèmes difficiles où la génération directe échoue, tandis que la génération directe suffit pour les problèmes faciles. La recherche guidée par la valeur combine intelligemment les deux approches.
• Validation Statistique : Des tests d'hypothèse montrent que la distribution des programmes générés par raffinement est statistiquement distincte de celle de la génération directe, confirmant que le raffinement explore de nouvelles régions de l'espace des preuves inaccessibles par échantillonnage simple.
• Analyse des Erreurs : Le modèle apprend à corriger efficacement les erreurs structurelles récurrentes (ex: "unsolved goals", "type mismatch"), mais reste limité pour les échecs sémantiques globaux complexes, bien que cela soit une amélioration significative par rapport aux méthodes précédentes.

5. Signification et Impact

Cet article propose un changement de paradigme dans la preuve de théorèmes formels par IA :

• Évolutivité (Scalability) : En évitant les longs contextes et les roll-outs massifs, la méthode offre une voie scalable pour améliorer les prouveurs sans augmenter exponentiellement les coûts de calcul.
• Utilisation Intelligente des Signaux : Elle démontre que les messages d'erreur des compilateurs, souvent négligés ou mal exploités, contiennent une structure riche qui peut être utilisée pour guider l'apprentissage et la recherche de manière efficace.
• Généralisation : Le cadre est agnostique au modèle et s'adapte bien à différentes tailles de modèles, suggérant qu'il pourrait être intégré dans les systèmes de preuve de nouvelle génération.

En résumé, "Compile to Compress" transforme le processus de débogage d'un fardeau computationnel en un mécanisme d'apprentissage structuré, permettant aux prouveurs formels d'atteindre des performances de pointe avec une efficacité computationnelle accrue.