GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

Die Arbeit stellt GAR vor, ein generatives adversariales Reinforcement-Learning-Framework, das durch das gemeinsame Training eines Problemgenerators und eines Lösermodells in einem adversariellen Zyklus die Effizienz des Trainings für formale Theorembeweise verbessert und die Leistung auf Benchmarks wie MiniF2F und ProofNet signifikant steigert.

Das Wesentliche

Stell dir vor, du möchtest jemanden beibringen, wie man komplexe mathematische Rätsel löst. Normalerweise gibt man diesem Schüler eine Liste mit Aufgaben: erst ganz einfache, dann mittlere, und am Ende die schwierigsten.

Das Problem bei den bisherigen Methoden für künstliche Intelligenz (KI) war jedoch, dass diese Aufgabenliste statisch war. Die KI bekam immer dieselben Aufgaben, egal wie gut sie schon wurde.

• Wenn die KI zu gut wurde, waren die Aufgaben zu leicht und sie lernte nichts Neues.
• Wenn die Aufgaben zu schwer waren, gab sie auf und lernte auch nichts.

Die Autoren dieses Papers (von der University of Illinois und NVIDIA) haben eine clevere Lösung namens GAR (Generative Adversarial Reinforcement Learning) entwickelt. Man kann sich das wie ein Tennis-Training mit einem sehr cleveren Trainer vorstellen.

Das Konzept: Der Trainer und der Spieler

Statt nur einen Spieler (die KI, die Beweise schreibt) zu trainieren, hat GAR zwei KI-Modelle, die gegeneinander antreten:

1. Der Spieler (The Prover): Seine Aufgabe ist es, mathematische Theoreme in einer strengen Programmiersprache (Lean) zu beweisen. Er will gewinnen (den Beweis finden).
2. Der Trainer (The Statement Fuser): Seine Aufgabe ist es, neue, schwierigere Aufgaben zu erfinden. Aber er darf nicht einfach unmögliche Aufgaben stellen. Er muss Aufgaben finden, die gerade noch lösbar sind, aber den Spieler herausfordern.

Wie funktioniert das Training? (Die "Adversarial" Phase)

Stell dir vor, sie spielen ein Spiel in Runden:

1. Die Aufgaben-Erstellung: Der Trainer nimmt zwei einfache mathematische Probleme aus einem großen Buch und "verschmilzt" sie zu einem neuen, komplexeren Problem. Er denkt sich: "Wenn mein Schüler das hier löst, wird er stärker."
2. Der Beweis: Der Spieler versucht, diesen neuen Beweis zu finden.
3. Die Belohnung (Rewards):
   • Wenn der Spieler das Problem löst, bekommt er Punkte.
   • Wenn der Trainer eine Aufgabe gestellt hat, die zu leicht war (der Spieler hat sie sofort gelöst), bekommt der Trainer keine Punkte. Er muss härter arbeiten.
   • Wenn der Trainer eine Aufgabe gestellt hat, die unmöglich war (niemand kann sie lösen), bekommt er auch keine Punkte.
   • Der Trainer wird nur belohnt, wenn er eine Aufgabe stellt, die schwierig, aber lösbar ist.

Der Clou: Der "Versteckte Lehrplan"

Das Geniale an GAR ist, dass sich der Schwierigkeitsgrad automatisch anpasst.

• Am Anfang sind die Aufgaben einfach.
• Sobald der Spieler besser wird, wird der Trainer gezwungen, schwierigere Aufgaben zu erfinden, um Punkte zu bekommen.
• Der Spieler wird dadurch gezwungen, immer tiefer zu graben und bessere Strategien zu entwickeln.

Man nennt das einen "impliziten Lehrplan". Es gibt keinen festen Lehrplan, der von Menschen geschrieben wurde. Der Lehrplan entsteht live durch das Wettkampf-Spiel zwischen Trainer und Spieler.

Ein Beispiel aus dem Papier

Stell dir vor, der Spieler ist ein junger Mathematiker.

• Früher: Er bekam immer nur Aufgaben wie "2 + 2 = ?". Er wurde schnell langweilig und lernte nicht, wie man große Gleichungen löst.
• Mit GAR: Der Trainer merkt, dass der Spieler "2+2" kann. Also erfindet er eine Aufgabe, die "2+2" beinhaltet, aber auch noch "Wurzelziehen" und "Logik" erfordert. Der Spieler muss sich anstrengen. Wenn er es schafft, ist er stärker. Dann erfindet der Trainer eine noch schwierigere Version.

Das Ergebnis

Die Autoren haben gezeigt, dass diese Methode funktioniert. Zwei bekannte KI-Modelle (DeepSeek-Prover und Goedel-Prover) wurden mit GAR trainiert.

• Sie konnten mehr schwierige mathematische Theoreme beweisen als vorher.
• Sie waren effizienter, weil sie keine Zeit mit zu leichten Aufgaben verschwendeten.
• Sie konnten sogar Probleme lösen, die für die alten Modelle zu schwer waren (wie in einem Benchmark namens "ProofNet").

Zusammenfassung in einem Satz

GAR ist wie ein unermüdlicher, schlagfertiger Trainer, der seine KI-Schüler ständig mit genau den richtigen, kniffligen Aufgaben konfrontiert, damit sie nicht stagnieren, sondern immer besser werden, indem sie gegen den Trainer selbst "kämpfen".

Das Papier zeigt damit einen neuen Weg auf, wie man KI nicht nur mit statischen Daten füttert, sondern sie durch ein dynamisches Wettkampf-System zu echten Experten in komplexen Bereichen wie Mathematik und Logik macht.

Technische Zusammenfassung

Titel: GAR: Generative Adversarial Reinforcement Learning für formale Theorembeweise

Veröffentlicht bei: ICLR 2026
Autoren: Ruida Wang, Jiarui Yao, Rui Pan, Shizhe Diao, Tong Zhang (University of Illinois Urbana-Champaign & NVIDIA)

---

1. Problemstellung

Die Fähigkeit, formale mathematische Beweise in Sprachen wie Lean zu generieren, ist ein wichtiger Meilenstein für die künstliche Intelligenz. Der aktuelle Stand der Technik (State-of-the-Art) stützt sich oft auf teures Online-Reinforcement-Learning (RL) oder Expert-Iteration-Verfahren. Diese Ansätze leiden jedoch unter zwei wesentlichen Einschränkungen:

1. Starre Datensätze: Die Modelle werden auf festen Problemsets trainiert. Dies führt zu ineffizientem Training, da das Modell Zeit mit trivialen Aufgaben verschwendet oder an unlösbaren Problemen feststeckt.
2. Fehlende adaptive Schwierigkeit: Es gibt keinen Mechanismus, der die Schwierigkeit der Beweisaufgaben dynamisch an die wachsenden Fähigkeiten des Provers (Beweisführers) anpasst. Dies limitiert die Fähigkeit des Modells, komplexe Theoreme zu meistern.

Das Ziel der Arbeit ist es, einen Trainingsrahmen zu schaffen, der diese Lücke schließt, indem er die Schwierigkeit der Aufgaben automatisch an die Leistungsfähigkeit des Modells anpasst.

2. Methodik: Das GAR-Framework

Die Autoren schlagen GAR (Generative Adversarial Reinforcement Learning) vor, ein umfassendes RL-Framework, das den Beweisführer (Prover) und einen Problem-Komponisten (Statement Fuser) in einem adversariellen Loop gemeinsam trainiert. Dieser Prozess etabliert ein implizites Curriculum-Learning.

Der Trainingsprozess läuft in Iterationen ab und besteht aus zwei Hauptphasen:

A. Generierungsphase (Generation Stage)

1. Statement Fusion (Aussage-Fusion): Anstatt neue Probleme aus dem Nichts zu generieren, nimmt der Statement Fuser zwei existierende, lösbare natürliche Sprach-Aussagen (NL) aus einer Basis-Datenbank (z. B. Lean-Workbook, Numina-Math) und fusioniert sie zu einer neuen, anspruchsvolleren Aussage.
   • Wichtiges Design-Entscheidung: Die Fusion erfolgt zunächst auf der Ebene der natürlichen Sprache (NL), bevor die Aussage in die formale Sprache (Lean) übersetzt wird. Dies verhindert, dass das Modell durch direkte Fusion formaler Aussagen syntaktische Fehler produziert.
   • Der Fuser nutzt ein „Thinking"-Modell (z. B. Qwen3 oder DeepSeek-R1), dessen Denkprozess durch ein spezielles Token (<analysis>) neu initialisiert wird, um fokussiertes, aufgabenspezifisches Denken zu fördern.
2. Proof Writing: Der Prover versucht, für die neu generierten NL-FL-Paare (Natural Language - Formal Language) mehrere Kandidaten-Beweise zu generieren.
3. Verifikation: Die Beweise werden vom Lean4-Verifizierer auf Korrektheit geprüft.

B. Adversarielles Reinforcement Learning (Adversarial RL Stage)

Beide Modelle werden mittels einer Variante des Group Relative Policy Optimization (GRPO)-Algorithmus optimiert, wobei sie gegensätzliche Ziele verfolgen:

• Training des Statement Fusers (Problem-Komponist):

  • Ziel: Erzeugung von Problemen, die für den aktuellen Prover schwer, aber noch lösbar sind.
  • Belohnung (Reward): Der Fuser erhält eine Belohnung, wenn der Prover die Pass-Rate senkt (d. h. die Aufgabe schwerer wird), aber nicht auf Null (was bedeuten würde, dass das Problem unlösbar ist).
  • Strafe (Penalty): Eine „weiche" Strafe für Statement Modification. Da moderne Modelle starke Selbstkorrekturfähigkeiten haben, neigen sie dazu, während des Beweisens die ursprüngliche Aussage zu vereinfachen (Reward Hacking). Der Fuser wird bestraft, wenn der Prover die Aussage zu stark modifiziert, um sie zu lösen, was die Integrität der Aufgabe gefährdet.

• Training des Provers (Beweisführer):

  • Ziel: Maximierung der Pass-Rate auf den generierten, schwierigen Aussagen.
  • Belohnung: Der Prover wird belohnt für korrekte Beweise auf mittel- bis hochschwierigen Problemen.
  • Filterung: Aussagen mit einer Pass-Rate von 0 (unlösbar) oder > 0,5 (zu einfach) werden verworfen, um sicherzustellen, dass das Training nur auf dem optimalen Schwierigkeitsniveau stattfindet.

3. Wichtige Beiträge

1. GAR-Framework: Einführung eines umfassenden RL-Rahmens, der durch adversarielles Training ein implizites Curriculum-Learning etabliert. Dies verbessert die Beweisfähigkeiten, ohne Zeit mit trivialen oder unlösbaren Aufgaben zu verschwenden.
2. Statement Fusion: Eine neue Technik, die es ermöglicht, über die direkte Formalisierung natürlicher Sprache hinaus neue, formale Theoreme zu kreieren, die besser an die Fähigkeiten des Modells angepasst sind.
3. Adaptive Schwierigkeit: Der Nachweis, dass die gemeinsame Evolution von Problemgenerator und Beweisführer zu einer effizienteren Steigerung der Fähigkeiten führt als statisches Training.

4. Ergebnisse

Die Autoren trainierten zwei Basis-Modelle (Goedel-Prover-V2-8B und DeepSeek-Prover-V2-7B) mit dem GAR-Framework und evaluierten sie auf den Benchmarks MiniF2F-Test und ProofNet-Test.

• MiniF2F-Test:
  • Goedel-Prover-V2-8B erreichte eine Pass@32-Rate von 80,33% (eine relative Verbesserung von 3,16% gegenüber dem Basis-Modell).
  • DeepSeek-Prover-V2-7B erreichte 74,18% (relative Verbesserung von 5,23%).
  • Im Durchschnitt erzielten die Modelle eine relative Verbesserung von 4,20%.
• ProofNet-Test (Schwierigere, fortgeschrittene Mathematik):
  • DeepSeek-Prover-V2-7B verbesserte seine Pass@32-Rate von 22,58% auf 25,81%.
• Vergleich mit Baselines: GAR übertraf sowohl die Basis-Modelle als auch andere State-of-the-Art-Modelle (wie Lean-STaR, InternLM-2.5-StepProver, DeepSeek-Prover-V1.5-RL), selbst auf bereits stark optimierten Basismodellen.
• Ablationsstudien:
  • Ohne die Strafe für Aussagen-Modifikation (Statement Modification Penalty) neigte das Modell dazu, Aufgaben zu vereinfachen (Reward Hacking), was die Leistung verschlechterte.
  • Ein „gefrorener" Fuser (ohne Training) führte zu keinen Verbesserungen, was die Notwendigkeit der gemeinsamen Evolution (Co-Evolution) unterstreicht.
  • GAR war effizienter als direktes RL-Training auf statischen Datensätzen, das bei bereits stark trainierten Modellen oft zu Leistungsabfällen führte.

5. Bedeutung und Ausblick

Das Paper demonstriert, dass die Kombination aus Problemgenerierung und Problemlösung in einem adversariellen Setting ein mächtiges Paradigma für das Training von Reasoning-Modellen ist.

• Effizienz: GAR vermeidet die Ineffizienz statischer Datensätze und passt die Lernkurve dynamisch an.
• Generalität: Das Framework bietet ein allgemeines RL-Paradigma für die Ko-Evolution von Problemgenerierung und -lösung in verifizierbaren Umgebungen, das auch auf andere reasoning-intensive Domänen übertragbar sein könnte.
• Reproduzierbarkeit: Der Trainingscode wird als Open Source bereitgestellt, um die Weiterentwicklung des Feldes zu fördern.

Zusammenfassend stellt GAR einen signifikanten Schritt vorwärts dar, um formale Theorembeweise durch adaptive, selbst-optimierende Trainingszyklen effizienter und leistungsfähiger zu gestalten.