Seed-Prover 1.5 Mastering Undergraduate-Level Theorem Proving via Learning from Experience
Documentation of the training methodologies and experimental scaling results of the Seed-Prover 1.5 formal theorem proving model.
Read Paper →Method
The system consists of a formal theorem proving model trained via agentic reinforcement learning and a hierarchical test-time scaling workflow.
Agentic Prover
The prover uses an incremental strategy to construct formal proofs step by step through multiple tool invocations. Once a lemma is compiled successfully, it is cached in memory and reused in subsequent reasoning steps, preventing the regeneration of verified code. The available tools include Lean verification, Mathlib search via embedding-based retrieval, and Python execution. During inference, generation terminates when the theorem is verified or when the interaction budget (64K maximum sequence length and a limit of 28 tool calls) is exhausted.
Post-training
The model is initialized using supervised fine-tuning (SFT) on synthetic data to learn tool invocation patterns in the Lean environment. Reinforcement learning (RL) optimization is implemented using VAPO. An outcome-based reward function is applied: the model receives a reward of \(1\) if a proof is verified by the Lean compiler, and \(-1\) otherwise. The proximal policy optimization objective is defined as:
\[\mathcal{L}_{PPO}(\theta) = - \frac{1}{G} \sum_{i=1}^{G} \frac{1}{|o_i|} \sum_{t=1}^{|o_i|} \min \left( r_{i,t}(\theta) \hat{A}_{i,t}, \text{clip}\left(r_{i,t}(\theta), 1 - \varepsilon_{\text{low}}, 1 + \varepsilon_{\text{high}}\right) \hat{A}_{i,t} \right)\]where \(G\) is the batch size, \(o_i\) is the trajectory of the \(i\)-th sample, \(\hat{A}_{i,t}\) is the estimated advantage at time step \(t\), \(\varepsilon\) is the clipping hyperparameter, and \(r_{i,t}(\theta)\) is the probability ratio.
Sketch Model
A sketch model synthesizes a lemma-style Lean sketch from a formal statement and its natural language proof. It decomposes the proposition into \(N\) independent sub-goals. The model is trained using VAPO with a hybrid reward signal. The reward function \(R\) requires the generation of at least three lemmas, structural correctness verified by Lean (\(S_{\text{FL}}\)), and semantic validity verified by an LLM-as-a-Judge (\(S_{\text{NL}}\)):
\[R = \begin{cases} 1 & \text{if } N_{\text{lemmas}} \ge 3 \land S_{\text{FL}} \ge 0 \land S_{\text{NL}} \ge 0.7, \\ -1 & \text{otherwise}. \end{cases}\]Test-Time Workflow
The system uses a hierarchical workflow coordinating three agents:
- Natural Language Prover: Generates lemma-style natural language proofs.
- Sketch Model: Converts natural language proofs into lemma-style Lean sketches.
- Agentic Lean Prover: Verifies individual lemmas.
For each unsolved lemma, the Agentic Prover attempts verification under a compute budget. If unverified, recursive decomposition (natural language proof to Lean sketch) is performed until leaf nodes are proved or the maximum search depth is reached.
Experiments
Evaluations were conducted using Lean v4.22.0 across multiple benchmarks: PutnamBench, FATE-H, FATE-X, CombiBench, IMO 2025, Putnam 2025, and a subset of Erdős problems.
Scaling Behavior of Agentic Prover Training
During RL training, batch-level accuracy increases from 50% to nearly 90% after 1000 steps. The average number of function calls per trajectory decreases from 15 to 10, accompanied by a reduction in average sequence length from ~28k to ~17k tokens. The model adapts its search tool usage based on the dataset, averaging 10 search calls per trajectory on Fate-H and 1–2 on Putnam.
Test-Time Workflow Evaluation
On PutnamBench, test-time compute scaling (search width and search depth) yields a log-linear increase in the solve rate. The majority of problems are solved within the initial hours, with the distribution extending to the 53rd hour.
The system solves 87.9% of PutnamBench, 80% of FATE-H, 33% of FATE-X, and 48% of CombiBench problems.
On the IMO 2025 and Putnam 2025 competitions, maximum search depth was capped at 4. The model solved 11 out of 12 problems from Putnam 2025 within 9 hours, using a maximum compute budget of 40 H20-days per problem.
