AMTFV: Agentic Mathematical Tool-Flow Verification for LLM Self-Correction

AMTFV : Agentic Mathematical Tool-Flow Verification for LLM Self-Correction

Rui Zou 1 , Yutao Zhu 1 , Mengqi Wei 2 , Ji-Rong Wen 1 \corresponding

Abstract Large language models have demonstrated strong mathematical problem-solving capabilities, yet reliably verifying their candidate answers remains challenging. Existing representative methods mainly revise outputs through natural-language reflection or assist verification by directly generating verification programs; the former may not reliably support exact computation, whereas the latter prematurely couples mathematical modeling with low-level implementation. We propose AMTFV (Agentic Mathematical Tool-Flow Verification). By introducing Mathematical Tool Flow (MTF) as an interrupt–execute–resume interface, AMTFV decouples verification modeling from concrete execution and supports exact computation through a mathematical toolbox. Specifically, the verification agent first constructs a verification workflow, encodes the mathematical objects and computational intent requiring reliable execution in an MTF request, and sends it to the mathematical toolbox agent. The latter parses the request, generates executable calls, and dispatches them to the backend for exact computation. Tool outputs then support candidate-answer adjudication, answer revision, and verification-workflow revision. We evaluate AMTFV on five challenging mathematical reasoning datasets with seven model configurations from DeepSeek, GPT, and Gemini. Experimental results show that AMTFV outperforms the representative baselines evaluated in this study overall; under an individual model configuration, it improves average accuracy over the strongest baseline by up to 8.3 8.3 percentage points, with larger gains on samples of medium and high verification complexity.

Introduction

Large language models (LLMs) have demonstrated strong mathematical reasoning capabilities (Yang et al. 2024 ; Guo and others 2025 ; Zhan et al. 2026 ) . Yet their answers to complex problems may remain unreliable because of computational errors, flawed symbolic derivations, omitted constraints, incomplete enumeration, or incorrect optimality judgments. Prior work further shows that rising answer accuracy can coexist with faulty assumptions, planning failures, and inadequate constraint handling in reasoning chains (Boye and Moell 2025 ) . A reliable mathematical reasoning system should therefore not only generate answers but also verify that they satisfy the original conditions and revise them when errors are detected (Cobbe et al. 2021 ; Song et al. 2025 ) .

Existing backward-verification methods mainly follow two paths. The first revises outputs through natural-language self-reflection, feedback-based rewriting, checklists, or repeated sampling (Pan et al. 2024 ; Kamoi et al. 2024 ; Madaan et al. 2023 ; Shinn et al. 2023 ; Cook et al. 2024 ; Wang et al. 2023 ) , but does not reliably detect and correct reasoning errors without external feedback (Huang et al. 2024 ; Tyen et al. 2024 ) . The second augments verification through code execution, such as Python programs (Gao et al. 2023 ; Chen et al. 2023 ; Gou et al. 2024 ; Song et al. 2025 ) . However, we argue that this can prematurely couple mathematical modeling and verification-target design with low-level implementation. Models are asked to generate executable programs before fully specifying the verification target, forcing them to construct verification objects while handling details such as loop boundaries and numerical precision. Such premature code generation can introduce implementation errors and make verification fragile, with two consequences. First, failures are difficult to localize among mathematical modeling, constraint abstraction, and program boundary handling. Second, exact computation may not be fully delegated to specialized tools, leaving reliability dependent on the model’s code-generation ability and ad hoc program quality. Backward verification therefore needs a clearer structure that separates mathematical verification modeling from low-level symbolic compilation, program execution, and exact computation.

This paper proposes AMTFV 1 1 1 Code will be released at https://github.com/TicusFFF/mathematical-self-correction/tree/main/S2-1˙AMTFV . (Agentic Mathematical Tool-Flow Verification), an autonomous framework for mathematical backward verification and self-correction. At its core is the introduction of Mathematical Tool Flow (MTF) as an intermediate interface that separates mathematical reasoning from concrete execution within the verification process. MTF follows an interrupt–execute–resume interaction pattern: during verification, the LLM emits a local computation request and then pauses, waits for the toolbox to finish execution, and resumes reasoning based on the returned result. In this way, the LLM and computational tools each play to their strengths: the LLM focuses on high-level mathematical reasoning, describing “what needs to be computed” solely in terms of mathematical objects and computational intent, and packages this as a structured MTF request. The mathematical toolbox agent receives the request, selects an appropriate mathematical tool according to the computation task (e.g., SymPy (Meurer et al. 2017 ) for symbolic computation and equation solving, or Fraction for exact rational arithmetic), generates an executable call and delegates its execution to the back end, after which the execution result is returned to the verification and correction module for candidate-answer adjudication, answer revision, or verification-workflow revision.

This design that decouples reasoning from execution allows the LLM to focus on mathematical modeling without being prematurely drawn into program implementation, delegates formal computation to a tool back-end better suited for precise execution, thereby more fully leveraging the LLM’s mathematical reasoning capabilities, and effectively mitigates the computational instability caused by the lack of reliable symbolic support in natural-language reflection and the tight coupling between logic and implementation in ad hoc code-based verification. Moreover, MTF preserves clear mathematical semantics, making the verification intent inspectable, revisable, and reusable. Figure 1 illustrates this distinction with an example of closed-form expression verification and correction: natural-language correction lacks symbolic execution, code-based verification tightly couples the verification target with its implementation, whereas AMTFV first explicitly constructs the verification target and then invokes mathematical tools through MTF, achieving a clean separation between reasoning and execution.

Figure 1: Comparison of natural-language reflection, direct code verification, and AMTFV for mathematical answer verification and correction.

We evaluate AMTFV on diverse mathematical reasoning tasks. In the main DeepSeek experiments, it achieves higher average final accuracy than natural-language reflection, feedback-based rewriting, checklist-guided correction, repeated forward-reasoning sampling, and ProgCo. Supplementary GPT and Gemini experiments likewise show higher average accuracy than verification-enhanced methods such as ProgCo. Compared with the strongest evaluated public baseline, AMTFV improves average accuracy by up to 8.3 8.3 percentage points. Further analyses suggest more reliable candidate-answer verification and correction, fewer cases where local checks pass despite incorrect final answers, and larger gains on samples of medium and high verification complexity.

Our contributions are threefold: (1) We introduce MTF, an interrupt–execute–resume interface at the core of AMTFV , which decouples mathematical verification modeling from low-level implementation details, avoids premature code generation, and allows LLMs to focus on high-level mathematical reasoning; (2) we introduce a mathematical toolbox agent that translates MTF requests into executable calls for appropriate mathematical tools in the backend, supporting more accurate and comprehensive backward verification of complex mathematical answers; and (3) we validate the effectiveness of AMTFV across diverse mathematical reasoning datasets and multiple mainstream base-model configurations.

Figure 2: Overview of the AMTFV framework.

Related Work

Our work relates to three research lines: LLM self-correction, tool-augmented mathematical reasoning and agents, and verification-driven reasoning and correction.

LLM self-correction. Methods for improving test-time outputs typically use feedback, reflection, checking, or multi-path sampling. Self-Refine iteratively refines outputs with self-generated feedback; Reflexion uses linguistic feedback for subsequent attempts; TICK structures evaluation and improvement with LLM-generated checklists; and Self-Consistency samples multiple reasoning paths and selects a consistent answer for stability (Madaan et al. 2023 ; Shinn et al. 2023 ; Cook et al. 2024 ; Wang et al. 2023 ) . Recent training and inference methods also enhance self-verification and self-correction: S 2 R uses reinforcement learning, while SPOC interleaves solution generation and verification in a single inference pass to trigger spontaneous correction (Ma et al. 2025 ; Zhao et al. 2025 ) . Studies show that without reliable external feedback, models do not consistently identify and correct their reasoning errors, especially on complex tasks where revisions may fail or errors are difficult to localize (Pan et al. 2024 ; Kamoi et al. 2024 ; Huang et al. 2024 ; Tyen et al. 2024 ) .

Tool-augmented mathematical reasoning and agents. Tool-augmented reasoning combines language models with external programs, code interpreters, or specialized tools to mitigate instability in exact computation and symbolic execution. PAL translates mathematical problems into Python-executed programs; Program-of-Thoughts separates numerical computation from natural-language reasoning; and ToRA integrates natural-language reasoning with tool calls for mathematical problem solving (Gao et al. 2023 ; Chen et al. 2023 ; Gou et al. 2024 ) . Tool-augmented mathematical agents such as AgentMath and R1-Code-Interpreter likewise use code interpreters or tool calls for complex mathematical tasks (Luo et al. 2026 ; Liu et al. 2026b ) . In broader agent research, ReAct interleaves reasoning with external actions, Toolformer learns to invoke APIs, and TRICE uses execution feedback for tool learning, while AutoGen, MetaGPT, and AgentVerse use multi-agent conversations, role specialization, or collaboration for complex tasks (Yao et al. 2023 ; Schick et al. 2023 ; Qiao et al. 2024 ; Wu et al. 2024 ; Hong et al. 2024 ; Chen et al. 2024 ) .

Verification-driven reasoning and correction. Complex mathematical reasoning requires both generating candidate answers and checking them against the original constraints and objective. Early verifier-based work trains verifiers to score or rank candidate solutions and select more reliable answers (Cobbe et al. 2021 ) . Recent failure analyses further show that correct final answers need not reflect reliable reasoning: faulty assumptions, planning failures, arithmetic errors, and inadequate constraint handling remain common (Boye and Moell 2025 ) . Most closely related, ProgCo uses program-driven verification to check candidate answers and program-driven refinement to provide concrete programmatic feedback for self-correction (Song et al. 2025 ) .

Overall, prior work improves correction through linguistic feedback, external tools, or program-driven verification. In contrast, AMTFV uses MTF as a mathematical-toolbox-oriented intermediate representation to decouple verification modeling from execution and use tool results to guide agentic self-correction, rather than merely adding a code executor.

Method

We develop AMTFV , an agentic mathematical verification and correction framework using MTF as its core interface. Given a problem q q and an initial candidate answer a 0 a_{0} extracted from the initial response, the system verifies, provides feedback on, and revises the candidate. Whenever verification or revision requires reliable computation, the agents invoke mathematical tools through the standardized MTF interface.

As shown in Figure 2 , AMTFV has three components. The left verification and correction module contains a verification agent, an answer-revision agent, and a verification-workflow revision agent. The central standardized MTF interface transmits computation requests and tool results. In the right mathematical tool invocation and execution module, the mathematical toolbox agent 𝒜 tool \mathcal{A}_{\mathrm{tool}} parses MTF requests, selects tools, and generates executable calls, which the mathematical toolbox backend executes. Results return to the left module for adjudication, feedback, and revision. This architecture decouples mathematical verification-target modeling from low-level tool execution. We describe the verification and correction module followed by the mathematical tool invocation and execution module.

Verification and Correction Module

Let 𝒜 ver \mathcal{A}{\mathrm{ver}} , 𝒜 ans \mathcal{A}{\mathrm{ans}} , and 𝒜 flow \mathcal{A}{\mathrm{flow}} denote the verification, answer-revision, and verification-workflow revision agents, respectively. At iteration t t , the system first invokes 𝒜 ver \mathcal{A}{\mathrm{ver}} :

( V t , r t , R t ) = 𝒜 ver ​ ( q , y t , a t ; V t − 1 ′ ) . (V{t},r{t},R{t})=\mathcal{A}{\mathrm{ver}}(q,y{t},a{t};V^{\prime}_{t-1}). (1)

Here, y t y{t} is the current response and a t a{t} its extracted candidate answer. The optional V t − 1 ′ V^{\prime}{t-1} is a reference verification workflow; if unavailable, 𝒜 ver \mathcal{A}{\mathrm{ver}} reconstructs one from a t a{t} . The executed workflow, adjudication result, and execution record are V t V{t} , r t ∈ { 0 , 1 } r{t}\in{0,1} , and R t R{t} , respectively. The system returns a t a{t} if r t = 1 r{t}=1 ; otherwise, it proceeds to feedback and revision.

Candidate Verification.

At iteration t t , 𝒜 ver \mathcal{A}{\mathrm{ver}} constructs V t V{t} to determine whether a t a{t} satisfies the constraints and objective of q q . For steps requiring reliable execution, such as symbolic simplification, enumerative counting, exact computation, or constraint solving, it sends MTF requests to 𝒜 tool \mathcal{A}{\mathrm{tool}} . Returned results are written to R t R{t} and used to produce r t r{t} . If verification at iteration t t produces an MTF request τ t ver \tau_{t}^{\mathrm{ver}} , the invocation is written as

κ t ver = 𝒜 tool ​ ( τ t ver ; 𝕋 ) , z t ver = Run ⁡ ( κ t ver ) . \kappa{t}^{\mathrm{ver}}=\mathcal{A}{\mathrm{tool}}(\tau{t}^{\mathrm{ver}};\mathbb{T}),\qquad z{t}^{\mathrm{ver}}=\operatorname{Run}(\kappa_{t}^{\mathrm{ver}}).

Here, 𝕋 \mathbb{T} is the set of tools exposed by the mathematical toolbox backend, κ t ver \kappa{t}^{\mathrm{ver}} the generated tool call, and z t ver z{t}^{\mathrm{ver}} its result.

Answer Revision.

When r t = 0 r{t}=0 , a t a{t} fails verification and the system invokes 𝒜 ans \mathcal{A}{\mathrm{ans}} . Given the problem q q , current response y t y{t} , verification workflow V t V{t} , and execution record R t R{t} , 𝒜 ans \mathcal{A}{\mathrm{ans}} produces feedback F t F{t} and a revised response y t ′ y^{\prime}{t} , from which the system extracts a t ′ a^{\prime}{t} :

( F t , y t ′ ) \displaystyle(F{t},y^{\prime}{t}) = 𝒜 ans ​ ( q , y t , V t , R t ) , \displaystyle=\mathcal{A}{\mathrm{ans}}(q,y{t},V{t},R{t}), (2)

a t ′ \displaystyle a^{\prime}{t} = Extract ⁡ ( y t ′ ) . \displaystyle=\operatorname{Extract}(y^{\prime}{t}).

To recompute an expression, enumerate a candidate set, or check constraint feasibility during revision, the agent may produce τ t ans \tau{t}^{\mathrm{ans}} and invoke the backend through 𝒜 tool \mathcal{A}{\mathrm{tool}} :

κ t ans = 𝒜 tool ​ ( τ t ans ; 𝕋 ) , z t ans = Run ⁡ ( κ t ans ) . \kappa{t}^{\mathrm{ans}}=\mathcal{A}{\mathrm{tool}}(\tau{t}^{\mathrm{ans}};\mathbb{T}),\qquad z{t}^{\mathrm{ans}}=\operatorname{Run}(\kappa_{t}^{\mathrm{ans}}).

The result z t ans z{t}^{\mathrm{ans}} may be added to R t R{t} and used to produce F t F{t} and y t ′ y^{\prime}{t} . If a t ′ ≠ a t a^{\prime}{t}\neq a{t} , the system updates the response and candidate and verifies the new candidate at the next iteration.

Verification-Workflow Revision.

If answer revision retains the candidate, i.e., a t ′ = a t a^{\prime}{t}=a{t} , the system invokes 𝒜 flow \mathcal{A}{\mathrm{flow}} . Using the current workflow V t V{t} and execution record R t R{t} , 𝒜 flow \mathcal{A}{\mathrm{flow}} diagnoses verification-target coverage, the mathematical objects, and computational evidence, then produces V t ′ V^{\prime}_{t} :

V t ′ = 𝒜 flow ​ ( q , y t , V t , R t ) . V^{\prime}{t}=\mathcal{A}{\mathrm{flow}}(q,y{t},V{t},R_{t}). (3)

Verification-workflow revision improves checks insufficiently covered by V t V{t} . If the original workflow checks only a subset of candidates, local relations, or intermediate computations, the revision may add the complete set, global optimum, symbolic equivalence, or constraint satisfiability as targets. If diagnosis or revision produces τ t flow \tau{t}^{\mathrm{flow}} , the backend is again invoked through 𝒜 tool \mathcal{A}_{\mathrm{tool}} :

κ t flow = 𝒜 tool ​ ( τ t flow ; 𝕋 ) , z t flow = Run ⁡ ( κ t flow ) . \kappa{t}^{\mathrm{flow}}=\mathcal{A}{\mathrm{tool}}(\tau{t}^{\mathrm{flow}};\mathbb{T}),\qquad z{t}^{\mathrm{flow}}=\operatorname{Run}(\kappa_{t}^{\mathrm{flow}}).

The result z t flow z{t}^{\mathrm{flow}} may update R t R{t} and guide construction of V t ′ V^{\prime}_{t} , which serves as the next iteration’s reference workflow.

Iteration Mechanism.

The response and candidate for the next iteration are updated as follows:

( y t + 1 , a t + 1 ) = { ( y t ′ , a t ′ ) , a t ′ ≠ a t , ( y t , a t ) , a t ′ = a t . (y{t+1},a{t+1})=\begin{cases}(y^{\prime}{t},a^{\prime}{t}),&a^{\prime}{t}\neq a{t},\ (y{t},a{t}),&a^{\prime}{t}=a{t}.\end{cases} (4)

If a t ′ ≠ a t a^{\prime}{t}\neq a{t} , the next iteration verifies a t ′ a^{\prime}{t} ; otherwise, it retains a t a{t} and uses V t ′ V^{\prime}_{t} as its reference workflow. Iteration stops upon successful verification or at the preset iteration limit.

Mathematical Tool Invocation and Execution Module

An MTF fragment τ \tau is a local mathematical computation request, enclosed by... tags, that is emitted within the ongoing verification trajectory. When the closing tag is reached, streamed generation is interrupted and the request is sent to the mathematical toolbox. The returned result is appended to the accumulated context, and verification continues in a follow-up model call. A verification trajectory may contain multiple such fragments; their interleaving with reasoning and returned tool results forms the MTF. Formally,

τ = ⟨ Γ τ , ℳ τ , ρ τ ⟩ . \tau=\langle\Gamma{\tau},\mathcal{M}{\tau},\rho_{\tau}\rangle.

Here, Γ τ \Gamma{\tau} is the context, such as variables, domains, parameter assumptions, or known constraints; ℳ τ \mathcal{M}{\tau} is the object to compute, construct, or verify, such as a set, expression, equation system, recurrence, or constraint system; and ρ τ \rho{\tau} specifies the return operation on ℳ τ \mathcal{M}{\tau} , such as cardinality, symbolic simplification, feasible solutions, a global optimum, or satisfiability.

The tuple schema for τ \tau can represent different verification tasks. The following example maps a symbolic-expression verification target to an MTF request and tool call.

Example: Symbolic-expression verification. A chocolate bar costs c c and a vanilla bar c + 2 c+2 . Jamie buys one chocolate and three vanilla bars, while Kevin buys five chocolate bars. The candidate answer is 8 ​ c + 6 8c+6 .

Let Δ ​ ( c ) = c + 3 ​ ( c + 2 ) + 5 ​ c − ( 8 ​ c + 6 ) \Delta(c)=c+3(c+2)+5c-(8c+6) . The candidate passes verification if and only if Simplify ⁡ ( Δ ​ ( c ) ) ≡ 0 \operatorname{Simplify}(\Delta(c))\equiv 0 .

MTF request.

This corresponds to τ = ⟨ { c ​ is symbolic } , Δ ​ ( c ) , Simplify ⟩ \tau=\langle{c\text{ is symbolic}},\Delta(c),\operatorname{Simplify}\rangle .

Tool call and result.

c = sympy.symbols("c") D = c+3(c+2)+5c-(8*c+6) z_tau = sympy.simplify(D)

The backend returns z τ = c ≢ 0 z{\tau}=c\not\equiv 0 ; hence the candidate fails verification and r t = 0 r{t}=0 .

Here, ρ τ = Simplify \rho{\tau}=\operatorname{Simplify} specifies symbolic verification. Counting, optimization, and constraint solving use the same template, replacing ℳ τ \mathcal{M}{\tau} with a set, objective, or constraint system and ρ τ \rho{\tau} with cardinality, optimum, satisfiability, or solution set. MTF thus uniformly expresses “context–object–return specification” for different verification targets. MTF represents mathematical computational intent, and 𝒜 tool \mathcal{A}{\mathrm{tool}} translates it into an executable call. Through τ \tau , the three agents specify the object and desired return; 𝒜 tool \mathcal{A}{\mathrm{tool}} selects a tool, generates a call, and dispatches it to the backend. Together, MTF and 𝒜 tool \mathcal{A}{\mathrm{tool}} form an intermediate computational interface to the toolbox. MTF also makes complete verification objects explicit. For counting, optimization, symbolic verification, or constraint solving, the backend may return a full set and its cardinality, a global optimum, a symbolic difference, or satisfiability. This helps AMTFV avoid checking only local candidate consistency while overlooking the complete target.

Let the set of tools exposed by the mathematical toolbox backend be

𝕋 = { 𝒯 sym , 𝒯 enum , 𝒯 exact , 𝒯 smt , … } . \mathbb{T}={\mathcal{T}{\mathrm{sym}},\mathcal{T}{\mathrm{enum}},\mathcal{T}{\mathrm{exact}},\mathcal{T}{\mathrm{smt}},\ldots}.

where 𝒯 sym \mathcal{T}{\mathrm{sym}} , 𝒯 enum \mathcal{T}{\mathrm{enum}} , 𝒯 exact \mathcal{T}{\mathrm{exact}} , and 𝒯 smt \mathcal{T}{\mathrm{smt}} support symbolic computation, enumeration, exact numerical computation, and constraint solving, respectively.

Given τ \tau and 𝕋 \mathbb{T} , 𝒜 tool \mathcal{A}{\mathrm{tool}} generates an executable call κ τ \kappa{\tau} :

κ τ = 𝒜 tool ​ ( τ ; 𝕋 ) = ( 𝒯 j , u j ) , 𝒯 j ∈ 𝕋 . \kappa{\tau}=\mathcal{A}{\mathrm{tool}}(\tau;\mathbb{T})=(\mathcal{T}{j},u{j}),\qquad\mathcal{T}_{j}\in\mathbb{T}.

Here, 𝒯 j \mathcal{T}{j} is the selected tool and u j u{j} its input. The agent selects 𝒯 j \mathcal{T}{j} according to ρ τ \rho{\tau} and constructs u j u{j} from Γ τ \Gamma{\tau} and ℳ τ \mathcal{M}_{\tau} .

The backend executes the call and returns

z τ = Run ⁡ ( κ τ ) = 𝒯 j ​ ( u j ) . z{\tau}=\operatorname{Run}(\kappa{\tau})=\mathcal{T}{j}(u{j}).

Here, z τ z{\tau} is the result specified by ρ τ \rho{\tau} .

The result z τ z_{\tau} is enclosed in and appended to execution record R R :

R ← Append ⁡ ( R , ( τ , 𝒯 j , u j , z τ ) ) . R\leftarrow\operatorname{Append}\bigl(R,(\tau,\mathcal{T}{j},u{j},z_{\tau})\bigr).

The three agents use results in R R for candidate-answer adjudication, answer revision, or workflow revision.

Our mathematical toolbox backend runs in Python: SymPy supports symbolic computation and equation solving, itertools combinatorial enumeration, and Fraction exact rational arithmetic. Python serves only as the environment for calls generated by 𝒜 tool \mathcal{A}_{\mathrm{tool}} .

DeepSeek-Flash DeepSeek-Flash-Think DeepSeek-Pro

Method A24 A25 B25 HMM AMO Avg A24 A25 B25 HMM AMO Avg A24 A25 B25 HMM AMO Avg

Initial Score 63.3 63.3 43.3 43.3 86.7 86.7 33.3 33.3 14.0 14.0 44.1 44.1 100.0 100.0 100.0 100.0 100.0 100.0 100.0 100.0 62.0 62.0 88.8 88.8 63.3 63.3 53.3 53.3 60.0 60.0 26.7 26.7 10.0 10.0 38.8 38.8

reflex 63.3 63.3 46.7 46.7 83.3 83.3 33.3 33.3 18.0 18.0 45.3 45.3 96.7 96.7 100.0 100.0 93.3 93.3 93.3 93.3 56.0 56.0 84.1 84.1 60.0 60.0 63.3 63.3 70.0 70.0 40.0 40.0 10.0 10.0 44.1 44.1

Self-Refine 66.7 66.7 60.0 60.0 86.7 86.7 50.0 50.0 14.0 14.0 50.6 50.6 93.3 93.3 100.0 100.0 90.0 90.0 96.7 96.7 56.0 56.0 83.5 83.5 66.7 66.7 66.7 66.7 86.7 86.7 56.7 56.7 16.0 16.0 53.5 53.5

Self-Refl. 63.3 63.3 46.7 46.7 86.7 86.7 33.3 33.3 16.0 16.0 45.3 45.3 96.7 96.7 100.0 100.0 93.3 93.3 100.0 100.0 60.0 60.0 86.5 86.5 66.7 66.7 60.0 60.0 73.3 73.3 40.0 40.0 8.0 8.0 44.7 44.7

CheckList 60.0 60.0 56.7 56.7 80.0 80.0 30.0 30.0 16.0 16.0 44.7 44.7 96.7 96.7 100.0 100.0 86.7 86.7 86.7 86.7 56.0 56.0 81.8 81.8 66.7 66.7 53.3 53.3 70.0 70.0 40.0 40.0 16.0 16.0 45.3 45.3

CoT-Tool 76.7 76.7 60.0 60.0 73.3 73.3 43.3 43.3 4.0 4.0 45.9 45.9 93.3 93.3 93.3 93.3 93.3 93.3 86.7 86.7 44.0 44.0 77.6 77.6 56.7 56.7 43.3 43.3 43.3 43.3 23.3 23.3 6.0 6.0 31.2 31.2

ProgCo 66.7 66.7 53.3 53.3 96.7 96.7 43.3 43.3 18.0 18.0 51.2 51.2 100.0 100.0 100.0 100.0 100.0 100.0 100.0 100.0 58.0 58.0 87.6 87.6 66.7 66.7 60.0 60.0 66.7 66.7 40.0 40.0 12.0 12.0 44.7 44.7

ProgCo-Py 66.7 66.7 60.0 60.0 90.0 90.0 43.3 43.3 24.0 24.0 52.9 52.9 100.0 100.0 100.0 100.0 100.0 100.0 100.0 100.0 60.0 60.0 88.2 88.2 80.0 80.0 60.0 60.0 73.3 73.3 43.3 43.3 14.0 14.0 49.4 49.4

AMTFV 80.0 \mathbf{80.0} 66.7 \mathbf{66.7} 93.3 \mathit{93.3} 60.0 \mathbf{60.0} 28.0 \mathbf{28.0} 61.2 \mathbf{61.2} 100.0 \mathbf{100.0} 100.0 \mathbf{100.0} 100.0 \mathbf{100.0} 100.0 \mathbf{100.0} 64.0 \mathbf{64.0} 89.4 \mathbf{89.4} 76.7 \mathit{76.7} 66.7 \mathbf{66.7} 93.3 \mathbf{93.3} 53.3 \mathit{53.3} 20.0 \mathbf{20.0} 57.1 \mathbf{57.1}

Table 1: Main results. Avg denotes sample-weighted average accuracy across the five datasets. In the AMTFV row, bold indicates the highest or tied-highest value among all correction methods in the corresponding column, and italics indicate the second-highest value.

Figure 3: Average accuracy of verification-enhanced methods under each base-model setting. The horizontal axis shows the seven base-model settings, and the vertical axis shows sample-weighted average accuracy (%) across the five datasets. Gray bars denote Initial Score, while the other bars show final accuracy with maxturn = 3 \texttt{max\turn}=3 . Blue annotations report the absolute improvement of AMTFV over the better result between ProgCo and ProgCo-Py, in percentage points.

Experiments

We evaluate AMTFV for mathematical reasoning verification and correction against self-correction, reasoning-enhanced, and verification-enhanced methods. We analyze its performance and gains through cross-model architectural comparisons, correction-state transitions, and verification-complexity bins. The supplementary material covers iteration budgets, correlations with empirical difficulty, MTF call types (see Supplementary Figure 9 ), and case processes.

Experimental Setup

Datasets. We use five hard-test mathematical reasoning datasets totaling 170 problems, abbreviated as A24, A25, B25, HMM, and AMO. AIME 2024 / AIME 2025 each contain 30 American Invitational Mathematics Examination problems assessing multistep reasoning and exact computation. BRUMO 2025 contains 30 challenging problems assessing complex-condition understanding and multistep reasoning. HMMT February 2025 contains 30 competition problems spanning algebra, geometry, combinatorics, and number theory (Hochlehnert et al. 2025 ; Pei et al. 2025 ) . AMO Bench contains 50 Olympiad-level problems with more diverse problem and answer formats (Liu et al. 2026a ) .

Base models. We cover DeepSeek, GPT, and Gemini. The main experiments use DeepSeek-Flash , DeepSeek-Flash-Think , and DeepSeek-Pro to compare correction across non-thinking, thinking, and stronger-model settings (DeepSeek 2026 ) . For cross-model generalization, we further compare ProgCo, ProgCo-Py, and AMTFV using GPT-5.4-Mini and GPT-5.4-Mini-Think (OpenAI 2026 ) , and Gemini-2.5-Flash-Lite and Gemini-2.5-Flash-Lite-Think (Google AI for Developers 2026a , b ) .

Compared methods. The main experiments compare three method classes. Natural-language correction includes reflex , the vanilla-reflex configuration from ProgCo; Self-Refine (Madaan et al. 2023 ) ; Self-Reflection (Shinn et al. 2023 ) , abbreviated as Self-Refl. in the table; and CheckList (Cook et al. 2024 ) . They represent vanilla reflection, iterative self-feedback, self-reflective feedback, and checklist-guided correction, respectively. The reasoning-enhanced CoT-Tool (Abedi Firouzjaei 2025 ; Wei et al. 2022 ; Wang et al. 2023 ) combines the Cogitator toolkit, multi-path chain-of-thought reasoning, and Self-Consistency selection. Verification-enhanced methods include ProgCo , which uses program-driven verification and refinement, and ProgCo-Py , our setting that enables Python-tool feedback in the official implementation (Song et al. 2025 ) . Cross-model and progressive comparisons focus on ProgCo, ProgCo-Py, and AMTFV , tracing the progression from programmatic verification through general Python-tool feedback to an MTF-based framework that decouples mathematical tool flows.

Evaluation settings and metrics. For each problem, the base model produces an initial response from which we extract a candidate answer. Except for Initial Score, all methods receive the same initial response and candidate. We set maxturn = 3 \texttt{max\turn}=3 for methods controlling iterative correction or tool-use rounds; others follow their standard procedures. The primary metric is final-answer accuracy, with cross-dataset Avg weighted by dataset size. The supplementary material details implementation and fairness settings (see Supplementary Tables 2 and 3 ). We also analyze correction-state transitions and verification-complexity bins.

Main Results

Table 1 compares the final-answer accuracy of AMTFV and representative baselines under the three main evaluation settings: DeepSeek-Flash, DeepSeek-Flash-Think, and DeepSeek-Pro. AMTFV achieves the highest average accuracy under all three DeepSeek settings. From Initial Score, it improves DeepSeek-Flash from 44.1 to 61.2, DeepSeek-Flash-Think from 88.8 to 89.4, and DeepSeek-Pro from 38.8 to 57.1: gains of + 17.1 +17.1 , + 0.6 +0.6 , and + 18.3 +18.3 percentage points, respectively. With identical initial answers and a fixed maximum iteration budget, these results suggest that MTF-based verification and correction can improve final-answer accuracy more than the compared methods under these settings.

The smaller DeepSeek-Flash-Think gain mainly reflects Initial Scores of 100.0 on A24, A25, B25, and HMM, leaving most room for correction on AMO. Most methods decline from this strong initial setting, indicating overcorrection risk. In contrast, AMTFV preserves accuracy on the four saturated datasets, improves AMO from 62.0 to 64.0, and raises average accuracy from 88.8 to 89.4, indicating that it better avoids aggregate degradation.

AMTFV also exceeds ProgCo and ProgCo-Py in average accuracy under all three DeepSeek settings. Over the better ProgCo-family result, its gains are approximately + 8.3 +8.3 , + 1.2 +1.2 , and + 7.7 +7.7 percentage points on DeepSeek-Flash, DeepSeek-Flash-Think, and DeepSeek-Pro. We next compare their progressive architectural differences under additional base models.

Architectural Variant Analysis

We further compare ProgCo, ProgCo-Py, and AMTFV across base models. They form a progressive architectural sequence: ProgCo uses program-driven verification and correction; ProgCo-Py adds Python execution feedback; and AMTFV adds MTF, a mathematical toolbox interface, and closed-loop verification-workflow revision. Unless stated otherwise, maxturn = 3 \texttt{max\turn}=3 .

Figure 3 compares average accuracy across all seven base-model settings. AMTFV ranks highest in every setting, exceeding the better of ProgCo and ProgCo-Py by + 0.6 +0.6 to + 8.3 +8.3 percentage points; its gains thus extend beyond DeepSeek. The supplementary material reports per-dataset GPT and Gemini results (see Supplementary Tables 4 and 5 ). Python execution feedback lets ProgCo-Py improve over ProgCo in some settings, but inconsistently. By contrast, AMTFV uses MTF to specify the mathematical objects, constraints, and computational objective before backend execution, then applies tool results to adjudication, answer revision, and verification-workflow revision. The comparison supports our design motivation: under the evaluated settings, decoupling verification targets from low-level execution and incorporating tool results into a multistep verification–correction loop can be more stable than adding general program-execution feedback alone.

Figure 4: Overall average-accuracy trajectories under different iteration budgets. The horizontal axis shows Initial Score, maxturn = 1 \texttt{max\turn}=1 , and maxturn = 3 \texttt{max\turn}=3 ; the vertical axis shows average accuracy across seven base-model settings. Curve-end values denote absolute improvements from Initial Score to maxturn = 3 \texttt{max\turn}=3 , in percentage points.

Figure 4 suggests that, under a fixed budget, AMTFV uses additional verification–correction rounds more effectively. The supplementary material provides trajectories for individual model settings (see Supplementary Figure 7 ).

Correction Behavior and Verification Complexity Analysis

We analyze AMTFV ’s gains through correction-state transitions, which measure error correction and preservation of correct answers, and verification-complexity bins, which show whether gains concentrate on examples requiring more complex interactions.

Correction Behavior Analysis

We characterize correction behavior with row-normalized transition matrices, where C C and W W denote correct and incorrect answers. W → C W\rightarrow C measures error correction, whereas C → W C\rightarrow W measures the risk of corrupting a correct answer.

Figure 5: Row-normalized correction-state transition matrices. Rows indicate initial correctness and columns indicate final correctness, where C C denotes a correct answer and W W an incorrect answer. Each cell reports the percentage of examples in the corresponding initial state that transition to the given final state, with each row normalized to 100%. Green borders and arrows highlight error-correcting transitions W → C W\rightarrow C , while red borders and arrows highlight error-introducing transitions C → W C\rightarrow W .

Figure 5 aggregates 7 × 170 = 1190 7\times 170=1190 model–problem instances across seven base models. AMTFV ’s W → C W\rightarrow C rate is 18.4%, versus 9.4% for ProgCo and 12.2% for ProgCo-Py. Its C → W C\rightarrow W rate is 2.8%, below ProgCo’s 3.7% and ProgCo-Py’s 4.2%. Thus, its gains primarily reflect better error correction and preservation of correct answers rather than aggressive rewriting.

Verification Complexity Analysis

Figure 6: Normalized accuracy gains over Initial Score across verification-complexity bins. The horizontal axis reports ( Final ​ Score − Initial ​ Score ) / Initial ​ Score (\mathrm{Final\ Score}-\mathrm{Initial\ Score})/\mathrm{Initial\ Score} , the accuracy gain normalized by initial accuracy. Low, Medium, and High bins are defined in the supplementary material.

We use the MTF call count per model–problem instance as an operational measure of verification complexity because it reflects the amount of computational interaction required for verification. The Low, Medium, and High bins correspond to at most one, two to three, and at least four MTF calls, respectively. The analysis covers 7 × 170 = 1190 7\times 170=1190 instances and compares all methods on the same examples per bin. Supplementary Figure 8 shows a positive relationship between problem-level verification complexity and empirical difficulty: Pearson r = 0.67 r=0.67 and Spearman ρ = 0.70 \rho=0.70 .

Figure 6 shows little gain from any verification-enhanced method in the Low bin. Normalized by Initial Score, AMTFV ’s gains are 39.2 % 39.2% and 84.6 % 84.6% in the Medium and High bins, exceeding ProgCo-Py by approximately 20.0 20.0 and 29.2 29.2 percentage points. Its advantage is therefore strongest when more verification interactions are required. The supplementary material provides the empirical-difficulty–verification-complexity analysis and complexity definition.

The supplementary material presents successful cases in minimality verification, combinatorial counting, lattice-point enumeration, and exact double summation (see Supplementary Table 6 ). They show how AMTFV uses MTF results for global constraints, exhaustive enumeration, and exact-computation verification, and detail an exact double-summation case from the B25 dataset.

Conclusion

We introduce AMTFV to decouple verification-target design from low-level implementation in mathematical backward verification. MTF separates mathematical verification modeling from tool execution, and its returned results support candidate adjudication and self-correction. Experiments show that AMTFV outperforms representative correction and verification methods across mathematical reasoning datasets and base models, with larger gains at medium or high verification complexity. Further correction-state analysis indicates that these gains primarily arise from correcting initially incorrect answers while preserving initially correct ones, rather than from aggressive rewriting. Future work will extend the framework beyond mathematical toolboxes to domain-specific systems, applying the “task modeling–specialized tool execution” paradigm to scientific tasks requiring reliable verification and computation.