Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data
  Synthesis and Self-Correction
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.
6892cb908da45ffb0a2b2490
Yong Lin
6892cb908da45ffb0a2b2491
Shange Tang
6892cb908da45ffb0a2b2492
Bohan Lyu
claimed_verified
2025-08-06T19:16:36.323Z
650267e7e751d03da933a24a
/avatars/f047a047d1de304cd97027463541bdf3.svg
Bohan22
user
Bohan22
6892cb908da45ffb0a2b2493
Ziran Yang
6892cb908da45ffb0a2b2494
Jui-Hui Chung
6892cb908da45ffb0a2b2495
Haoyu Zhao
6892cb908da45ffb0a2b2496
Lai Jiang
6892cb908da45ffb0a2b2497
Yihan Geng
6892cb908da45ffb0a2b2498
Jiawei Ge
6892cb908da45ffb0a2b2499
Jingruo Sun
6892cb908da45ffb0a2b249a
Jiayun Wu
6892cb908da45ffb0a2b249b
Jiri Gesi
6892cb908da45ffb0a2b249c
Ximing Lu
6892cb908da45ffb0a2b249d
David Acuna
6892cb908da45ffb0a2b249e
Kaiyu Yang
6892cb908da45ffb0a2b249f
Hongzhou Lin
6892cb908da45ffb0a2b24a0
Yejin Choi
6892cb908da45ffb0a2b24a1
Danqi Chen
6892cb908da45ffb0a2b24a2
Sanjeev Arora
6892cb908da45ffb0a2b24a3
Chi Jin
Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data
  Synthesis and Self-Correction
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, a series of open-source language models, achieves state-of-the-art performance in automated theorem proving through scaffolded data synthesis, verifier-guided self-correction, and model averaging.
scaffolded data synthesis verifier-guided self-correction model averaging automated theorem proving MiniF2F PutnamBench pass@32 pass@184 pass@1024