LLMSTEP: LLM proofstep suggestions in Lean

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked every number, fraction, page and table reference, quotation and technique step; all matched; changed only two when-to-use lines, marked as Inference because they are the study’s own advice.

source: Welleck and Saha, arXiv:2310.18457v1 (27 Oct 2023), 4 pages of text plus references, no appendix. A tool paper for Lean 4. Nothing in it concerns Verus; each Verus form below is an inference.

what is built, what is measured, what stays trusted

LLMSTEP is an editor-side tool. Inside a Lean proof the user writes llmstep <prefix>; the tactic sends the current proof state and the prefix to a model server, gets back candidate next tactics, runs each in Lean, and shows them colour-coded in the Infoview, where a click inserts one.

• measured: (a) how many theorems the default model closes under best-first search (Table 1, p.3), and (b) seconds to return N suggestions on three kinds of hardware (Table 2, p.4)
• not measured: whether users prove more or faster with the tool; there is no user study
• trusted: Lean, which checks each suggestion. The Introduction (p.1) puts the division of labour this way: “Doing so can be mutually beneficial: proof assistants provide correctness guarantees on language model outputs, while language models may help make proof assistants easier to use.”
• Inference: the model and server are outside the trusted base, since a suggestion only enters the proof after Lean has run it.

technique 1: run every suggestion in the prover and sort into three classes

what it is: before a suggestion is shown, it is applied to the current state, and the outcome decides its label.

when to use: Inference: whenever a model proposes several candidate next steps and a checker call is cheap compared with a human reading a wrong suggestion.

steps (Section 3.1, “Lean tactic”, p.2)

1. send the current state x_t and the prefix to the server
2. receive the list of suggested tactics
3. apply each one in Lean to the current state
4. label it: “Namely, a checked suggestion is valid if applying the tactic leads to a state with no errors and at least one goal.”
5. or: “A tactic is complete if it leads to a state with no errors and no goals.”
6. anything else is invalid
7. display all three classes in different colours

The paper’s example (Figure 3, p.4): for example : R ⊆ S → S ⊆ T → R ⊆ T := by with an empty prefix, five suggestions come back: exact subset_trans, exact Set.Subset.trans, tauto, intro, intros h1 h2. The caption: “The first three suggestions each finish the proof, and the last two are valid.”

Verus form. Inference: Verus has no goal list, so the three classes need new definitions. Take a candidate to be one proof annotation (an assert(...), an assert ... by block, a call to a proof fn, an invariant clause, a decreases clause) inserted at the failing point, then run Verus on that function:

• complete: the function now verifies with no errors
• valid: the inserted annotation itself raises no error, and the function’s original error remains or moves; the fact is true and may be a step
• invalid: a syntax or mode error, or Verus cannot prove the inserted assert

What changes: Lean’s valid class says the proof moved to a new state; the Verus valid class only says a true fact was added, which can be useless. A rule is needed for progress, such as fewer reported errors. What does not carry over: one-tactic granularity; a Verus step often needs an invariant and an assert together. Also, a suggestion containing assume or admit() would be labelled complete by this rule and must be rejected before checking.

evidence: none for this technique alone; the paper reports no rate of valid or complete suggestions.

limits: each check costs a prover run per suggestion; the paper gives no timing for the checking half, only for the server (Table 2).

technique 2: prefix-constrained suggestions

what it is: the user supplies the first tokens of the wanted step; the model completes only steps beginning with them.

when to use: Inference: the user knows the kind of step (an exact, an intro) and wants the model to fill in the rest.

steps (Section 3.1, p.2)

1. the tactic takes a prefix argument: “LLMSTEP takes a prefix as an argument, i.e., a sequence of tokens that will start the suggested tactics.”
2. state and prefix go to the server together
3. Inference: the prefix is appended after the [PROOFSTEP] marker of technique 3 so that decoding continues from it; the paper does not say how the server enforces the prefix
4. suggestions are checked as in technique 1

The paper’s example: the prefix intr yields tactics such as intro h x.

Verus form. Inference: prefixes select the annotation kind: assert(, assert forall, invariant, decreases, reveal(, or the name of a lemma family such as lemma_seq_. This turns an open request into a constrained completion and lets an agent, not only a human, ask for one specific kind of annotation at one location.

evidence: none; Table 2’s 17 timing examples each contain “a tactic state and a prefix” (Section 4, p.4) but no quality comparison with and without a prefix is given.

technique 3: the proofstep training format

what it is: fine-tune a causal language model on pairs of proof state and the human’s next tactic, laid out as one string.

steps (Section 3.1, “Language model”, p.2-3)

1. extract (state, next-tactic) pairs from a proof corpus; here Lean Mathlib through the LeanDojo Benchmark 4 dataset
2. format each as [GOAL]tactic-state[PROOFSTEP]next-tactic<|endoftext|>
3. fine-tune; the default is Pythia 2.8b
4. at use, feed [GOAL] + state + [PROOFSTEP] (+ prefix) and decode

The paper ties the format to earlier work (p.3): “This format corresponds to the proofstep objective described in [7].” Reference [7] is Han et al., proof artifact co-training.

Verus form. Inference: Verus exposes no intermediate states, so pairs must be made differently: take a verified function, delete one annotation, record Verus’s error for the damaged function as the state, and the deleted annotation as the target. The format then reads [GOAL] function text and error, [PROOFSTEP] the annotation. Not in the paper: any such deletion scheme.

evidence (Table 1, p.3; best-first search, 10-minute timeout, beam search with expansion size 32)

• miniF2F-test: Pythia 2.8b 27.9% (68/244) at 1×32 and the same at 2×32; ReProver without retrieval 22.1% (54/244) at 1×64
• mathlib4-test (LeanDojo random split; the table gives no counts): Pythia 47.6% at 1×32 and 50.1% at 2×32; ReProver 48.6% at 1×64
• mathlib4-valid: Pythia 48.8% and 51.2%; miniF2F-valid: 26.2% for both Pythia rows; no ReProver numbers

limits: the ReProver figures are not reruns. Section 4 (p.3): “We report mathlib4-test from [19] and miniF2F-test from [15], since miniF2F without retrieval was not available in [19].” Inference: hardware and Lean versions may differ between the rows being compared.

technique 4: thin prover-side client, swappable model server

what it is: three separate parts, so that model and hardware can change without touching the prover integration.

steps (Section 3.1, p.2-3)

1. the parts: “LLMSTEP consists of three parts: (1) a Lean tactic, (2) a language model, (3) a server.”
2. the tactic is a Lean 4 metaprogram; the server is Python (Figure 1 caption, p.2)
3. the server holds the model, answers requests from the tactic, and relays suggestions back
4. usage (Section 3.1, “Usage”, p.3): start a server suited to the hardware; import LLMSTEP as a Lean 4 package; call llmstep <prefix>
5. choose the model by hardware (Section 4, p.4): “Therefore, we suggest using Pythia when a GPU is available, and Reprover on CPU.”

Verus form. Inference: the client is an editor or command-line wrapper around the verus binary, not a Verus-language construct, because Verus has no tactic or metaprogramming layer in which to write the client. It reads the failing function and error, calls the server, and performs technique 1’s checks.

evidence, average over 17 examples, time for the server to return N suggestions (Table 2, p.4)

• CPU (MacBook Pro, 2.6 GHz 6-core i7): Pythia 2.8b 8.39s for N=1 and 49.10s for N=10; ReProver 0.95s and 3.16s
• Colab GPU (NVIDIA T4): Pythia 1.01s and 1.68s
• GPU with vLLM (GTX 1080Ti): Pythia 0.11s and 0.25s

limits: the paper names the bottleneck (Section 3.1, p.3): “The server is the key computational bottleneck in LLMSTEP, as it hosts a (possibly large) language model.” vLLM does not support ReProver’s architecture (Section 4, p.4).

technique 5: judging a step-suggestion model by proof search

what it is: since single-step quality is hard to score, let the model drive a search to full proofs and count theorems closed.

steps (Section 4, “Proof search”, p.3)

1. use best-first search, with LeanDojo for interaction with Lean
2. set the budget as attempts × expansion size per iteration × maximum iterations, under a timeout
3. here: 10-minute timeout, expansion size 32 by beam search (chosen for memory), and a second attempt of 32 samples (2×32) to match the 64 expansions of the compared system
4. report the fraction of theorems closed per split

Verus form. Inference: best-first search over tactic states has no direct Verus counterpart. The usable part is the budget accounting: report candidate annotations generated per function as attempts × candidates per round × rounds, with a wall-clock cap, so that systems are compared at equal generation budgets.

contradictions and numbers that do not add up

• Section 4 (p.3) says the Pythia model “can exceed the number of closed theorems by ReProver on Lean Dojo Benchmark 4 and miniF2F”. Table 1 shows that on mathlib4-test this holds only at 2×32 (50.1% against 48.6%); at 1×32 Pythia is below ReProver (47.6%).
• Both percentages with fractions check: 54/244 = 22.1%, 68/244 = 27.9%.
• The second attempt changes nothing on miniF2F (68/244 both times) and adds 2.5 points on mathlib4-test. The first attempt uses beam search and the second is called “32 samples”; the paper does not say how the second attempt differs.
• Section 4 (p.4) says GPU inference “can yield suggestions in 1 second or less”; the Colab rows of Table 2 are 1.01s and 1.68s.
• The Introduction (p.1) says the baseline model “outperforms recent open-source tactic-prediction models”, plural; Table 1 compares against one, ReProver.

what is already done, and threat

Done: the interaction pattern of model suggests, prover checks, user clicks, for Lean 4, with open code. The related-work section notes that LeanInfer reuses LLMSTEP’s checking and display utilities (Section 2, p.2).

Inference on threat: none direct. It is a 2023 assistive tool for human mathematicians in Lean, with a 2.8-billion-parameter model that closes 27.9% of miniF2F-test. Its lasting content for VL is the three-class check, which is a cheap filter between a generator and an agent.

techniques for the catalog

• three-class checked suggestion — run each model suggestion in the prover and label it complete (no goals left), valid (no error, goals remain) or invalid
• prefix-constrained step suggestion — the caller fixes the first tokens of the next step and the model completes only steps that begin with them
• proofstep fine-tuning format — train on strings [GOAL]state[PROOFSTEP]next-step extracted from an existing proof library
• client/server suggestion split — a small prover-side client sends state to a separate model server so the model and hardware can be swapped
• search-based evaluation at fixed budget — score a step model by theorems closed under best-first search with budget attempts × expansion × iterations and a timeout

Last edited: 2026-10-13