StepFun-Prover Preview: Let's Think and Verify Step by Step

1. Introduction

• Prior methods often need substantially more proof attempts: increasing sampling from 32 to 64 yields only 3%–4% accuracy gains, limiting usability for non-experts.The passage attributes this inefficiency to rigid, predefined reasoning patterns that do not fully leverage Lean 4 feedback.Source: §1 · p. 1
• The paper asks whether theorem provers can develop their own ways to reason, interact with a formal verifier, and derive proofs efficiently.The proposed exploration lets the model decide when to stop using tools, without a fixed interaction limit.Source: §1 · pp. 1–2
• The proposed framework interleaves natural-language reasoning, Lean 4 code, and real-time environment feedback, trained through cold start followed by iterative reinforcement learning and supervised fine-tuning.The training stages establish interaction patterns and then refine capabilities using proof outcomes.Source: §1 · p. 2
• StepFun-Prover-Preview-32B surpasses all counterparts by over 4% on pass@1, while the 7B model catches up to DeepSeek-Prover-V2-671B and Kimina-Prover-72B.Figure 1 compares pass@1 across maximum Lean4-REPL interactions; StepFun-Prover used a 20K context window, while the baselines used at least 32K.Source: §1 · p. 2, Figure 1 · p. 2

2. Methodology

• The end-to-end training pipeline is presented as a framework for developing tool-integrated reasoning models.Figure 2 gives the pipeline overview.Source: §2 · p. 2, Figure 2 · p. 3
• The pipeline overview identifies data preparation alongside tool-integrated reinforcement learning and an iterative RL-SFT cycle.These components are shown on the left of Figure 2.Source: Figure 2 · p. 3
• Figure 2 also depicts a tool-integrated reasoning pattern as part of the training pipeline.The reasoning pattern is shown on the right side of the figure.Source: Figure 2 · p. 3

2.1. Cold Start for Tool-integrated Reasoning

• The authors compile formal mathematics problems from the Lean Workbook and STP dataset, and use Kimina-Autoformalizer-7B to autoformalize selected Numina Math 1.5 problems.Source: §2.1 · p. 3
• The collected and autoformalized problems can contain tautologies, contradictory premises, irrelevant conclusions, or trivial and ill-posed tasks.Source: §2.1 · p. 3
• DeepSeek-V3 filters low-quality problems before the authors construct cold-start dataset D0 through two parallel processes.Source: §2.1 · p. 3
• The multi-turn process collects approximately 8,000 effective trajectories, while the single-turn process removes intermediate tactic blocks and reasoning steps from Kimina-Prover-72B proofs.The single-turn data retains natural-language reasoning and the final Lean 4 answer.Source: §2.1 · p. 3

2.2. Two-stage Supervised Fine-tuning

• The first supervised fine-tuning stage uses question-answer pairs from the open-sourced STP dataset to establish basic Lean 4 syntax and proof-structure understanding.Source: §2.2 · pp. 3–4
• Continual supervised fine-tuning on cold-start dataset D0 establishes initial tool-integrated reasoning and proof-generation capabilities.Source: §2.2 · p. 4
• The two-stage process yields the cold-started model M0.Source: §2.2 · p. 4

2.3. Response Patterns Fusion

• M0 struggled to integrate the distinct response patterns from Claude and Kimina.The authors describe its performance as significantly below expectations.Source: §2.3 · p. 4
• The fusion process used M0 to correct incorrect Kimina-Prover-72B responses while preserving valid reasoning, producing dataset D1.Source: §2.3 · p. 4
• Fine-tuning exclusively on D1 produced M1, which was intended to harmonize the response styles and initialize subsequent reinforcement learning.Source: §2.3 · p. 4

2.4. Tool-integrated Reinforcement Learning

• Rollouts combine natural-language reasoning, Lean 4 sketches, and real-time sandbox feedback in an iterative trajectory.The model can continue with another solution or provide a final answer after receiving execution output.Source: §2.4 · p. 4
• The model marks its final proof with </think>; REPL verification assigns reward 1 to passing proofs and 0 otherwise.The authors use this binary outcome reward with GRPO and omit the KL term to promote exploration.Source: §2.4 · p. 4
• For each training problem, the method samples candidate answers and computes a group-based advantage from their binary rewards.Source: §2.4 · p. 5
• Figure 3 presents training reward alongside test accuracy measured as pass@1 for tool-integrated GRPO.Source: Figure 3 · p. 5

2.5. Iterative RL-SFT Cycle

• After the first reinforcement-learning phase converges, the authors collect correct trajectories from problems scoring below 0.5 training accuracy.Source: §2.5 · p. 5
• They retain trajectories that comprehensively analyze REPL feedback and use them for another supervised fine-tuning round.Source: §2.5 · p. 5
• A secondary reinforcement-learning phase follows to further enhance tool-integrated reasoning capabilities.Source: §2.5 · p. 5

2.6.1. Supervised Fine-tuning

• SFT uses distinct strategies for non-reasoning code-completion data and tool-integrated reasoning data.The non-reasoning stage leaves thinking content blank; reasoning-data SFT trains on interpretation of REPL feedback and follow-up actions, while masking REPL feedback in loss computation.Source: §2.6.1 · pp. 5–6

2.6.2. Reinforcement Learning

• The RL setup generates eight samples per problem, allows up to 16384 tokens, and sets a 60-second REPL execution timeout.Rollouts use batch size 512, temperature 1.0, and top-p 0.999.Source: §2.6.2 · p. 6
• RL data selection retains prompts with success rates strictly between 0 and 1, excluding consistently trivial or currently unsolvable problems.Success rates are computed from REPL feedback on rollouts gathered during training, rather than filtering statically before training.Source: §2.6.2 · p. 6
• Lean4-REPL remote-server optimizations accelerated multi-turn RL training by over 10x and enabled training with unlimited interaction times.Source: §2.6.2 · p. 7

3. Experimental Results

• Evaluations use Numina’s corrected miniF2F benchmark, Lean 4.20.0, and 32 responses per query to estimate pass@1.The REPL timeout is 60 seconds and maximum generation length is 20480 tokens unless otherwise specified.Source: §3.1 · p. 7, §3 · p. 7

3.1. Results on MiniF2F Benchmark

• 70.0% pass@1 on miniF2F-test lets StepFun-Prover-Preview-32B surpass prior SOTA results with a smaller model size.The result is reported in Table 1.Source: Table 1 · p. 7, §3.1 · p. 7

3.2.1. Test Time Scaling in Tool-integrated Reasoning

• StepFun-Prover-Preview-32B improves consistently on miniF2F-test when its maximum generation length is extended.Table 2 reports performance across generation lengths.Source: §3.2.1 · p. 7, Table 2 · p. 8
• Successful miniF2F-test proofs can emerge after multiple rounds of REPL interaction and refinement.Figure 4 shows the interaction-frequency distribution for successful proofs using 32 responses per problem.Source: Figure 4 · p. 8, §3.2.1 · p. 8

3.2.2. Diverse Reasoning Patterns

• The model demonstrates proactive Lean 4 warning resolution, proof restructuring after time thresholds, and iterative improvement from REPL feedback.The examples include restructuring when execution exceeds 60 seconds.Source: §3.2.2 · p. 8

4. Related Work

• Earlier LLM theorem provers generated individual proof steps or complete proofs, often pairing generation with Best-First Search or Monte Carlo Tree Search.Search heuristics improve exploration but add computational overhead.Source: §4 · p. 9
• Recent multi-turn tool-integrated reasoning incorporates environment feedback during reasoning, unlike earlier models that used it only for final correctness checks.Reported application settings include REPLs, search engines, and formal verifiers.Source: §4 · p. 9
• Formal-mathematics systems support iterative proof revision, but often abstract away learning dynamics and limit model autonomy.The paper identifies test-time self-directed tool use from environment feedback as an underexplored opportunity.Source: §4 · p. 9

5. Conclusion

• The end-to-end pipeline combines cold-start data synthesis and tool-integrated reinforcement learning; the resulting model reaches 70.0% pass@1 on miniF2F-test through iterative proof refinement using real-time environment feedback.The authors identify transferring formal-reasoning rigor to LLMs and developing multi-agent systems for mathematical discovery as future work.Source: §5 · p. 9

A. Examples of Tool-integrated Reasoning

• The prompt lets the model check partial Lean 4 solutions in the REPL and continue revising them until the proof is complete and correct.Partial solutions are enclosed in <sketch> tags, with REPL feedback returned between <REPL> tags.Source: A. Examples of Tool-integrated Reasoning · p. 13
• The worked example asks for a proof that a cyclic sum of three rational expressions is nonnegative for positive real x, y, and z.The terms are (x^2 - z^2)/(y + z), (y^2 - x^2)/(z + x), and (z^2 - y^2)/(x + y).Source: A. Examples of Tool-integrated Reasoning · p. 13
• The reasoning explores clearing denominators and factoring differences of squares, while noting that individual terms can have opposing signs and may cancel.The common denominator is (y+z)(z+x)(x+y); the text does not establish a completed proof.Source: A. Examples of Tool-integrated Reasoning · pp. 13, 15
• After Lean reports an unexpected end-of-input syntax error and an unsolved goal, the model reviews the feedback and tries a different tactic-based proof approach.The shown attempt begins by deriving positivity of the three denominator sums and clearing denominators.Source: A. Examples of Tool-integrated Reasoning · pp. 16–17
• REPL errors revealed that linarith failed on the expanded numerator goal and that apply did not match the goal proving the denominator product non-negative.The output shows the expanded polynomial goal and the mismatch between a strict product positivity result and the non-strict goal.Source: A. Examples of Tool-integrated Reasoning · pp. 17–18
• The proof clears denominators using the three pairwise sums, whose positivity follows from the assumptions that x, y, and z are positive.It records each sum as positive and uses field_simp to transform the rational expression.Source: A. Examples of Tool-integrated Reasoning · p. 20
• The revised algebraic approach rewrites the cleared numerator as x^4 + y^4 + z^4 - x^2*y^2 - x^2*z^2 - y^2*z^2, then as half the sum of three squared differences.The proof uses the non-negativity of each squared difference to establish the numerator bound.Source: A. Examples of Tool-integrated Reasoning · pp. 20–21

• The REPL reports a complete, error-free proof of the inequality for positive x, y, and z.Source: A. Examples of Tool-integrated Reasoning · pp. 21, 24
• After clearing denominators, the proof rewrites the numerator as a sum of squares, establishing its non-negativity.The resulting polynomial is expressed as one-half the sum of the squares of pairwise differences of x^2, y^2, and z^2.Source: A. Examples of Tool-integrated Reasoning · p. 24
• The proof establishes that the denominator product is positive by proving each pairwise sum positive and multiplying those facts.This supplies the positivity needed when clearing the denominators.Source: A. Examples of Tool-integrated Reasoning · p. 24

A. Examples of Tool-integrated Reasoning

• The prover rewrote the inequality as half the sum of three squared differences, then proved each square nonnegative.The displayed identity is x^4 + y^4 + z^4 - x^2*y^2 - x^2*z^2 - y^2*z^2 = (1/2) * ((x^2 - y^2)^2 + (y^2 - z^2)^2 + (z^2 - x^2)^2).Source: A. Examples of Tool-integrated Reasoning · p. 25
• The completed proof also established its denominator was positive by multiplying the positive terms y + z, z + x, and x + y.The analysis describes the resulting solution as complete and correct.Source: A. Examples of Tool-integrated Reasoning · p. 25
• After several failed attempts, REPL feedback helped StepFun-Prover identify a sum-of-squares structure, revise its strategy, and complete the proof correctly.The analysis identifies this recognition as the turning point in the proof.Source: A. Examples of Tool-integrated Reasoning · p. 25