Goedel-Prover-V2: Scaling Formal Theorem Proving
Reading
About this week
How does pairing scaffolded data synthesis with verifier-guided self-correction overcome data scarcity in formal theorem proving? Can structured compiler feedback and subproblem generation outperform sheer parameter scaling in complex mathematical reasoning?
Goedel-Prover-V2 addresses data scarcity and output homogenization in Lean 4 formal reasoning through three key innovations: scaffolded data synthesis, verifier-guided self-correction, and weight averaging. Rather than relying on brute-force scaling, it extracts unsolved subgoals from failed proofs to build a progressive synthetic curriculum, while using real-time Lean compiler feedback to iteratively repair incorrect proof steps.
Empirically, this framework delivers exceptional sample efficiency. The compact 8B model achieves an 84.6% pass@32 on MiniF2F—matching the 80× larger DeepSeek-Prover-V2-671B—while the 32B model sets a new state-of-the-art with 90.4% on MiniF2F and leads PutnamBench with 86 solved problems. The work reframes formal automated reasoning from a parameter-scaling challenge into an interactive, verifier-guided data problem.
Join us at CASI for discussion at 8 pm, and (optional) quiet reading from 7 pm.