MLn Club (ML Reading Group) #18: Goedel-Prover-V2: Scaling Formal Theorem Proving
Welcome to Week 18: Goedel-Prover-V2: Scaling Formal Theorem Proving
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?
The Paper Link Here
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.
📖 Reading Recommendations, Questions, or Comments? Contact us here!
🔎 View past meeting notes here.
What's this?
A super warm group of folks discussing their favorite topics!
In the first half, we host an optional quiet reading space
In the second half, we have a discussion where people can talk about what they found interesting about the reading and ask questions about things they didn't understand
When/Where:
CMU AI Safety Initiative's Office, 201 Craig Street, right across the PNC bank. Look for the open door up the stairs.
8pm discussion, 7pm optional quiet reading time.
Here's how it usually goes:
7:00 PM — arrival and settling in
8:00 PM — introductions
8:10 PM — discussion time
9:00 PM — wrap up then open discussion
Who's it for?
People who've been wanting to read up on the latest papers in ML and other fields but just haven't been able to find the time/motivation.
Why:
We've been procrastinating too much on our readings, even though we have so much fun doing them. We know we're not alone in this and want to keep others accountable for learning more about what they're passionate about!
We've also met a ton of really fun friends by discussing what we care about!
Rules/guidelines on how to act:
Act like a host, include people in conversations, talk to people even if they're strangers, offer to explain what you know, and keep an open mind! come to read stuff and find super fun friends :)
Bring snacks if you're feeling kind!