PaperlayerView exact revision on arXiv

Source-linked AI summary

Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving

Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, Chi Jin

arXiv:2502.07640v3cs.LGcs.AI

TL;DR

Formal theorem proving lacks abundant, benchmark-relevant statements and proofs, limiting training data for language-model provers. Goedel-Prover addresses this by autoformalizing Numina problems into Lean and using expert iteration to accumulate verified proofs. Its supervised model reaches 57.6% Pass@32 on miniF2F, solves 7 PutnamBench problems at Pass@512, and releases its resources openly.

  • Problem

    Formal theorem proving faces a scarcity of formalized mathematical statements and proofs, while existing resources can be limited or distribution-shifted from general benchmarks.

  • Method

    The authors autoformalize Numina problems into Lean and use eight rounds of expert iteration to collect verified proofs for supervised fine-tuning.

  • Results

    57.6% Pass@32 on miniF2F surpasses DeepSeek-Prover-V1.5-RL by 7.6%, while Goedel-Prover-SFT solves 7 PutnamBench problems at Pass@512.

  • Takeaways & Limitations

    Expert iteration with large-scale formalized statements can achieve state-of-the-art formal proof generation, with codes, models, datasets, and proofs open-sourced.

  • Takeaways & Limitations

    One initially solved PutnamBench problem was excluded after being identified as mis-formalized, reducing the reported count from 8 to 7.

Abstract

from arXiv · show

We introduce Goedel-Prover, an open-source language model that achieves state-of-the-art (as of April 5 2025) performance in automated formal proof generation for mathematical problems. A key challenge in this field is the scarcity of formalized mathematical statements and proofs, which we address through the following approaches. First, we train LLMs to convert natural language math problems from the Numina dataset to equivalent formal statements in Lean 4. This process creates the dataset Goedel-Pset-v1, which includes 1.64 million formal statements. Next, we develop a large dataset of formal proofs by training a series of provers. Each new prover can prove many statements that previous ones could not, and these new proofs are added to the training set for the next prover. Finally, we obtain the dataset Goedel-Pset-v1-solved, which contains proofs for over 800K statements from Goedel-Pset-v1. Supervised fine-tuning (SFT) of DeepSeek-Prover-V1.5-Base on Goedel-Pset-v1-solved (i.e., no RL) yields a Goedel-Prover-SFT that achieves a success rate of 57.6% (Pass@32) on miniF2F, surpassing the previous leader DeepSeek-Prover-V1.5-RL (trained using SFT + RL on a proprietary dataset) by 7.6%. On PutnamBench, Goedel-Prover-SFT successfully solves 7 problems (Pass@512), ranking first on the leaderboard. We provide extensive discussion of our training methodology, highlighting the key design choices that contribute to Goedel-Prover's strong performance. Further RL training (including DPO) improves Goedel-Prover-SFT's success rate to over 60% (Pass@32) on miniF2F. To aid future research, we provide extensive discussion of our training methodology and design choices. We also fully open-source our codes, models, and datasets. Additionally, we open-source formal proofs for 29.7K problems in Lean Workbook, nearly doubling the 15.7K solved by prior provers.

1 Introduction

Goedel-Prover addresses scarce formal theorem-proving data by autoformalizing informal problems and iteratively generating verified Lean proofs. The resulting open-source system achieves strong results across miniF2F, PutnamBench, and Lean Workbook.

  • Motivation: Formal theorem proving is difficult to scale because publicly available formal statements and proofs remain scarce.Lean Workbook contains 140K formal statements but only 15.7K with proofs, while Mathlib4 has substantial distribution shift from benchmarks such as miniF2F.
  • Data construction: 1.64 million formal statements are created by converting Numina problems into Lean with two diverse formalizers and content-preservation checks.The formalizers are trained on Lean Workbook pairs and Claude-sonnet-3.5 annotations.
  • Proof generation: Eight expert-iteration rounds cumulatively collect verified proofs, with each prover supplying training data for the next.Proof candidates are checked with Lean, and newly solved statements are added for subsequent supervised fine-tuning.
  • Results: 57.6% Pass@32 on miniF2F surpasses DeepSeek-Prover-V1.5-RL’s 50.0% by 7.6%.Goedel-Prover-SFT also remains ahead across the reported sampling budgets.
  • Open resources: 29.7K Lean Workbook problems are solved, compared with 15.7K collectively solved by InternLM2.5-Step-Prover and InternLM-Math-Plus.The authors also open-source their codes, models, datasets, and newly discovered proofs.
  • Results: 7 PutnamBench problems are solved at Pass@512, placing Goedel-Prover-SFT first on the leaderboard.The result is reported for Goedel-Prover-SFT.
  • Further training: Further DPO and RL training raises miniF2F performance above 60% Pass@32, but these models tend to overfit shortcuts and benefit less from added inference compute.The final model discussed in the main result is trained purely through supervised fine-tuning.

2 Related Work

Related work develops automated theorem proving through symbolic search, proof assistants, learning-based methods, whole-proof generation, and autoformalized data. Goedel-Prover builds on expert iteration and diverse Lean formalization of informal problems.

  • Automated theorem proving: Traditional automated theorem provers use first-order logic, decision procedures, search, and machine-learned heuristics, but struggle with complex theorems and human-readable proofs.
  • Learning-based methods: Learning-based theorem proving uses language models with proof assistants and explores lemma retrieval, Monte Carlo tree search, and natural-language reasoning.
  • Evaluation caveat: The PutnamBench count is 7 rather than 8 because one initially solved problem was found to be mis-formalized.
  • Expert iteration: Expert iteration alternates between proving unsolved theorems and adding discovered proofs to the prover’s training data.
  • Whole-proof generation: Whole-proof generation produces complete proofs directly, avoiding costly search and potentially reducing testing latency and computational cost.
  • Autoformalization: Autoformalization translates informal mathematical statements into formal ones to address the shortage of high-quality formal theorem-proving data.
  • Goedel-Prover: Goedel-Prover formalizes Numina and a private dataset, using two formalizers to increase the diversity of formalization styles.

3 Method

The method converts informal mathematics into diverse Lean statements, assesses their quality, and uses expert iteration to build proof data and successive provers.

  • 3.1 Statement Formalization: Informal Numina and AOPS problems are translated into Lean statements using two supervised formalizers trained from different F-I statement sources.Formalizer A uses Lean Workbook pairs, while Formalizer B is trained on 170K Claude-generated statements that passed Lean compilation.
  • 3.2 Expert Iteration: Each iteration uses the current prover to collect new proofs, adds them to training data, and produces the next prover through supervised fine-tuning.The process is repeated for 8 iterations, with consistent improvement observed from the first iteration.
  • 3.1 Statement Formalization: The formalized statements are assessed for Lean compilation and faithfulness to the original problem, including its assumptions, conditions, and implicit definitions.These checks are called Compiling Correctness and Faithfulness and Completeness.
  • 3.2 Expert Iteration: Expert iteration generates 16 proofs per statement, verifies them with Lean, retains successful solutions, and uses them for supervised fine-tuning from DeepSeek-Prover-V1.5-Base.Each iteration trains the next prover on cumulatively collected correct solutions.
  • 3.2 Expert Iteration: Training and verification operate at large scale, covering a 1.78M-statement inference set and requiring 64 H100 GPUs for inference plus 8,000 CPUs for verification.The reported Pass@16 inference takes 6 hours, while proof verification takes 10 hours.

4 Results

The evaluation covers miniF2F, ProofNet, Lean Workbook, PutnamBench, and held-out formalized problems, with performance improving across iterations and benchmarks.

  • Benchmarks: The evaluation uses formal theorem-proving benchmarks spanning high-school, undergraduate, Lean Workbook, PutnamBench, and a held-out formalized dataset.miniF2F contains 488 Lean 4 problems, while ProofNet contains 371 undergraduate-level problems.
  • Iteration Results: Performance improves relatively consistently across expert-iteration rounds as the model is evaluated on four datasets.Figure 4 associates each iteration with a gradually larger problem set and more training data.
  • Main Results: Goedel-Prover-SFT achieves 62.7% Pass@3200 on miniF2F versus DeepSeek-Prover-V1.5-RL’s 54.9%.The model improves over the comparison systems across inference compute budgets.
  • PutnamBench Performance: Goedel-Prover-SFT solves 7 out of 644 PutnamBench problems at Pass@512, achieving first place on the leaderboard.ABEL also solves 7 with Pass@596, while InternLM2.5-Step-Prover solves 6 under its reported budget.
  • Proofs Found in Lean Workbook: The model discovers 29.7K Lean Workbook proofs, compared with 15.7K previously open-sourced proofs.Lean Workbook contains 140K formalized problems.

5 Dissecting the training recipe

The training recipe benefits from scaling formal statements and diversifying formalization styles, while dataset distribution shifts create task-specific trade-offs. Alternative divide-and-conquer synthesis was ineffective, and RL-based methods improved low-budget performance but limited inference-time scaling.

  • Data scale: Scaling up the formal statement set consistently improves average performance across miniF2F, ProofNet, and NuminaTest.The evaluation averages performance across the three datasets for provers trained on different statement-set sizes.
  • Formalization diversity: Mixed formalization styles outperform single-style training, indicating that statements from both formalizers improve performance.The ablation compares iter-8 provers trained on statements from Formalizer A, Formalizer B, or both.
  • Alternative synthesis: The divide-and-conquer synthesis pipeline solves 76 miniF2F validation problems versus 158 for DeepSeek-Prover-V1.5-RL, adding only one uniquely solved problem.The pipeline generated proof sketches with o1-preview and used DeepSeek-Prover-V1.5-RL to prove the resulting subgoals.
  • Dataset correlations: Mathlib4 improves ProofNet performance but reduces performance on miniF2F and NuminaTest, reflecting distribution shift among datasets.Mathlib4 and ProofNet emphasize mathematical-concept manipulation, whereas the other datasets contain more Olympiad-style problems.
  • DPO and RL: RL methods improve miniF2F performance at Pass@32, but their gains are limited at Pass@3200 and can accompany longer proofs and excessive pattern preference.The RL-trained model increasingly favors patterns such as try; length-penalized DPO reduces this overfitting, but inference-time scaling remains less effective than for SFT.

6 Discussion

The discussion examines how formalization choices affect prover effectiveness and how candidate formalizations are filtered for validity and appropriateness. Reasonable-looking formalizations can still produce different proof outcomes.

  • Formalization effects: Reasonable formalizations can yield different prover outcomes, with the final prover solving some statements from one formalizer but not the other.Table 6 gives examples where the successful formalizer changes between problems.
  • Quality filtering: For each Numina problem, the pipeline generates eight formalizations per formalizer, filters them with CC and FC tests, and randomly selects one valid statement from each formalizer.If a formalizer produces no valid statements, the problem is excluded for that formalizer.

B Expert Iteration Details

Expert iteration progressively expands the training data with formalized statements and proofs, while incorporating Mathlib4 later to address ProofNet performance. The appendix also contrasts benchmark distributions and formalization examples.

  • Statement evaluation: The expert-iteration details include prompts for the Faithfulness and Completeness test and a quality assessment of formalized statements.The supplied appendix materials identify these evaluation components without specifying their full contents.
  • Dataset composition: Mathlib4 emphasizes manipulation of advanced mathematical concepts, unlike miniF2F’s competition problems, which require complex reasoning over relatively elementary facts.This distribution difference motivates distinguishing benchmark behavior during training-data design.
  • Formalization examples: The appendix provides examples involving pre-defined objects in Mathlib4 and an example that does not rely on pre-defined objects in miniF2F.These examples illustrate contrasting formalization contexts across the two datasets.

C.2 ProofNet and miniF2F

ProofNet draws primarily from undergraduate pure mathematics textbooks and covers abstract domains whose formulations rely heavily on Mathlib4 definitions.

  • Dataset composition: ProofNet covers real and complex analysis, linear algebra, abstract algebra, and topology from undergraduate pure mathematics textbooks.Its problems rely largely on abstract and general formulations of mathematical definitions in Mathlib4.

D Alternative approach for synthesizing data

The alternative pipeline uses proof sketches to decompose formal problems into subproblems, solves them separately, and assembles the results. Although it solved one additional difficult miniF2F problem, its efficiency was low, while DPO introduced shortcut-like proof patterns.

  • Pipeline: The pipeline prompts o1-preview for step-by-step proof sketches, removes subgoal proofs, and uses Lean to extract subproblems and conditions.DeepSeek-Prover-V1.5-RL then attempts each subproblem 32 times before successful subproofs are assembled into a proof of the original problem.
  • Pipeline: The approach solves the original theorem only when all extracted subproblems are successfully proved and assembled.
  • Results: 1 additional problem was proved among 244 miniF2F validation problems, indicating low efficiency for this alternative pipeline.The additional problem was non-trivial and required relatively complex reasoning.
  • Results: The pipeline’s complexity may reduce efficiency because failure of any subproblem can cause failure of the entire problem.
  • DPO: DPO training can produce repeated uses of the “all goals” and “try” tactics, described as shortcuts that motivate length regularization.

E.2 GRPO training

The GRPO stage trains on challenging but manageable statements, verifies generated proofs through Lean compilation, and explores prompt selection, reward design, and training settings. Training reward can diverge from held-out proof accuracy, which plateaus despite continued reward increases.

  • Training setup: 80K statements with pass ratios in (0, 1/2] are used for GRPO training, with 16 generated proofs per problem verified by compilation.The Goedel-Prover-SFT serves as the base model within OpenRLHF using GRPO.
  • Training settings: The KL penalty has little effect on training; 0.003 is selected, batch size 256 is used, and one training epoch is retained because more epochs do not improve final accuracy.Batch size 128 produced very similar performance, while tested KL penalties were 0.03, 0.003, 0.00003, and 0.
  • Reward and accuracy: Reward and evaluation diverge: average training reward keeps increasing, while Pass@16 accuracy plateaus after approximately 20 training steps.The passage attributes this discrepancy possibly to misalignment between the optimization objective and evaluation metric.
  • Prompt selection: Prompt difficulty matters: the selected (0, 1/2] range is described as challenging yet manageable, and alternative pass-ratio ranges are compared.The experiments include (0, 1/4], (0, 3/4], and (0, 1].
  • Reward design: Correctly compiling proofs receive +8 and failed proofs receive -8, while timeout cases are investigated with alternative reward assignments.Table 11 reports the timeout-reward investigation under fixed rewards for successful and failed compilation.

F Discussion

The discussion examines Goedel-Prover-SFT’s high-level proof style, its one-shot generation process, and possible extensions using interactive search and symbolic computation. High-level tactics compress intermediate reasoning, while SymPy helps only a small subset of otherwise unsolved problems and is excluded from reported results.

  • The Proof Style: Goedel-Prover-SFT often uses high-level tactics such as nlinarith and simp, which internally handle multiple reasoning steps.Figure 13 illustrates proofs in which intermediate steps are absorbed into high-level tactics.
  • Search and online interaction: The prover currently generates an entire proof without feedback, whereas compiler interaction could expose goal changes after each tactic for subsequent search.The discussion presents search and online interaction as potential future improvements.
  • SymPy: SymPy can address some advanced simplifications that require combinations of Lean tactics, including transformations involving logarithmic and trigonometric functions.The passage contrasts these capabilities with Lean’s ring tactic for algebraic simplification.
  • SymPy: SymPy solves 0.8% of miniF2F problems left unsolved by Goedel-Prover-SFT at Pass@32, but does not improve Pass@3200 results.Consequently, SymPy simplification is excluded from the reported results despite being identified for further exploration.
Loading 2502.07640v3…