Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Lean-STaR: Learning to Interleave Thinking and Proving

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked every number in Tables 1 to 10 (summed Tables 6 and 7 columns), quotations, section and page references, technique steps against Sections 3.2 to 3.3 and Appendices A, C, G; changed: the 4-days cost no longer credited to each iteration, the no-goals success test marked as carried over from best-first search, Table 5 similarity wording, one unmarked limit and one cause marked as the authors’ attribution; Verus forms are marked inference and not checked against Verus sources.

source: Lin, Sun, Welleck, Yang, arXiv:2407.10040v5 (15 Mar 2025), ICLR 2025, 22 pages with appendices A to H. The prover is Lean 4 and the tasks are mathematics; the Verus forms below are inferences.

what is measured and what stays trusted

The paper trains a 7-billion-parameter model to write one short natural-language thought before each Lean tactic, then retrains it on its own Lean-checked proofs. It measures the fraction of the 244 miniF2F-test problems proved, and of a 320-theorem random subset of Leandojo4-v9-test (novel premises) (Table 1 caption, p.7).

  • headline, InternLM2-7b base, sampling, N=50, K=32, temperature 0.7 (Table 1, p.7): few-shot 28.7%, SFT 29.5%, Lean-CoT 32.8%, Lean-STaR after iteration 1 34.0%, after iteration 2 34.8%; with K=64, 36.1%
  • on the 320 Leandojo theorems, same setting: 29.7%, 30.6%, 35.6%, 38.4%, 39.4%
  • InternLM2-plus-7b, K=32 (Table 2, p.8): few-shot 40.9%, SFT 41.3%, Lean-CoT 43.4%, Lean-STaR iteration 1 45.4%; with K=64, 46.3%
  • trusted: Lean alone decides success. The thoughts are never checked, and may be wrong. Figure 2’s caption (p.4): “Note that there is a calculation error in the thought (in red), but this does not affect the correctness of the proof because the calculation task is actually completed by the interactive theorem prover (i.e., Lean’s nlinarith) instead of the language model.”
  • Inference: the thought is a search aid with no evidential weight; a reader of a Lean-STaR proof must not treat its comments as an explanation that has been verified.

technique 1: retrospective rationale generation

what it is: making (state, thought, tactic) training triples from existing (state, tactic) pairs by showing a strong model the human’s tactic and asking it to write the reasoning that would lead there, phrased as if the tactic were not yet known.

when to use: a corpus of checked proofs exists, it contains no reasoning, and asking a model to reason forward from the state alone gives poor results. The paper reports that last point (Section 3.2.2, p.4): “In turn, we find that even the most powerful GPT-4 model does not perform well in generating the correct rationale through few-shot prompting (Brown et al., 2020).”

steps

  1. take (state, tactic) pairs from successful proof trajectories (Section 3.2.2, p.4-5); the paper draws 17,256 trajectories from LeanDojo Benchmark 4 and annotates 52,438 steps with GPT-4-0125 (Section 4.1, p.7)
  2. drop steps whose tactic contains a newline (Section 4.1, p.7)
  3. give the oracle model the state and the ground-truth tactic (Section 3.2.2, p.5)
  4. prompt it with one worked example and four rules (Appendix G, p.19-20); three of them read: “Craft reasoning that is comprehensive yet concise, contained ideally within two sentences.”; “Begin reasoning with the objective of the Given Theorem, ensuring logical progression, rather than constructing it retrospectively from the Given Tactic.”; “Avoid mentioning the Given Tactic and specific statement names from the Given Tactic throughout your reasoning.”
  5. require three output parts in order: planning of reasoning, reasoning, tactic (Appendix G, p.20)
  6. keep the reasoning as the thought t_i, giving D_T = {(s_i, t_i, a_i)}

The purpose of the rules is stated (Section 3.2.2, p.5): “The design principle of the prompt is to prevent the oracle model from generating hindsight-like thoughts.”

The paper’s example (Figure 6, p.20): state a b n : ℕ ⊢ ¬(n ≠ 0 ∧ a ≠ 0) ↔ n = 0 ∨ a = 0, tactic simp only [not_and_or, ne_eq, not_not]; the generated thought says the proof uses the logical equivalence between a negated conjunction and a disjunction of negations, without naming the lemmas.

Verus form. Inference: Verus has no per-step state, so the pair has to be constructed: take a verified function, remove one proof annotation (an assert(...), an assert ... by block, a call to a proof fn, an invariant clause, a decreases clause), and treat the function without it plus Verus’s resulting error as the state and the removed annotation as the tactic. The oracle then writes two sentences that start from the failing obligation and end at the annotation. The thought is stored as a Rust // comment directly above the annotation; the paper prints its thoughts the same way, as -- Reasoning: comments beside each tactic (Appendix H, p.22). What does not carry over: a Verus annotation is often useless alone (an invariant plus an assert are needed together), so removing a single one may leave a state from which the single target is not the natural next step.

evidence: Lean-CoT, trained on these triples starting from the SFT model, reaches 32.8% against SFT’s 29.5% on miniF2F-test (244 problems; Table 1, p.7), and 43.4% against 41.3% with the plus model (Table 2, p.8). For the plus model 140,000 thoughts were annotated with GPT-4o (Section 4.3, p.9).

limits: no check that a thought is correct or even relevant; the paper gives no rate. Section 5 (p.9-10) notes that GPT-4 annotation “may incur a significant cost and possibly introduce biases”. Appendix C (p.15) raises leakage of miniF2F into GPT-4 and argues against it from Table 5 (technique 5).

technique 2: thought-augmented step prediction (Lean-CoT)

what it is: a model that, given a proof state, emits a thought and then a tactic, trained in two fine-tuning stages.

steps

  1. SFT: fine-tune the base model for 1 epoch on (state, next-tactic) pairs, 231,240 examples from LeanDojo Benchmark 4 v9; learning rate warmed up over the first 20% of steps to 2×10⁻⁵, then cosine decay to zero (Section 4.1, p.7)
  2. Lean-CoT: fine-tune the SFT model on D_T from technique 1 (Section 3.2.2, p.5)
  3. at inference, for each state generate thought then tactic; only the tactic goes to Lean (Section 3.2.2, p.4, where the model is written π_M(a_i, t_i | s_i) = π_M(a_i | t_i, s_i) π_M(t_i | s_i))

Verus form. Inference: for a prompted, not fine-tuned, agent the same shape is: before each annotation it adds, write at most two sentences on why the current Verus error calls for it. For fine-tuning, the data are technique 1’s triples. Nothing here depends on Lean besides the availability of a state.

evidence: as under technique 1. By category on miniF2F-test (Table 6, p.17; counts of problems, base model): Lean-CoT solves 80 in total against SFT’s 72 (my sums of the table’s columns, which match 32.8% and 29.5% of 244); AMC goes from 3 to 7 of 45, IMO stays at 0 of 20.

limits: the gain is 8 problems of 244 from one sampling run; no variance is reported.

technique 3: expert iteration over thought-augmented proofs (Lean-STaR)

what it is: let the current model attempt many theorems, keep every (state, thought, tactic) step from proofs Lean accepts, and fine-tune on them; repeat.

when to use: a checker gives a binary correct signal and unproved statements are plentiful.

steps (Section 3.2.3, p.5, and Appendix A.1, p.14)

  1. start from Lean-CoT and the set of initial states of the theorems; the paper samples on the LeanDojo Benchmark 4 dataset
  2. sample K = 32 trajectories per problem at temperature 1.0, with a total of N = 5 tactic generations per problem and 1 minute per problem
  3. keep only successful trajectories: “Then we create a new dataset D1 by filtering the generated trajectories to include only the successful ones.”
  4. de-duplicate, and keep up to 3 proof trajectories per problem
  5. iteration 1: fine-tune the SFT model for 1 epoch on D_T ∪ D_1 (32,231 pairs collected) to get M_1
  6. iteration 2: generate D_2 with M_1 (19,324 pairs; Table 4, p.14) and fine-tune M_1 further on D_2
  7. stop after a fixed number of iterations (Figure 3 caption, p.5); the base model gets two, the plus model one

Cost given (Appendix A.1, p.14): “In this setup, each problem needs on average about 0.5 A100 minutes.” Collecting D_1 took about 4 days on 8 A100 GPUs.

Two ways to do step 5 are compared (Table 9, p.19; Pass@32, N=50, T=0.7): joint training (SFT model on GPT-4 data plus STaR data) gives 34.0% base and 43.9% plus; continue training (Lean-CoT on STaR data only) gives 33.2% base and 45.5% plus. The paper’s reading (Appendix F, p.18): “It seems that there are no difference between these two methods.”

Verus form. Inference: the loop needs (a) a pool of Rust functions with specifications and no proofs, (b) the model proposing annotated versions, (c) Verus as the filter, with any output containing assume, admit() or a changed requires/ensures rejected before counting as success, (d) de-duplication and a per-function cap, (e) fine-tuning. What changes: in Lean the statement is fixed by the theorem; in Verus the filter must also confirm that the executable code and the specification are unchanged, or the model learns to weaken them. Inference from outside this paper: SAFE (Chen et al., ICLR 2025, studied in automated_proof_generation_for_rust_code_20261012.md) already runs a self-training loop of this kind for Verus, so the loop itself is not new for Rust.

evidence

  • miniF2F-test, base model, K=32: 32.8% → 34.0% → 34.8% over two iterations (Table 1, p.7); Leandojo subset 35.6% → 38.4% → 39.4%
  • control without thoughts: expert iteration on (state, tactic) pairs from the SFT model gives 30.7% base and 43.0% plus, against 34.0% and 45.4% for Lean-STaR (Section 4.4 and Table 3, p.9). The paper concludes: “This shows that Lean-STaR’s performance gains do not only come from the use of expert iteration.”
  • more samples help the thought model longer (Table 10, p.19): from S×K = 32 to 64, SFT with search stays at 30.7%, SFT with sampling goes 29.5% → 30.3%, Lean-STaR 34.8% → 36.1%. The paper’s explanation (Appendix F.1, p.18): “We believe this is because thoughts increase the diversity of outputs and contribute to exploration in the theorem proving space.”

limits: gains shrink per iteration (+1.2 then +0.8 points; Table 4, p.14) while collecting D_1 alone took about 4 days on 8 A100 GPUs (Appendix A.1, p.14); the cost of iteration 2 is not given. Section 5 (p.10): “Also, expert iteration could face a bottleneck due to CPU and IO limitations, which might slow down the process due to a sluggish speed of Lean ITP.” Only theorems the model can already prove within 5 generations enter the data, so hard theorems contribute nothing; that consequence is an inference.

technique 4: parallel trajectory sampling with resampling of illegal steps

what it is: a proof-search procedure that replaces best-first search. Run K independent attempts; in each, sample one step at a time; when the prover rejects a step, discard it and sample again from the same state.

when to use: the model emits free text before each step; the authors attribute best-first search’s poor results to average log-probability being an unreliable quality indicator then (p.6, quoted below), not tested separately.

steps (Section 3.3, “Sampling”, p.6)

  1. for each problem start K attempts in parallel from the initial state
  2. at state s_i sample one thought and tactic
  3. if the tactic is legal, append it and move to the new state
  4. if not: “Otherwise, we ignore this ai and use language model M to sample a new tactic given state si.”
  5. stop an attempt after N tactic generations in that attempt (Section 3.3, p.6); that no goals means success is stated for best-first search (p.6), and Inference: the same test applies to sampling
  6. report pass@K; the paper uses N=50, K=32 or 64, temperature 0.7, and for K=64 samples 32 twice (Table 1 caption, p.7)

why not best-first search. The paper says so early (Section 3.3, p.5): “Our preliminary experiments indicate that best-first search with beam search does not work well for the thoughts in the natural language format.” And gives a cause (p.6): “We attribute this to using average log probabilities, which may not be a reliable quality indicator when the thought sequence tj is generated.”

Verus form. Inference: an attempt is a growing list of annotations on one function. After each added annotation run Verus; if the new annotation itself is rejected (syntax error, or an assert Verus cannot prove), drop it and resample at the same point; otherwise keep it. Cap total generations per attempt at N and run K attempts with nonzero temperature. Ranking candidates by model log-probability should be avoided when the model writes comments first. What does not carry over: Lean tells legal from illegal per tactic at once; a Verus run re-checks the whole function, so each step costs a full verification.

evidence (Table 8, p.18; miniF2F-test, 244 problems, N=50, S×K=32)

  • SFT: best-first search with beam search 30.7%, best-first search with sampled tokens 29.9%, sampling 29.5%
  • Lean-CoT: 25.4%, 27.0%, 32.8%
  • Lean-STaR iteration 2: 26.2%, 29.5%, 34.8%
  • so search suits the plain model slightly better and sampling suits the thought models by 5 to 9 points

cost claim (Section 3.3, p.6): evaluating sampling and best-first search with equal S × K “took approximately the same amount of GPU time”.

limits: Inference: no backtracking beyond the current state; an attempt that takes a legal but useless step keeps going down that path.

technique 5: leakage check by comparing found proofs with reference proofs

what it is: a table that sorts the benchmark’s reference proofs by kind and counts how many generated proofs equal them.

steps (Appendix C and Table 5, p.15; the caption says it is similar to the analysis in Thakur et al. (2024))

  1. split miniF2F-test’s 244 entries: 82 have a proof in the benchmark (11 linarith, 12 norm_num, 2 nlinarith, 18 two-tactic, 39 longer or complex) and 162 have only sorry
  2. for each successful generated proof, test exact match and first-tactic match with the reference
  3. count distinct successful proofs per class

result: of 112 successful proofs, 7 match exactly (6 of them single-tactic linarith or norm_num), and 90 of 112 (80.36%) are distinct; 48 successes are on problems with no reference proof. The paper’s sentence: “If we set aside straightforward simple cases, there is only one proof generated by LeanSTaR is the same as the proofs mentioned in the miniF2F.”

Verus form. Inference: for a Verus benchmark with published reference proofs, compare each accepted proof’s annotations with the reference after normalising whitespace; report exact matches separately for one-line proofs. It bounds memorisation of proofs; it says nothing about memorised statements.

contradictions and numbers that do not add up

  • The abstract states “(43.4% → 46.3%, Pass@64)”. In Table 2 (p.8), 43.4% at K=64 is the SFT model; the untouched InternLM2-plus-7b at K=64 is 42.2%. The Introduction (p.2) instead compares 45.4% (pass@32) with “the previous results of 43.4% (pass@32)”, which in Table 2 is the published best-first-search figure with N=1000, K=1, S=32, reproduced by the authors at 42.6%.
  • Lean-STaR with the plus model at K=32 is 45.4% in Table 2 and Section 4.4, and 45.5% in Tables 3 and 9. Table 7’s column sums to 111 of 244 = 45.49% (my sum), so one figure is truncated and the other rounded. Likewise the plus baseline: Table 7 sums to 100 of 244 = 40.98%, printed as 40.9%.
  • Table 5 counts 112 successful proofs of 244 (45.9%), a rate that matches no row of Tables 1 or 2; the paper does not say which model or setting produced it.
  • Table 6’s caption says thought-augmented methods “improve performance on all categories”; in the table Lean-CoT is below SFT on MATH Algebra level 2 (9 against 10) and Number Theory level 4 (4 against 5), and Lean-STaR is below Lean-CoT on AMC (5 against 7).
  • Section 3.2.3 fine-tunes the SFT model on D_T ∪ D_1; Section 4.3 fine-tunes the Lean-CoT model on D_1 for the plus model. Table 9 shows the two choices swap rank between models.
  • “significantly” is used for all gains; no significance test or repeated run is reported. 34.8% against 29.5% is 85 against 72 problems.
  • The expert-iteration budget is N = 5 generations per problem (Appendix A.1), a tenth of the evaluation’s N = 50; the paper does not comment.

what is already done, and threat

Done: the demonstration that short free-text reasoning before each proof step, learned from hindsight annotations and then from self-generated checked proofs, raises proof rate over the same model without it, with a no-thought expert-iteration control.

Inference on threat: low and indirect. The work is on competition mathematics in Lean with a small open model, and a 2025 result of 46.3% on miniF2F-test. Its relevance to agent-written verified Rust is the recipe for making reasoning-annotated training data out of any corpus of checked proofs, which a competitor with a Verus corpus could apply.

techniques for the catalog

  • retrospective rationale generation — give a strong model the state and the known next step and have it write a two-sentence forward-looking reason, to build (state, thought, step) training data
  • anti-hindsight prompt rules — require reasoning to start from the goal, not name the given step or its lemmas, and place the step last
  • thought-before-step prediction — train or prompt the prover to emit a short informal thought before each formal step, sending only the step to the checker
  • thought-augmented expert iteration — sample proofs with the current model, keep checker-accepted trajectories with their thoughts, de-duplicate, cap per problem, and fine-tune
  • no-thought expert-iteration control — run the same self-training on (state, step) pairs alone to separate the effect of thoughts from that of self-training
  • parallel sampling with illegal-step resampling — run K independent attempts, resample at the same state when the checker rejects a step, cap total generations at N
  • reference-proof match table — classify benchmark reference proofs by length and count exact and first-step matches among generated proofs to bound memorisation

Last edited: