32B übertrifft 671B: OProver, das vollständig quelloffene mathematische Theorembeweis-Modell von M-A-P, erreicht den 1. Platz in 5 von 3 Bewertungen

Formalisierte Theorembeweise sind seit jeher der anspruchsvollste Test für die logische Fähigkeit von Large Language Models (LLMs). Jeder Schritt der Ableitung muss von der Lean 4-Kernmaschine verifiziert werden.

In den letzten zwei Jahren hat die Open-Source-Community auf Benchmarks wie MiniF2F und PutnamBench stetig bessere Ergebnisse erzielt. Die Wachstumspfade werden jedoch immer ähnlicher: Modellvergrößerung, Datenerweiterung sowie die Integration von Suchalgorithmen und mehrfachen Korrekturen in der Deploy-Phase.

Ein zentrales Problem besteht weiterhin darin, dass Suchsignale, Compiler-Feedback und Fehlerbehebungen in der Regel erst in der Deploy-Phase als externe Prozesse integriert werden. Das Modell lernt in der Trainings-Phase nicht systematisch, wie es diese Signale nutzen kann, was zu einer "Strategiedisparität zwischen Training und Deployment" führt.

Um diese Herausforderung zu meistern, haben die M-A-P Open-Source-Community und Teams wie die Universität Nanjing OProver vorgeschlagen –

ein Lean 4-Theorembeweis-Framework, das Suchverstärkung, Compiler-Feedback und mehrfache Korrekturen direkt in die Trainingsstrategie integriert.

In fünf Lean 4 whole-proof prover-Evaluierungen hat OProver-32B drei erste und zwei zweite Plätze belegt:

Bei MiniF2F (93,3), ProverBench (58,2) und PutnamBench (11,3) liegt es vor LongCat-Flash-Prover w/ TIR und übertrifft in allen fünf Evaluierungen den 671B-DeepSeek-Prover-V2.

Das Forschungsteam hat gleichzeitig die OProofs-Datensammlung mit 1,76 Millionen formalierten Aussagen und 6,80 Millionen compiler-verifizierten Beweisen sowie sieben Modellgewichte (8B/32B) Open-Source gemacht.

Der Code, die Gewichte und die Trainingsskripte sind vollständig Open-Source.

Strategiedisparität: Der Kernkonflikt zwischen Training und Deployment

In den letzten Jahren haben Lean 4-Prover-Systeme wie Goedel-Prover-V2, DeepSeek-Prover-V2 und Kimina-Prover den Pass@32-Wert auf MiniF2F auf ein hohes Niveau gebracht. Gleichzeitig wurden Suchalgorithmen, Compiler-Feedback oder Self-Correction eingeführt.

Das Problem besteht darin, dass diese Signale hauptsächlich als Verstärkungsprozesse in der Deploy-Phase außerhalb des bereits trainierten Provers integriert werden, anstatt bereits in der Trainings-Phase in die Lernziele aufgenommen zu werden.

Das führt zu einer Disparität:

• In der Trainings-Phase sieht das Modell hauptsächlich klare Supervisionspaare von Theorem → verifizierter Beweis.
• In der Deploy-Phase werden dem System jedoch die gefundenen relevanten Beweise, die fehlgeschlagenen Versuche der vorherigen Runde und das Feedback des Lean-Compilers erneut bereitgestellt, um mehrfache Korrekturen durchzuführen.

Der Kerngedanke von OProver besteht darin, die Trainingsziele mit dem Beweisprozess in der Deploy-Phase auszurichten: Das Modell soll bereits in der Trainings-Phase lernen, wie es eine agentische Verbesserungsschleife ausführt, indem es mehrfache Korrekturen, das Suchen nach relevanten Beweisen und das Compiler-Feedback als Teil der Trainingsstrategie aufnimmt, anstatt sie in der Deploy-Phase als externe Verpackung hinzuzufügen.

Leichtgewichtig und end-to-end trainierbar

Deploy-Phase: Reparaturzyklus mit begrenzter Anzahl von Runden

OProver modelliert den Theorembeweis als einen Reparaturzyklus mit begrenzter Anzahl von Runden.

Die Strategie basiert auf der formalierten Zielaussage, den top-k compiler-verifizierten Beweisen aus der Suchdatenbank, dem Beweisversuch der vorherigen Runde und den Diagnoseinformationen, die der Lean 4-Compiler zurückgibt, um den nächsten Beweisversuch zu generieren. Wenn eine Runde erfolgreich ist, gilt die gesamte Trajektorie als erfolgreich.

Trainings-Phase: Zweistufiges Training

• Kontinuierliches Pre-Training (CPT): Pre-Training auf einer gemischten Datensammlung von etwa 65 Milliarden Token, von denen etwa 30 % aus Lean 4-Daten von OProofs, 20 % aus Code-Daten (OpenCoder), 40 % aus mathematischen Datensammlungen (Nemotron-Math-4-Plus) und 10 % aus langen CoT-Daten stammen.
• Iteratives Post-Training: Abwechselnd agentisches Beweisrollen, SFT (basierend auf Reparaturproben auf Rundenebene) und RL (basierend auf dem GSPO-Algorithmus und der Schwierigkeitsmenge).

Das Schlüsselkonzept besteht darin, dass die Suchergebnisse, die fehlgeschlagenen Versuche und das Compiler-Feedback nicht mehr nur als externe Prozesse in der Deploy-Phase integriert werden, sondern in die zu lernende Beweisstrategie des Modells aufgenommen werden.

Koevolution von Daten und Modell

Die OProofs-Datensammlung und die Prover-Strategie fördern sich in der Iteration gegenseitig.

In jeder Iteration werden die neuen verifizierten Beweise, die der aktuelle Prover auf der Aufgabenbank generiert, der OProofs-Datensammlung hinzugefügt und in die Suchdatenbank indexiert.

Die Reparaturtrajektorien werden zu Trainingsbeispielen für die nächste SFT-Runde, und die noch ungelösten "Schwierigkeitsgruppen" liefern Trainingssignale für die nächste RL-Runde.

Daten, Training und Strategie bilden einen kontinuierlich sich entwickelnden geschlossenen Kreis.

OProofs: Lean 4-Datensammlung für agentische Prover

Das Forschungsteam hat gleichzeitig OProofs erstellt und Open-Source gemacht, das etwa 1,76 Millionen formalisierte Aussagen und 6,80 Millionen compiler-verifizierte Beweise enthält.

Von diesen Beweisen haben 4,29 Millionen die gefundenen relevanten Beweis-Kontexte beibehalten, und 859.000 Proben enthalten das Feedback des Lean-Compilers aus vorherigen fehlgeschlagenen Versuchen. Das Modell lernt nicht nur, "was der endgültige korrekte Beweis ist", sondern auch, "wie man nach einem fehlgeschlagenen Beweis die Suchergebnisse und das Compiler-Feedback nutzen kann, um weiter zu reparieren".

OProofs besteht aus zwei Konstruktionszweigen.

1. Neu-Beweis von öffentlichen Ressourcen

Unter Verwendung von öffentlichen Lean-Ressourcen wie NuminaMath-LEAN, Lean-Workbook und Leanabell-Prover-FormalStmt als Ausgangspunkt werden die Daten gereinigt und duplikatfrei gemacht. Anschließend werden Beweise neu generiert und verifiziert, und gleichzeitig werden Suchkontexte, fehlgeschlagene Versuche und Reparaturtrajektorien gesammelt.

2. Von natürlicher Sprache zur Formalisierung

Mathematische Aussagen werden aus Common Crawl und GitHub extrahiert, automatisch mit CriticLean in Lean 4 formalisisiert und dann durch den agentischen Beweisprozess generiert und verifiziert.

In Bezug auf die Abdeckung erstreckt sich OProofs über mehrere mathematische Bereiche: Algebra 60,1 %, Analysis 13,7 %, Zahlentheorie 13,0 %, Geometrie 6,8 %. Die Schwierigkeitsverteilung liegt hauptsächlich auf der Ebene von elementaren (27,4 %) und Gymnasialniveau (48,9 %), und es gibt auch 18,9 % Probleme auf Bachelor-Niveau und 4,8 % auf Master-Niveau.

Drei erste und zwei zweite Plätze in fünf Evaluierungen

Das Forschungsteam hat OProver auf fünf Lean 4-Benchmarks (MiniF2F, MathOlympiad, ProofNet, ProverBench, PutnamBench) evaluiert und standardmäßig den Pass@32-Wert basierend auf 64 unabhängigen multi-round rollouts ohne Bias berichtet.

Im Bereich der Open-Weight whole-proof prover gibt es drei Schlussfolgerungen für OProver-32B:

1. 32B übertrifft 671B

OProver-32B übertrifft in allen fünf Evaluierungen den DeepSeek-Prover-V2 (671B) und liegt bei MiniF2F (93,3), ProverBench (58,2) und PutnamBench (11,3) vor LongCat-Flash-Prover w/ TIR (560B).

2. 8B erreicht das Niveau von 32B

OProver-8B übertrifft in allen fünf Benchmarks den Goedel-Prover-V2-32B, obwohl es nur ein Viertel der Parameter hat.

3. Iteratives Post-Training bringt kontinuierliche Verbesserungen

Bei MiniF2F-Test steigt der Wert von OProver-8B von 79,5 auf 91,8 (+12,3) und der von OProver-32B von 84,7 auf 93,3 (+8,6).

Ablations-Experiment: Gemeinsame Beiträge von Suche und Compiler-Feedback

Das Entfernen des mehrfachen Compiler-Feedbacks führt zu einem deutlichen Rückgang: OProver-32B fällt bei PutnamBench von 11,3 auf 7,0 und bei ProofNet von 33,2 auf 25,8.

Nach der weiteren Entfernung der Suche sinkt die Leistung weiter auf 5,9 und 24,7.

Dies zeigt, dass die Verbesserung nicht einfach durch die Best-of-N-Sampling-Methode erreicht wird, sondern durch die Synergie zwischen der suchverstärkten Beweisgenerierung und der mehrfachen Korrektur, die durch das Compiler-Feedback geleitet wird.

Dabei liefert das Feedback des Lean-Compilers das Hauptsignal für die Reparatur, und der Suchkontext liefert die relevante Beweisstruktur und die zu referenzierenden Beweisabschnitte.

Erweiterung bei der Testphase: Stabile Verbesserung durch mehr Inferenzbudget

Mit der Erhöhung des Inferenzbudgets von 8 auf 256 steigt die Leistung von OProver-32B in allen fünf Benchmarks stabil: MiniF2F von 87,5 auf 92,8, MathOlympiad von 15,5 auf 22,0, ProofNet von 25,6 auf 32,8, ProverBench von 51,3 auf 56,9, PutnamBench von 6,4 auf 11,3.

Die optimale Budgetzuweisung hängt von der Schwierigkeit des Benchmarks ab: Die meisten Benchmarks profitieren eher von einer Erhöhung der Reparaturtiefe, während bei Schwierigkeiten wie PutnamBench ein Gleichgewicht zwischen Reparaturtiefe und paralleler Exploration erforderlich ist.

Open-Source und Veröffentlichung

Das Forschungsteam hat gleichzeitig das OProver-Modell, die Daten und den Trainingscode Open-Source gemacht, einschließlich Checkpoints für verschiedene Trainingsphasen, der OProofs-Datensammlung und der Trainingspipeline.

• m-a-p/OProver-32B / OProver-8B — Endmodell

• m-a-p/OProver-32B-Base / Round1 — Checkpoints für verschiedene Phasen von 32B

• m-a-p/OProver-8B-Base / Round1 / Round2 — Checkpoints für verschiedene Phasen von 8B

• m-a-p/OProofs — 1,76 Millionen Aussagen / 6,80 Millionen Beweise / 1,