Résumé Technique : Apprentissage par Renforcement Vérifié par Processus pour la Preuve de Théorèmes via Lean

Énoncé du Problème

La preuve automatique de théorèmes (ATP - Automated Theorem Proving) vise à générer des preuves formelles pour des théorèmes mathématiques. Bien que les modèles de langage de grande taille (LLM) aient progressé dans les tâches de raisonnement, ils reposent généralement sur le langage naturel (NL) ou sur des récompenses binaires (correct/incorrect) lors de l'apprentissage par renforcement (RL). Cela crée un fossé :

1. Feedback Sparse (Épars) : Les approches de RL standard utilisent souvent uniquement un signal binaire final (preuve réussie/échouée), ce qui fournit une attribution de crédit éparse et peine à guider le modèle à travers de longues chaînes de raisonnement.
2. Non structuré vs Structuré : Contrairement aux assistants de preuve symboliques (ex: Lean, Coq, Isabelle) qui offrent une vérification fine de type théorique pour chaque étape de raisonnement, les LLM sont entraînés sur des séquences de jetons (tokens) avec des récompenses scalaires.
3. Modèles de Récompense de Processus (PRM) : Bien que des travaux récents utilisent des PRM pour fournir des récompenses au niveau de l'étape, ceux-ci nécessitent souvent de grands ensembles de données annotées ou reposent sur une supervision de type Chaîne de Pensée (CoT) en langage naturel, manquant ainsi de la rigueur de la vérification symbolique.

Le défi central abordé est la manière de tirer parti du feedback riche et structuré d'un assistant de preuve symbolique (Lean) pour entraîner les LLM sans dépendre de PRM externes potentiellement bruités ou d'annotations humaines.

Méthodologie

Le papier propose l'Apprentissage par Renforcement Vérifié par Processus, un cadre qui intègre le feedback symbolique de Lean directement dans un objectif d'Optimisation de Politique Relative de Groupe (GRPO - Group Relative Policy Optimization). La méthode se compose de trois composantes principales :

1. Oracle de Processus Symbolique

Au lieu de traiter Lean uniquement comme un vérificateur final, les auteurs l'utilisent comme un oracle de processus durant l'entraînement.

• Analyse syntaxique (Parsing) : Les preuves générées sont analysées en séquences de tactiques ($T_1, \dots, T_N$) basées sur l'Arbre de Syntaxe Abstraite (AST).
• Vérification : Le processus d'élaboration de Lean fournit deux types de signaux :
  • Signal de Résultat (Outcome) : Un score binaire global $g(Y) \in \{0, 1\}$ indiquant si l'ensemble de la preuve est valide.
  • Signal de Processus : Un feedback fin pour chaque tactique, identifiant les étapes localement valides et l'emplacement spécifique de la première erreur.

2. Stratégie d'Attribution de Crédit

Pour combler l'écart entre le feedback symbolique et le RL au niveau du jeton, les auteurs introduisent des règles d'attribution spécifiques :

• Propagation de la Première Erreur : Si une tactique $T_j$ échoue, toutes les tactiques suivantes ($T_k$ où $k \ge j$) sont considérées comme erronées. Cela reflète la nature causale des preuves : un préfixe invalide invalide toute la chaîne de raisonnement suivante.
• Scoring de Tactique ($\phi$) :
  • Si la preuve réussit ($g(Y)=1$), toutes les tactiques reçoivent un score positif (1).
  • Si la preuve échoue ($g(Y)=0$) :
    • Les tactiques précédant la première erreur reçoivent un score partiel ($d_1$).
    • La première tactique erronée et toutes les suivantes reçoivent un score de pénalité ($d_2$).
• Mapping au Niveau du Jeton (Token) : L'avantage au niveau de la tactique est assigné uniquement au premier jeton de chaque tactique (le mot-clé, ex: intro, apply). Cela s'aligne sur le point de décision sémantique où la stratégie de preuve est déterminée.

3. Objectif de RL (Intégration GRPO)

Le cadre combine les avantages de résultat (outcome) et de processus dans un objectif GRPO unique :

• Avantage de Résultat ($A_{outcome}$) : Calculé sur la base du statut global de réussite/échec par rapport à la moyenne du groupe.
• Avantage de Processus ($A_{process}$) : Calculé sur la base des scores de tactique, normalisés par la moyenne du groupe pour tenir compte de la difficulté du problème.
• Avantage Combiné : Pour un jeton $t$ appartenant au premier jeton de la tactique $j$ dans la réponse $i$ :
  $$A_{i,t} = A_{outcome, i, t} + A_{process, i, j}$$
  Pour les jetons non-premiers, seul l'avantage de résultat est appliqué. Cette formulation évite le besoin d'un modèle de valeur ou d'un PRM auxiliaire, en s'appuyant uniquement sur la vérité terrain du vérificateur.

Contributions Clés

1. Formalisation du Feedback Symbolique : Les auteurs formalisent le feedback de niveau tactique de Lean en signaux d'entraînement scalaires, permettant une attribution de crédit fine au niveau du jeton sans guidage en langage naturel.
2. RL Guidé par un Vérificateur Symbolique : Ils intègrent les récompenses de résultat et de tactique dérivées directement de Lean dans un cadre de RL, fournissant une attribution de crédit dense et vérifiable.
3. Amélioration Stable des Benchmarks : L'approche démontre des améliorations constantes sur les benchmarks MiniF2F et ProofNet, surpassant le RL basé uniquement sur le résultat et les baselines classiques sans nécessiter de PRM externes ou de notation en langage naturel.

Résultats Expérimentaux

Les expériences ont été menées en utilisant STP-Lean et DeepSeek-Prover-V1.5 (modèles de 7B) sur les benchmarks MiniF2F-Test et ProofNet-Test.

• Gains de Performance :
  • STP-Lean : La méthode proposée a amélioré le pass@64 de MiniF2F de +2,5% (de 56,7% à 59,2%) et le pass@32 de ProofNet de +1,4%.
  • DeepSeek-Prover-V1.5 : Des améliorations constantes, bien que marginales, ont été observées dans tous les réglages.
• Comparaison aux Baselines :
  • La méthode a surpassé le GRPO "Outcome-only", qui présentait une instabilité et n'a pas réussi à s'améliorer sur ProofNet dans certaines configurations.
  • Elle a obtenu des résultats compétitifs face à de fortes baselines de recherche arborescente (ex: InternLM2.5-StepProver, DeepSeek-Prover-RL+RMaxTS) tout en utilisant une approche de génération en un seul passage (single-shot) sans budget massif de recherche à l'inférence.
• Études d'Ablation :
  • Assignation de Jeton : Assigner le crédit au premier jeton de la tactique a donné les résultats les plus stables par rapport à une distribution du crédit sur tous les jetons ou sur le dernier jeton.
  • Propagation de la Première Erreur : La suppression de cette règle a considérablement dégradé les performances, confirmant la nécessité de traiter les étapes suivantes comme invalides après une erreur.
  • Timeouts : Un délai de vérification de 15 secondes a fourni le meilleur équilibre, encourageant des preuves concises sans rejeter les preuves complexes valides.

Signification et Revendications

Le papier affirme que les assistants de preuve symboliques ne doivent pas être vus uniquement comme des outils d'évaluation, mais comme des oracles de processus actifs pendant l'entraînement. En exploitant le "feedback structuré riche et fin" inhérent aux systèmes de raisonnement formel, les auteurs démontent une voie vers des cadres de RL qui combinent la scalabilité des LLM avec la fiabilité de la vérification symbolique.

L'étude souligne que :

• Signaux Denses et Vérifiables : L'utilisation des journaux d'erreurs et des arbres d'élaboration du prouveur fournit un signal de récompense dense et fondé, supérieur aux résultats binaires épars ou aux PRM appris.
• Stabilité : La combinaison des récompenses de résultat globales et des récompenses de tactiques locales stabilise l'entraînement, évitant la convergence prématurée observée dans l'entraînement par tactique seule et les problèmes de parcimonie de l'entraînement par résultat seul.
• Efficacité : Cette approche atteint des performances de pointe ou compétitives sans la surcharge de calcul de la recherche arborescente ou les besoins en données de l'entraînement de PRM séparés.

Les auteurs restent modestes quant aux limites, notant que leur méthode repose sur des scores de récompense fixes ($d_1, d_2$) plutôt que sur des estimateurs d'avantage appris, et qu'elle se concentre actuellement sur les preuves Lean pures sans CoT, laissant ouvert le design de récompenses pour le raisonnement de longue forme en langage naturel.