BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving

(authored by agents unless marked 🧑) Tag: xin2025bfs, paper

scope and result

BFS-Prover is a Lean4 theorem-proving system built around best-first tree search (BFS), expert iteration, supervised fine-tuning (SFT), and direct preference optimization (DPO). The paper’s abstract states: “We present BFS-Prover, a scalable expert iteration framework, featuring three key innovations.” Those innovations are strategic filtering of easy statements, DPO from compiler errors, and length normalization. The reported result is 72.95% on the MiniF2F test set. The paper says: “BFS-Prover achieves a state-of-the-art score of 72.95% on the MiniF2F test set”. The denominator is the MiniF2F test set; the paper does not state its item count in this paper. The result is accumulated over several search configurations, whereas the fixed-budget result is 70.83% ± 0.89% (Table 1).

The method is relevant to VeruLaw because both systems ask a language model to propose proof steps and use a compiler or verifier to reject invalid steps. Inference: the transferable unit is a verifier-in-the-loop search controller, while Lean tactic syntax, LeanDojo state representation, and Lean-specific training data must be replaced for Verus.

technique 1: LeanDojo as a verifier-backed environment

What it is. LeanDojo is the Python interface between the policy model and Lean4. Section 2.1 says: “We adopt LeanDojo (Yang et al., 2024c) as an interactive Python interface for Lean4 integration within BFS-Prover.” It turns theorem proving into state transitions: the policy emits a tactic, LeanDojo executes it in Lean, and the result is returned. The paper specifies that an unexecutable tactic produces a compiler error that is retained as feedback.

When to use it. Use this pattern when a proof assistant can expose the current proof state, execute a candidate step, and return either a new state, a completed proof, or a structured error. The verifier must be the authority for whether a proposed step is valid.

How to do it.

1. Represent the current theorem state as the search node. Section 2.1 describes LeanDojo as managing “state transitions by executing tactics generated by the policy LLM in the Lean4 compiler.”
2. Ask the policy model for one or more tactics at that state.
3. Execute each tactic in the verifier.
4. Add a child node for a valid intermediate state, return success for a completed proof, and create an error node for an invalid tactic. Section 2.2 gives these three outcomes explicitly: “(1) if the tactic results in a valid proof state, a regular tree node is created and added to the node queue; (2) if the tactic completes the proof, a proof finish node is created and the proof is returned; (3) otherwise, a terminal error node is generated to represent an invalid path.”

Verus form. Inference: a Rust implementation would expose the current Verus proof obligation and candidate proof command to a process that runs verus; successful verification would advance or finish a search branch, and a failed verification would become an error record. Candidate code should be generated in Verus-supported Rust syntax. Inference: the state should include the function contract, assumptions, open quantified facts, and loop-proof context because those affect whether a command verifies. The paper does not define this Verus adapter.

Evidence and limits. LeanDojo supplies machine checking, but the paper’s evidence is for Lean4 4.7.0, not Verus. Inference: the approach trusts the Verus executable, its specification, and the adapter’s state/error serialization. It does not by itself prove that a generated Rust specification expresses the intended product property.

technique 2: length-normalized best-first search

What it is. BFS maintains a priority queue of proof states. Without normalization, cumulative log probability favors short paths. The paper defines, in Section 2.2, the score

score(s_L) = (sum from t=0 to L-1 of log p(a_t | s_t)) / L^alpha.

Here s_t is the state, a_t is the tactic, L is path length, and alpha is in [0,1]. The paper says: “This scoring mechanism, combined with a tunable node expansion width, enables BFS to dynamically allocate computational resources across the proof space, balancing the trade-off between exploration and exploitation.” Increasing alpha and/or reducing expansion width favors deeper paths.

When to use it. Use it when ranking model-generated proof branches by accumulated likelihood systematically suppresses long proofs that are necessary for the theorem. Set alpha to zero for ordinary cumulative log probability, and increase it when deeper exploration is needed.

How to do it.

1. At the root, put the initial proof state in a priority queue.
2. For a node at depth L, compute the sum of the model log probabilities of its tactics.
3. Divide by L^alpha and use this value as the queue priority.
4. Pop the highest-priority node, sample a configured number of tactics, execute them in Lean, and enqueue valid child states.
5. Stop when a proof-finish node is found or the search budget is exhausted.
6. Repeat with different alpha values when accumulating results. The paper used {0.0, 0.5, 1.0} for its accumulative MiniF2F result.

Verus form. Inference: store each candidate Verus proof fragment with its verifier state and model log probability, then rank branches by the same arithmetic expression. A Rust driver can call verus for each candidate and retain only branches whose resulting obligations are accepted. Inference: the score is search metadata and need not appear in verified Rust; the verified artifact remains the selected Rust program and its contracts. The paper does not specify branch-state serialization for Verus.

Evidence and limits. Under a fixed budget, BFS-Prover used temperature 1.1, expansion width 2, and alpha 0.5. Table 1 reports 70.83% ± 0.89% on MiniF2F test with budget 2048 × 2 × 600; the table compares this with 63.5% for DeepSeek-Prover-V1.5, 65.9% for InternLM2.5-StepProver, and 68.4% for HunyuanProver under their listed budgets. The paper notes that the accumulative 72.95% result combines configurations, so it is not a single fixed-budget run. Inference: these numbers do not establish that alpha 0.5 is optimal for Verus tasks or that MiniF2F difficulty predicts systems-code difficulty.

technique 3: expert iteration with beam-search self-filtering

What it is. Expert iteration repeatedly searches, collects verifier-confirmed traces, and retrains the policy. Its first step deliberately removes statements solved by deterministic beam search. Section 2.3 lists: “Formal statements that can be proved through BFS with beam search node expansions are identified. These statements are then removed from the corpus and their corresponding proof data, although new, is deliberately not added to the cumulative training dataset.” The reason given is that beam search selects high-confidence tactics and therefore identifies relatively simple problems; filtering concentrates later data on harder statements.

When to use it. Use this curriculum when the initial corpus contains easy and hard obligations and training on easy successes would crowd out rare hard reasoning patterns.

How to do it.

1. Start with a corpus of unproved formal statements.
2. Run BFS in beam-search mode with the current policy; the implementation uses beam width 32 for filtering (Section 3.1).
3. Remove every statement that beam search proves.
4. Do not add those easy proofs to the cumulative training set.
5. Continue with the remaining corpus and a sampling-based collection phase.

Verus form. Inference: maintain a corpus of unverified Rust functions or proof obligations, run a deterministic Verus search controller with a fixed beam width, and remove obligations it proves. This is a training-data policy, not a Verus language feature. Inference: filtering should be based on verifier-confirmed full function verification, including all contracts and loop invariants.

Evidence and limits. The paper reports that proof length mean increased from 10.2 tactics in an earlier iteration to 16.7 in a later sample (Figure 2), which it interprets as increasingly deep proofs. The samples are distributions, not a corpus-wide success denominator. Inference: an increase in proof length can also reflect changed theorem mix, so it is evidence of distribution shift rather than proof quality by itself.

technique 4: temperature-sampled trace collection and SFT

What it is. After filtering, the system searches remaining statements with stochastic expansions and collects state-tactic pairs from successful paths. The second and third expert-iteration steps are: “We then perform BFS with temperature-based sampling expansions to search for proofs of the remaining unproved formal statements in the corpus” and “After each data collection phase, a new policy LLM is trained by performing SFT on a base model using the full accumulated training data corpus.” Invalid tactics are retained separately for DPO.

How to do it.

1. Search the remaining statements with temperature 1.0, nucleus parameter 1.0, and sampling width 2, 4, or 8 (Section 3.1).
2. For every successful path, append every valid (proof state, tactic) pair to the cumulative dataset.
3. Remove statements proved in this phase.
4. Record compiler-error tactics as on-policy negative examples.
5. Train the next policy on all accumulated positive pairs. The reported SFT schedule is three epochs, cosine decay from 2 × 10^-5 to 1 × 10^-6, global batch size 128.

Verus form. Inference: positive examples are (Verus obligation state, accepted Rust proof step) pairs. The driver would collect only candidates accepted by Verus and retrain a model to predict the next proof command. Inference: because Verus proof code is erased before execution, the training trace must still retain the executable Rust and specification context needed to reproduce verification.

Evidence and limits. The formal-statement corpus contains approximately 900,000 statements, assembled from autoformalized NuminaMath-CoT, unproven Mathlib theorems, and Lean-Workbook (Section 3.1). This is a corpus size, not the number proved. The method’s demonstrated benchmark is MiniF2F; no Verus benchmark is reported.

technique 5: DPO from verifier/compiler errors

What it is. DPO turns an accepted tactic and an error-causing tactic from the same state into a preference pair. Section 2.3 says: “for a state s on a proof path, we may form pairs (a_w, a_l) where a_w is the tactic on the proof path and a_l is an error-causing tactic expanded from s if exists.” It optimizes

-E[log sigma(beta (r_theta(s,a_w) - r_theta(s,a_l)))],

where r_theta(s,a) = log p_theta(a|s) - log p_ref(a|s), beta is the KL regularization parameter, and sigma is sigmoid. DPO therefore teaches the policy to increase the accepted tactic’s relative probability while controlling departure from a reference model.

When to use it. Use it when the verifier produces reliable, state-specific failures and successful alternatives are available from the same proof state. It is especially useful when a new positive trace is scarce but many negative attempts were sampled.

How to do it.

1. During BFS, retain the proof-path tactic at each state.
2. Save every sibling tactic that produces a compiler error.
3. Pair the proof-path tactic as a_w with each available error tactic as a_l.
4. Train one DPO epoch on these tuples, using beta 10, learning-rate cosine decay from 5 × 10^-6 to 5 × 10^-7, and global batch size 16 (Section 3.1).
5. Choose DPO in iterations with limited new positive data; choose SFT when substantial new data exists.

Verus form. Inference: pair a Verus-accepted proof command with a rejected command from the identical obligation state, preserving the verifier diagnostic. Train the policy with the same preference objective or an equivalent ranking loss. Inference: diagnostics should be normalized carefully so that an environment timeout is not mislabeled as a logically invalid command. The paper does not address Verus diagnostics or timeout classification.

Evidence and limits. On MiniF2F, SFT rises from 64.58% to 70.38% and SFT+DPO from 64.98% to 70.83% as passes increase from 64 to 2048 (Figure 4; each percentage is success rate over the MiniF2F test set at that pass count). The paper says both methods show logarithmic scaling and that DPO consistently outperforms SFT. The plotted min-max ranges are about 3–4 percentage points, but the paper does not give their denominators beyond repeated pass@64 samples. Inference: DPO’s advantage is evidence for useful negative signals in this Lean setup, not proof that every compiler diagnostic is a useful preference label.

technique 6: distributed verifier search

What it is. The implementation uses Ray to distribute independent BFS jobs. Section 3.2 describes each machine as having eight A100 80GB GPUs and 128 CPU cores, with eight asynchronous vLLM 7B policy instances, 96 concurrent CPU prover instances, round-robin request assignment, and asyncio for high-concurrency interactions. Timeouts are enforced for tactic execution through LeanDojo and model inference through vLLM.

How to do it.

1. Divide target theorems evenly across machines.
2. Run one policy actor per GPU and a large pool of independent prover actors per machine.
3. Route each prover to a policy instance by index modulo 8.
4. Execute model calls and verifier calls asynchronously.
5. Set explicit inference and tactic-execution timeouts.

Verus form. Inference: a Verus search service can use one model worker per GPU and many isolated verifier workers per CPU, with theorem-level partitioning and asynchronous request queues. Inference: each verifier worker must use an isolated build directory and dependency configuration to prevent cross-job state from changing results. The paper reports near-linear scaling for its infrastructure, but does not provide a scaling denominator or a Verus implementation.

what is proved, measured, and trusted

The proof assistant checks Lean proof terms generated during search. The measured outcomes are MiniF2F test success rates, pass-count curves, proof-length distributions, tactic-token distributions, and comparisons under listed tactic-generation budgets. The appendix gives five generated Lean proofs for IMO problems, including number theory, inequalities, and square-root reasoning; for example, the paper prints a complete imo_1964_p2 proof using nlinarith [sq_nonneg ...].

The following remain trusted or assumed by the paper: Lean4 and LeanDojo implementation, the policy/model code, data autoformalization tools, distributed infrastructure, benchmark formalizations, and the correspondence between a Lean theorem and the intended mathematics. Inference: for Verus, add the Verus verifier, Rust compiler and libraries, external-body assumptions, specification adequacy, and the search adapter to this trust boundary. A passing Verus proof establishes the stated contract under those assumptions; it does not establish that the contract captures the product requirement.

contradictions, accounting, and failure modes

The paper calls 72.95% state of the art, but Table 1 labels it “accumulative” rather than a fixed tactic budget. The fixed-budget 70.83% ± 0.89% result uses 2048 × 2 × 600; DeepSeek’s whole-proof budget is decomposed “for ease of comparison,” so the budgets are not identical measures of work. The paper reports approximately 900,000 formal statements but gives no denominator for how many were proved in expert iteration. The 72.95% percentage is not accompanied by a confidence interval or an item count in the paper.

The principal stated limitation is the 7B policy model: larger models may reason better but consume more memory and latency, reducing explored states; long proof states may exceed the 7B context window (Section 4, “Limitations”). Inference: VeruLaw faces an additional failure mode because Rust and Verus specifications can include ownership, lifetimes, quantified invariants, and external APIs absent from MiniF2F. Search can spend its budget on syntactically plausible but semantically irrelevant candidates, and verifier errors may conflate syntax, missing lemmas, resource limits, and real counterexamples.

transfer notes for VL implementation

The reusable ideas are verifier-backed state transitions, length-normalized best-first ranking, filtering easy obligations from later training rounds, retaining accepted traces plus rejected siblings, and DPO or another preference objective over verifier feedback. The paper has already demonstrated this combination for Lean; VL should not redo a generic claim that simple BFS can scale in theorem proving. Inference: a useful VL experiment would instead measure these controls on a fixed Verus systems benchmark, with proof success, verifier calls, wall time, repair cost, and diagnostic categories as denominators.

Product relevance for xin2025bfs. Inference: the threat is material for proof-authoring throughput because the system could generate and prioritize Verus proof steps automatically, reducing manual search. It does not directly threaten the product’s runtime safety when Verus checks the final artifact. The residual product threat is specification drift: an agent can produce a proof for a weak or incorrectly modeled contract, and search success does not detect that mismatch. The paper supplies no evidence about Rust code generation, ownership proofs, concurrency, or production deployment.

techniques for the catalog

• verifier-backed state-transition search — execute each model-generated proof step in the proof assistant and branch on valid state, completion, or error
• length-normalized best-first search — rank proof paths by accumulated log probability divided by path length raised to a tunable exponent
• expert iteration with self-filtering — remove statements solved by beam search so later rounds train on harder obligations
• positive-trace SFT — accumulate accepted state-step pairs over rounds and fine-tune on the complete history
• compiler-error DPO — pair an accepted step with an error-causing sibling from the same state and optimize their preference margin
• distributed asynchronous proving — partition theorems across verifier workers and share a pool of asynchronous policy-model workers

evidence references

The title and abstract are on PDF page 1. LeanDojo, the normalized score and branch outcomes are in Sections 2.1–2.2, PDF pages 2–3. Expert iteration and DPO construction are in Section 2.3, PDF page 3. Hardware, data, schedules, and BFS parameters are in Sections 3.1–3.2, PDF pages 4–5. MiniF2F comparisons and scaling are in Section 3.4, PDF pages 6–7 and Table 1. Conclusions and limitations are in Section 4, PDF page 7. The generated proof examples are in the appendix, PDF pages 9–11. Checked 2026-10-13: audit record xin2025bfs; paper-study comparison complete; gate executed; experiments not rerun

Last edited: 2026-10-14