Technische Samenvatting: OProver: Een Geïntegreerd Kader voor Agente Formele Bewijsvoering

Probleemstelling

Recente vooruitgang in formele bewijsvoering, met name binnen het Lean 4-ecosysteem, heeft gebruikgemaakt van grootschalige bewijsgeneratie en verifikaatbewuste training om de prestaties op benchmarks zoals MiniF2F en PutnamBench te verbeteren. Een kritieke beperking blijft echter bestaan: agente bewijsvoeringscapaciteiten (retrieval, compilerfeedback en iteratieve reparatie) worden doorgaans behandeld als heuristieken op het moment van inferentie die worden toegepast op een vaste bewijzer, in plaats van als geleerde beleidsregels die in het trainingsproces zijn geïntegreerd.

Dit creëert een mismatch tussen training en inferentie. Modellen die voornamelijk zijn getraind op afgeronde, succesvolle bewijzen, komen pas tijdens de implementatie in aanraking met compilerfeedback en geretrieveerde context, in distributies waarvoor ze nooit zijn geoptimaliseerd. Bovendien richten bestaande formele corpora zich op eindproducten (stellingen en geverifieerde bewijzen) en laten ze de multi-rond-interactielocaties achterwege – mislukte pogingen, geretrieveerde context en compilerdiagnostiek – die essentieel zijn om te leren hoe bewijzen gerepareerd moeten worden. Bijgevolg blijft het supervisiessignaal dat in de praktijk bewijsreparatie drijft, grotendeels onbenut in modeltraining.

Methodologie

Het artikel presenteert OProver, een geïntegreerd kader dat retrieval, compilerfeedback en iteratieve reparatie direct integreert in het beleid van de bewijzer via een co-evolutionaire trainingspijplijn.

1. Het OProver-kader

OProver behandelt formele bewijsvoering als een begrensd, multi-rond verfijningsproces. In elke ronde $t$ baseert het beleid $\pi$ zich op een compacte toestand $X_t = (s, R_t, p_{t-1}, f_{t-1})$, waarbij:

• $s$: De doelstelling van de stelling.
• $R_t$: De top-$k$ geretrieveerde, door de compiler geverifieerde bewijzen uit een geheugen $M$.
• $p_{t-1}$: De vorige bewijspoging.
• $f_{t-1}$: De ruwe tekstuele compilerfeedback (diagnostiek) van de Lean 4-verifier.

Het beleid genereert een herziene poging $p_t$. Als de verificatie faalt, wordt de ruwe feedback teruggegeven aan het beleid voor de volgende ronde. Cruciaal is dat het beleid zich uitsluitend baseert op de meest recente poging en feedback, waardoor lokale correctiesignalen behouden blijven terwijl de toestand compact blijft.

2. OProofs: Een Geïntegreerd Trainingscorpus

Om dit kader te ondersteunen, construeren de auteurs OProofs, een grootschalig corpus dat specifiek is ontworpen voor agente bewijsvoering. In tegenstelling tot eerdere datasets die alleen definitieve bewijzen bewaren, registreert OProofs geserialiseerde trajecten, waaronder:

• Geretrieveerde context.
• Mislukte pogingen.
• Ruwe compilerfeedback.
• Aansluitende reparaties.

OProofs is opgebouwd uit drie bronnen: publieke Lean-bronnen, grootschalige bewijssynthese (autoformalisatie + verificatie) en sporen van OProvers eigen agente bewijsvoering. Het bevat 1,77 miljoen unieke Lean-stellingen en 6,86 miljoen door de compiler geverifieerde bewijzen, gekoppeld aan 1,07 miljoen agente trajecten.

3. Co-evolutionaire Trainingspijplijn

Het trainingsproces volgt een iteratieve lus (Algoritme 1) waarbij de bewijzer en het corpus co-evolueren:

1. Voortgezette Pretraining (CPT): Een basismodel wordt getraind op een mengsel van Lean-code, wiskunde en data voor redeneren met lange context om OProver-Base te creëren.
2. Iteratieve Post-training:
   • Agente Rollouts: Het huidige beleid voert multi-rond bewijsvoering uit op een pool van stellingen, met retrieval uit het huidige geheugen $M_k$ en verificatie met de Lean-compiler.
   • Datacollectie: Nieuw geverifieerde bewijzen worden toegevoegd aan het corpus en geïndexeerd in het retrieval-geheugen. Mislukte pogingen en succesvolle reparaties worden ontbonden in voorbeelden op ronniveau $(s, R_t, p_{t-1}, f_{t-1}) \to p_t$.
   • Supervised Fine-Tuning (SFT): Het model wordt bijgewerkt met de verzamelde reparatievoorbeelden.
   • Versterkend Leren (RL): Group Sequence Policy Optimization (GSPO) wordt toegepast op moeilijkere, onopgeloste gevallen, met behulp van een beloningssignaal gebaseerd op verificatiesucces en formatcorrectheid.
   • Recirculatie: Het bijgewerkte corpus en geheugen voeden de volgende iteratie, waardoor het beleid kan leren van zijn eigen verbeterde bewijzen.

Belangrijkste Bijdragen

1. Geïntegreerd Kader voor Agente Bewijsvoering: OProver verenigt retrieval, feedback en iteratieve reparatie in één geleerd beleid, waardoor de mismatch tussen training en inferentie wordt geëlimineerd door het model te trainen om deze signalen te gebruiken als onderdeel van zijn kernstrategie in plaats van als externe heuristieken.
2. OProofs Corpus: De constructie van een grootschalig corpus (1,77 miljoen stellingen, 6,86 miljoen bewijzen) dat expliciet multi-turn interactiegeschiedenissen behoudt, inclusief mislukte pogingen en ruwe compilerfeedback, en supervisie biedt die eerder onbeschikbaar was in formele datasets.
3. Co-evolutiepijplijn: Een trainingsmethodologie waarbij de bewijzer nieuwe data genereert (geverifieerde bewijzen en reparatietrajecten) die direct worden opgenomen in het trainingscorpus en het retrieval-geheugen, waardoor een zelfverbeterende lus ontstaat.
4. State-of-the-Art Prestaties: OProver bereikt topprestaties onder open-gewicht bewijzers voor volledige bewijzen, en toont aan dat agente verfijningsstrategieën aanzienlijk grotere modellen kunnen overtreffen.

Experimentele Resultaten

OProver werd geëvalueerd op vijf Lean 4-benchmarks: MiniF2F, MathOlympiadBench, ProofNet, ProverBench en PutnamBench.

• Prestaties: Het OProver-32B-model behaalde de beste Pass@32-scores op drie benchmarks (MiniF2F: 93,3%, ProverBench: 58,2%, PutnamBench: 11,3%) en de op één na beste op de andere twee (MathOlympiad: 22,8%, ProofNet: 33,2%).
• Efficiëntie: OProver-32B (32 miljard parameters) presteerde beter dan de 671B DeepSeek-Prover-V2 en de 560B LongCat-Flash-Prover (met TIR) op de meeste benchmarks, ondanks aanzienlijk minder parameters. Zelfs de 8B-variant presteerde beter dan de 32B Goedel-Prover-V2 op alle benchmarks.
• Scaling op het Moment van Testen: De prestaties verbeterden consistent met een verhoogd rekenbudget (meer samples of verfijningsrondes), zij het met afnemende meeropbrengst. De optimale allocatie tussen verfijningdiepte en samplingbreedte varieerde per benchmarkmoeilijkheidsgraad.
• Ablatiestudies: Het verwijderen van multi-turn compilerfeedback veroorzaakte de meest significante prestatiedaling, wat de iteratieve verfijning bevestigt als de primaire drijvende kracht van winst. Het verwijderen van verrijking door retrieval veroorzaakte ook consistente, zij het kleinere, dalingen, wat de complementaire waarde van retrieval-grondvesting benadrukt.

Betekenis en Claims

Het artikel stelt dat OProver aantoont dat agente formele bewijsvoering effectief kan worden geleerd als een geïntegreerd beleid in plaats van dat het wordt samengesteld uit afzonderlijke modules op het moment van inferentie. Door te trainen op het volledige traject van bewijsconstructie, falen en reparatie, leert het model om compilerfeedback en geretrieveerde context te benutten als intrinsieke onderdelen van zijn redeneerproces.

De auteurs benadrukken dat de prestatiewinst niet louter het gevolg is van modelgrootte, maar voortkomt uit de synergie tussen verrijking door retrieval-grondvesting en door de compiler geleide iteratieve verfijning. De co-evolutie van het OProver-beleid en het OProofs-corpus stelt het systeem in staat om continu zijn bewijsvoeringscapaciteiten te verbeteren door te leren van zijn eigen succesvolle en mislukte pogingen, waarmee een nieuw paradigma wordt gevestigd voor het trainen van systemen voor formeel redeneren.