Paper Link👁️

Goedel-Prover: Pushing the Limits of Automated Theorem Proving Through Large-Scale Data Synthesis

1. Introduction

Large language models (LLMs) have demonstrated remarkable reasoning capabilities, particularly in solving mathematical problems. There are two main approaches to tackling math problems: the informal approach, which involves reasoning in natural language, and the formal approach, which relies on proof assistants such as Lean and Isabelle that use formal and machine checkable mathematical languages. State-of-the-art reasoning LLMs such as OpenAI o1 and Deepseek R1 excel at informal math but not at formal math. While the informal approach is more intuitive to humans, it also poses significant challenges in proof verification, undermining its reliability in practical applications.

We introduce Goedel-Prover, a state-of-the-art (SOTA) open-source model for formal mathematics that generates machine-verifiable proofs. On the miniF2F benchmark at Pass@32, our model achieves a 57.6% success rate, surpassing the previous SOTA open-source model for whole-proof generation by a significant 7.6% margin. On the challenging PutnamBench, our model successfully solves 7 problems at Pass@512, securing 1st place on the leaderboard. Additionally, we have cumulatively generated 29.7K formal proofs for problems in the Lean Workbook, a substantial increase over the 15.7K proofs produced by prior methods. A key challenge in formal mathematics is data scarcity. To address this, we train LLMs to auto-formalize a large corpus of mathematical problems, converting natural language descriptions into formal statements. We then train a prover through an iterative process, alternating between generating proofs for these formalized statements and refining the model using the newly discovered proofs. Our project contributes to the open-source community for advancing research in formal theorem proving, and developing more capable mathematical reasoning systems.

Caption: The Pass@N metric indicates that we generate N proofs for a single problem; if any one of these N proofs successfully solves the problem, it is considered solved. (Left): The performance of Pass@32 for full proof generation on miniF2F. Due to limited compute, we compare with DeepSeek-Prover-v1.5 on the Pass@32 metric. (Middle): This sub-figure presents a comparison of Goedel-Prover-SFT and Deepseek-Prover-v1.5 in terms of miniF2F performance across different inference budgets, ranging from Pass@32, 64, 128, ..., 4 * 6400, to 16 * 6400. The performance numbers of Deepseek-Prover-v1.5 are directly taken from Table 1 of Xin et al. (2024b). Due to computational resource constraints, we tested Goedel-Prover-SFT only up to Pass@4 × 6400. Notably, Goedel-Prover-SFT's Pass@256 already exceeds the Pass@16 * 6400 performance of Deepseek-Prover-v1.5-RL (without inference time tree search). (Right): The number of problems solved in Lean-workbook by Goedel-Prover-SFT compared to prior works. InternLM2.5-Step-Prover and InternLM-Math-Plus collectively solve and open-source 15.7K samples, while we solve and open-source 29.7K samples.

2. Evaluation Results

Model	Compute (Pass)	miniF2F-test
TheoremLamma	128	33.6%
DeepSeek-Prover-V1	32	46.1%
DeepSeek-Prover-V1.5-SFT	32	48.2%
DeepSeek-Prover-V1.5-RL	32	50.0%
Goedel-Prover-SFT	32	57.6%
------------------------	------------------	------------------
DeepSeek-Prover-V1.5-SFT	3200	53.3%
DeepSeek-Prover-V1.5-RL	3200	54.9%
Goedel-Prover-SFT	3200	62.7%
------------------------	------------------	------------------
DeepSeek-Prover-V1.5-SFT	25600	55.8%
DeepSeek-Prover-V1.5-RL	25600	58.5%
Goedel-Prover-SFT	25600	64.7%

Caption: Comparison of Goedel-Prover-SFT with existing methods for whole proof generation on miniF2F, assessing performance across various inference time computations.

MultiDataset

	miniF2F	ProofNet	FormalNumina	Lean-workbook
Deepseek-Prover-v1.5-RL	50.0%	16.0%	54.0%	14.7%
Goedel-Prover-SFT	57.6%	15.2%	61.2%	21.2%

Caption: Comparison of Goedel-Prover-SFT with Deepseek-Prover-v1.5-RL for whole proof generation on miniF2F, ProofNet,FormalNumina,Lean-workbook. We report the Pass@32 performance for miniF2F, ProofNet, and FormalNumina datasets. For the Lean-workbook, we evaluate performance using Pass@16 due to the large number of problems (140K) it contains, allowing us to save on computational costs. FormalNumina is a private test set created by formalizing a randomly sampled collection of 250 problems from Numina.

Putnam

Ranking	Model	Type	Num-solved	Compute
1	Goedel-Prover-SFT 🟩	Whole Proof Generation	7	512
1	ABEL	Tree Search Method	7	596
3	Goedel-Prover-SFT 🟩	Whole Proof Generation	6	32
3	InternLM2.5-StepProver 🟩	Tree Search Method	6	2×32×600
5	InternLM 7B	Whole Proof Generation	4	4096
6	GPT-4o	Whole Proof Generation	1	10
7	COPRA (GPT-4o) 🟩	Whole Proof Generation	1	1
8	ReProver w/ retrieval 🟩	Whole Proof Generation	0	1
9	ReProver w/o retrieval 🟩	Whole Proof Generation	0	1

Caption: Our model rank the 1st on Putnam Leaderboard. The performance numbers for existing works are taken from the leaderboard. 🟩 indicates open sourced models.

3. Dataset Downloads

We are also releasing 29,7K proofs of the problems in Lean-workbook found by our Goedel-Prover-SFT.

Datasets	Download
Lean-workbook-proofs	🤗 HuggingFace

4. Citation

@article{lin2024Goedelprover,
      title={Goedel-Prover: Pushing the Limit of Automated Theorem Proving Through Large Scale Data Synthesizing}, 
      author={Yong Lin and Shange Tang and Bohan Lyu and Jiayun Wu and Hongzhou Lin and Kaiyu Yang and Jia Li and Mengzhou Xia and Danqi Chen and Sanjeev Arora and Chi Jin},
}