Technische Samenvatting: Proces-Geverifieerd Reinforcement Learning voor Stellingbewijzen via Lean

Probleemstelling

Geautomatiseerd Stellingbewijzen (Automated Theorem Proving, ATP) streeft naar het genereren van formele bewijzen voor wiskundige stellingen. Hoewel Large Language Models (LLMs) geavanceerd zijn in redeneertaken, vertrouwen ze tijdens Reinforcement Learning (RL) doorgaans op natuurlijke taal (NL) of binaire uitkomstbeloningen (correct/incorrect). Dit creëert een kloof:

1. Spaarzame Feedback: Standaard RL-benaderingen gebruiken vaak alleen een finaal binair signaal (bewijs geslaagd/gefaald), wat zorgt voor spaarzame credit assignment en moeite heeft om het model door lange redeneerketens te leiden.
2. Ongestructureerd vs. Gestructureerd: In tegenstelling tot symbolische bewijsassistenten (bijv. Lean, Coq, Isabelle), die een fijnmazige, typetheoretische verificatie van elke redeneerstap bieden, worden LLMs getraind op tokensequenties met scalaire beloningen.
3. Process Reward Models (PRMs): Hoewel recent werk gebruikmaakt van PRMs om stap-niveau beloningen te bieden, vereisen deze vaak grote geannoteerde datasets of vertrouwen ze op NL-gebaseerde CoT-supervisie, wat de rigoureuze betrouwbaarheid van symbolische verificatie mist.

De kernuitdaging die wordt aangepakt, is hoe de rijke, gestructureerde feedback van een symbolische bewijsassistent (Lean) direct kan worden ingezet om LLMs te trainen zonder te vertrouwen op externe, potentieel ruisgevoelige PRMs of menselijke annotaties.

Methodologie

Het paper stelt Proces-Geverifieerde Reinforcement Learning voor, een framework dat de symbolische feedback van Lean direct integreert in een Group Relative Policy Optimization (GRPO) objectief. De methode bestaat uit drie hoofdonderdelen:

1. Symbolische Proces Oracle

In plaats van Lean enkel als een finale verifieerder te behandelen, gebruikt de auteur het als een proces-oracle tijdens de training.

• Parsing: Geleerde bewijzen worden geparsed in sequenties van tactieken ($T_1, \dots, T_N$) op basis van de Abstract Syntax Tree (AST).
• Verificatie: Het elaboratieproces van Lean levert twee soorten signalen:
  • Uitkomstsignaal: Een globale binaire score $g(Y) \in \{0, 1\}$ die aangeeft of het gehele bewijs geldig is.
  • Processignaal: Fijnmazige feedback voor elke tactiek, waarbij lokale correcte stappen en de specifieke locatie van de eerste fout worden geïdentificeerd.

2. Credit Assignment Strategie

Om de kloof tussen symbolische feedback en token-niveau RL te overbruggen, introduceren de auteurs specifieke toewijzingsregels:

• First-Error Propagation: Als een tactiek $T_j$ faalt, worden alle daaropvolgende tactieken ($T_k$ waar $k \ge j$) als foutief beschouwd. Dit weerspiegelt de causale aard van bewijzen: een ongeldig prefix invalideert de gehele daaropvolgende redeneerketen.
• Tactiek-niveau Scoring ($\phi$):
  • Als het bewijs slaagt ($g(Y)=1$), ontvangen alle tactieken een positieve score (1).
  • Als het bewijs faalt ($g(Y)=0$):
    • Tactieken vóór de eerste fout ontvangen een gedeeltelijke score ($d_1$).
    • De eerste foutieve tactiek en alle daaropvolgende ontvangen een strafscore ($d_2$).
• Token-niveau Mapping: De tactiek-niveau advantage wordt alleen toegewezen aan het eerste token van elke tactiek (het keyword, bijv. intro, apply). Dit komt overeen met het semantische beslispunt waar de bewijsstrategie wordt bepaod.

3. RL Objectief (GRPO Integratie)

Het framework combineert uitkomst- en proces-advantages in één enkel GRPO objectief:

• Outcome Advantage ($A_{outcome}$): Berekend op basis van de globale pass/fail status relatief aan het groepsgemiddelde.
• Process Advantage ($A_{process}$): Berekend op basis van de tactiek-niveau scores, genormaliseerd door het gemiddelde van de groep om rekening te houden met de moeilijkheidsgraad van het probleem.
• Gecombineerde Advantage: Voor een token $t$ die behoort tot het eerste token van tactiek $j$ in respons $i$:
  $$A_{i,t} = A_{outcome, i, t} + A_{process, i, j}$$
  Voor niet-eerste tokens wordt alleen de outcome advantage toegepast. Deze formulering voorkomt de noodzaak van een value model of auxiliary PRM, door uitsluitend te vertrouwen op de ground truth van de verifier.

Belangrijkste Bijdragen

1. Formalisering van Symbolische Feedback: De auteurs formaliseren de tactiek-niveau feedback van Lean naar scalaire trainingssignalen, wat fijnmazige, token-niveau credit assignment mogelijk maakt zonder natuurlijke taalbegeleiding.
2. Symbolische Verifier-Gestuurde RL: Zij integreren uitkomst- en tactiek-niveau beloningen die rechtstreeks uit Lean afgeleid zijn in een RL-framework, wat zorgt voor een dichte en verifieerbare credit assignment.
3. Stabiele Benchmark Verbeteringen: De aanpak vertoont consistente verbeteringen op de MiniF2F en ProofNet benchmarks, waarbij zij "outcome-only" RL en vanilla baselines overtreffen zonder externe PRMs of NL-notatie te vereisen.

Experimentele Resultaten

Experimenten werden uitgevoerd met STP-Lean en DeepSeek-Prover-V1.5 (7B modellen) op de MiniF2F-Test en ProofNet-Test benchmarks.

• Prestatiewinst:
  • STP-Lean: De voorgestelde methode verbeterde de MiniF2F pass@64 met +2,5% (van 56,7% naar 59,2%) en ProofNet pass@32 met +1,4%.
  • DeepSeek-Prover-V1.5: Er werden consistente, zij het marginale, verbeteringen waargenomen in alle settings.
• Vergelijking met Baselines:
  • De methode presteerde beter dan "Outcome-only" GRPO, die instabiliteit vertoonde en in sommige configuraties niet verbeterde op ProofNet.
  • Het behaalde concurrerende resultaten ten opzichte van sterke tree-search baselines (bijv. InternLM2.5-StepProver, DeepSeek-Prover-RL+RMaxTS) terwijl het een single-shot generatie-aanpak gebruikte zonder massieve inference-time search budgetten.
• Ablatie Studies:
  • Token Toewijzing: Het toewijzen van credit aan het eerste token van een tactiek leverde de meest stabiele resultaten op vergeleken met het verdelen van credit over alle tokens of het laatste token.
  • First-Error Propagation: Het verwijderen van deze regel verslechterde de prestaties aanzienlijk, wat de noodzaak bevestigt om daaropvolgende stappen als ongeldig te behandelen na een fout.
  • Timeouts: Een verificatie-timeout van 15 seconden bood de beste balans, waardoor beknopte bewijzen werden aangemoedigd zonder geldige complexe bewijzen te verwerpen.

Betekenis en Claims

Het paper claimt dat symbolische bewijsassistenten niet enkel moeten worden gezien als evaluatietools, maar als actieve proces-niveau reward oracles tijdens de training. Door gebruik te maken van de "rijke, fijnmazige gestructureerde feedback" die inherent is aan formele redeneersystemen, demonstreren de auteurs een pad naar RL-frameworks die de schaalbaarheid van LLMs combineren met de betrouwbaarheid van symbolische verificatie.

De studie benadrukt dat:

• Dichte, Verifieerbare Signalen: Het gebruik van de error logs en elaboratiebomen van de prover een solide, dichte reward signaal biedt dat superieur is aan spaarzame binaire uitkomsten of geleerde PRMs.
• Stabiliteit: De combinatie van globale outcome rewards en lokale tactiek rewards stabiliseert de training, wat voortijdige convergentie voorkomt (gezien bij tactiek-alleen training) en de problemen van sparsity (gezien bij outcome-alleen training) oplost.
• Efficiëntie: Deze aanpak bereikt state-of-the-art of concurrerende prestaties zonder de computationele overhead van tree search of de datavereisten voor het trainen van aparte PRMs.

De auteurs blijven bescheiden over beperkingen, waarbij zij opmerken dat hun methode vertrouwt op vaste reward scores ($d_1, d_2$) in plaats van geleerde advantage estimators en momenteel focust op non-CoT, pure Lean bewijzen, wat ruimte laat voor het ontwerp van rewards voor langdurige natuurlijke taalredenering.