Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction
Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, Jiayun Wu, Jiri Gesi, Ximing Lu, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, Chi Jin
cs.LG
Aug 5, 2025 · v1
TL;DR
Trains open-source theorem-proving LLMs using Lean compiler feedback for self-correction, evaluated on MiniF2F and PutnamBench.
Abstract
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.
Problem
Automated theorem proving in Lean remains challenging, with existing open-source models limited in their ability to handle difficult benchmarks like MiniF2F and PutnamBench at high accuracy rates.
Approach
Goedel-Prover-V2 uses the expert iteration and reinforcement learning pipeline with three innovations: scaffolded data synthesis that generates synthetic tasks of increasing difficulty, verifier-guided self-correction using Lean compiler feedback for iterative proof revision, and model averaging by merging checkpoints to mitigate decreased output diversity in later training stages.
Results
Goedel-Prover-V2-8B reaches 84.6% pass@32 on MiniF2F, outperforming DeepSeek-Prover-V2-671B despite being 80x smaller. The 32B flagship model achieves 88.1% on MiniF2F at pass@32 (90.4% with self-correction) and solves 86 problems on PutnamBench at pass@184, surpassing DeepSeek-Prover-V2-671B's 47 problems at pass@1024.
