VerifiAgent: a Unified Verification Agent in Language Model Reasoning

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

scope and contribution

The paper presents VerifiAgent, a training-free verification agent for mathematical, logical, commonsense, and hybrid natural-language reasoning. Its stated mechanism is sequential: meta-verification checks structure, then adaptive tool verification checks task-specific correctness. The authors write: “VerifiAgent is a plug-and-play verification framework that empowers frozen LLMs to utilise external mechanisms to verify the correctness of solutions of diverse reasoning tasks.” (section 3, p. 3). The implementation uses a frozen backbone LLM and three external tools: a Python interpreter, a search engine, and a symbolic solver. The paper’s claim is that this combination gives generality and fine-grained feedback without task-specific verifier training.

The evaluation uses GSM8K (300 questions), MATH (350), FOLIO (204), ProverQA (300), StrategyQA (229), HotpotQA (200), and ReWild (491), as listed in Table 8 (Appendix A, p. 12). Unless stated otherwise, both reasoner and verifier use GPT-4o; alternative verifier experiments use o1-mini (section 4.1, p. 4). The authors report accuracy, precision, and recall, but do not report confidence intervals or statistical tests.

technique: two-layer verification

Use this when a generated answer must be checked for both internal reasoning quality and external computational or factual correctness. The paper’s definition is: “The first level is to do a Meta Verification, and the second level is to do a Tool-based Adaptive Verification.” (section 3, p. 3).

Steps from the paper:

1. Rewrite the solution in a unified form: first list all the known conditions and the final objective provided in the problem (section 3.1, p. 3). The prompt template requires Conditions: [...] and Objective: [...] (Appendix E, p. 20).
2. Divide the answer into explicit logical steps (section 3.1, p. 3; Appendix E, p. 20).
3. Check completeness: the answer is self-contained, addresses every part, and has a clear conclusion (section 3.1, p. 3; Appendix E, p. 20).
4. Check consistency by examining each transition from one step to the next for jumps, gaps, or inconsistencies (section 3.1, p. 3; Appendix E, p. 20).
5. If the structural check passes, select an external tool according to task type (section 3.2, p. 3). Section 3.2 gives the Python interpreter for verifying calculations in mathematical reasoning and a search engine for knowledge-based commonsense reasoning, and says hybrid tasks can combine tools. The pairing of a symbolic solver with logical reasoning comes from the prompt (Z3 Theorem Prover “excels at solving logical reasoning problems”, Appendix E, p. 20) and the tool-usage analysis (ProverQA used the symbolic solver 100% of the time, section 5, p. 8).
6. Execute the selected tool and inspect its result. The agent may make repeated calls and “autonomously determines the required number of external tool calls, continuing until it gathers sufficient information to validate the answer.” (section 3.2, p. 3).
7. Produce Correct or Incorrect, an error reason, and a revision method. Figure 1 specifies that the error reason identifies the erroneous step and the revision method explains how to avoid it (section 3, Figure 1, p. 4); the prompt adds that the revision method is summarised from the tool verification result (Appendix E, p. 22).

Inference: For Verus, the structural layer can be a prompt or proof-review checklist, while the tool layer should be replaced by compiling and running Verus plus inspecting solver obligations. The paper does not describe Verus. A Verus analogue would preserve explicit preconditions and postconditions in requires and ensures, preserve step decomposition as lemmas or proof blocks, and use assert/reveal and solver diagnostics instead of Python or a search engine. A spec fn should state mathematical conditions; executable Rust should perform the computation; proof functions should establish the relation. This transfer is an inference, not a reported result.

The paper’s worked mathematical example (Appendix E, pp. 13–15) first lists conditions and objective, then divides the solution into five explicit steps. Its worked ProverQA (logical reasoning) example exposes an unsupported implication (listening to one’s body leads to proper medical attention) by encoding it in Z3 and receiving Uncertain, after which the agent evaluates the answer as Incorrect (Appendix E, pp. 17–19). Its worked MATH example is on pp. 12–15, where the Python interpreter returns 12 where the candidate said 10. A Taco Bell StrategyQA example using the search engine is on pp. 15–17. This illustrates why structural plausibility alone is insufficient.

technique: meta-verification prompt decomposition

Use this when a candidate answer is long or its conclusion may hide omitted premises. The paper defines completeness as “a solution that is self-contained, fully addresses every part of the question, and contains a clear result or conclusion” and consistency as reasoning “that follows a logical structure with no jumps, gaps, or inconsistencies.” (section 3.1, p. 3).

The prompt’s concrete procedure is: list conditions and objective; split the answer into steps; verify that the final independent step contains the answer; then inspect each step-to-step transition (Appendix E, p. 20). The prompt says: “You should analyse the reasoning flow one by one, from Step 1 to Step 2, from Step 2 to Step 3, …” (Appendix E, p. 20). If the answer is incomplete, the prompt says there is no need to check logical consistency (Appendix E, p. 20).

Inference: In a Verus workflow, this decomposition corresponds to writing a lemma with explicit requires facts, a sequence of assert statements, and a final ensures target. Every assertion should be justified by the current context; an unsupported natural-language implication becomes an unproved assertion and should fail verification. The paper gives no Verus code, so this is an inferred mapping.

technique: adaptive external tool verification

Use this when the candidate’s correctness depends on arithmetic, factual retrieval, or satisfiability rather than only prose coherence. The paper states: “This level leverages external tools, such as Python program interpreter, search engine and symbolic solver, to cross-check the correctness of the solution.” (section 3.2, p. 3).

The paper’s tool instructions are operational. For Python: understand the problem, write a program, ensure it is clean and executable with no extra output, start with def solver():, and end with ans = solver() (Appendix E, p. 20). For Z3: import z3, encode variables and constraints, check satisfiability and both a constraint and its negation, and classify the constraint check as Agree, Contradict, unsolvable, or Uncertain (code template, Appendix E, pp. 20–21; worked example, pp. 18–19). For search: identify missing information, ask one clear question per call, and iterate until enough information is gathered (Appendix E, pp. 20–21). The agent then compares tool output with the candidate and revises its evaluation (section 3.2, p. 3; Appendix E, p. 21).

Inference: For Verus, arithmetic should be encoded as Rust expressions and checked by Verus’s SMT backend; factual claims require trusted specification or an external evidence pipeline because Verus cannot establish facts about the world. Logical alternatives can be represented as predicates and discharged with assert or lemmas. Search results must remain outside the proof’s trusted kernel unless converted into reviewed assumptions. This is an inference.

technique: confidence and feedback

VerifiAgent returns a binary evaluation plus a confidence score. The paper defines Vscore by applying softmax to the Correct/Incorrect token and the top five alternative-token log probabilities: “Vscore represents the confidence score for the verification result token t.” (section 3.3, p. 3). For solutions deemed incorrect, the feedback “includes the identified error reason, derived from the two levels of verification, and a potential revision method that incorporates observations from tool execution results” (section 3.3, pp. 3–4).

The authors test three feedback choices on cases initially marked incorrect: result only, result plus error reason, and result plus error reason plus revision method. They test precaution-based feedback (use feedback before generating a new solution) and post-editing feedback (edit the previous solution). Table 4 reports, for GPT-4o, initial MATH/ProverQA/StrategyQA accuracy of 69.4/75.3/84.3; precaution feedback with error reason 74.9/77.0/85.6; with mitigation method 73.4/77.6/86.0; post-editing with mitigation method 72.6/74.3/83.8 (Table 4, p. 6). The paper does not state the denominator for Table 4. Inference: the initial MATH and ProverQA values equal GPT-4o’s Table 3 values, so the table is probably over the full test sets (MATH 350, ProverQA 300, StrategyQA 229; Table 8, p. 12); the initial StrategyQA value is 84.3 in Table 4 but 84.2 in Table 3. The paper’s text says: “Overall, precaution-based feedback consistently outperforms post-editing-based feedback”, and that for post-editing, richer feedback helped math but simpler feedback was better for logic and commonsense (section 4.4, p. 7).

Inference: A Verus service could expose proof diagnostics as structured error locations and repair suggestions, but a confidence score must be treated as heuristic metadata, not proof evidence. Verus acceptance, with its solver and axioms, is the evidence-bearing result; token probabilities remain untrusted.

evidence and limits

Table 2 compares VerifiAgent with vanilla, deductive, and backward verifiers. On the stated datasets, VerifiAgent accuracy/precision/recall are GSM8K 0.96/0.96/1.00, MATH 0.85/0.86/0.92, FOLIO 0.76/0.78/0.97, ProverQA 0.77/0.82/0.95, StrategyQA 0.84/0.85/0.95, HotpotQA 0.61/0.56/0.92, and ReWild 0.78/0.88/0.89 (Table 2, p. 5). VerifiAgent is not best in every column: for example on ReWild precision the Deductive Verifier has 0.91 against 0.88, and on ProverQA recall the Deductive Verifier has 0.98 against 0.95 (Table 2, p. 5). The paper does not state a single shared denominator in Table 2; dataset sizes are in Table 8.

For inference scaling, Table 3 reports average samples in parentheses. GPT-4o with VerifiAgent (GPT-4o) reaches MATH 74.0 with 1.5 samples versus majority vote 73.5 with 10; with o1-mini it reaches 78.0 with 1.8. On ProverQA the corresponding values are 77.3 with 1.6, 77.7 with 1.3, versus 77.0 with 10; on StrategyQA 86.0 with 1.3 and 87.3 with 1.2, versus 85.6 with 10 (Table 3, p. 6). Table 10 reports average dollar cost per instance, including reasoner and scaling method; for GPT-4o on MATH, majority vote costs $0.175whileVerifiAgentGPT-4ocosts$0.047 and o1-mini costs $0.051 (Appendix D, p. 12). On ProverQA the costs are similar (0.025 for majority vote against 0.024 and 0.028), as the paper notes (Appendix D, p. 12). Inference: these are model- and setting-specific results, not a general cost guarantee, and the accuracy gaps over majority vote with the GPT-4o verifier are small on ProverQA (77.3 against 77.0) and MATH (74.0 against 73.5).

Ablation in Table 7 removes each layer. On MATH, full VerifiAgent is 0.85 accuracy, removing meta-verification gives 0.79, and removing tool verification gives 0.75; on ProverQA the values are 0.77, 0.74, and 0.74; on StrategyQA 0.84, 0.83, and 0.78 (section 4.6, Table 7, p. 8). The authors report that tool verification tends to improve accuracy and precision while meta-verification primarily improves recall (section 4.6, p. 8).

Inference: the trusted base of the method includes the backbone LLM’s instruction following, external-tool implementations and outputs, the symbolic solver’s correctness, dataset labels, and the prompt’s mapping from tool observations to Correct/Incorrect. The authors state: “VerifiAgent heavily relies on the instruction-following capabilities of the backbone LLM” and that it “currently supports only three verification tools” (end of section 6, p. 9). Their Limitations section names representative-model selection caused by LLM cost and the three-tool set (p. 9). VerifiAgent’s accuracy on tool-use outputs is lower than on chain-of-thought outputs in Table 6 (p. 7), and the authors say it “is not designed specifically for program or tool-use evaluation” (section 4.5, p. 8).

Inference: For a product that generates agent-written verified Rust, this work is a moderate threat to orchestration and triage, not to kernel-level proof guarantees. It could select proof-checking tools, detect incomplete explanations, and prioritize repairs, but it cannot replace Verus checking or establish properties outside encoded specifications. VL should reuse the explicit two-layer decomposition, iterative tool calls, and structured error feedback; it should not redo the paper’s benchmark comparison or treat Vscore as a soundness certificate.

techniques for the catalog

• two-layer verification — first check completeness and consistency, then cross-check with a task-appropriate external tool
• meta-verification decomposition — turn conditions, objective, and answer into explicit steps and inspect every transition
• adaptive tool selection — choose Python, search, symbolic solving, or a combination from the reasoning type
• iterative tool calls — continue tool interactions until evidence is sufficient for evaluation
• structured feedback — return result, error reason, and revision method for a new attempt
• verifier confidence — compute a normalized token score as heuristic confidence, separate from proof evidence
• verifier-guided inference scaling — sample candidates and stop on a verified answer, falling back to majority vote at a sample cap Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Since Vscore represents the confidence of the verification result, this indicates that the VerifiAgent is more confident when identifying correct solutions compared to incorrect ones.”): I read the whole paper text including the appendix and checked every quotation, number (Tables 2, 3, 4, 7, 8, 10, Table 6 direction), page and section reference, and the technique steps against it. Changed: the Appendix E page citations (the meta-verification prompt quote is on p. 20, search instructions on pp. 20–21); the worked example labelled commonsense is the ProverQA logical example; tool pairing for logic now cites the prompt and section 5; consistency is “inconsistencies”, not “contradictions”; unsolvable is lowercase in the code; the “derived from both layers” claim now follows the paper (error reason from both layers, revision method from tool observations, pp. 3–4); the Table 4 denominator is now marked Inference and the 84.3 versus 84.2 StrategyQA mismatch noted; the limitations quotes are at the end of section 6 and in the Limitations section, not section 5; added that VerifiAgent is not best in every Table 2 column; the trusted-base sentence is marked Inference. Not checked: external sources, the cited related work, Appendix B and Figures 5–7 in detail, the linked code, and the arXiv v2 link beyond the arXiv identifier printed on the paper (2504.00406v2).

Last edited: 2026-10-17