Source-linked AI summary
STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
Kefan Dong, Tengyu Ma
TL;DR
LLM theorem proving lacks abundant high-quality training data, and expert iteration can plateau because correct proofs are sparse. STP has a conjecturer generate adaptive related statements for a prover to solve, with both roles supplying training signals. It reaches 28.5% on LeanWorkbook and state-of-the-art whole-proof results on several benchmarks.
Problem
High-quality training data for LLM reasoning is scarce, and expert iteration becomes less effective when correct proofs are rare.
Method
STP jointly uses a conjecturer to generate related conjectures and a prover to prove them, training the conjecturer on statements barely provable by the current prover.
Results
28.5% of LeanWorkbook statements were proved, compared with 13.2% for expert iteration, while STP achieved state-of-the-art whole-proof results on miniF2F-test, ProofNet-test, and PutnamBench.
Takeaways & Limitations
STP extends training beyond the original dataset through mutually training conjecturing and proving roles and improves performance across common formal-proof benchmarks.
Takeaways & Limitations
RL or expert iteration cannot train indefinitely without continuously collecting more theorem statements or math problems, and LeanWorkbook contains unprovable formal statements.
Abstract
from arXiv · showhide
A fundamental challenge in formal theorem proving by LLMs is the lack of high-quality training data. Although reinforcement learning or expert iteration partially mitigates this issue by alternating between LLM generating proofs and finetuning them on correctly generated ones, performance quickly plateaus due to the scarcity of correct proofs (sparse rewards). To keep improving the models with limited data, we draw inspiration from mathematicians, who continuously develop new results, partly by proposing novel conjectures or exercises (which are often variants of known results) and attempting to solve them. We design the Self-play Theorem Prover (STP) that simultaneously takes on two roles, conjecturer and prover, each providing training signals to the other. The conjecturer is trained iteratively on previously generated conjectures that are barely provable by the current prover, which incentivizes it to generate increasingly challenging conjectures over time. The prover attempts to prove the conjectures with standard expert iteration. We evaluate STP with both Lean and Isabelle formal versifiers. With 51.3 billion tokens generated during the training in Lean, STP proves 28.5% of the statements in the LeanWorkbook dataset, doubling the previous best result of 13.2% achieved through expert iteration. The final model achieves state-of-the-art performance among whole-proof generation methods on miniF2F-test (65.0%, pass@3200), Proofnet-test (23.9%, pass@3200) and PutnamBench (8/644, pass@3200). We release our code, model, and dataset in this URL: https://github.com/kfdong/STP.
1 Introduction
LLM theorem proving is constrained by scarce high-quality training data and the sparse rewards of expert iteration. STP addresses this by generating and proving adaptive conjectures, improving performance across formal-proof benchmarks.
- High-quality reasoning data is expensive to collect, while advanced mathematical theorems are orders of magnitude scarcer than other data sources.
- 98.5% of compute in one proof-sampling process yielded no successful proofs, limiting the training signal available to expert iteration.
- STP jointly trains a conjecturer that generates related statements and a prover that attempts to prove them, allowing both roles to provide training signals.
- STP trains the conjecturer on correct, elegant, challenging conjectures that are barely provable by the current prover, gradually increasing conjecture difficulty.
- 28.5% of LeanWorkbook statements were proved after roughly 241M generated proofs and 3.6M conjectures, compared with 13.2% for expert iteration.
- STP achieved 65.0% pass@3200 on miniF2F-test, 23.9% on ProofNet-test, and 8/644 on PutnamBench among whole-proof generation methods.
2 Additional Related Works
Related work includes autoformalization, synthetic formal conjecture generation, self-play theorem proving, and automatic task generation in other domains. STP is positioned as a practical self-play approach for Lean and Isabelle.
- Autoformalization creates formal proof data by translating natural-language mathematical statements or proofs into formal language.
- Prior formal-conjecturing work generates synthetic statements with neural networks or human-written generators, which can support prover training.
- Poesia et al. proposed related self-play training, whereas STP starts from a pretrained model and targets Lean and Isabelle with an infinite space of proof-step actions.
- Model-generated tasks have also been explored in alignment, programming puzzles, video games, and classic reinforcement-learning environments.
3 Method
STP combines supervised initialization, self-play between a conjecturer and prover, and final retraining to generate training signals from increasingly challenging conjectures and proofs.
- STP uses three stages: supervised model initialization, self-play training, and final retraining.
- 3.1 Model initialization by supervised finetuning: The prover SFT dataset teaches formal proof generation from statement-proof pairs extracted from existing proof libraries.Training loss is computed on the proof output, while the prompt and statement serve as inputs.
- 3.1 Model initialization by supervised finetuning: The conjecturer receives a seed theorem, its proof, and an extracted lemma, then generates a related conjecture.The lemma guides generation toward conjectures related to the seed theorem.
- 3.2 Self-play training: During self-play, the prover attempts generated conjectures and dataset statements, while verified proofs train the prover and selected conjectures train the conjecturer.The verifier supplies correctness signals for both roles.
- 3.2 Self-play training: An elegancy filter removes conjectures with unusually short minimum proofs relative to conjecture length, while Wasserstein-based reweighting preserves diversity across topics.The filter removes the lowest 20% by the minimum-proof-length-to-conjecture-length ratio; reweighting matches selected conjectures toward unproved statements.
- 3.2 Self-play training: The prover retains correct generated proofs with statement or conjecture pass rates below 1/2, deduplicates them, and trains on a three-iteration replay buffer.Proof training also uses reciprocal weighting, length discounting, and, for Lean, a faster-verification reward.
- 3.2 Self-play training: Final retraining starts from the pre-SFT base model and combines the SFT data with correct self-play proofs whose empirical pass rates are at most 1/4.At most 16 distinct proofs are retained per statement or conjecture.
4 Experiments
STP is evaluated across Lean and Isabelle with multiple baselines, datasets, and inference settings. The experiments show improved scaling, downstream generalization, and stronger benchmark performance, while also identifying dataset and verifier constraints.
- Implementation details: STP training uses LeanWorkbook as a primary statement source, with additional validation datasets for Lean and Isabelle translations of Lean4 statements.LeanWorkbook contains around 89K Lean4 statements; Lean combines it with miniF2F-valid and ProofNet-valid, while Isabelle uses translated statements.
- Implementation details: STP includes periodic refreshing from the base model to reduce forgetting of proof skills during long self-play training.The replay buffer is reset after retraining on all previously generated correct proofs.
- Implementation details: The Isabelle setup disables several advanced tactics and imposes proof-step and whole-proof timeouts to support more training iterations under limited compute.The disabled tactics include sledgehammer, mason, smt, metis, and sos; timeouts are 10s per step and 360s per proof.
- Lean results: 28.5% of LeanWorkbook statements are proved after 241M generated proofs and 3.6M generated conjectures, compared with 13.2% for prior expert iteration.The Lean run generates 51.3B tokens across 48 STP iterations.
- Lean results: STP achieves state-of-the-art performance among whole-proof generation methods across miniF2F and ProofNet inference-time sample budgets.Tree-search sample budgets are not fully comparable because those methods also process verifier proof states.
- Lean results: 8 out of 644 PutnamBench problems are solved with 3200 samples, surpassing the prior best result of 6 problems.With 128 samples per problem, STP solves 7 out of 644 problems.
5 Conclusion
STP combines conjecturing and proving so the two roles provide training signals to each other, extending training beyond the original dataset and improving performance.
- STP simultaneously assigns the model two roles, conjecturer and prover, whose training signals support each other.
- The approach goes beyond statements in the given dataset and its performance continuously improves.
- The final model significantly outperforms the DeepSeek-Prover-V1.5 series and achieves state-of-the-art performance among whole-proof generation methods on common formal proof benchmarks.
A Additional Implementation Details
The implementation details illustrate STP's Lean input-output formats for theorem proving and conjecturing, together with procedures for constructing diverse conjecturer prompts.
- The appendix provides concrete input and output formats for the model, including Lean theorem-proving examples.
- Conjecturer examples use formatting tokens such as <lemma>, <easy theorem>, and <hard theorem> to structure seed statements, proofs, and generated conjectures.
- Prover examples show Lean statements paired with generated proof code using arithmetic, modular reasoning, and nonnegativity lemmas.
- Conjecturer prompts are built from correct theorem-proof pairs by extracting used lemmas, optionally adding a trivial lemma, and creating statement-proof-lemma entries.
- Prompt diversity is encouraged by limiting each lemma to at most 0.1n occurrences and allowing each statement-lemma pair only once.
A.3 Pseudo-code for preparing the conjecturer dataset.
The conjecturer dataset is prepared by filtering generated conjectures for low but positive prover success, proof validity, lemma usage, and an elegancy threshold, then re-weighting the retained examples.
- The preparation input contains seed statements, seed proofs, lemmas, generated conjectures, generated proofs, and unproved statements.
- Examples are selected when conjectures have low but positive empirical pass rates, their generated proofs are correct, and the designated lemma is used.
- Duplicate conjectures are removed before computing each conjecture's elegancy score from the shortest correct proof length relative to conjecture length.
- An elegancy filter retains conjectures whose score is at least the 20%-quantile threshold κ.
- The retained dataset is re-weighted using a distribution that minimizes Wasserstein distance to the unproved statements.
- LeanWorkbook supplies 89,221 deduplicated formal Lean4 statements after reducing an original 140K natural-language/formal-statement collection.
A.5 Re-weighting the conjecturing dataset
STP re-weights generated conjectures to match the distribution of unproved statements, using embedding-based distances and Wasserstein optimization while limiting excessive weights for stability.
- The re-weighting method addresses mode collapse, where conjectures increasingly concentrate on algebraic manipulation because LeanWorkbook contains many inequality questions.
- Wasserstein projection is intended to align conjecture and unproved-statement topic distributions when a distance function separates topics.
- Matching cost is the negative cosine similarity between statement embeddings from the current model's averaged final hidden layer.
- The theoretical algorithm assigns each unproved statement to its nearest generated conjecture and accumulates the resulting weights.
- The practical implementation caps individual conjecture weights to avoid instability and permits different matching weights for important unproved statements.
A.6 Implementation details for expert iteration.
The appendix compares vanilla and optimized expert iteration with STP and parallel sampling, and describes Isabelle-specific verification constraints. Optimized expert iteration addresses limited proof diversity, while STP achieves the strongest cumulative pass-rate result among the compared methods.
- Expert iteration variants: Vanilla expert iteration samples proofs only for unproved dataset statements and retrains from the base model using accumulated correct proofs.
- Expert iteration variants: The limited number of newly generated correct proofs makes consecutive vanilla expert-iteration models differ only slightly.
- Comparisons: Figure 5 compares LeanWorkbook pass rates across STP, expert iteration, and parallel sampling, and compares Isabelle-translation pass rates between STP and baselines.Red crosses mark self-play training refresh points.
- Expert iteration variants: Optimized expert iteration generates proofs for all dataset statements and retains at most 16 proofs per statement for training.This requires slightly more sampling, but the low dataset pass rate makes the budget difference insignificant.
- Comparisons: STP outperforms both expert-iteration implementations and parallel sampling on LeanWorkbook cumulative pass rate, while optimized expert iteration exceeds vanilla expert iteration.
- Isabelle verification: Isabelle experiments reject conjectures equivalent to the prompt and invalidate proofs containing specified automated tactics, while allowing selected replacements for the keyword “sledgehammer.”Verification tries the replacement tactics sequentially and rejects the proof if none succeeds.
A.9 Compute resources
The experiments run primarily on TPU-v4 infrastructure using vLLM for generation and Levanter for training. Heavy proof filtering means LLM training consumes less than 25% of TPU compute wall-clock time.
- Hardware and software: Experiments primarily use TPU-v4 VMs with 32 nodes, each containing 4 TPU chips, 8 TPU cores, 240 CPU cores, and 400G memory.
- Hardware and software: The pipeline uses vLLM to generate LLM outputs and Levanter to train the LLM.
- Compute profile: Less than 25% of TPU-compute wall-clock time is spent on LLM training because generated proofs are heavily filtered before dataset construction.
- Evaluation: The appendix presents additional experiment results using both Lean and Isabelle formal verifiers.
B.1 Additional results with Lean
Additional Lean results show state-of-the-art PutnamBench performance and indicate that retraining on generated-conjecture proofs improves miniF2F and ProofNet performance.
- PutnamBench: 8 out of 644 PutnamBench problems are solved by STP, achieving state-of-the-art performance.
- Ablation: Retraining with generated-conjecture proofs in addition to successfully proved dataset statements improves miniF2F-test and ProofNet-test performance.The reported gain is about 2–3% at pass@128.
- Ablation: Table 2 reports pass rates on miniF2F and ProofNet.
B.2 Additional results with Isabelle
The Isabelle appendix documents PutnamBench evaluation and lists sampled LeanWorkbook statements that STP did not prove, including examples of unclear translations and false formalizations.
- Evaluation: PutnamBench evaluation is associated with the models’ commit d49896f, and Table 3 reports the benchmark results.
- Unproved statements: The appendix lists 20 randomly selected LeanWorkbook statements that were not proved during STP training, alongside formal and natural-language versions and correctness assessments.
- Formalization issues: One sampled theorem is marked incorrect because its Lean statement contains an xy term where the intended expression should use x * y.
- Unproved statements: Several sampled statements illustrate mathematical claims involving inequalities, sums, functional equations, matrices, and systems of equations.
- Formalization issues: The appendix flags unclear natural-language statements and formalization issues, including an incorrect complex-matrix claim and an inequality whose stated upper bound fails as variables approach zero.
- Unproved statements: Other sampled statements include geometric-mean inequalities, factorial bounds, and function identities, with some accompanying natural-language formulations.