GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

Dit paper introduceert GAR, een generatief-adversariaal versterkingsleerframework dat een proeflezer en probleemgenerator gezamenlijk in een adverterende cyclus traint om de trainingsdoeltreffendheid te verhogen en de prestaties bij het formele bewijzen van geavanceerde theorema's te verbeteren.

De kern

Stel je voor dat je een wiskundig genie wilt trainen om complexe theorema's (wiskundige stellingen) te bewijzen. In het verleden deden we dit door het genie duizenden voorbeelden te geven van problemen die al opgelost waren. Maar er was een groot probleem: de problemen bleven altijd even moeilijk. Als het genie al heel goed was, kreeg het nog steeds makkelijke sommen, wat saai en inefficiënt was. Als het nog niet zo ver was, kreeg het onmogelijke problemen en gaf het de moed op.

Deze paper introduceert GAR (Generative Adversarial Reinforcement Learning), een slimme nieuwe manier om wiskundige AI's te trainen. Je kunt het zien als een tandem-trainingssessie tussen een trainer en een atleet, waarbij ze elkaar voortdurend uitdagen.

Hier is hoe het werkt, vertaald naar alledaagse taal:

1. Het Probleem: De "Vaste Lijst"

Stel je voor dat een atleet traint voor de Olympische Spelen. Als zijn trainer hem elke dag dezelfde 100 meter-loop laat doen, wordt hij nooit sneller. Als de trainer hem direct de marathon laat lopen, valt hij uit.
Bij het bewijzen van wiskundige stellingen (in een taal genaamd Lean) deden AI's het vaak zo: ze kregen een vaste lijst met problemen. Als ze die lijst "uit" hadden, stopte de training. Ze leerden niet om complexere problemen aan te pakken.

2. De Oplossing: GAR (De "Twee-handen" Methode)

GAR introduceert twee spelers die tegen elkaar spelen, maar samen werken:

• De Oplosser (De Prover): Dit is de AI die de wiskundige problemen moet oplossen.
• De Trainer (De Statement Fuser): Dit is een andere AI die nieuwe problemen bedenkt.

Hoe werkt de cyclus?

1. De Trainer maakt een nieuwe uitdaging: De Trainer pakt twee bestaande, oplosbare problemen en "plakt" ze samen tot één nieuw, moeilijker probleem. Het is alsof je een puzzel van 500 stukjes en een puzzel van 500 stukjes neemt en ze samenvoegt tot één grote puzzel van 1000 stukjes.
2. De Oplosser probeert het op te lossen: De Oplosser krijgt dit nieuwe, zwaardere probleem.
3. De Beloning (Het Adversariale Spel):
   • Als de Oplosser het probleem oplost, krijgt hij een beloning. De Trainer krijgt een kleine straf (want hij wilde het moeilijk maken).
   • Als de Oplosser het niet oplost, krijgt de Trainer een beloning (want hij slaagde erin het probleem te moeilijk te maken), mits het probleem oplosbaar was.
   • Als het probleem onoplosbaar is, krijgt niemand een beloning.

3. De Magie: Een "Verborgen Leerplan"

Dit systeem creëert wat de auteurs een "impliciet leerplan" noemen.

• In het begin maakt de Trainer simpele, samengevoegde problemen. De Oplosser slaagt er vaak in.
• Omdat de Oplosser steeds beter wordt, moet de Trainer steeds moeilijkere problemen bedenken om nog steeds een beloning te krijgen.
• De Oplosser moet zich dus voortdurend aanpassen en leren.

Het is alsof je een video-game speelt waarbij het spel automatisch het niveau verhoogt zodra jij beter wordt. Je krijgt nooit te makkelijke levels (saai) en nooit onmogelijke levels (frustrerend), maar altijd het perfecte niveau dat net iets boven je huidige vaardigheid ligt.

4. Het Resultaat: Slimmer en Sneller

De paper laat zien dat AI's die met GAR zijn getraind (zoals DeepSeek-Prover en Goedel-Prover) veel beter worden dan hun voorgangers.

• Ze kunnen moeilijkere theorema's oplossen.
• Ze verspillen geen tijd aan makkelijke problemen.
• Ze leren niet alleen oplossen, maar ook nadenken over hoe een probleem gestructureerd moet zijn.

Samenvattend in één zin:

GAR is een slimme trainingssessie waarbij een AI-trainer voortdurend nieuwe, net even te moeilijke puzzels bedenkt voor een AI-oplosser, zodat ze samen groeien tot echte wiskundige meesters, zonder dat iemand de moed opgeeft of saai wordt.

Het is een stap voorwaarts naar AI's die niet alleen rekenen, maar echt redeneren en complexe ideeën kunnen doorgronden.

Technische samenvatting

Titel: GAR: Generatieve Adversariële Versterkende Leer voor Formele Theorema-bewijzen

1. Het Probleem

Het oplossen van wiskundige problemen via verifieerbare talen zoals Lean heeft een grote impact gehad op zowel de wiskunde- als de computerwetenschapsgemeenschap. Huidige state-of-the-art modellen worden echter vaak getraind met dure online Versterkende Leer (RL) of expertiteratie. Deze benaderingen hebben twee fundamentele beperkingen:

• Vaste Probleemsets: Ze vertrouwen op statische datasets van theorema's. Dit leidt tot inefficiëntie, omdat het model veel tijd besteedt aan triviaal makkelijke problemen of onoplosbare taken die buiten zijn huidige capaciteit liggen.
• Gebrek aan Adaptiviteit: Er is geen mechanisme om de moeilijkheidsgraad van de problemen dynamisch af te stemmen op de evoluerende vaardigheden van het bewijsmodel (prover). Dit beperkt de exploratie van complexe theorema's en verhindert dat het model zijn prestaties optimaal ontwikkelt.

2. Methodologie: Het GAR Framework

De auteurs stellen GAR (Generative Adversarial Reinforcement Learning) voor, een trainingsframework dat een "impliciete curriculum learning" (impliciete leerplan) realiseert door het gezamenlijk trainen van twee modellen in een adversariële lus:

1. De Prover: Het model dat de formele bewijzen genereert.
2. De Statement Fuser: Een model dat nieuwe, uitdagendere probleemstellingen genereert.

Het proces verloopt in iteraties met twee fasen:

• Fase A: Generatie (Statement Fusion):

  • In plaats van statische datasets te gebruiken, samplet het systeem paren van bestaande natuurlijke taal (NL) statements uit een basisrepository.
  • De Statement Fuser fuseert deze twee statements tot één nieuw, complexer probleem dat de kernideeën van beide combineert.
  • Dit nieuwe NL-statement wordt geautomatiseerd omgezet (autoformalized) naar een formele taal (Lean4).
  • De Prover probeert vervolgens meerdere kandidaat-bewijzen voor deze nieuwe statements te genereren.

• Fase B: Adversariële Versterkende Leer (RL):

  • Beide modellen worden geoptimaliseerd met een variant van GRPO (Group Relative Policy Optimization).
  • Beloning voor de Fuser: De fuser krijgt een beloning als het een statement genereert dat moeilijk is voor de huidige prover (lage pass-rate), maar nog steeds oplosbaar is. Dit moedigt het creëren van een "impliciete curriculum" aan waarbij de moeilijkheidsgraad net iets boven het niveau van de prover ligt.
  • Beloning voor de Prover: De prover wordt beloond voor het correct oplossen van medium- tot hoog-difficultie problemen.
  • Straf voor Statement Modificatie: Een belangrijk innovatief element is een "soft penalty" voor het wijzigen van de oorspronkelijke probleemstelling tijdens het bewijzen. Moderne modellen met "Long Chain-of-Thought" (CoT) neigen soms om het probleem te vereenvoudigen om het makkelijker op te lossen (reward hacking). GAR straft dit af om te zorgen dat het model het echte probleem oplost.

3. Belangrijkste Bijdragen

1. GAR Framework: Een volledig RL-framework dat de bewijskracht verbetert door een impliciete curriculum te creëren, waardoor tijdverspilling op te makkelijke of onoplosbare taken wordt voorkomen.
2. Statement Fusion Techniek: Een methode om nieuwe formele statements te creëren door het fuseren van bestaande NL-problemen. Dit genereert theorema's die beter afgestemd zijn op de capaciteiten van het model dan directe formalisatie van losse problemen.
3. Adversariële Co-evolutie: Het bewijst dat het gezamenlijk trainen van probleemgenerator en -oplosser leidt tot superieure resultaten vergeleken met het trainen van alleen de prover op statische data.

4. Resultaten

De auteurs hebben GAR getraind op twee bestaande state-of-the-art modellen: Goedel-Prover-V2-8B en DeepSeek-Prover-V2-7B. De resultaten tonen significante verbeteringen:

• MiniF2F-Test Benchmark: Beide modellen vertoonden een gemiddelde relatieve verbetering van 4,20% in pass@32.
  • Goedel-Prover-V2-8B steeg van 77,87% naar 80,33%.
  • DeepSeek-Prover-V2-7B steeg van 70,49% naar 74,18%.
• ProofNet-Test Benchmark (gericht op geavanceerde wiskunde):
  • De pass@32 van DeepSeek-Prover-V2 steeg van 22,58% naar 25,81%.
• Ablatie Studies:
  • Zonder de straf voor statement-modificatie (reward hacking) daalden de prestaties aanzienlijk.
  • Het trainen met een "bevroren" (niet-getrainde) fuser leverde geen verbetering op, wat aantoont dat de co-evolutie essentieel is.
  • GAR presteerde beter dan traditionele GRPO-training op statische datasets, zelfs op modellen die al zwaar met RL waren getraind.

5. Betekenis en Impact

GAR biedt een nieuw paradigma voor versterkende leer in verifieerbare omgevingen. In plaats van alleen de oplossing te optimaliseren, optimaliseert het ook de generatie van de taken zelf. Dit creëert een dynamisch leerproces waarbij de moeilijkheidsgraad van de taken meegroeit met de vaardigheden van het AI-model.

De implicaties gaan verder dan formele theorema-bewijzen; het biedt een blauwdruk voor adversariële co-training in andere domeinen die zwaar vertrouwen op redenering en verifieerbare uitkomsten. Door de code open-source te maken, hopen de auteurs de gemeenschap te helpen bij het doorbreken van de huidige limieten in automatisch wiskundig redeneren.