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
2025-08-06
Summary
This paper talks about Goedel-Prover-V2, a series of open-source AI models designed to prove mathematical theorems automatically with high accuracy using new methods like scaffolded data synthesis, verifier-guided self-correction, and model averaging.
What's the problem?
The problem is that teaching computers to prove complex math theorems is very difficult because the search space for possible proofs is huge and existing methods often get stuck or make errors.
What's the solution?
Goedel-Prover-V2 solves this by creating training data in steps that build on one another (scaffolded data synthesis), letting the model check and fix its own mistakes (verifier-guided self-correction), and combining multiple models to make decisions (model averaging), which together help the system find proofs more efficiently and accurately.
Why it matters?
This matters because automating theorem proving can help mathematicians verify proofs faster, discover new proofs, and support advancements in fields that rely on complex math like computer science and physics.
Abstract
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.