🤖 AI

Process-Verified Reinforcement Learning for Theorem Proving via Lean

Dieses Paper führt ein Reinforcement-Learning-Framework ein, das den Lean-Beweisassistenten als symbolische Prozess-Orakel nutzt, um dichtes, feingranulares und korrektes Feedback auf Taktik-Ebene bereitzustellen, wodurch die Theorem-Proving-Leistung auf Benchmarks wie MiniF2F und ProofNet im Vergleich zu herkömmlichen, nur auf Ergebnissen basierenden Belohnungsmethoden signifikant verbessert wird.

Ursprüngliche Autoren: Minsu Kim, Se-Young Yun

Veröffentlicht 2026-06-19

📖 4 Min. Lesezeit☕ Kaffeepausen-Lektüre

CC BY 4.0

Ursprüngliche Autoren: Minsu Kim, Se-Young Yun

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie bringen einem Roboter bei, komplexe mathematische Rätsel zu lösen. In der Vergangenheit war die Art und Weise, wie wir diese Roboter (das waren große Sprachmodelle) trainierten, wie ein Spiel von „Heiß oder Kalt“ mit einem sehr strengen Schiedsrichter.

Der alte Weg: Der „Bestanden oder Nicht Bestanden“-Coach
Früher schrieb der Roboter eine vollständige Lösung zu einem mathematischen Problem auf. Der Schiedsrichter (ein Computerprogramm namens Lean) sah sich die endgültige Antwort an und sagte nur eines: „Du hast es richtig gemacht!“ oder „Du hast es falsch gemacht.“

Wenn der Roboter einen Fehler machte, wusste er nicht, warum. Hatte er schon im allerersten Schritt einen Fehler gemacht? Hatte er in der Mitte die falsche Formel verwendet? Oder war ihm einfach die Zeit ausgegangen? Es war, als würde ein Schüler eine Prüfung mit einer „6“ erhalten, ohne das korrigierte Blatt zu sehen. Der Roboter musste raten, was schiefgelaufen war, und es erneut versuchen, was langsam und ineffizient war.

Der neue Weg: Der „Schritt-für-Schritt“-Coach
Dieses Paper stellt eine intelligentere Methode vor, um den Roboter zu trainieren. Anstatt nur auf die endgültige Antwort zu warten, beobachtet der Lean-Schiedsrichter den Denkprozess des Roboters Schritt für Schritt.

Stellen Sie sich ein mathematisches Beweisführen wie das Bauen eines Turms aus Blöcken vor.

Der alte Weg: Sie bauen den ganzen Turm, und wenn er am Ende umkippt, sagt der Coach nur: „Schlechter Turm.“ Sie müssen raten, welcher Block den Einsturz verursacht hat.
Der neue Weg (dieses Paper): Der Coach beobachtet Sie beim Setzen jedes einzelnen Blocks.
- Wenn Sie einen Block korrekt platzieren, gibt Ihnen der Coach ein kleines „Gut gemacht!“ (ein positives Signal).
- Wenn Sie einen Block falsch platzieren, sagt der Coach sofort: „Stopp! Dieser Block ist falsch.“
- Entscheidend: Der Coach erklärt, dass, weil dieser Block falsch war, jeder einzelne Block, den Sie darauf setzen, nun ungültig ist, selbst wenn sie für sich genommen okay aussehen. Dies wird als „First-Error Propagation“ bezeichnet. Es lehrt den Roboter, dass ein einziger Fehler das gesamte Fundament ruiniert.

Wie es in dem Paper funktioniert
Die Forscher verwendeten eine Methode namens Reinforcement Learning (Bestärkendes Lernen). Hier ist die Aufschlüsselung ihres „Geheimrezepts“:

Der Oracle (Orakel): Sie nutzten den Lean-Beweisassistenten nicht nur als Endrichter, sondern als Prozess-Orakel. Das bedeutet, er fungt als ein Super-Lehrer, der die Regeln der Logik perfekt versteht und Fehler in Echtzeit erkennen kann.
Die Feedback-Schleife: Wenn der Roboter versucht, ein Problem zu lösen, bricht Lean die Lösung in eine Sequenz von „Taktiken“ (kleinen logischen Schritten) herunter.
- Wenn der gesamte Beweis funktioniert, erhält der Roboter eine große Belohnung.
- Wenn der Beweis fehlschlägt, sagt Lean dem Roboter genau, welcher Schritt fehlgeschlagen ist. Der Roboter lernt, dass die Schritte vor dem Fehler in Ordnung waren, aber der Schritt bei dem Fehler und alles danach falsch sind.
Das Credit-System: Das Paper fand heraus, dass der wichtigste Teil eines Schritts das allerste Wort (oder Token) dieses Schritts ist. Es ist wie das „Kommandowort“ (z. B. „Addiere“, „Multipliziere“, „Nimm an“). Die Forscher entschieden, die Belohnung oder Strafe spezifisch an dieses erste Wort zu geben. Dies hilft dem Roboter zu lernen, das richtige „Kommando“ für die Aufgabe zu wählen, anstatt nur den ganzen Satz auswendig zu lernen.

Die Ergebnisse
Als sie diese neue Methode auf berühmten mathematischen Benchmarks (MiniF2F und ProofNet) testeten:

Lernten die Roboter schneller und machten weniger Fehler.
Wurden sie stabiler und zuverlässiger als Roboter, die nur mit „Bestanden/Nicht Bestanden“-Feedback trainiert wurden.
Sie schnitten besser ab als Roboter, die versuchten, andere, weniger präzise Methoden zu nutzen, um zu erraten, welche Schritte gut waren.

Das große Ganze
Die wichtigste Erkenntnis ist, dass formale Beweisassistenten (wie Lean) nicht nur dazu verwendet werden sollten, Antworten am Ende zu prüfen. Sie können auch als Coaches während des Trainingsprozesses eingesetzt werden. Indem man der KI dichtes, spezifisches Feedback dazu gibt, wie sie denkt, anstatt nur darauf, was sie schlussfolgert, können wir intelligentere und zuverlässigere KI für das Lösen harter logischer Probleme bauen.

Was sie nicht getan haben
Das Paper ist sehr spezifisch über das, was es erreicht hat. Es hat nicht behauptet, alle mathematischen Probleme zu lösen, noch behauptet, dass diese Methode beim Schreiben von Geschichten oder beim Chatten mit Menschen funktioniert. Es geht rein darum, KIs beizubringen, mathematische Theoreme unter Verwendung der Sprache Lean zu beweisen. Sie merkten auch an, dass sie ihre Methode nicht mit anderen „gelernten“ Coaches verglichen haben, da diese riesige Mengen an menschlich geschriebenen Beispielen erfordern würden, die für diese spezielle Art von Mathematik noch nicht existieren.

Technisches Resümee: Prozessverifiziertes Reinforcement Learning für das Theorembeweisen mittels Lean

Problemstellung

Das automatisierte Theorembeweisen (Automated Theorem Proving, ATP) zielt darauf ab, formale Beweise für mathematische Theoreme zu generieren. Während Large Language Models (LLMs) Fortschritte bei Denkaufgaben erzielt haben, verlassen sie sich im Rahmen von Reinforcement Learning (RL) typischerweise auf natürliche Sprache (NL) oder binäre Ergebnissignale (korrekt/inkorrekt). Dies schafft eine Lücke:

Spärliches Feedback (Sparse Feedback): Standardmäßige RL-Ansätze verwenden oft nur ein finales binäres Signal (Beweis bestanden/fehlgeschlagen), was eine spärliche Kreditzuweisung (Credit Assignment) zur Folge hat und Schwierigkeiten bereitet, das Modell durch lange Argumentationsketten zu führen.
Unstrukturiert vs. Strukturiert: Im Gegensatz zu symbolischen Beweisassistenten (z. B. Lean, Coq, Isabelle), die ein feingranulareses, typentheoretisches Feedback für jeden einzelnen Denkschritt bieten, werden LLMs auf Token-Sequenzen mit skalaren Belohnungen trainiert.
Prozess-Belohnungsmodelle (Process Reward Models, PRMs): Während neuere Arbeiten PRMs nutzen, um schrittweise Belohnungen bereitzustellen, erfordern diese oft große annotierte Datensätze oder verlassen sich auf NL-basierte CoT-Supervision (Chain-of-Thought), wobei es ihnen an der rigorosen Korrektheit symbolischer Verifikation mangelt.

Die zentrale Herausforderung besteht darin, wie das reichhaltige, strukturierte Feedback eines symbolischen Beweisassistenten (Lean) nutzen kann, um LLMs zu trainieren, ohne auf externe, potenziell verrauschte PRMs oder menschliche Annotationen angewiesen zu sein.

Methodik

Das Paper schlägt Prozessverifiziertes Reinforcement Learning vor, ein Framework, das Leans symbolisches Feedback direkt in eine Group Relative Policy Optimization (GRPO)-Zielfunktion integriert. Die Methode besteht aus drei Hauptkomponenten:

1. Symbolischer Prozess-Orakel (Symbolic Process Oracle)

Anstatt Lean lediglich als finalen Verifizierer zu betrachten, nutzt der Autor Lean als Prozess-Orakel während des Trainings.

Parsing: Generierte Beweise werden basierend auf dem Abstrakten Syntaxbaum (AST) in Sequenzen von Taktiken ( $T_1, \dots, T_N$ ) zerlegt.
Verifikation: Der Elaborationsprozess von Lean liefert zwei Arten von Signalen:
- Ergebnissignal (Outcome Signal): Ein globales binäres Score $g(Y) \in \{0, 1\}$ , das angibt, ob der gesamte Beweis gültig ist.
- Prozesssignal (Process Signal): Feingranulares Feedback für jede Taktik, das lokal korrekte Schritte sowie den spezifischen Ort des ersten Fehlers identifiziert.

2. Strategie zur Kreditzuweisung (Credit Assignment Strategy)

Um die Lücke zwischen symbolischem Feedback und Token-Level RL zu schließen, führen die Autoren spezifische Zuweisungsregeln ein:

Fehler-Propagierung (First-Error Propagation): Wenn eine Taktik $T_j$ fehlschlägt, werden alle nachfolgenden Taktiken ( $T_k$ mit $k \ge j$ ) als fehlerhaft behandelt. Dies spiegelt die kausale Natur von Beweisen wider: Ein ungültiger Präfix invalidiert die gesamte nachfolgende Argumentationskette.
Taktik-Level Scoring ( $\phi$ ):
- Wenn der Beweis besteht ( $g(Y)=1$ ), erhalten alle Taktiken einen positiven Score (1).
- Wenn der Beweis fehlschlägt ( $g(Y)=0$ $g (Y) = 0$ ):
  - Taktiken vor dem ersten Fehler erhalten einen partiellen Score ( $d_1$ ).
  - Die erste fehlerhafte Taktik und alle nachfolgenden erhalten einen Penalty-Score ( $d_2$ ).
Token-Level Mapping: Der Taktik-Level-Vorteil wird nur dem ersten Token jeder Taktik zugewiesen (dem Schlüsselwort, z. B. intro, apply). Dies richtet sich nach dem semantischen Entscheidungspunkt, an dem die Beweisstrategie festgelegt wird.

3. RL-Zielfunktion (GRPO-Integration)

Das Framework kombiiert Outcome- und Prozess-Vorteile in einer einzigen GRPO-Zielfunktion:

Outcome-Vorteil ( $A_{outcome}$ ): Wird basierend auf dem globalen Pass/Fail-Status relativ zum Gruppenmittelwert berechnet.
Prozess-Vorteil ( $A_{process}$ ): Wird basierend auf den Taktik-Scores berechnet, normiert durch die Mittelwert-Belohnung der Gruppe, um die Schwierigkeit des Problems zu berücksichtigen.
Kombinierter Vorteil: Für ein Token $t$ , das zum ersten Token der Taktik $j$ in Antwort $i$ gehört:
$A_{i,t} = A_{outcome, i, t} + A_{process, i, j}$
Für Nicht-Erst-Token wird nur der Outcome-Vorteil angewendet. Diese Formulierung vermeidet die Notwendigkeit eines Value-Modells oder eines zusätzlichen PRM und stützt sich ausschließlich auf den Verifizierer als Grundwahrheit (Ground Truth).

Zentrale Beiträge

Formalisierung von symbolischem Feedback: Die Autoren formalisieren das Taktik-Level-Feedback von Lean in skalare Trainingssignale, was eine feingranulare, Token-Level Kreditzuweisung ohne natürliche Sprachführung ermöglicht.
Symbolisch Verifizierer-gesteuertes RL: Sie integrieren Outcome- und Taktik-Level-Belohnungen, die direkt aus Lean abgeleitet sind, in ein RL-Framework und bieten so eine dichte und verifizierbare Kreditzuweisung.
Stabile Benchmark-Verbesserungen: Der Ansatz zeigt konsistente Verbesserungen auf den Benchmarks MiniF2F und ProofNet und übertrifft dabei Outcome-only RL sowie Vanilla-Baselines, ohne externe PRMs oder NL-Notation zu benötigen.

Experimentelle Ergebnisse

Die Experimente wurden mit STP-Lean und DeepSeek-Prover-V1.5 (7B Modelle) auf den Benchmarks MiniF2F-Test und ProofNet-Test durchgeführt.

Leistungssteigerungen:
- STP-Lean: Die vorgeschlagene Methode verbesserte MiniF2F pass@64 um +2,5 % (von 56,7 % auf 59,2 %) und ProofNet pass@32 um +1,4 %.
- DeepSeek-Prover-V1.5: Es wurden konsistente, wenn auch marginale Verbesserungen in allen Einstellungen beobachtet.
Vergleich mit Baselines:
- Die Methode übertraf das "Outcome-only" GRPO, welches Instabilitäten zeigte und in einigen Konfigurationen auf ProofNet keine Verbesserung erzielte.
- Sie erreichte kompetitive Ergebnisse gegenüber starken Tree-Search-Baselines (z. B. InternLM2.5-StepProver, DeepSeek-Prover-RL+RMaxTS) bei Verwendung eines Single-Shot-Generierungsansatzes ohne massives Inference-Time-Search-Budget.
Ablationsstudien:
- Token-Zuweisung: Die Zuweisung von Credit an den ersten Token einer Taktik lieferte die stabilsten Ergebnisse im Vergleich zur Verteilung des Credits über alle Token oder den letzten Token.
- Fehler-Propagierung: Das Entfernen dieser Regel verschlechterte die Leistung signifikant, was die Notwendigkeit bestätigt, nachfolgende Schritte als ungültig zu behandeln, sobald ein Fehler auftritt.
- Timeouts: Ein 15-sekündiger Verifikations-Timeout bot das beste Gleichgewicht, indem er prägnante Beweise förderte, ohne valide komplexe Beweise zu verwerfen.

Bedeutung und Behauptungen

Das Paper behauptet, dass symbolische Beweisassistenten nicht nur als Evaluierungswerkzeuge, sondern als aktive Prozess-Belohnungs-Orakel während des Trainings betrachtet werden sollten. Durch die Nutzung des "reichhaltigen, feingranularen strukturierten Feedbacks", das in formalen Reasoning-Systemen inhärent ist, demonstrieren die Autoren einen Weg zu RL-Frameworks, die die Skalierbarkeit von LLMs mit der Zuverlässigkeit symbolischer Verifikation kombinieren.

Die Studie hebt hervor:

Dichte, verifizierbare Signale: Die Nutzung der eigenen Error-Logs und Elaboration-Trees des Provers liefert ein fundiertes, dichtes Belohnungssignal, das einem spärlichen binären Outcome oder gelernten PRMs überlegen ist.
Stabilität: Die Kombination aus globalen Outcome-Belohnungen und lokalen Taktik-Belohnungen stabilisiert das Training und verhindert die vorzeitige Konvergenz, die beim Taktik-only-Training auftritt, sowie die Sparsamkeitsprobleme beim Outcome-only-Training.
Effizienz: Dieser Ansatz erreicht State-of-the-Art oder kompetitive Leistungen ohne den Rechenaufwand von Tree-Search oder die Datenanforderungen für das Training separater PRMs.

Die Autoren bleiben hinsichtlich der Limitationen bescheiden und merken an, dass ihre Methode auf festen Reward-Scores ( $d_1, d_2$ ) statt auf gelernten Advantage-Schätzern basiert und sich derzeit auf reine (Nicht-CoT) Lean-Beweise konzentriert, was die Gestaltung von Belohnungen für langwieriges natürliches Sprach-Reasoning offen lässt.