AdverMCTS: Combating Pseudo-Correctness in Code Generation via Adversarial Monte Carlo Tree Search

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

central technique

AdverMCTS couples a Solver that generates code with an Attacker that searches for tests exposing hidden bugs. The paper defines pseudo-correctness as solutions that “overfit the visible public tests but fail to generalize to hidden test cases” (Abstract, PDF p. 1); Fig. 7 labels such codes “pass public, fail hidden” (p. 8). Its abstract says: “we propose A DVER MCTS, a novel adversarial Monte Carlo Tree Search framework that combats pseudo-correctness by coupling code search with active vulnerability discovery.” (Abstract, PDF p. 1). The paper frames this as a minimax-style game between Solver and Attacker.

Inference: for Verus, the analogous attack is generating counterexamples to candidate specifications, invariants, and abstraction boundaries before trusting a proof. The paper’s execution tests remain finite evidence, not a universal theorem.

technique: solver MCTS with strict admission

The Solver tree starts at the problem (root s0 = P); each node is a partial chain-of-thought. It runs Selection, Expansion, Simulation/code synthesis, and Backpropagation (Sec. 3.3, PDF p. 3). Selection uses a UCB-style rule over value Q, an LLM prior P, and visit counts (Eq. 1, p. 3; cpuct = 4, Sec. 4.1, p. 5). Expansion samples k next thoughts from the LLM; simulation completes each new thought into a full code candidate. A candidate enters the shared Code Pool only if it passes the public tests Tpub and the accumulated global adversarial suite Tglobal (Sec. 3.3, p. 3).

The reward combines public pass rate Rpub and an adversarial penalty. If a candidate is later found to fail a global or newly generated test, a penalty −V is applied to the Solver node, and values of nodes along the trajectory are updated (Sec. 3.3, p. 3); V = 0.1 (Sec. 4.1, p. 5). Algorithm 1 gives the admission steps: evaluate on Tpub; require rpub=1.0 and PASS ALL(C,Tglobal); add to Cpool, removing the “oldest/lowest-score code” when |Cpool| > Kmax (Appendix E, PDF p. 17).

How to apply it. (1) Initialize a Solver tree at the problem and an empty code pool and empty global test filter (Algorithm 1, p. 17). (2) Select and expand a Solver node. (3) Generate a complete candidate and run public tests. (4) Admit it only if it passes all public tests and all current global tests. (5) Let attacker penalties reduce values of Solver nodes of codes later exposed by a new test. (6) Final-rerank candidates by pass rate on public tests, then on global tests (Sec. 3.6, p. 5; Algorithm 1, p. 17).

Verus form. Inference: a Solver node can contain a candidate Rust implementation plus its requires/ensures; strict admission should require successful Verus verification and all executable regression tests. An Attacker-generated counterexample should become a failing test or proof obligation. Use proof fn, assert, and loop invariant declarations only in valid Verus syntax; a confidence or MCTS value cannot replace a proof result.

technique: attacker MCTS and divergence-driven test synthesis

The Attacker keeps a persistent tree whose root is the problem plus the current code pool, {P, Cpool}; the tree is retained across iterations and search resumes from it when the pool reaches a certain capacity (Sec. 3.4, PDF p. 4). Algorithm 1 runs the Attacker only when |Cpool| ≥ 2 (p. 17). At a selected attacker thought, the Attacker expands a testing strategy such as “Check boundary condition for N = 0” or “Test with large prime inputs” (Sec. 3.4, p. 4), aimed at specific vulnerability types “rather than random fuzzing”. It then generates a batch of k candidate tests conditioned on (P, Cpool, σnew). Multi-sample generation reduces variance of generation (Sec. 3.4, p. 4).

Tests are scored by output divergence: Rdiv(T)=I[∃i,j:Oi(T)≠Oj(T)]·wdiv (Eq. 2, Sec. 3.4, p. 4), where wdiv normalizes by the number of unique outputs. The most discriminative test in the batch is selected, and its reward is backpropagated up the Attacker tree. Divergence cannot detect the case where all candidates agree on the same wrong output, which the authors state explicitly (Sec. 3.4, p. 4). Algorithm 1 also applies a divergence threshold θthresh before the arbiter is called (p. 17).

When candidates disagree, an LLM Output Arbiter reads the problem, test input, and divergent outputs, and returns an expected output and a validity flag (Eq. 3, Sec. 3.5, pp. 4–5). Ambiguous or invalid tests are discarded. Valid (test, expected output) pairs enter the global filter; codes that produced incorrect outputs get a penalty −V on their Solver nodes (Sec. 3.5, p. 5).

How to apply it. (1) Keep a persistent attacker tree and current candidate pool. (2) Select a vulnerability thought using MCTS. (3) Generate multiple tests conditioned on the pool. (4) Execute candidates and keep the test with highest output divergence. (5) Ask an arbiter to determine expected output and validity. (6) Add valid tests to the global filter and penalize failing candidates. (7) Backpropagate divergence reward into the attacker tree (Secs. 3.4–3.5, pp. 4–5).

Verus form. Inference: generate boundary inputs, malformed states, and model-vs-implementation comparison cases. For each candidate, execute bounded tests and ask Verus to prove the universal contract; a disagreement is a counterexample-guided repair signal. The arbiter’s expected value is trusted input unless independently proved by a reference model. Verus can encode the reference as a spec fn and prove equivalence with ensures; it cannot infer the intended specification from disagreement alone.

evidence and limitations

Experiments use APPS and TACO, 100 problems per split, with at most five public tests per problem (|Tpub| = 5); robust correctness is pass rate and pass@1 on hidden tests (Sec. 4.1, PDF p. 5). Backbones are Qwen3-4B-Instruct-2507 and Qwen3-8B for both agents, plus DeepSeek-V3.2 in a scaling experiment; the maximum interaction depth is 16 rollouts and the Attacker uses N = 2 rollouts per iteration (Sec. 4.1, p. 5).

Table 1 (Qwen3-4B-Instruct, p. 6) reports AdverMCTS pass@1: APPS Intro 61, Interview 52, Competition 36 (average 49.67); TACO Easy 55, Medium 37, Hard 22 (average 38.00). The strongest baseline there, RethinkMCTS, has APPS average 43.67 and TACO average 33.67. With Qwen3-8B, AdverMCTS gets APPS average 36.00 and TACO average 28.00, against RethinkMCTS 31.67 and 25.33. Table 2 (p. 8) repeats the full-method row (61.0, 52.0, 36.0, avg 49.7; 55.0, 37.0, 22.0, avg 38.0; backbone not named there, identical to the Table 1 4B-Instruct row). Removing Solver Context lowers averages to 46.0 and 34.7; Best-of-N gives 45.7 and 34.0; Random-MCTS gives 43.7 and 32.3 (Table 2, PDF p. 8). The module ablation (Fig. 4, Sec. 4.4, pp. 6–7) reports that removing the Attacker tree (AT-Tree) gives the largest drop.

In the attacker discrimination analysis (Fig. 7, PDF p. 8) 291 pseudo-correct codes are examined: 165 are killed (recall 56.7%) and 126 survive. In the true-correct group, 44 are mis-killed (false-positive rate 16.1%) and 230 survive; precision is 78.95%. Inference: the true-correct total of 274 is my sum of 230 and 44 from the figure, and 44/274 = 16.1% and 165/(165+44) = 78.95% reproduce the paper’s rates.

The arbiter comparison reports labeled-test validity on TACO (measured against gold code) of 79.88% versus 37.88% for majority voting; downstream APPS average pass@1 is 49.67 versus 43.67, and TACO average is 37.33 versus 32.67 (Table 3, PDF p. 8). The paper’s own TACO average for the full method is 38.00 in Tables 1 and 2 but 37.33 in Table 3, and TACO-Hard is 22.0 in Table 1 but 20.0 for the re-ranking row of Table 4 (Appendix C.2, p. 14); the paper does not explain these differences. The conclusion says: “By coupling a Solver MCTS with an active Attacker MCTS, A DVER MCTS constructs a progressively hostile environment that co-evolves with the solution candidates.” (Conclusion, PDF p. 8).

Further reported results: at similar token budgets AdverMCTS gets higher pass@1 than MCTS-Thought, and N = 16 rollouts beat the baseline at N = 32 with fewer tokens (Fig. 5, Sec. 4.5, p. 7). Appendix C.2 (Table 4, pp. 13–14) finds that using adversarial tests as a hard re-ranking filter beats a soft continuous penalty (for example APPS Intro 61.0 vs 57.0). Appendix C.3 finds an inverted-U effect: Attacker rollouts from 1 to 2 help, more can hurt (Fig. 9, p. 14). Appendix C.1 (Fig. 8, p. 13) reports that MCTS-Thought with Qwen3-4B-Instruct improves from 43.44% to 55.33% pass@1 on APPS and from 31.00% to 43.67% on TACO when the full hidden test suite is used as verification, which the authors read as evidence that sparse public tests are the bottleneck.

What is measured is hidden-test correctness, adversarial-test discrimination, labeled-test validity, and token/cost tradeoffs. Trusted components include hidden test labels, the arbiter, execution engine, public tests, and code-generation model. Output divergence misses unanimous wrong candidates; an arbiter can mislabel a test; public and global suites remain finite; and the search does not prove semantic correctness for all inputs.

Inference: threat to agent-written verified Rust is high for specification overfitting and medium for proof search. VL should reuse adversarial candidate generation, persistent counterexample suites, strict admission, and penalty feedback. It should not treat adversarial tests as a substitute for Verus’s universal proof, nor redo generic MCTS if a direct proof obligation is already discharged. The paper’s Appendix C.1 gives test-side evidence for the pseudo-correctness problem in code generation; VL’s open question is whether adversarial specification mutation finds missing postconditions without weakening accepted contracts. The paper does not evaluate Verus, Rust, specifications, or proofs.

techniques for the catalog

• solver MCTS — search code candidates with selection, expansion, simulation, and feedback backpropagation (Inference: proof candidates for Verus)
• strict candidate admission — retain only candidates passing public and accumulated adversarial checks
• attacker MCTS — search targeted vulnerability strategies conditioned on the current candidate pool
• divergence-driven multi-sample tests — generate batches and score inputs that make candidate outputs disagree
• arbiter-labeled counterexamples — adjudicate expected outputs and discard ambiguous tests before adding them
• persistent global test filter — accumulate hard cases and penalize every candidate that fails them
• hierarchical test reranking — select final candidates by public pass rate, then global pass rate Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “the active “purification” of the search space via adversarial counter-examples proves to be more compute-efficient than brute-force scaling of reasoning paths.”): read the whole paper text, including the appendices and Algorithm 1, and checked every quotation, number, equation, section and page reference, and technique step against it, with the Fig. 7 counts checked on the rendered page image; changed the abstract quotation (it was not word for word), moved Table 2, Fig. 7, Table 3 and the conclusion from p. 7 to p. 8, corrected “five public tests” to a maximum of five, attributed the main AdverMCTS per-split figures to Table 1 (p. 6) instead of Table 2, added backbones, budgets, the |Cpool| ≥ 2 and θthresh details, the Fig. 7 survivor counts, the paper’s own number inconsistencies, and appendix findings, and marked my own derivations as Inference; did not check the cited related work, the anonymous code link, the prompts in Appendix D beyond reading them, or any Verus claim, which are my inferences and not in the paper.

Last edited: 2026-10-17