Goedel-Prover-V2: Skalierung des formalen Theorembeweisens durch gestufte Datensynthese und Selbstkorrektur

papers.abstract

Wir stellen Goedel-Prover-V2 vor, eine Reihe von Open-Source-Sprachmodellen, die einen neuen State-of-the-Art im automatisierten Theorembeweis setzen. Basierend auf der Standard-Pipeline für Experteniteration und Reinforcement Learning integriert unser Ansatz drei Schlüsselinnovationen: (1) Gestufte Datensynthese: Wir generieren synthetische Aufgaben mit steigendem Schwierigkeitsgrad, um das Modell darauf zu trainieren, zunehmend komplexe Theoreme zu beherrschen; (2) Verifizierer-gesteuerte Selbstkorrektur: Wir ermöglichen es dem Modell, seine Beweise iterativ zu überarbeiten, indem es Feedback vom Lean-Compiler nutzt; (3) Modellmittelung: Wir kombinieren Modell-Checkpoints, um den Rückgang der Modellausgabevielfalt in späteren Trainingsphasen zu mildern. Unser kleines Modell, Goedel-Prover-V2-8B, erreicht 84,6 % pass@32 auf MiniF2F und übertrifft DeepSeek-Prover-V2-671B unter demselben Maßstab, obwohl es 80-mal kleiner ist. Unser Flaggschiffmodell, Goedel-Prover-V2-32B, erzielt 88,1 % auf MiniF2F bei pass@32 im Standardmodus und 90,4 % im Selbstkorrekturmodus, womit es den bisherigen SOTA deutlich übertrifft. Zudem löst unser Flaggschiffmodell 86 Probleme auf PutnamBench bei pass@184 und sichert sich damit den ersten Platz unter den Open-Source-Modellen auf der Bestenliste, wobei es den Rekord von DeepSeek-Prover-V2-671B von 47 gelösten Problemen bei pass@1024 mit einem deutlich kleineren Modell und geringerem Rechenbudget übertrifft. Zum Zeitpunkt seiner Veröffentlichung (Juli-August 2025) erreicht Goedel-Prover-V2 die insgesamt beste Leistung unter allen Open-Source-Theorembeweisern. Es zählt auch zu den leistungsstärksten Modellen – einschließlich Closed-Source-Systemen mit öffentlich berichteter Leistung – unter einem begrenzten Testzeit-Rechenbudget. Unsere Modelle, der Code und die Daten werden unter https://github.com/Goedel-LM/Goedel-Prover-V2 veröffentlicht.

English

We introduce Goedel-Prover-V2, a series of open-source language models that set a new state-of-the-art in automated theorem proving. Built on the standard expert iteration and reinforcement learning pipeline, our approach incorporates three key innovations: (1) Scaffolded data synthesis: We generate synthetic tasks of increasing difficulty to train the model to master increasingly complex theorems; (2) Verifier-guided self-correction: We enable the model to iteratively revise its proofs by leveraging feedback from the Lean compiler; (3) Model averaging: We merge model checkpoints to mitigate the decrease in model output diversity in later stages of training. Our small model, Goedel-Prover-V2-8B, reaches 84.6% pass@32 on MiniF2F and outperforms DeepSeek-Prover-V2-671B under the same metric, despite being 80X smaller. Our flagship model, Goedel-Prover-V2-32B, achieves 88.1% on MiniF2F at pass@32 in standard mode and 90.4% in self-correction mode, outperforming prior SOTA by a large margin. Additionally, our flagship model solves 86 problems on PutnamBench at pass@184, securing the first place among open-source models on the leaderboard, surpassing DeepSeek-Prover-V2-671B's record of solving 47 problems by pass@1024 with a significantly smaller model size and compute budget. At the time of its release (July-August 2025), Goedel-Prover-V2 achieves the strongest overall performance among all open-source theorem provers. It also ranks among the top-performing models--including closed-source systems with publicly reported performance--under a constrained test-time compute budget. Our models, code, and data are released at https://github.com/Goedel-LM/Goedel-Prover-V2.

Goedel-Prover-V2: Skalierung des formalen Theorembeweisens durch gestufte Datensynthese und Selbstkorrektur

Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction

papers.abstract

Support