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).

The paper studies mathematical reasoning. Inference: its transferable idea for verified Rust is a formalize-then-check loop with solver feedback. The authors distinguish it from interactive theorem provers: “The premises and conclusions in the context may not be continuously derived, with gaps between them.” (section 3, p. 4) The Critic checks whether each conclusion is true under its premises; a complete proof script is not required (sections 3 and 4.2, pp. 4, 7–8).

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

Inference: 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 the authors say makes formalization easier than producing a fully detailed interactive-theorem-prover proof (section 4.2, pp. 7–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

Inference: 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 useful premises for the conclusion under review. The paper also uses relationships between premises: Figure 5 illustrates checking Prop1 → Prop3 rather than only Prop1 ∧ Prop2 → Prop3, using the graph’s derivation of Prop2 from Prop1 (sections 3.1–3.2, p. 6).

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). Inference: this reduces prompt size only if the graph identifies sufficient premises; the reported input bound does not establish proof soundness.

technique 3: tool-integrated Critic

Inference: use this when LLM-only critique is unreliable on calculations or logical satisfiability. The paper says, “Instead, it passes the problem to three LLM-based agents that are integrated with three specific tools.” (section 3.3, p. 6) The Critic does not directly generate and execute code. Section 3.2.1 names SymPy and Z3; it does not identify the third tool (p. 6). 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).

Figure 6 illustrates this judgment-checking sequence; the paper does not require this fixed tool order for every judgment:

  1. Provide the relevant formal premises and conclusion to the Critic (section 3.2, p. 6).
  2. Call the symbolic calculator to factor the expression defining f(x) (Figure 6, appendix A, p. 12).
  3. After reasoning about the factor’s sign, call the logic solver on the negated implication; it returns unsat, and the Critic concludes the judgment is true (Figure 6, appendix A, p. 12).
  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.

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

Last edited: