VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked the Algorithm 1 steps, equation 1, Lemma 2.1, the hyperparameters of Appendix A, every check lemma and hint in Appendix B and C, the quotations, page and section references, the figure readings and the Verus sketch; corrected the pass@5000 inference (Figure 3 shows about 0.5 and 0.14 on Dafny, not 0.4 and 0.1), the rollout-MCTS ablation credit (it also removes widen nodes), the prompt-statement claim, the Figures 3 to 6 reference, unsupported statements on Verus speed, verifier cost and comparison with Clover, a reworded future-work claim, a missing depth-limit case, and five unmarked inferences.

source: Brandfonbrener, Henniger, Raja, Prasad, Loughridge, Cassano, Hu, Yang, Byrd, Zinkov, Amin; arXiv:2402.08147v2 (24 May 2024), preprint, 18 pages: 10 of body, Appendix A to D on pp.13-18. Page numbers below are PDF pages.

the one idea

A program in Dafny or Coq is written top to bottom, one definition after another. The verifier can be run on the part written so far. If that part already fails, the authors argue nothing appended later can save it, so the search should drop it at once. If it passes, it is worth extending. VerMCTS builds a tree search around that single bit of information, with an LLM proposing the next chunk and no training of any kind.

proved, measured, trusted

Proved: Lemma 2.1 (p.5), a one-paragraph argument that the score the verifier gives a partial program is an upper bound on the expected best outcome reachable from it.

Measured: pass@T, the fraction of runs that reach a verified and checked program within T generated tokens, for T up to 5000, on 15 problems (9 in Dafny, 6 of them also in Coq), with Phind-CodeLlama-34B-v2 as the only model. All results are curves in Figures 3 to 5 (Figure 6 shows search-tree statistics and Figure 7 a hyperparameter sweep); the paper has no table of results and does not state the number of runs n per problem.

Trusted: Dafny and Coq as judges; the problem statement in English as the specification, since the model writes its own formal lemma statements; and a hidden check lemma per problem that ties the model’s lemma to the intended property (technique 5).

technique 1: score a partial program by verifying the prefix

What it is. A three-valued score for a program prefix. From the signature in Algorithm 1 (p.4): the verifier maps a string to −1, 0 or +1.

• 0: not scorable yet. Appendix C (p.18) gives the prefix datatype Expr = with nothing after it.
• +1: what is there verifies; it may be incomplete. Appendix C: the same datatype with one constructor Const(val: int) written.
• −1: verified as a failure. Appendix C: a complete Evaluate function over Expr that carries a reads env clause that should not be there.

When to use it. When programs are generated left to right in units that the verifier can check one at a time, and when a rejected unit cannot be repaired by later text. The paper states the property it relies on: “Beyond being noiseless, the verifier has one more important property: if a partial program fails the verifier, no subsequent completion can yield success.” (Section 2.2, p.4)

Steps, from Section 2.1 (p.3) and Section 2.2 (p.4):

1. A state is the user prompt plus the partial program. An action is one line in Dafny or one command ending in a dot in Coq, with a cap on tokens per action. The next state is the concatenation.
2. Run the verifier on the prefix.
3. If the prefix ends inside a unit that cannot be checked, return 0.
4. If the checkable part is rejected, return −1.
5. Otherwise return +1.
6. Reward exists only for complete programs: “This terminal reward is 1 if the complete program is accepted and -1 if it is rejected.” (Section 2.1, p.3)

Verus form. Inference: the unit is one item inside the verus! macro body: a spec fn, a proof fn, or an executable function with its requires and ensures. A prefix that ends in the middle of an item scores 0. A prefix of whole items is handed to Verus; any verification error in a finished item scores −1. Inference on what does not carry over: Rust resolves names regardless of order, so a finished function may call a spec fn or lemma that has not been written yet. That gives an unresolved-name error which a later item would fix, so the paper’s property fails for that error class. A Verus harness must either score unresolved names as 0 or tell the model to define before use and treat a forward reference as −1. Inference: the same holds for Dafny’s top-level declarations, and the paper does not discuss it; its prompts ask for definitions in dependency order.

Evidence. The ablation is the Rollout MCTS baseline, which replaces this technique and also the widen child (each node has a fixed 3 children, Appendix A, p.13), so it does not isolate prefix verification from widening; the paper has no ablation of widen nodes alone: “We expand by sampling a fixed number of actions k from the LLM and evaluate by rolling out with the LLM to a terminal node before querying the reward function.” (Section 4.3, p.6) In Figure 3 (p.7) the paper ranks the averaged curves as VerMCTS first, rollout MCTS second, whole sampling third, Reflexion last (Section 5.1, p.7). The paper prints no values for the rollout curve.

Where it fails. The authors name it: “However, the scoring is limited by coarse granularity and lack of lookahead in the scoring function.” (Section 7, p.9) For Dafny the scoring unit is a whole function, so a wrong first line of a function is found only at its last line. On the Appendix C failure the paper comments: “Unfortunately, we only confirm the error once the whole function is generated.” (Appendix C, p.18) For Coq the unit is a single command, which is fine-grained but does not help with longer proofs that need a plan (Section 7, p.9). Inference: a +1 says only that nothing is wrong yet; a function that verifies but is useless for the later lemma also gets +1.

technique 2: evaluate and maybe expand

What it is. One procedure that replaces the separate expand and evaluate steps of Monte Carlo tree search. It keeps asking the LLM for more text until the verifier can say something, and it adds a node to the tree only if the verdict is +1.

Steps, Algorithm 1 (p.4), with input a prefix s and a depth limit L:

1. Set score to 0, depth to 0, and the extension a to the empty string.
2. While score is 0 and depth is below L: append one LLM completion of s + a to a; set score to Verifier(s + a); add 1 to depth.
3. If score is −1, or depth reached L, return value −1 and no child.
4. Otherwise return value +1 and the child s + a.
5. If the child is a complete program that passes, the search ends with success (Figure 2, p.2).

The paper’s sentence for step 2: “Explicitly, from a node containing the string s we continue to extend a with the LLM until the verifier is able to return a valid score.” (Section 2.2, p.4)

Why not rollouts or a learned value. Rollouts cost many LLM calls, a value network needs training data, and both are noisy, whereas the verifier is exact and cheap next to the LLM (Section 2.2, p.4).

Verus form. Inference: a child node is the prefix extended by one or more whole verified items. Step 2 is: generate line by line until the item’s closing brace, then run Verus on the file. The depth limit L bounds how long one item may get. Inference: the paper counts only tokens and calls the verifier computationally cheap relative to the LLM (Section 1, p.2) without giving verifier times, so that claim has to be measured for Verus.

Where it fails or what it assumes. Inference: step 3 returns −1 when the depth limit is hit with the score still 0. That is not a verified failure, so in that case the value can be below the true value and Lemma 2.1’s proof, which treats every −1 as a certain failure, does not cover it. The same happens when the score becomes +1 only on the L-th completion, because the test is “score = −1 or depth = L”.

technique 3: a widen child instead of a fixed branching factor

What it is. Every node gets one extra child called widen, with value 0. Selecting it does not go deeper; it adds another real child to the same parent. The tree can therefore become as wide as needed at hard points and stay narrow at easy ones.

Steps, from Section 2.2 (p.3-4):

1. When a node is created, give it a widen child with value 0.
2. Select with the PUCT-style score of equation (1): score(s) = p_s · c_UCT · sqrt(log N_parent / N_s) + (sum of the values seen at s) / N_s, where N_s is the visit count.
3. Use prior p_s = 1.0 for ordinary nodes and p_widen below 1.0 for widen nodes.
4. If the selected leaf is ordinary, run evaluate-and-maybe-expand on it.
5. If it is a widen node, run evaluate-and-maybe-expand on its parent. “When the widen node w with parent s is selected, instead of adding a child to w, we add a child to s (i.e. add a sibling to w).” (Section 2.2, p.3)
6. Backpropagate the returned +1 or −1 to the root in the standard way. A failed expansion adds no node and still lowers the value of the path (Figure 1, p.2).
7. Stop on a complete verified program, or on the token or time limit.

The problem it solves, as the paper puts it: with a fixed k children per node, a small k can leave the search stuck when none of the k can be completed, and a large k wastes samples on easy parts (Section 2.2, p.3).

Settings found by sweep on one Dafny problem (Appendix A, p.13): temperature 1.0, exploration coefficient c_UCT = 3, widen prior 0.1. The rollout MCTS baseline uses 3 fixed children per node, temperature 0.8 and coefficient 1; Reflexion uses temperature 0.4; whole sampling 0.6. All use nucleus sampling with p = 0.95.

Verus form. Inference: nothing in the tree policy depends on the language. The values of c_UCT and the widen prior were tuned for a 34B open model on Dafny (the paper found performance fairly stable across the swept values, Figure 7, p.13), so they might need a new sweep.

Evidence. Figure 6 and Section 5.2 (p.8): node count grows roughly linearly with tokens, while depth grows early and then flattens. The authors read this as a search that first drives one branch to the end and widens afterwards. Figure 7 (p.13) shows the pass rate on the tuning problem is fairly stable across the swept values.

technique 4: the optimism argument

What it is. A justification for using +1 as the value of any prefix that has not failed. Lemma 2.1 (p.5): the value v(s) returned by Algorithm 1 is at least the expected optimal value of s + a over the extensions a that the LLM and verifier produce. The proof has two cases. If v(s) is −1 the extension is a certain failure and the two sides are equal. If v(s) is +1 it is the largest value any state can have, so the bound is immediate.

How to use it. Inference: treat the verifier as a pruning oracle, not as a ranking: the bound is tight only on the −1 side. Among surviving prefixes all the discrimination comes from backpropagated failures of their descendants and from visit counts. The authors’ hypothesis is that this extra optimism pushes the search deeper (Section 2.3, p.5).

Verus form. Not language-specific.

Limits. Inference: the lemma is true for any scoring that never underestimates, including one that always returns +1, so it does not by itself show that the verifier’s score is a useful guide. The empirical comparison with rollout MCTS carries that claim. The future-work paragraph (Section 7, p.10) calls the method a “blind” search that only uses scalar reward signal; it does not discuss this point about the lemma.

technique 5: a hidden check lemma to pin down what was proved

What it is. When the model writes both the lemma statement and its proof, a verifier pass shows only that some lemma of that name holds. The benchmark therefore appends a lemma with the intended statement whose proof is a single call to the model’s lemma. If the model’s statement is weaker or different, the appended lemma does not verify.

Steps, from Section 3.2 (p.5-6) and Appendix B (p.13-18):

1. In the prompt, fix the names of the functions and of the lemma, and for some problems the formal statement itself (for example Opt0 in B.5, p.16, and Factorial in B.6, p.17); other prompts give it in words.
2. Require the output to pass the verifier and some syntactic checks, for example a proof marker and a problem-specific minimum number of lines.
3. Append the check lemma to the verifier input only. “In order to check whether a model has proven a property, we inject a second lemma with it, and prove it by referring to the lemma we asked the model to write.” (Section 3.2, p.5)
4. Count success only if the combined file verifies.

The model never sees the check: “Note that the check lemma is only injected into the verifier input.” (Section 3.2, p.6)

The paper’s example for the factorial problem (Appendix B.6, p.17), in Dafny:

lemma CHECK_FacPositive(n: nat) ensures fac(n) > 0 { FacPositive(n); }

Verus form. Inference, a sketch that has not been compiled, for a model asked to write spec fn fac and proof fn fac_positive:

proof fn check_fac_positive(n: nat)
    ensures fac(n) > 0
{
    fac_positive(n);
}

Inference: this works in Verus because calling a proof fn brings its ensures into scope provided its requires holds, so a model lemma with an extra requires or a weaker ensures makes the check fail. The check also depends on the model having used the prescribed names and parameter order.

When to use it. Inference: for any task where the generator states its own theorem. It needs a human to have written the intended statement once; unlike Clover-style reconstruction, which this paper does not discuss, it calls no LLM.

Where it fails.

• It checks the lemma, not the definitions. Inference: if the model defines fac wrongly, for example as the constant 1, fac(n) > 0 still holds. The check for Opt0 (Eval(Optimize(e), env) == Eval(e, env), Appendix B.5, p.16) is satisfied by an Optimize that returns its input (inference). Inference: that is why Opt0 Opt adds an optimal predicate, but optimal is again model-written.
• The check lemma for the reverse problem is unfinished in the paper: Appendix B.8 (p.17) prints CHECK__reverse_permutes with a TODO comment and an empty body, so of the two requested properties only involution is checked.
• Appendix B.2 (p.14) prints, under the heading for Coq, a check lemma in Dafny syntax identical to the Dafny one.

technique 6: pass@T, success within a token budget

Steps, from Section 4.1 (p.6):

1. For each problem do n independent runs, each allowed up to T_max generated tokens, stopping a run early on success.
2. For each T up to T_max, mark each run 1 if it had succeeded within T tokens, else 0.
3. Report the mean over the n runs and a 95% Wilson interval: “In the results, we report the mean of these n binary variables and also 95% Wilson intervals [Wilson, 1927].”

Why. A tree search run costs far more than one sample, so pass@k would favour it unfairly; and tokens do not depend on hardware. “In contrast pass@T really estimates the dominant cost of generation, namely how many tokens need to be generated to yield success.” (Section 4.1, p.6)

Verus form. Inference: usable as is. For Verus it leaves out verifier time, which the paper calls cheap relative to the LLM; a fair Verus comparison would report verifier seconds beside tokens. It also counts generated tokens only, so a method that feeds long error messages back, as Reflexion does, is not charged for reading them.

what the experiments show

Setup (Sections 4.2 to 4.4, p.6-7): one base model, Phind-CodeLlama-34B-v2; four methods on top of it (VerMCTS, rollout MCTS, whole-program sampling repeated until the budget is spent, Reflexion with verifier errors shown to the model); hyperparameters tuned on the Dafny Opt0 problem and then fixed. For Coq only, the prompts carry syntax hints.

Numbers stated in the text:

• about a 30% absolute gain in average pass@5000 over whole sampling (abstract: more than 30% “across the suite”; Section 5.1, p.7, states it once, for both languages together)
• “This amounts to a 4x relative improvement on Dafny and on Coq, whole sampling does not even get a pass rate above 0 at this budget.” (Section 5.1, p.7)
• per problem, VerMCTS is the best method or within the margin of error (Section 5.1, p.8)
• “That said, some problems are clearly challenging: on one problem in Dafny and three in Coq, none of the algorithms find a solution within 5000 tokens.” (Section 5.1, p.8) So nothing solves 1 of 9 Dafny problems and 3 of 6 Coq problems at that budget.
• Reflexion is the weakest method. The authors offer three possible reasons: the model handles errors in low-resource languages badly, it handles the long Reflexion context badly, and Reflexion makes backtracking hard (Section 5.1, p.7).

The paper gives no per-method pass@5000 value in text. Reading Figure 3 (p.7) by eye at T = 5000, approximately: Dafny, VerMCTS 0.5, rollout MCTS 0.2, whole sampling 0.14, Reflexion 0.05; Coq, VerMCTS 0.29, rollout MCTS 0.19, whole sampling and Reflexion about 0. Inference: those readings are consistent with the 4x claim on Dafny and a gain of roughly 30 points on both.

things to read with care

• The tuning problem is in the test suite. “We tune hyperparameters on one particular problem (opt0) in Dafny, but only checking for verification and not additionally checking for correctness.” (Appendix A, p.13)
• The Coq hints are strong. For Opt0 they give the induction to use and the full tactic line for the addition case (Appendix B.5, p.16); for Factorial they name the two library lemmas for the base and inductive cases (Appendix B.6, p.17). Inference: the Coq results measure assembling a hinted proof more than finding one.
• Section 3.1 (p.5) says the suite has nine problems and a few lines later a total of 15; the 15 counts each language version. Three problems (Food, Days, Reverse) exist only in Dafny.
• Section 2.1 (p.3) introduces the MDP as a tuple of five objects and then says defining it consists of defining these four.
• The temperature sweeps for VerMCTS and rollout MCTS are printed as [0.6, 0.8, 1.0, 1.0, 1.4], with 1.0 twice (Appendix A, p.13).
• The number of runs n, the depth limit L and the per-action token cap are not given in the paper.
• One model from 2023. Inference: the weak Reflexion result may not hold for models that read verifier errors well; the paper itself lists that as the first possible reason.

already done, which VL should not redo

• Tree search over program prefixes with the verifier as the node filter, including the widen-node trick and the argument for why failures can be discarded.
• The comparison showing that, for a weak open model on small multi-definition problems, VerMCTS (prefix verification plus widen nodes) beats rollout MCTS, repeated whole-program sampling and error-feedback prompting at equal generated tokens.
• The check-lemma method of confirming that a model-stated lemma is the intended one.
• Inference: not done: the setting the authors mention as an adaptation, “Our technique can be adapted to a setting where the interfaces and specifications are given, and the code is verified at each step by additional code containing assertions or proofs.” (Section 7, p.9); any use of the error text inside the search; any language with loops, mutation or ownership; any accounting of verifier time.

threat to VeruLaw

Inference: low. This is a 2024 search method demonstrated on nine textbook problems with a 34B open model, in Dafny and Coq, with no Rust. It needs no training and is easy to reproduce, so it is a baseline anyone can run, and a reviewer of VL’s agent loop could reasonably ask how it compares with prefix-verified tree search at equal token cost. Its durable contribution to VL is the observation that a verifier verdict on an unfinished file is a free, exact pruning signal, plus the check-lemma guard against a generator that proves the wrong theorem.

techniques for the catalog

• prefix verification score: run the verifier on the program written so far and score it +1 if nothing fails, −1 if a finished unit fails, 0 if no unit is finished.
• failure monotonicity pruning: discard a failed prefix permanently because no later text can make it verify.
• evaluate-and-maybe-expand: extend a prefix with the LLM until the verifier can score it, and add it to the search tree only on +1.
• widen node: give every tree node a zero-valued child whose selection adds a sibling instead of a descendant, so width grows only where the search stalls.
• lower prior for widening: set the selection prior of widen nodes below that of ordinary nodes to prefer depth.
• optimistic value bound: treat every not-yet-failed prefix as having the maximum value and let backpropagated failures separate the branches.
• hidden check lemma: append a lemma with the intended statement that is proved by one call to the model’s lemma, and require the whole file to verify.
• syntactic success checks: require a proof marker and a minimum number of lines before counting a verified output as a solution.
• pass@T: report the fraction of runs that succeed within T generated tokens, with Wilson intervals, to compare methods of unequal cost per attempt.
• rollout-MCTS ablation: replace verifier scoring and widen nodes with fixed-k expansion and LLM rollouts to a complete program, to measure what the verifier-in-the-loop search adds.

Last edited: 2026-10-13