💬 NLP

OProver: A Unified Framework for Agentic Formal Theorem Proving

OProver ist ein einheitliches Framework für agentenbasiertes formales Theorembeweisen in Lean 4, das iterative Beweisrevision mit Compiler-Feedback und Retrieval integriert und durch eine neuartige Trainingspipeline, die fortgesetztes Pretraining, überwachtes Fine-Tuning auf Reparatur-Trajektorien und Verstärkungslernen auf schwierigen Fällen kombiniert, state-of-the-art-Leistung über mehrere Benchmarks hinweg erzielt.

Ursprüngliche Autoren: David Ma, Kaijing Ma, Shawn Guo, Yunfeng Shi, Enduo Zhao, Jiajun Shi, Zhaoxiang Zhang, Gavin Cheung, Jiaheng Liu, Zili Wang

Veröffentlicht 2026-05-19

📖 4 Min. Lesezeit☕ Kaffeepausen-Lektüre

CC BY 4.0

Ursprüngliche Autoren: David Ma, Kaijing Ma, Shawn Guo, Yunfeng Shi, Enduo Zhao, Jiajun Shi, Zhaoxiang Zhang, Gavin Cheung, Jiaheng Liu, Zili Wang

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 versuchen, ein sehr schwieriges Mathe-Rätsel zu lösen, müssen die Lösung jedoch in einer strengen, roboterhaften Sprache namens Lean 4 verfassen. Wenn Sie auch nur einen winzigen Tippfehler oder einen logischen Fehler machen, lehnt der Computer (der „Compiler") das Ganze ab und sagt: „Nein, falsch."

Lange Zeit arbeiteten KI-Modelle, die diese Rätsel lösten, wie ein Schüler bei einer Prüfung: Sie rieten eine Antwort, und wenn diese falsch war, rieten sie einfach erneut von vorne. Sie lernten nicht wirklich, warum sie falsch lagen, und nutzten das spezifische Feedback des Computers nicht, um ihre Fehler zu korrigieren.

OProver ist ein neues System, das das Spiel verändert. Anstatt nur zu raten, agiert es wie ein perfektionistischer Detektiv, der niemals aufgibt. So funktioniert es, unter Verwendung einfacher Analogien:

1. Der „agentische" Detektiv (Der Beweiser)

Stellen Sie sich OProver nicht als statisches Lehrbuch vor, sondern als einen Detektiv, der einen mehrstufigen Untersuchungsprozess hat.

Der alte Weg: Der Detektiv schreibt eine Theorie auf, der Richter (der Computer) sagt „Falsch", und der Detektiv schreibt eine völlig neue Theorie von vorne.
Der OProver-Weg: Der Detektiv schreibt eine Theorie auf. Der Richter sagt: „Sie haben hier einen Fehler gemacht: Sie haben den falschen Zahlentyp verwendet." Der Detektiv bearbeitet dann diesen spezifischen Teil der Theorie, prüft ihn erneut und verfeinert ihn weiter, bis der Richter sagt: „Richtig!"

OProver ist darauf trainiert, diesen Tanz aus „Bearbeiten und Verfeinern" automatisch durchzuführen. Es rät nicht nur; es lernt, auf die spezifischen Beschwerden des Richters zu hören und diese zu beheben.

2. Die „Bibliothek der Lösungen" (Abruf)

Bevor der Detektiv mit dem Schreiben beginnt, arbeitet er nicht im luftleeren Raum. Er geht in eine riesige Bibliothek (genannt Abrufgedächtnis).

Wenn der Detektiv versucht, ein Rätsel über Dreiecke zu lösen, holt die Bibliothek sofort die 5 besten Beweise über Dreiecke heraus, die andere Detektive zuvor erfolgreich gelöst haben.
OProver liest diese „Spickzettel", um zu sehen, wie andere Menschen ähnliche Probleme gelöst haben, und nutzt ihre Strategien als Leitfaden. Dies hilft dem Detektiv, häufige Fallen zu vermeiden.

3. Die „selbstverbessernde Schleife" (Das Training)

Dies ist der magischste Teil. Normalerweise werden KI-Modelle auf einem festen Datensatz trainiert und dann sich selbst überlassen. OProver ist anders; es hat einen selbstverbessernden Zyklus.

Schritt 1: OProver versucht, eine Reihe von Rätseln zu lösen.
Schritt 2: Wenn es erfolgreich ist, speichert es diese Lösung in der Bibliothek, damit sie als „Spickzettel" für zukünftige Probleme verwendet werden kann.
Schritt 3: Wenn es scheitert, speichert es die gesamte Geschichte darüber, wie es gescheitert ist, was der Computer gesagt hat und wie es es schließlich korrigiert hat.
Schritt 4: Das System nutzt diese „Scheitergeschichten", um sich selbst beizubringen, wie es beim nächsten Mal besser machen kann.

Es ist wie ein Schüler, der nach jeder Prüfung nicht nur die richtigen Antworten auswendig lernt, sondern auch genau aufschreibt, warum er bei bestimmten Fragen falsch lag, und diese Notizen zu seinem Lernleitfaden hinzufügt. Mit der Zeit wird der Schüler schlauer, und der Lernleitfaden wird dicker und hilfreicher.

4. Das Ergebnis: Ein Super-Schüler

Die Studie testete dieses System an fünf verschiedenen „Mathematik-Olympiaden" (von Schulniveau bis hin zu sehr schwierigen Universitätswettbewerben).

Die Leistung: OProver (speziell die 32-Milliarden-Parameter-Version) wurde zum besten Performer unter allen Open-Source-KI-Beweisführern. Es löste mehr Probleme korrekt als jedes andere ähnliche System, sogar besser als viel größere Modelle.
Warum das wichtig ist: Es bewies, dass es der KI die Fähigkeit zu geben, Feedback zu hören, vergangene Lösungen nachzuschlagen und ihre eigene Arbeit iterativ zu korrigieren, viel mächtiger ist, als sie nur größer zu machen oder besser im Raten zu machen.

Zusammenfassung

OProver ist eine KI zur Lösung von Matheaufgaben, die nicht nur „raten und prüfen" betreibt. Es ist ein kooperativer Lerner, der:

Zuerst nachschlägt, ob ähnliche gelöste Probleme existieren.
Einen Beweis verfasst.
Auf die spezifischen Fehlermeldungen des Computers hört.
Seine Arbeit bearbeitet, um diese Fehler zu beheben.
Dies wiederholt, bis es erfolgreich ist, und speichert dann die Lektion für das nächste Mal.

Indem es das „Scheitern" in eine Lernmöglichkeit verwandelt und ein laufendes Protokoll darüber führt, was funktioniert, ist OProver zur besten Open-Source-KI für das formale Beweisen mathematischer Theoreme heute geworden.

Technische Zusammenfassung: OProver: Ein einheitliches Framework für agentices formales Theorembeweisen

Problemstellung

Jüngste Fortschritte im formalen Theorembeweisen, insbesondere im Ökosystem von Lean 4, haben groß angelegte Beweisgenerierung und verifiziererbewusstes Training genutzt, um die Leistung bei Benchmarks wie MiniF2F und PutnamBench zu verbessern. Eine kritische Einschränkung besteht jedoch weiterhin: agentices Beweisfähigkeiten (Abruf, Compiler-Feedback und iterative Reparatur) werden typischerweise als Inferenzzeit-Heuristiken behandelt, die auf einen festen Beweiser angewendet werden, anstatt als gelernte Richtlinien in den Trainingsprozess integriert zu werden.

Dies erzeugt eine Train-Inferenz-Mismatch. Modelle, die primär auf finalisierte, erfolgreiche Beweise trainiert wurden, treffen auf Compiler-Feedback und abgerufenen Kontext nur während des Einsatzes, in Verteilungen, für die sie nie optimiert wurden. Darüber hinaus konzentrieren sich bestehende formale Korpora auf Endprodukte (Aussagen und verifizierte Beweise) und lassen die mehrstufigen Interaktionsverläufe – gescheiterte Versuche, abgerufter Kontext und Compiler-Diagnosen – aus, die für das Erlernen der Beweisreparatur unerlässlich sind. Folglich bleibt das Überwachungssignal, das die Beweisreparatur in der Praxis antreibt, beim Modelltraining weitgehend ungenutzt.

Methodik

Die Arbeit stellt OProver vor, ein einheitliches Framework, das Abruf, Compiler-Feedback und iterative Reparatur direkt in die Richtlinie des Beweisers durch einen ko-evolutionären Trainingspipeline integriert.

1. Das OProver-Framework

OProver behandelt Theorembeweisen als eine begrenzte, mehrstufige Verfeinerungsschleife. In jeder Runde $t$ konditioniert die Richtlinie $\pi$ auf einen kompakten Zustand $X_t = (s, R_t, p_{t-1}, f_{t-1})$ , wobei:

$s$ : Die Ziel-Theoremaussage.
$R_t$ : Top- $k$ abgerufene, vom Compiler verifizierte Beweise aus einem Speicher $M$ .
$p_{t-1}$ : Der vorherige Beweisversuch.
$f_{t-1}$ : Das rohe textuelle Compiler-Feedback (Diagnosen) vom Lean-4-Verifizierer.

Die Richtlinie generiert einen revidierten Versuch $p_t$ . Falls die Verifizierung fehlschlägt, wird das rohe Feedback an die Richtlinie für die nächste Runde zurückgegeben. Entscheidend ist, dass die Richtlinie nur auf dem neuesten Versuch und dem Feedback konditioniert, wodurch lokale Korrektursignale erhalten bleiben, während der Zustand kompakt bleibt.

2. OProofs: Ein einheitliches Trainingskorpus

Um dieses Framework zu unterstützen, konstruieren die Autoren OProofs, ein groß angelegtes Korpus, das speziell für agentices Beweisen entwickelt wurde. Im Gegensatz zu früheren Datensätzen, die nur finale Beweise bewahren, zeichnet OProofs serialisierte Trajektorien auf, einschließlich:

Abgerufener Kontext.
Gescheiterter Versuche.
Roher Compiler-Feedbacks.
Nachfolgender Reparaturen.

OProofs wird aus drei Quellen erstellt: öffentlichen Lean-Ressourcen, groß angelegter Beweissynthese (Autoformalisierung + Verifizierung) und Spuren aus dem eigenen agenticen Beweisen von OProver. Es enthält 1,77 Millionen eindeutige Lean-Aussagen und 6,86 Millionen vom Compiler verifizierte Beweise, gepaart mit 1,07 Millionen agenticen Trajektorien.

3. Ko-evolutionärer Trainingspipeline

Der Trainingsprozess folgt einer iterativen Schleife (Algorithmus 1), bei der Beweiser und Korpus ko-evolvieren:

Fortgesetztes Pretraining (CPT): Ein Basismodell wird auf einer Mischung aus Lean-Code, Mathematik und Daten für langkontextuelles Schlussfolgern trainiert, um OProver-Base zu erstellen.
Iteratives Nachtraining:
- Agentic Rollouts: Die aktuelle Richtlinie führt mehrstufiges Beweisen auf einem Theorempool durch, ruft aus dem aktuellen Speicher $M_k$ ab und verifiziert mit dem Lean-Compiler.
- Datensammlung: Neu verifizierte Beweise werden zum Korpus hinzugefügt und in den Abrufspeicher indiziert. Gescheiterte Versuche und erfolgreiche Reparaturen werden in rundenbasierte Beispiele $(s, R_t, p_{t-1}, f_{t-1}) \to p_t$ zerlegt.
- Supervised Fine-Tuning (SFT): Das Modell wird unter Verwendung der gesammelten Reparaturbeispiele aktualisiert.
- Reinforcement Learning (RL): Group Sequence Policy Optimization (GSPO) wird auf schwierigere ungelöste Fälle angewendet, wobei ein Belohnungssignal basierend auf Verifizierungserfolg und Formatkorrektheit verwendet wird.
- Zirkulation: Das aktualisierte Korpus und der Speicher speisen die nächste Iteration, wodurch die Richtlinie aus ihren eigenen verbesserten Beweisen lernen kann.

Hauptbeiträge

Einheitliches Framework für agentices Beweisen: OProver vereint Abruf, Feedback und iterative Reparatur in einer einzigen gelernten Richtlinie und eliminiert die Train-Inferenz-Mismatch, indem das Modell trainiert wird, diese Signale als Teil seiner Kernstrategie zu nutzen, anstatt als externe Heuristiken.
OProofs-Korpus: Die Konstruktion eines groß angelegten Korpus (1,77 Millionen Aussagen, 6,86 Millionen Beweise), das mehrstufige Interaktionsverläufe explizit bewahrt, einschließlich gescheiterter Versuche und roher Compiler-Feedbacks, und damit Überwachungssignale bereitstellt, die in formalen Datensätzen zuvor nicht verfügbar waren.
Ko-evolutionärer Pipeline: Eine Trainingsmethode, bei der der Beweiser neue Daten (verifizierte Beweise und Reparaturtrajektorien) generiert, die sofort in das Trainingskorpus und den Abrufspeicher zurückgeführt werden, wodurch eine sich selbst verbessernde Schleife entsteht.
State-of-the-Art-Leistung: OProver erzielt Spitzenresultate unter Open-Weight-Ganzzahl-Beweisern und zeigt, dass agentices Verfeinerungsstrategien erheblich größere Modelle übertreffen können.

Experimentelle Ergebnisse

OProver wurde auf fünf Lean-4-Benchmarks evaluiert: MiniF2F, MathOlympiadBench, ProofNet, ProverBench und PutnamBench.

Leistung: Das OProver-32B-Modell erzielte die besten Pass@32-Werte auf drei Benchmarks (MiniF2F: 93,3 %, ProverBench: 58,2 %, PutnamBench: 11,3 %) und den zweitbesten Wert auf den anderen beiden (MathOlympiad: 22,8 %, ProofNet: 33,2 %).
Effizienz: OProver-32B (32 Milliarden Parameter) übertraf den 671-Milliarden-DeepSeek-Prover-V2 und den 560-Milliarden-LongCat-Flash-Prover (mit TIR) auf den meisten Benchmarks, trotz deutlich weniger Parametern. Selbst die 8-Milliarden-Variante übertraf den 32-Milliarden-Goedel-Prover-V2 auf allen Benchmarks.
Skalierung zur Laufzeit: Die Leistung verbesserte sich konsistent mit erhöhten Rechenbudgets (mehr Stichproben oder Verfeinerungsrunden), wenn auch mit abnehmenden Grenzerträgen. Die optimale Aufteilung zwischen Verfeinerungstiefe und Stichprobenbreite variierte je nach Schwierigkeitsgrad des Benchmarks.
Ablationsstudien: Das Entfernen von mehrstufigem Compiler-Feedback verursachte die signifikanteste Leistungsverschlechterung und bestätigte die iterative Verfeinerung als primären Treiber der Gewinne. Das Entfernen der Abruf-Augmentierung verursachte ebenfalls konsistente, wenn auch kleinere, Einbußen und unterstreicht den komplementären Wert der Abrufverankerung.

Bedeutung und Behauptungen

Die Arbeit behauptet, dass OProver zeigt, dass agentices formales Theorembeweisen effektiv als einheitliche Richtlinie gelernt werden kann, anstatt aus separaten Inferenzzeit-Modulen zusammengesetzt zu werden. Durch das Training auf dem gesamten Verlauf des Beweisaufbaus, des Scheiterns und der Reparatur lernt das Modell, Compiler-Feedback und abgerufenen Kontext als intrinsische Teile seines Schlussfolgerungsprozesses zu nutzen.

Die Autoren betonen, dass die Leistungsgewinne nicht lediglich auf der Skalierung des Modells beruhen, sondern aus der Synergie zwischen abrufaugmentierter Verankerung und compilergeführter iterativer Verfeinerung resultieren. Die Ko-Evolution der OProver-Richtlinie und des OProofs-Korpus ermöglicht es dem System, seine Beweisfähigkeiten kontinuierlich zu verbessern, indem es aus seinen eigenen erfolgreichen und gescheiterten Versuchen lernt, und etabliert ein neues Paradigma für das Training formaler Schlussfolgerungssysteme.