Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Step-Wise Formal Verification for LLM-Based Mathematical Problem Solving

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

framework and scope

MATH-VF verifies natural-language mathematical solutions one reasoning step at a time. It has an LLM Formalizer that translates a problem and solution into SimpleMath, then a Critic that checks each formal judgment with reasoning plus SymPy and Z3. The paper’s central claim is that “MATH-VF not only evaluates the correctness of solutions, but also provides constructive feedback for incorrect ones.” (section 1, p. 3) It evaluates three tasks: determining whether one solution is correct, selecting a correct solution from candidates, and refining an incorrect solution (section 4, p. 7).

This is verification of mathematical reasoning, not Rust verification. Its transferable idea is a formalize-then-check loop with solver feedback. The authors distinguish it from interactive theorem provers: natural-language solutions are easier to formalize in their first-order-like language, but the resulting context can contain gaps between premises and conclusions (sections 1 and 3, pp. 2–4). The method therefore checks local judgments rather than requiring a complete proof script.

technique 1: formalize a solution into SimpleMath and a Fitch context

Use this when source reasoning is natural language and a complete Lean or Coq proof is too expensive to generate. SimpleMath extends first-order language with constants and syntactic sugar. The paper’s Fibonacci example writes a recursive definition and translates it into universally quantified predicates for the base and recursive cases (section 3.1, p. 4).

Step by step:

  1. Prompt the Formalizer with the grammar, inference rules, few-shot examples, problem, and natural-language solution (section 3.1, p. 4).
  2. Convert the result into a Fitch-style context whose statements are facts, assumptions, theorems, definitions, or conclusions (section 3.1, pp. 4–5).
  3. Represent each conclusion with its useful premises as a judgment Tᵢ ⊢ Qᵢ (section 3.2, p. 6).
  4. Ask the Critic to determine whether each conclusion follows and explain an error when it does not (section 3.2, p. 6).

The paper reports that, on MATH500, “over 90% of the statements in the natural language solutions generated by the generator can be correctly formalized and verified” (section 3.1, p. 5). This denominator is statements, not complete problems. The method can leave gaps between premises and conclusions, which makes it easier than a fully detailed interactive-theorem-prover proof (section 4.2, p. 8).

Inference: In Verus, a similar front end could translate prose into Rust specifications and proof obligations, but the acceptance boundary must be a Verus-checked function or lemma. SimpleMath judgments are not a substitute for executable Rust semantics; omitted premises could become unsoundly weak requires clauses.

technique 2: sparse solution graph for relevant premises

Use this when a long solution contains many statements but each conclusion depends on only a few. MATH-VF builds a directed Solution Graph: each node is a statement, and an edge enters a conclusion exactly when the source statements are its direct premises (section 3.1, pp. 5–6). The Critic receives only the premises connected to the conclusion under review.

The paper contrasts the dense baseline, where the total input is C₁(n)=1+2+…+n=n(n+1)/2 statements, with its sparse bound C₂(n)≤n×M, where M is the maximum number of premises for any conclusion (section 3.2.2, p. 6). Its statistics say M≤4 in almost all formal solutions, so the input is usually at most 4n statements (section 3.2.2, p. 6). This is a token-budget technique, not a proof-soundness theorem; it assumes the Formalizer correctly identifies direct dependencies.

Inference: A VL proof assistant could build a dependency graph of Verus lemmas and pass only referenced facts to an LLM repair prompt. Verus itself still checks the complete proof context, so graph sparsity should optimize prompting rather than remove required hypotheses.

technique 3: tool-integrated Critic

Use this when LLM-only critique is unreliable on calculations or logical satisfiability. The Critic invokes specialized agents for symbolic calculation and logic solving rather than directly generating and executing code (section 3.3, p. 7). SymPy handles symbolic and numerical operations such as differentiation, equation solving, and factoring; Z3 checks satisfiability for supported theories including linear arithmetic, bit vectors, arrays, datatypes, and strings (section 3.2.1, p. 6).

A judgment-checking sequence is:

  1. Provide the relevant formal premises and conclusion to the Critic (section 3.2, p. 6).
  2. Use symbolic calculation to simplify or evaluate expressions (Figure 6, appendix A, p. 9).
  3. Invoke a logic solver to test whether the conclusion follows from the premises (Figure 6, appendix A, p. 9).
  4. Return true or a reason for failure; pass that feedback to the Generator for regeneration (sections 3.2–3.4, pp. 6–7).

The paper says, “our Critic model determines the validity of a judgment by leveraging both reasoning and tool invocations.” (section 3.2, p. 6) In the refinement task, generation repeats until validation passes or a maximum iteration limit is reached (section 3.4, p. 7).

Inference: The Verus analogue is to route arithmetic or sequence properties to verified lemmas and use verifier diagnostics as feedback. SymPy/Z3 results cannot be trusted as replacements for Verus’s proof checker unless their claims are independently encoded and proved in Verus.

evidence, limits, and product threat

On task one, Table 1 reports MATH-VF discriminative accuracy of 93.2% (DeepSeek-v2.5), 95.7% (DeepSeek-v3), 92.4% (Qwen2.5-72B), and 94.3% (Qwen2.5-14B); the denominator is the evaluation judgments for each generator model, and “Discrimin.” is verifier accuracy (Table 1, p. 7). On task two, eight candidates are generated per problem, and a MATH-VF selection is accepted only when every step is judged correct (section 4.2, p. 8). Table 3 reports MATH-VF accuracies of 83.6%, 90.5%, 86.4%, and 88.7% for the four generators, versus self-consistency and a primary Critic (Table 3, p. 8). On refinement, Table 4 reports MATH-VF versus self-refine: 83.5 vs 80.9 for DeepSeek-v2.5, 92.4 vs 90.1 for DeepSeek-v3, 86.2 vs 83.7 for Qwen2.5-72B, and 82.6 vs 80.1 for Qwen2.5-14B (Table 4, p. 8).

The paper reports lower average ProcessBench F1 than trained Qwen2.5-MATH-PRM-72B: 74.1 versus 78.3, while MATH-VF has lower standard deviation 0.029 versus 0.062 (Table 2, p. 7). Limitations include syntax errors in Formalizer output and inability to judge whether a correct local step advances toward the goal (limitations, p. 9). Inference: threat to agent-written verified Rust is medium to high if an LLM is allowed to weaken specifications or omit premises; the useful contribution is solver-backed, step-level feedback, while the final artifact must still pass Verus.

techniques for the catalog

  • SimpleMath formalization: translate natural-language steps into a first-order-like Fitch context
  • sparse solution graph: provide each critic only the direct premises of its conclusion
  • tool-integrated criticism: combine LLM reasoning with symbolic calculation and SMT satisfiability checks
  • feedback refinement: regenerate a failed solution using critic explanations until a bounded stopping condition
  • all-steps selection: accept a candidate only when every formalized step is judged correct Checked 2026-10-15 against paper zhou2025mathvf: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced

Last edited: