PaperlayerView exact revision on arXiv

Source-linked AI summary

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

arXiv:2508.03613v1cs.LGcs.AI

TL;DR

Automated theorem proving must produce rigorous, machine-verifiable Lean proofs, yet prior systems often rely on massive models or costly inference. Goedel-Prover-V2 combines verifier-guided self-correction, scaffolded data synthesis, and model averaging with expert iteration and reinforcement learning, achieving leading open-source performance at smaller scale and lower inference cost.

  • Problem

    Automated theorem proving requires rigorous Lean proofs, while prior systems often depend on massive models or computationally intensive inference.

  • Method

    Goedel-Prover-V2 combines verifier-guided self-correction, scaffolded data synthesis, model averaging, expert iteration, and reinforcement learning.

  • Results

    Goedel-Prover-V2 achieves state-of-the-art open-source performance across benchmarks, including 88.1% MiniF2F pass@32 for 32B and 86 PutnamBench problems at pass@184.

  • Takeaways & Limitations

    The results indicate that strong formal theorem proving can be advanced without extremely large models, vast computational resources, or proprietary technology.

  • Takeaways & Limitations

    Seed Prover solved 331 PutnamBench problems, but it is not open-source and its test-time computational budget is unclear.

Abstract

from arXiv · show

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.

1 INTRODUCTION

Goedel-Prover-V2 targets the challenge of rigorous, machine-verifiable theorem proving while reducing dependence on massive models and costly inference. It combines verifier-guided self-correction, scaffolded data synthesis, and model averaging, achieving strong performance and efficiency across benchmarks.

  • Automated theorem proving requires step-by-step, machine-verifiable proofs in formal languages such as Lean.
  • Prior systems often depend on massive models or computationally intensive inference with complex search and enormous budgets.
  • 88.1% pass@32 on MiniF2F is achieved by the 32B model, rising to 90.4% with self-correction and surpassing larger prior systems.
  • Goedel-Prover-V2 combines verifier-guided self-correction, scaffolded data synthesis, and model averaging across its framework, data, and training pipelines.
  • The authors aim for the open-source release to support community progress toward reliable formal proof verification.

2 METHOD

The method builds high-quality Lean statement data and trains whole-proof generators with verifier feedback, scaffolded synthesis, expert iteration, reinforcement learning, and model averaging. Its pipeline combines formal and informal data curation with parallel proof sampling and serial self-correction.

  • 2 METHOD: The training workflow combines verifier-guided proof correction, scaffolded statement synthesis, supervised fine-tuning, reinforcement learning, and model averaging.
  • Verifier-guided self-correction: Verifier-guided self-correction parses Lean verification failures and feeds corrective guidance back to the model for iterative proof repair.
  • Statement curation: Formalizer training filters statements using Lean syntax checks and LLM-based semantic evaluation, retaining only statements that pass both checks.
  • Scaffolded data synthesis: Scaffolded synthesis creates appropriately difficult related problems through extracted Lean subgoals and LLM-generated simpler, harder, or sub-problems.
  • Reinforcement learning: The RL strategy samples complete proofs in parallel and performs serial self-correction for each proof, using separate inputs for generation and first-round correction.
  • Model averaging: Model averaging addresses reduced output diversity in later SFT and RL stages, where pass@1 rises while pass@N can decline.

3 EVALUATION

Goedel-Prover-V2 is evaluated across MiniF2F, PutnamBench, and the newly constructed MathOlympiadBench, with standard generation, self-correction, scaling, and training-strategy analyses. The models show strong performance at modest sampling budgets, while self-correction and model averaging improve selected outcomes.

  • Evaluation setup: Goedel-Prover-V2 is evaluated on MiniF2F, PutnamBench, and MathOlympiadBench under Lean 4.9.0-rc1 using pass@N.The evaluation includes standard whole-proof generation, verifier-guided correction, scaling across inference budgets, and analyses of reinforcement learning and model averaging.
  • Main results: 86 PutnamBench problems are solved by Goedel-Prover-V2-32B under pass@184 with error correction, 39 more than the previous open-source state of the art.The result secures the best open-source theorem prover position on the leaderboard.
  • Scaling analysis: 88.1% pass@32 on MiniF2F is reached by Goedel-Prover-V2-32B at a lower sampling regime, surpassing DeepSeek-Prover-V2-671B’s 82.4% and Kimina-Prover-72B’s 84.0%.The advantage persists across inference budgets, while self-correction adds approximately two percentage points under pass@32 and pass@64.
  • Self-correction analysis: 92.7% average pass@32 on MiniF2F is achieved with extended context and more revision iterations, surpassing the model’s 92.2% without self-correction at pass@8192.Removing compiler feedback significantly lowers performance, and removing prior reasoning slightly degrades it.
  • RL and model averaging: Pass@1 consistently increases with more reinforcement-learning steps, while correction pass@N continues improving where vanilla pass@N stabilizes.Across both settings, pass@N first rises and then falls as the model-averaging coefficient α increases, indicating an optimal averaging ratio.

4 RELATED WORKS

Formal theorem proving has progressed from whole-proof generation and verifier-guided refinement toward Goedel-Prover-V2’s iterative self-revision framework for long chain-of-thought proofs.

  • Formal Theorem Proving: Whole-proof generation produces complete Lean proofs in one pass, while proof-search methods incrementally explore derivation paths with verifier feedback.
  • Proof Search: Tree-based proof search improves correctness but incurs high computational cost, motivating more efficient self-refinement mechanisms.
  • Self-Repair and Verifier-Guided Refinement: Verifier-in-the-loop strategies improve success rates through iterative correction rather than brute-force search.
  • Goedel-Prover-V2: Goedel-Prover-V2 iteratively proposes and refines candidate proofs until they satisfy the Lean checker, combining self-revision with long chain-of-thought reasoning.

5 CONCLUSION AND DISCUSSION

Goedel-Prover-V2 combines long-chain-of-thought reasoning, compiler-guided self-correction, scaffolded data synthesis, training, and model averaging to advance open-source formal proof generation.

  • Conclusion: 88.1% on MiniF2F at pass@32 rises to 90.4% with self-correction for the 32B model, outperforming larger models at lower inference cost.
  • Test-Time Proof Repair: 1–2 percentage points improve the MiniF2F amortized budget scaling curve when faulty proof segments are repaired instead of regenerating entire failed proofs.Lean 4 compiler feedback and the extract goal tactic isolate an unsolved subgoal for independent repair and reinsertion.
  • Open-Source Impact: Open-sourcing the trained models is intended to catalyze further advances and provide a practical, efficient platform for formal reasoning research.

A DETAILS OF MATHOLYMPIADBENCH

MathOlympiadBench provides human-verified Olympiad formalizations and exposes mismatches in MiniF2F where formal statements can be weaker than, or inconsistent with, their informal problems.

  • Benchmark Construction: MathOlympiadBench preprocessing removes incomplete statements, multi-file distributions, multiple theorems per problem, and Mathlib incompatibilities.Verification ensures each problem has exactly one formal theorem with its informal statement and that formal statements compile with sorry.
  • Formalization Quality: At least 3 shared IMO cases reveal MiniF2F formalizations that are weaker than or do not match their informal statements, issues not observed in MathOlympiadBench.
  • Formalization Quality: MiniF2F asks for a general recurrence in one case, whereas the informal problem requires computing the specific value f(4, 1981), making the formal proof substantially easier.MathOlympiadBench instead formalizes the final numerical-value requirement.

A.2 IMO 1983, PROBLEM 6: INCOMPLETE VS. FULL CONDITION

The case studies identify incomplete and mismatched MiniF2F formalizations: one omits an equality condition, while another encodes a different inequality version than its informal statement.

  • IMO 1983, Problem 6: The omitted equality condition means MiniF2F does not represent the full two-part requirement of the informal problem.
  • IMO 1983, Problem 6: The IMO 1983 problem asks for both an inequality proof and the equality condition, but MiniF2F formalizes only the inequality.MathOlympiadBench provides a complete formalization.
  • IMO 1962, Problem 2: The IMO 1962 problem appears in two inequality versions, but MiniF2F pairs the nested-square-root informal statement with a simpler difference-of-square-roots formal statement.
  • IMO 1962, Problem 2: MathOlympiadBench keeps the informal and formal statements consistent for the selected version of the IMO 1962 problem.

C DETAILS FOR JUDGING FORMALIZATION

The section evaluates whether Lean formalizations preserve a problem’s essential mathematical content, assumptions, goals, and original structure. Examples show that faithful translations retain the intended reasoning, while flawed ones can replace construction with verification or omit conditions.

  • The judging criteria are key-element coverage, mathematical accuracy, structural fidelity, and comprehensiveness of assumptions, conditions, and goals.
  • Appropriate translations preserve the original problem’s assumptions, goals, mathematical content, and reasoning structure.The quadratic example preserves the vertex, symmetry, intercepts, and proof logic; another example accurately captures assumptions and the goal.
  • Inappropriate translations can change a construction task into verification by assuming the desired equation instead of deriving it.The tangent-line example omits subtracting circle equations, which is central to deriving the line equation.
  • Ignoring original assumptions can make a formal statement inappropriate even when its displayed conclusion resembles the source problem.One inequality translation omits the condition a, b, c, d > 0.

D DETAILS FOR INFORMAL-BASED SCAFFOLDED DATA SYNTHESIS

Informal-based scaffolded synthesis uses language models to generate proof problems at varied difficulty levels, then filters and formalizes them for training. The pipeline combines harder variants with simpler subproblems tied to core solution steps.

  • Simpler problems are designed as standalone, proof-based exercises reflecting core steps in the original solution.They are intended to help students build the skills needed for the original problem.
  • The synthesis process checks that problems are self-contained, diverse, nontrivial, and require meaningful proofs.It also excludes undefined dependencies and trivial calculations or straightforward derivations.
  • Generated problems must be self-contained, mathematically valid, solvable, proof-based, and meaningfully different from the original.The prompts explicitly reject requests to compute, evaluate, or find answers instead of prove statements.
  • For efficiency, Qwen3-32B generates multiple hard questions in one inference because repeated single-problem generation produced fewer distinct problems.The authors observed that same-inference questions were likely to differ from one another.

E RL TRAINING DETAILS

The paper describes its reinforcement-learning training setup as a separate detailed component of the overall theorem-proving pipeline.

  • The authors introduce a dedicated section to explain their reinforcement-learning training in detail.
  • The reinforcement-learning training details follow the paper’s broader data-synthesis and formalization methods.
  • This passage signals that the section provides methodological detail rather than reporting a benchmark result.

E.1 RL IMPLEMENTATION

The RL implementation jointly trains whole-proof generation and first-round self-correction with a hybrid GRPO-based method. Training uses bounded response lengths, overlong penalties, and dynamic sampling while tracking rewards across tasks.

  • The multi-task RL pipeline improves performance on whole-proof and self-correction tasks simultaneously without additional framework or algorithm design.
  • Training collects 50K challenging statements and 50K self-correction samples, each containing a statement, an SFT output, and an error message.The 8B and 32B runs consumed approximately 46K and 64K unique inputs on one epoch, respectively.
  • The maximum response length is 24K tokens, with a 4K overlong buffer and penalty factor 1; the objective uses token-averaged policy loss without KL or entropy terms.
  • Figure 10 compares 32B and 8B training rewards and generation lengths for whole-proof and self-correction tasks.Rewards average all generated rollouts, including those later filtered by dynamic sampling.

E.2 FURTHER DISCUSSION ON RL

The authors compare tool-use and multi-turn reinforcement learning for self-correction, highlighting substantial capability and engineering challenges, particularly for small models working with complex Lean language.

  • The study explores both tool-use and multi-turn reinforcement learning for training with self-correction.
  • Tool-use requires dedicated tool-calling design and strong protocol-following ability, especially for complex and lengthy Lean scenarios.These requirements are particularly challenging for the relatively small model.
  • Multi-turn approaches introduce engineering challenges, especially during rollout.
Loading 2508.03613v1…