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

# AMTFV: Agentic Mathematical Tool-Flow Verification for LLM Self-Correction
Source: [https://arxiv.org/html/2607.29549](https://arxiv.org/html/2607.29549)
###### 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 to8\.38\.3percentage points, with larger gains on samples of medium and high verification complexity\.

## Introduction

Large language models \(LLMs\) have demonstrated strong mathematical reasoning capabilities\(Yanget al\.[2024](https://arxiv.org/html/2607.29549#bib.bib26); Guo and others[2025](https://arxiv.org/html/2607.29549#bib.bib27); Zhanet al\.[2026](https://arxiv.org/html/2607.29549#bib.bib28)\)\. 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](https://arxiv.org/html/2607.29549#bib.bib33)\)\. 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\(Cobbeet al\.[2021](https://arxiv.org/html/2607.29549#bib.bib14); Songet al\.[2025](https://arxiv.org/html/2607.29549#bib.bib1)\)\.

Existing backward\-verification methods mainly follow two paths\. The first revises outputs through natural\-language self\-reflection, feedback\-based rewriting, checklists, or repeated sampling\(Panet al\.[2024](https://arxiv.org/html/2607.29549#bib.bib15); Kamoiet al\.[2024](https://arxiv.org/html/2607.29549#bib.bib16); Madaanet al\.[2023](https://arxiv.org/html/2607.29549#bib.bib2); Shinnet al\.[2023](https://arxiv.org/html/2607.29549#bib.bib3); Cooket al\.[2024](https://arxiv.org/html/2607.29549#bib.bib4); Wanget al\.[2023](https://arxiv.org/html/2607.29549#bib.bib5)\), but does not reliably detect and correct reasoning errors without external feedback\(Huanget al\.[2024](https://arxiv.org/html/2607.29549#bib.bib17); Tyenet al\.[2024](https://arxiv.org/html/2607.29549#bib.bib18)\)\. The second augments verification through code execution, such as Python programs\(Gaoet al\.[2023](https://arxiv.org/html/2607.29549#bib.bib22); Chenet al\.[2023](https://arxiv.org/html/2607.29549#bib.bib23); Gouet al\.[2024](https://arxiv.org/html/2607.29549#bib.bib24); Songet al\.[2025](https://arxiv.org/html/2607.29549#bib.bib1)\)\. 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 proposesAMTFV111Code 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\(Meureret al\.[2017](https://arxiv.org/html/2607.29549#bib.bib25)\)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](https://arxiv.org/html/2607.29549#Sx1.F1)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, whereasAMTFVfirst explicitly constructs the verification target and then invokes mathematical tools through MTF, achieving a clean separation between reasoning and execution\.

![Refer to caption](https://arxiv.org/html/2607.29549v1/x1.png)Figure 1:Comparison of natural\-language reflection, direct code verification, andAMTFVfor mathematical answer verification and correction\.We evaluateAMTFVon 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,AMTFVimproves average accuracy by up to8\.38\.3percentage 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 ofAMTFV, 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 ofAMTFVacross diverse mathematical reasoning datasets and multiple mainstream base\-model configurations\.

![Refer to caption](https://arxiv.org/html/2607.29549v1/x2.png)Figure 2:Overview of theAMTFVframework\.
## 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\(Madaanet al\.[2023](https://arxiv.org/html/2607.29549#bib.bib2); Shinnet al\.[2023](https://arxiv.org/html/2607.29549#bib.bib3); Cooket al\.[2024](https://arxiv.org/html/2607.29549#bib.bib4); Wanget al\.[2023](https://arxiv.org/html/2607.29549#bib.bib5)\)\. Recent training and inference methods also enhance self\-verification and self\-correction: S2R uses reinforcement learning, while SPOC interleaves solution generation and verification in a single inference pass to trigger spontaneous correction\(Maet al\.[2025](https://arxiv.org/html/2607.29549#bib.bib29); Zhaoet al\.[2025](https://arxiv.org/html/2607.29549#bib.bib30)\)\. 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\(Panet al\.[2024](https://arxiv.org/html/2607.29549#bib.bib15); Kamoiet al\.[2024](https://arxiv.org/html/2607.29549#bib.bib16); Huanget al\.[2024](https://arxiv.org/html/2607.29549#bib.bib17); Tyenet al\.[2024](https://arxiv.org/html/2607.29549#bib.bib18)\)\.

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\(Gaoet al\.[2023](https://arxiv.org/html/2607.29549#bib.bib22); Chenet al\.[2023](https://arxiv.org/html/2607.29549#bib.bib23); Gouet al\.[2024](https://arxiv.org/html/2607.29549#bib.bib24)\)\. Tool\-augmented mathematical agents such as AgentMath and R1\-Code\-Interpreter likewise use code interpreters or tool calls for complex mathematical tasks\(Luoet al\.[2026](https://arxiv.org/html/2607.29549#bib.bib31); Liuet al\.[2026b](https://arxiv.org/html/2607.29549#bib.bib32)\)\. 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\(Yaoet al\.[2023](https://arxiv.org/html/2607.29549#bib.bib19); Schicket al\.[2023](https://arxiv.org/html/2607.29549#bib.bib20); Qiaoet al\.[2024](https://arxiv.org/html/2607.29549#bib.bib21); Wuet al\.[2024](https://arxiv.org/html/2607.29549#bib.bib34); Honget al\.[2024](https://arxiv.org/html/2607.29549#bib.bib35); Chenet al\.[2024](https://arxiv.org/html/2607.29549#bib.bib36)\)\.

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\(Cobbeet al\.[2021](https://arxiv.org/html/2607.29549#bib.bib14)\)\. 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](https://arxiv.org/html/2607.29549#bib.bib33)\)\. Most closely related, ProgCo uses program\-driven verification to check candidate answers and program\-driven refinement to provide concrete programmatic feedback for self\-correction\(Songet al\.[2025](https://arxiv.org/html/2607.29549#bib.bib1)\)\.

Overall, prior work improves correction through linguistic feedback, external tools, or program\-driven verification\. In contrast,AMTFVuses 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 developAMTFV, an agentic mathematical verification and correction framework using MTF as its core interface\. Given a problemqqand an initial candidate answera0a\_\{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](https://arxiv.org/html/2607.29549#Sx1.F2),AMTFVhas 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 iterationtt, the system first invokes𝒜ver\\mathcal\{A\}\_\{\\mathrm\{ver\}\}:

\(Vt,rt,Rt\)=𝒜ver​\(q,yt,at;Vt−1′\)\.\(V\_\{t\},r\_\{t\},R\_\{t\}\)=\\mathcal\{A\}\_\{\\mathrm\{ver\}\}\(q,y\_\{t\},a\_\{t\};V^\{\\prime\}\_\{t\-1\}\)\.\(1\)
Here,yty\_\{t\}is the current response andata\_\{t\}its extracted candidate answer\. The optionalVt−1′V^\{\\prime\}\_\{t\-1\}is a reference verification workflow; if unavailable,𝒜ver\\mathcal\{A\}\_\{\\mathrm\{ver\}\}reconstructs one fromata\_\{t\}\. The executed workflow, adjudication result, and execution record areVtV\_\{t\},rt∈\{0,1\}r\_\{t\}\\in\\\{0,1\\\}, andRtR\_\{t\}, respectively\. The system returnsata\_\{t\}ifrt=1r\_\{t\}=1; otherwise, it proceeds to feedback and revision\.

##### Candidate Verification\.

At iterationtt,𝒜ver\\mathcal\{A\}\_\{\\mathrm\{ver\}\}constructsVtV\_\{t\}to determine whetherata\_\{t\}satisfies the constraints and objective ofqq\. 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 toRtR\_\{t\}and used to producertr\_\{t\}\. If verification at iterationttproduces an MTF requestτtver\\tau\_\{t\}^\{\\mathrm\{ver\}\}, the invocation is written as

κtver=𝒜tool​\(τtver;𝕋\),ztver=Run⁡\(κtver\)\.\\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,κtver\\kappa\_\{t\}^\{\\mathrm\{ver\}\}the generated tool call, andztverz\_\{t\}^\{\\mathrm\{ver\}\}its result\.

##### Answer Revision\.

Whenrt=0r\_\{t\}=0,ata\_\{t\}fails verification and the system invokes𝒜ans\\mathcal\{A\}\_\{\\mathrm\{ans\}\}\. Given the problemqq, current responseyty\_\{t\}, verification workflowVtV\_\{t\}, and execution recordRtR\_\{t\},𝒜ans\\mathcal\{A\}\_\{\\mathrm\{ans\}\}produces feedbackFtF\_\{t\}and a revised responseyt′y^\{\\prime\}\_\{t\}, from which the system extractsat′a^\{\\prime\}\_\{t\}:

\(Ft,yt′\)\\displaystyle\(F\_\{t\},y^\{\\prime\}\_\{t\}\)=𝒜ans​\(q,yt,Vt,Rt\),\\displaystyle=\\mathcal\{A\}\_\{\\mathrm\{ans\}\}\(q,y\_\{t\},V\_\{t\},R\_\{t\}\),\(2\)at′\\displaystyle a^\{\\prime\}\_\{t\}=Extract⁡\(yt′\)\.\\displaystyle=\\operatorname\{Extract\}\(y^\{\\prime\}\_\{t\}\)\.To recompute an expression, enumerate a candidate set, or check constraint feasibility during revision, the agent may produceτtans\\tau\_\{t\}^\{\\mathrm\{ans\}\}and invoke the backend through𝒜tool\\mathcal\{A\}\_\{\\mathrm\{tool\}\}:

κtans=𝒜tool​\(τtans;𝕋\),ztans=Run⁡\(κtans\)\.\\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 resultztansz\_\{t\}^\{\\mathrm\{ans\}\}may be added toRtR\_\{t\}and used to produceFtF\_\{t\}andyt′y^\{\\prime\}\_\{t\}\. Ifat′≠ata^\{\\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\.,at′=ata^\{\\prime\}\_\{t\}=a\_\{t\}, the system invokes𝒜flow\\mathcal\{A\}\_\{\\mathrm\{flow\}\}\. Using the current workflowVtV\_\{t\}and execution recordRtR\_\{t\},𝒜flow\\mathcal\{A\}\_\{\\mathrm\{flow\}\}diagnoses verification\-target coverage, the mathematical objects, and computational evidence, then producesVt′V^\{\\prime\}\_\{t\}:

Vt′=𝒜flow​\(q,yt,Vt,Rt\)\.V^\{\\prime\}\_\{t\}=\\mathcal\{A\}\_\{\\mathrm\{flow\}\}\(q,y\_\{t\},V\_\{t\},R\_\{t\}\)\.\(3\)Verification\-workflow revision improves checks insufficiently covered byVtV\_\{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τtflow\\tau\_\{t\}^\{\\mathrm\{flow\}\}, the backend is again invoked through𝒜tool\\mathcal\{A\}\_\{\\mathrm\{tool\}\}:

κtflow=𝒜tool​\(τtflow;𝕋\),ztflow=Run⁡\(κtflow\)\.\\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 resultztflowz\_\{t\}^\{\\mathrm\{flow\}\}may updateRtR\_\{t\}and guide construction ofVt′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:

\(yt\+1,at\+1\)=\{\(yt′,at′\),at′≠at,\(yt,at\),at′=at\.\(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\)Ifat′≠ata^\{\\prime\}\_\{t\}\\neq a\_\{t\}, the next iteration verifiesat′a^\{\\prime\}\_\{t\}; otherwise, it retainsata\_\{t\}and usesVt′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τ\\tauis a local mathematical computation request, enclosed by<tool\_flow\>\.\.\.</tool\_flow\>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τ\\taucan 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 costsccand a vanilla barc\+2c\+2\. Jamie buys one chocolate and three vanilla bars, while Kevin buys five chocolate bars\. The candidate answer is8​c\+68c\+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 ifSimplify⁡\(Δ​\(c\)\)≡0\\operatorname\{Simplify\}\(\\Delta\(c\)\)\\equiv 0\.MTF request\.<tool\_flow\>Context: c is symbolic\.Object: Delta\(c\)=c\+3\*\(c\+2\)\+5\*c\-\(8\*c\+6\)\.Return: simplify\(Delta\(c\)\)\.</tool\_flow\>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\)\+5\*c\-\(8\*c\+6\)z\_tau = sympy\.simplify\(D\)The backend returnszτ=c≢0z\_\{\\tau\}=c\\not\\equiv 0; hence the candidate fails verification andrt=0r\_\{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 helpsAMTFVavoid 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τ\\tauand𝕋\\mathbb\{T\},𝒜tool\\mathcal\{A\}\_\{\\mathrm\{tool\}\}generates an executable callκτ\\kappa\_\{\\tau\}:

κτ=𝒜tool​\(τ;𝕋\)=\(𝒯j,uj\),𝒯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 anduju\_\{j\}its input\. The agent selects𝒯j\\mathcal\{T\}\_\{j\}according toρτ\\rho\_\{\\tau\}and constructsuju\_\{j\}fromΓτ\\Gamma\_\{\\tau\}andℳτ\\mathcal\{M\}\_\{\\tau\}\.

The backend executes the call and returns

zτ=Run⁡\(κτ\)=𝒯j​\(uj\)\.z\_\{\\tau\}=\\operatorname\{Run\}\(\\kappa\_\{\\tau\}\)=\\mathcal\{T\}\_\{j\}\(u\_\{j\}\)\.Here,zτz\_\{\\tau\}is the result specified byρτ\\rho\_\{\\tau\}\.

The resultzτz\_\{\\tau\}is enclosed in<result\>and appended to execution recordRR:

R←Append⁡\(R,\(τ,𝒯j,uj,zτ\)\)\.R\\leftarrow\\operatorname\{Append\}\\bigl\(R,\(\\tau,\\mathcal\{T\}\_\{j\},u\_\{j\},z\_\{\\tau\}\)\\bigr\)\.The three agents use results inRRfor 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\}\}\.

Table 1:Main results\. Avg denotes sample\-weighted average accuracy across the five datasets\. In theAMTFVrow, bold indicates the highest or tied\-highest value among all correction methods in the corresponding column, and italics indicate the second\-highest value\.![Refer to caption](https://arxiv.org/html/2607.29549v1/x3.png)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 withmax\_turn=3\\texttt\{max\\\_turn\}=3\. Blue annotations report the absolute improvement ofAMTFVover the better result between ProgCo and ProgCo\-Py, in percentage points\.

## Experiments

We evaluateAMTFVfor 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](https://arxiv.org/html/2607.29549#A3.F9)\), 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 2025each contain 30 American Invitational Mathematics Examination problems assessing multistep reasoning and exact computation\.BRUMO 2025contains 30 challenging problems assessing complex\-condition understanding and multistep reasoning\.HMMT February 2025contains 30 competition problems spanning algebra, geometry, combinatorics, and number theory\(Hochlehnertet al\.[2025](https://arxiv.org/html/2607.29549#bib.bib10); Peiet al\.[2025](https://arxiv.org/html/2607.29549#bib.bib11)\)\.AMO Benchcontains 50 Olympiad\-level problems with more diverse problem and answer formats\(Liuet al\.[2026a](https://arxiv.org/html/2607.29549#bib.bib12)\)\.

Base models\.We cover DeepSeek, GPT, and Gemini\. The main experiments useDeepSeek\-Flash,DeepSeek\-Flash\-Think, andDeepSeek\-Proto compare correction across non\-thinking, thinking, and stronger\-model settings\(DeepSeek[2026](https://arxiv.org/html/2607.29549#bib.bib7)\)\. For cross\-model generalization, we further compare ProgCo, ProgCo\-Py, andAMTFVusingGPT\-5\.4\-MiniandGPT\-5\.4\-Mini\-Think\(OpenAI[2026](https://arxiv.org/html/2607.29549#bib.bib37)\), andGemini\-2\.5\-Flash\-LiteandGemini\-2\.5\-Flash\-Lite\-Think\(Google AI for Developers[2026a](https://arxiv.org/html/2607.29549#bib.bib8),[b](https://arxiv.org/html/2607.29549#bib.bib9)\)\.

Compared methods\.The main experiments compare three method classes\. Natural\-language correction includesreflex, the vanilla\-reflex configuration from ProgCo;Self\-Refine\(Madaanet al\.[2023](https://arxiv.org/html/2607.29549#bib.bib2)\);Self\-Reflection\(Shinnet al\.[2023](https://arxiv.org/html/2607.29549#bib.bib3)\), abbreviated asSelf\-Refl\.in the table; andCheckList\(Cooket al\.[2024](https://arxiv.org/html/2607.29549#bib.bib4)\)\. They represent vanilla reflection, iterative self\-feedback, self\-reflective feedback, and checklist\-guided correction, respectively\. The reasoning\-enhancedCoT\-Tool\(Abedi Firouzjaei[2025](https://arxiv.org/html/2607.29549#bib.bib6); Weiet al\.[2022](https://arxiv.org/html/2607.29549#bib.bib13); Wanget al\.[2023](https://arxiv.org/html/2607.29549#bib.bib5)\)combines the Cogitator toolkit, multi\-path chain\-of\-thought reasoning, and Self\-Consistency selection\. Verification\-enhanced methods includeProgCo, which uses program\-driven verification and refinement, andProgCo\-Py, our setting that enables Python\-tool feedback in the official implementation\(Songet al\.[2025](https://arxiv.org/html/2607.29549#bib.bib1)\)\. Cross\-model and progressive comparisons focus on ProgCo, ProgCo\-Py, andAMTFV, 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 setmax\_turn=3\\texttt\{max\\\_turn\}=3for 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](https://arxiv.org/html/2607.29549#A1.T2)and[3](https://arxiv.org/html/2607.29549#A1.T3)\)\. We also analyze correction\-state transitions and verification\-complexity bins\.

### Main Results

Table[1](https://arxiv.org/html/2607.29549#Sx3.T1)compares the final\-answer accuracy ofAMTFVand representative baselines under the three main evaluation settings: DeepSeek\-Flash, DeepSeek\-Flash\-Think, and DeepSeek\-Pro\.AMTFVachieves 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\.3percentage 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,AMTFVpreserves 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\.

AMTFValso 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\.7percentage 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, andAMTFVacross base models\. They form a progressive architectural sequence: ProgCo uses program\-driven verification and correction; ProgCo\-Py adds Python execution feedback; andAMTFVadds MTF, a mathematical toolbox interface, and closed\-loop verification\-workflow revision\. Unless stated otherwise,max\_turn=3\\texttt\{max\\\_turn\}=3\.

Figure[3](https://arxiv.org/html/2607.29549#Sx3.F3)compares average accuracy across all seven base\-model settings\.AMTFVranks highest in every setting, exceeding the better of ProgCo and ProgCo\-Py by\+0\.6\+0\.6to\+8\.3\+8\.3percentage points; its gains thus extend beyond DeepSeek\. The supplementary material reports per\-dataset GPT and Gemini results \(see Supplementary Tables[4](https://arxiv.org/html/2607.29549#A2.T4)and[5](https://arxiv.org/html/2607.29549#A2.T5)\)\. Python execution feedback lets ProgCo\-Py improve over ProgCo in some settings, but inconsistently\. By contrast,AMTFVuses 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\.

![Refer to caption](https://arxiv.org/html/2607.29549v1/x4.png)Figure 4:Overall average\-accuracy trajectories under different iteration budgets\. The horizontal axis shows Initial Score,max\_turn=1\\texttt\{max\\\_turn\}=1, andmax\_turn=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 tomax\_turn=3\\texttt\{max\\\_turn\}=3, in percentage points\.Figure[4](https://arxiv.org/html/2607.29549#Sx4.F4)suggests that, under a fixed budget,AMTFVuses additional verification–correction rounds more effectively\. The supplementary material provides trajectories for individual model settings \(see Supplementary Figure[7](https://arxiv.org/html/2607.29549#A2.F7)\)\.

### Correction Behavior and Verification Complexity Analysis

We analyzeAMTFV’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, whereCCandWWdenote correct and incorrect answers\.W→CW\\rightarrow Cmeasures error correction, whereasC→WC\\rightarrow Wmeasures the risk of corrupting a correct answer\.

![Refer to caption](https://arxiv.org/html/2607.29549v1/x5.png)Figure 5:Row\-normalized correction\-state transition matrices\. Rows indicate initial correctness and columns indicate final correctness, whereCCdenotes a correct answer andWWan 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 transitionsW→CW\\rightarrow C, while red borders and arrows highlight error\-introducing transitionsC→WC\\rightarrow W\.Figure[5](https://arxiv.org/html/2607.29549#Sx4.F5)aggregates7×170=11907\\times 170=1190model–problem instances across seven base models\.AMTFV’sW→CW\\rightarrow Crate is 18\.4%, versus 9\.4% for ProgCo and 12\.2% for ProgCo\-Py\. ItsC→WC\\rightarrow Wrate 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

![Refer to caption](https://arxiv.org/html/2607.29549v1/x6.png)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 covers7×170=11907\\times 170=1190instances and compares all methods on the same examples per bin\. Supplementary Figure[8](https://arxiv.org/html/2607.29549#A3.F8)shows a positive relationship between problem\-level verification complexity and empirical difficulty: Pearsonr=0\.67r=0\.67and Spearmanρ=0\.70\\rho=0\.70\.

Figure[6](https://arxiv.org/html/2607.29549#Sx4.F6)shows little gain from any verification\-enhanced method in the Low bin\. Normalized by Initial Score,AMTFV’s gains are39\.2%39\.2\\%and84\.6%84\.6\\%in the Medium and High bins, exceeding ProgCo\-Py by approximately20\.020\.0and29\.229\.2percentage 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](https://arxiv.org/html/2607.29549#A4.T6)\)\. They show howAMTFVuses MTF results for global constraints, exhaustive enumeration, and exact\-computation verification, and detail an exact double\-summation case from the B25 dataset\.

## Conclusion

We introduceAMTFVto 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 thatAMTFVoutperforms 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\.

## References

- H\. Abedi Firouzjaei \(2025\)Cogitator: a python toolkit for chain\-of\-thought prompting\.Zenodo\.External Links:[Document](https://dx.doi.org/10.5281/zenodo.15331821),[Link](https://github.com/habedi/cogitator)Cited by:[Experimental Setup](https://arxiv.org/html/2607.29549#Sx4.SSx1.p3.1)\.
- J\. Boye and B\. Moell \(2025\)Large language models and mathematical reasoning failures\.External Links:2502\.11574,[Link](https://arxiv.org/abs/2502.11574)Cited by:[Introduction](https://arxiv.org/html/2607.29549#Sx1.p1.1),[Related Work](https://arxiv.org/html/2607.29549#Sx2.p4.1)\.
- W\. Chen, Y\. Su, J\. Zuo, C\. Yang, C\. Yuan, C\. Chan, H\. Yu, Y\. Lu, Y\. Hung, C\. Qian, Y\. Qin, X\. Cong, R\. Xie, Z\. Liu, M\. Sun, and J\. Zhou \(2024\)AgentVerse: facilitating multi\-agent collaboration and exploring emergent behaviors\.InThe Twelfth International Conference on Learning Representations,Cited by:[Related Work](https://arxiv.org/html/2607.29549#Sx2.p3.1)\.
- W\. Chen, X\. Ma, X\. Wang, and W\. W\. Cohen \(2023\)Program of thoughts prompting: disentangling computation from reasoning for numerical reasoning tasks\.Transactions on Machine Learning Research\.External Links:[Link](https://openreview.net/forum?id=YfZ4ZPt8zd)Cited by:[Introduction](https://arxiv.org/html/2607.29549#Sx1.p2.1),[Related Work](https://arxiv.org/html/2607.29549#Sx2.p3.1)\.
- K\. Cobbe, V\. Kosaraju, M\. Bavarian, M\. Chen, H\. Jun, L\. Kaiser, M\. Plappert, J\. Tworek, J\. Hilton, R\. Nakano, C\. Hesse, and J\. Schulman \(2021\)Training verifiers to solve math word problems\.External Links:2110\.14168,[Document](https://dx.doi.org/10.48550/arXiv.2110.14168),[Link](https://arxiv.org/abs/2110.14168)Cited by:[Introduction](https://arxiv.org/html/2607.29549#Sx1.p1.1),[Related Work](https://arxiv.org/html/2607.29549#Sx2.p4.1)\.
- J\. Cook, T\. Rocktäschel, J\. Foerster, D\. Aumiller, and A\. Wang \(2024\)TICKing all the boxes: generated checklists improve LLM evaluation and generation\.InNeurIPS 2024 Workshop on Language Gamification,External Links:[Link](https://neurips.cc/virtual/2024/106582)Cited by:[Introduction](https://arxiv.org/html/2607.29549#Sx1.p2.1),[Related Work](https://arxiv.org/html/2607.29549#Sx2.p2.1),[Experimental Setup](https://arxiv.org/html/2607.29549#Sx4.SSx1.p3.1)\.
- DeepSeek \(2026\)DeepSeek v4 preview release\.Note:https://api\-docs\.deepseek\.com/news/news260424Accessed: 2026\-07\-22Cited by:[§A\.1](https://arxiv.org/html/2607.29549#A1.SS1.p1.1),[Experimental Setup](https://arxiv.org/html/2607.29549#Sx4.SSx1.p2.1)\.
- L\. Gao, A\. Madaan, S\. Zhou, U\. Alon, P\. Liu, Y\. Yang, J\. Callan, and G\. Neubig \(2023\)PAL: program\-aided language models\.InProceedings of the 40th International Conference on Machine Learning,Proceedings of Machine Learning Research, Vol\.202,pp\. 10764–10799\.External Links:[Link](https://proceedings.mlr.press/v202/gao23f.html)Cited by:[Introduction](https://arxiv.org/html/2607.29549#Sx1.p2.1),[Related Work](https://arxiv.org/html/2607.29549#Sx2.p3.1)\.
- Google AI for Developers \(2026a\)Gemini 2\.5 flash\-lite\.Note:https://ai\.google\.dev/gemini\-api/docs/models/gemini\-2\.5\-flash\-liteAccessed: 2026\-07\-22Cited by:[§A\.1](https://arxiv.org/html/2607.29549#A1.SS1.p1.1),[Experimental Setup](https://arxiv.org/html/2607.29549#Sx4.SSx1.p2.1)\.
- Google AI for Developers \(2026b\)Gemini api openai compatibility\.Note:https://ai\.google\.dev/gemini\-api/docs/openaiAccessed: 2026\-06\-05Cited by:[§A\.1](https://arxiv.org/html/2607.29549#A1.SS1.p1.1),[Experimental Setup](https://arxiv.org/html/2607.29549#Sx4.SSx1.p2.1)\.
- Z\. Gou, Z\. Shao, Y\. Gong, Y\. Shen, Y\. Yang, M\. Huang, N\. Duan, and W\. Chen \(2024\)ToRA: a tool\-integrated reasoning agent for mathematical problem solving\.InThe Twelfth International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=Ep0TtjVoap)Cited by:[Introduction](https://arxiv.org/html/2607.29549#Sx1.p2.1),[Related Work](https://arxiv.org/html/2607.29549#Sx2.p3.1)\.
- D\. Guoet al\.\(2025\)DeepSeek\-R1 incentivizes reasoning in LLMs through reinforcement learning\.Nature645,pp\. 633–638\.External Links:[Document](https://dx.doi.org/10.1038/s41586-025-09422-z),[Link](https://doi.org/10.1038/s41586-025-09422-z)Cited by:[Introduction](https://arxiv.org/html/2607.29549#Sx1.p1.1)\.
- A\. Hochlehnert, H\. Bhatnagar, V\. Udandarao, S\. Albanie, A\. Prabhu, and M\. Bethge \(2025\)A sober look at progress in language model reasoning: pitfalls and paths to reproducibility\.InSecond Conference on Language Modeling,Note:Dataset page:https://huggingface\.co/datasets/bethgelab/sober\_reasoningExternal Links:[Link](https://openreview.net/forum?id=90UrTTxp5O)Cited by:[Experimental Setup](https://arxiv.org/html/2607.29549#Sx4.SSx1.p1.1)\.
- S\. Hong, M\. Zhuge, J\. Chen, X\. Zheng, Y\. Cheng, J\. Wang, C\. Zhang, Z\. Wang, S\. K\. S\. Yau, Z\. Lin, L\. Zhou, C\. Ran, L\. Xiao, C\. Wu, and J\. Schmidhuber \(2024\)MetaGPT: meta programming for a multi\-agent collaborative framework\.InThe Twelfth International Conference on Learning Representations,Cited by:[Related Work](https://arxiv.org/html/2607.29549#Sx2.p3.1)\.
- J\. Huang, X\. Chen, S\. Mishra, H\. S\. Zheng, A\. W\. Yu, X\. Song, and D\. Zhou \(2024\)Large language models cannot self\-correct reasoning yet\.InThe Twelfth International Conference on Learning Representations,External Links:[Link](https://proceedings.iclr.cc/paper_files/paper/2024/hash/8b4add8b0aa8749d80a34ca5d941c355-Abstract-Conference.html)Cited by:[Introduction](https://arxiv.org/html/2607.29549#Sx1.p2.1),[Related Work](https://arxiv.org/html/2607.29549#Sx2.p2.1)\.
- R\. Kamoi, Y\. Zhang, N\. Zhang, J\. Han, and R\. Zhang \(2024\)When can LLMs actually correct their own mistakes? a critical survey of self\-correction of LLMs\.Transactions of the Association for Computational Linguistics12,pp\. 1417–1440\.External Links:[Link](https://aclanthology.org/2024.tacl-1.78/),[Document](https://dx.doi.org/10.1162/tacl%5Fa%5F00713)Cited by:[Introduction](https://arxiv.org/html/2607.29549#Sx1.p2.1),[Related Work](https://arxiv.org/html/2607.29549#Sx2.p2.1)\.
- J\. Liu, S\. An, S\. Zhou, D\. Ma, Y\. Lin, X\. Lv, X\. Wang, X\. Li, Z\. Wang, X\. Cao, and X\. Cai \(2026a\)AMO\-bench: large language models still struggle in high school math competitions\.InFindings of the Association for Computational Linguistics: ACL 2026,San Diego, California, United States,pp\. 2120–2137\.External Links:[Link](https://aclanthology.org/2026.findings-acl.101/),[Document](https://dx.doi.org/10.18653/v1/2026.findings-acl.101)Cited by:[Experimental Setup](https://arxiv.org/html/2607.29549#Sx4.SSx1.p1.1)\.
- Y\. Liu, Y\. Chen, J\. Zhou, Y\. Hao, J\. Wang, Y\. Zhang, N\. Li, and C\. Fan \(2026b\)R1\-code\-interpreter: LLMs reason with code via supervised and multi\-stage reinforcement learning\.InThe Fourteenth International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=FNlNH0iFOx)Cited by:[Related Work](https://arxiv.org/html/2607.29549#Sx2.p3.1)\.
- H\. Luo, H\. Feng, Q\. Sun, C\. Xu, K\. Zheng, Y\. Wang, T\. Yang, H\. Hu, and Y\. Tang \(2026\)AgentMath: empowering mathematical reasoning for large language models via tool\-augmented agent\.InThe Fourteenth International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=e2s7YHeVZW)Cited by:[Related Work](https://arxiv.org/html/2607.29549#Sx2.p3.1)\.
- R\. Ma, P\. Wang, C\. Liu, X\. Liu, J\. Chen, B\. Zhang, X\. Zhou, N\. Du, and J\. Li \(2025\)S2R: teaching LLMs to self\-verify and self\-correct via reinforcement learning\.InProceedings of the 63rd Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\),Vienna, Austria,pp\. 22632–22654\.External Links:[Link](https://aclanthology.org/2025.acl-long.1104/),[Document](https://dx.doi.org/10.18653/v1/2025.acl-long.1104)Cited by:[Related Work](https://arxiv.org/html/2607.29549#Sx2.p2.1)\.
- A\. Madaan, N\. Tandon, P\. Gupta, S\. Hallinan, L\. Gao, S\. Wiegreffe, U\. Alon, N\. Dziri, S\. Prabhumoye, Y\. Yang, S\. Gupta, B\. P\. Majumder, K\. Hermann, S\. Welleck, A\. Yazdanbakhsh, and P\. Clark \(2023\)Self\-refine: iterative refinement with self\-feedback\.InAdvances in Neural Information Processing Systems,Vol\.36,pp\. 46534–46594\.External Links:[Link](https://proceedings.neurips.cc/paper_files/paper/2023/hash/91edff07232fb1b55a505a9e9f6c0ff3-Abstract-Conference.html)Cited by:[Introduction](https://arxiv.org/html/2607.29549#Sx1.p2.1),[Related Work](https://arxiv.org/html/2607.29549#Sx2.p2.1),[Experimental Setup](https://arxiv.org/html/2607.29549#Sx4.SSx1.p3.1)\.
- A\. Meurer, C\. P\. Smith, M\. Paprocki, O\. Čertík, S\. B\. Kirpichev, M\. Rocklin, A\. Kumar, S\. Ivanov, J\. K\. Moore, S\. Singh, T\. Rathnayake, S\. Vig, B\. E\. Granger, R\. P\. Muller, F\. Bonazzi, H\. Gupta, S\. Vats, F\. Johansson, F\. Pedregosa, M\. J\. Curry, A\. R\. Terrel, S\. Roučka, A\. Saboo, I\. Fernando, S\. Kulal, R\. Cimrman, and A\. Scopatz \(2017\)SymPy: symbolic computing in python\.PeerJ Computer Science3,pp\. e103\.External Links:[Link](https://peerj.com/articles/cs-103/),[Document](https://dx.doi.org/10.7717/peerj-cs.103)Cited by:[Introduction](https://arxiv.org/html/2607.29549#Sx1.p3.1)\.
- OpenAI \(2026\)GPT\-5\.4 mini model\.Note:https://developers\.openai\.com/api/docs/models/gpt\-5\.4\-miniAccessed: 2026\-07\-22Cited by:[§A\.1](https://arxiv.org/html/2607.29549#A1.SS1.p1.1),[Experimental Setup](https://arxiv.org/html/2607.29549#Sx4.SSx1.p2.1)\.
- L\. Pan, M\. Saxon, W\. Xu, D\. Nathani, X\. Wang, and W\. Y\. Wang \(2024\)Automatically correcting large language models: surveying the landscape of diverse automated correction strategies\.Transactions of the Association for Computational Linguistics12,pp\. 484–506\.External Links:[Link](https://aclanthology.org/2024.tacl-1.27/),[Document](https://dx.doi.org/10.1162/tacl%5Fa%5F00660)Cited by:[Introduction](https://arxiv.org/html/2607.29549#Sx1.p2.1),[Related Work](https://arxiv.org/html/2607.29549#Sx2.p2.1)\.
- Q\. Pei, Z\. Pan, H\. Lin, X\. Gao, Y\. Li, Z\. Tang, C\. He, R\. Yan, and L\. Wu \(2025\)ScaleDiff: scaling difficult problems for advanced mathematical reasoning\.Note:Dataset page:https://huggingface\.co/datasets/QizhiPei/ScaleDiff\-MathExternal Links:2509\.21070,[Link](https://arxiv.org/abs/2509.21070)Cited by:[Experimental Setup](https://arxiv.org/html/2607.29549#Sx4.SSx1.p1.1)\.
- S\. Qiao, H\. Gui, C\. Lv, Q\. Jia, H\. Chen, and N\. Zhang \(2024\)Making language models better tool learners with execution feedback\.InProceedings of the 2024 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies \(Volume 1: Long Papers\),Mexico City, Mexico,pp\. 3550–3568\.External Links:[Link](https://aclanthology.org/2024.naacl-long.195/),[Document](https://dx.doi.org/10.18653/v1/2024.naacl-long.195)Cited by:[Related Work](https://arxiv.org/html/2607.29549#Sx2.p3.1)\.
- T\. Schick, J\. Dwivedi\-Yu, R\. Dessì, R\. Raileanu, M\. Lomeli, E\. Hambro, L\. Zettlemoyer, N\. Cancedda, and T\. Scialom \(2023\)Toolformer: language models can teach themselves to use tools\.InAdvances in Neural Information Processing Systems,Vol\.36,pp\. 68539–68551\.External Links:[Link](https://proceedings.neurips.cc/paper_files/paper/2023/hash/d842425e4bf79ba039352da0f658a906-Abstract-Conference.html)Cited by:[Related Work](https://arxiv.org/html/2607.29549#Sx2.p3.1)\.
- N\. Shinn, F\. Cassano, A\. Gopinath, K\. Narasimhan, and S\. Yao \(2023\)Reflexion: language agents with verbal reinforcement learning\.InAdvances in Neural Information Processing Systems,Vol\.36,pp\. 8634–8652\.External Links:[Link](https://proceedings.neurips.cc/paper_files/paper/2023/hash/1b44b878bb782e6954cd888628510e90-Abstract-Conference.html)Cited by:[Introduction](https://arxiv.org/html/2607.29549#Sx1.p2.1),[Related Work](https://arxiv.org/html/2607.29549#Sx2.p2.1),[Experimental Setup](https://arxiv.org/html/2607.29549#Sx4.SSx1.p3.1)\.
- X\. Song, Y\. Wu, W\. Wang, J\. Liu, W\. Su, and B\. Zheng \(2025\)ProgCo: program helps self\-correction of large language models\.InProceedings of the 63rd Annual Meeting of the Association for Computational Linguistics \(Volume 2: Short Papers\),Vienna, Austria,pp\. 944–959\.External Links:[Link](https://aclanthology.org/2025.acl-short.73/),[Document](https://dx.doi.org/10.18653/v1/2025.acl-short.73)Cited by:[Introduction](https://arxiv.org/html/2607.29549#Sx1.p1.1),[Introduction](https://arxiv.org/html/2607.29549#Sx1.p2.1),[Related Work](https://arxiv.org/html/2607.29549#Sx2.p4.1),[Experimental Setup](https://arxiv.org/html/2607.29549#Sx4.SSx1.p3.1)\.
- G\. Tyen, H\. Mansoor, V\. Carbune, P\. Chen, and T\. Mak \(2024\)LLMs cannot find reasoning errors, but can correct them given the error location\.InFindings of the Association for Computational Linguistics: ACL 2024,Bangkok, Thailand,pp\. 13894–13908\.External Links:[Link](https://aclanthology.org/2024.findings-acl.826/),[Document](https://dx.doi.org/10.18653/v1/2024.findings-acl.826)Cited by:[Introduction](https://arxiv.org/html/2607.29549#Sx1.p2.1),[Related Work](https://arxiv.org/html/2607.29549#Sx2.p2.1)\.
- X\. Wang, J\. Wei, D\. Schuurmans, Q\. V\. Le, E\. H\. Chi, S\. Narang, A\. Chowdhery, and D\. Zhou \(2023\)Self\-consistency improves chain of thought reasoning in language models\.InInternational Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=1PL1NIMMrw)Cited by:[Introduction](https://arxiv.org/html/2607.29549#Sx1.p2.1),[Related Work](https://arxiv.org/html/2607.29549#Sx2.p2.1),[Experimental Setup](https://arxiv.org/html/2607.29549#Sx4.SSx1.p3.1)\.
- J\. Wei, X\. Wang, D\. Schuurmans, M\. Bosma, B\. Ichter, F\. Xia, E\. H\. Chi, Q\. V\. Le, and D\. Zhou \(2022\)Chain\-of\-thought prompting elicits reasoning in large language models\.InAdvances in Neural Information Processing Systems,Vol\.35,pp\. 24824–24837\.External Links:[Link](https://proceedings.neurips.cc/paper_files/paper/2022/hash/9d5609613524ecf4f15af0f7b31abca4-Abstract-Conference.html)Cited by:[Experimental Setup](https://arxiv.org/html/2607.29549#Sx4.SSx1.p3.1)\.
- Q\. Wu, G\. Bansal, J\. Zhang, Y\. Wu, B\. Li, E\. Zhu, L\. Jiang, X\. Zhang, S\. Zhang, J\. Liu, A\. H\. Awadallah, R\. W\. White, D\. Burger, and C\. Wang \(2024\)AutoGen: enabling next\-gen LLM applications via multi\-agent conversations\.InFirst Conference on Language Modeling,External Links:[Link](https://openreview.net/forum?id=BAakY1hNKS)Cited by:[Related Work](https://arxiv.org/html/2607.29549#Sx2.p3.1)\.
- A\. Yang, B\. Zhang, B\. Hui, B\. Gao, B\. Yu, C\. Li, D\. Liu, J\. Tu, J\. Zhou, J\. Lin, K\. Lu, M\. Xue, R\. Lin, T\. Liu, X\. Ren, and Z\. Zhang \(2024\)Qwen2\.5\-Math technical report: toward mathematical expert model via self\-improvement\.External Links:2409\.12122,[Link](https://arxiv.org/abs/2409.12122)Cited by:[Introduction](https://arxiv.org/html/2607.29549#Sx1.p1.1)\.
- S\. Yao, J\. Zhao, D\. Yu, N\. Du, I\. Shafran, K\. Narasimhan, and Y\. Cao \(2023\)ReAct: synergizing reasoning and acting in language models\.InInternational Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=WE_vluYUL-X)Cited by:[Related Work](https://arxiv.org/html/2607.29549#Sx2.p3.1)\.
- S\. Zhan, Y\. Lai, Z\. Lu, D\. Lin, Z\. Yang, and F\. Tan \(2026\)MathSmith: towards extremely hard mathematical reasoning by forging synthetic problems with a reinforced policy\.InProceedings of the AAAI Conference on Artificial Intelligence,Vol\.40,pp\. 34602–34610\.External Links:[Document](https://dx.doi.org/10.1609/aaai.v40i41.40760)Cited by:[Introduction](https://arxiv.org/html/2607.29549#Sx1.p1.1)\.
- X\. Zhao, T\. Xu, X\. Wang, Z\. Chen, D\. Jin, L\. Tan, Y\. Lin, Z\. Yu, Z\. Zhao, Y\. He, S\. Wang, H\. Fang, S\. Chandar, and C\. Zhu \(2025\)Boosting LLM reasoning via spontaneous self\-correction\.InSecond Conference on Language Modeling,External Links:[Link](https://openreview.net/forum?id=9DCQAGBoII)Cited by:[Related Work](https://arxiv.org/html/2607.29549#Sx2.p2.1)\.

Supplementary Material

The main text reports complete results under the primary DeepSeek evaluation settings\. This supplementary document provides implementation details and fair\-comparison settings, together with detailed results for verification\-enhanced methods under GPT and Gemini, analyses of iteration budgets, the relationship between empirical difficulty and verification complexity, MTF call types, successful cases, and complete case\-process comparisons\. These materials further documentAMTFV’s evaluation protocol, cross\-model performance, runtime behavior, verification\-complexity signal, distribution of tool calls, and verification–correction process\.

## Appendix AImplementation Details and Fair\-Comparison Protocol

This section describes base\-model configurations, shared initialization, generation parameters, method budgets, and answer evaluation\. Experimental settings are controlled separately for each base model\. For example, under DeepSeek\-Flash, all compared methods use the same model identifier and reasoning mode and, when applicable, share the same initial response, candidate answer, temperature, maximum number of outer iterations, and final evaluation criteria\. Each GPT and Gemini setting follows the same principle\. Here, “the same configuration” refers only to comparisons among methods using the same base model; it does not imply identical configurations across different base models\.

### A\.1Base Models and Reasoning Configurations

Table[2](https://arxiv.org/html/2607.29549#A1.T2)lists the model settings used in this paper and their corresponding official model identifiers\. Names with the\-Thinksuffix are experimental labels used to distinguish reasoning configurations, not additional official model identifiers\. For example, GPT\-5\.4\-Mini and GPT\-5\.4\-Mini\-Think use the same base model with different reasoning configurations; the two Gemini settings likewise use the same base model and differ only in whether thinking is enabled\. Model identifiers and descriptions of reasoning capabilities follow the corresponding official documentation\(DeepSeek[2026](https://arxiv.org/html/2607.29549#bib.bib7); OpenAI[2026](https://arxiv.org/html/2607.29549#bib.bib37); Google AI for Developers[2026a](https://arxiv.org/html/2607.29549#bib.bib8),[b](https://arxiv.org/html/2607.29549#bib.bib9)\)\.

Table 2:Base models and reasoning configurations\.\-Thinkdenotes an experimental setting in which the corresponding reasoning mode is enabled\.
### A\.2Shared Initialization and Within\-Model Fairness

For each base\-model–problem pair, we first use the base model to generate an initial response and extract its initial candidate answer\. reflex, Self\-Refine, Self\-Refl\., CheckList, ProgCo, ProgCo\-Py, andAMTFVall begin from the same corresponding pregenerated initial response and candidate answer\. During execution, these shared initial outputs are loaded in read\-only form rather than resampled by each method\. This design reduces variation from initial responses, so observed differences under the same base\-model setting more directly reflect the methods’ reflection, verification, tool invocation, or correction procedures\. Because CoT\-Tool does not revise an existing response, it directly generates candidate paths from the original problem according to its standard multi\-path reasoning procedure\.

Each method retains the prompt templates and procedures specified by its original paper or official implementation\. We do not rewrite prompts from different methods into a common template because prompt design and processing steps are themselves part of each method\. For a given base model, all methods use the same model identifier, reasoning mode, and applicable shared inputs\. Different base models retain their respective official default configurations; to preserve their individual characteristics, we do not force GPT, Gemini, and DeepSeek to use the same absolute context length\.

### A\.3Generation Parameters and Method Budgets

Model requests use a common OpenAI\-compatible Chat Completions format\. Whenever the parameter is supported, temperature is set to0\. The context window, maximum output length, and other unspecified sampling parameters retain the defaults of the corresponding model API\. Thus, all methods using the same base model share that API’s default context and output limits, while different base models retain their own defaults\.

We did not conduct an extensive hyperparameter search\. The iteration\-budget analysis evaluatesmax\_turn∈\{1,3\}\\texttt\{max\\\_turn\}\\in\\\{1,3\\\}, while the main experiments usemax\_turn=3\\texttt\{max\\\_turn\}=3, giving all iterative methods the same upper bound on outer correction rounds\. The remaining parameters follow the original method specifications or the defaults of the corresponding model API\.

For methods with iterative correction or verification structures, the maximum number of outer iterations is uniformly set tomax\_turn=3\\texttt\{max\\\_turn\}=3\. Following its multi\-path consistency procedure, CoT\-Tool independently generates and selects among33reasoning paths\. Table[3](https://arxiv.org/html/2607.29549#A1.T3)summarizes the outer reasoning budget for each method\. Thus, every iterative method runs for at most33rounds; because their internal structures differ, the numbers of model calls, feedback steps, or tool calls within each round are not forced to be identical\.

Together with the shared initialization described above, the official pipeline performs no randomized local sampling, data shuffling, or stochastic preprocessing, so no local random seed is required\. Each reported model–method–problem result comes from one official run, and the supplementary material includes the raw outputs used to compute the reported aggregates\.

Table 3:Outer reasoning budgets used by different methods\.
### A\.4Mathematical Tool Execution

Both ProgCo\-Py andAMTFVcan receive Python execution feedback, but each organizes tool use according to its own method definition\.AMTFVuses MTF to express the mathematical object to be verified and the desired return, after which the mathematical toolbox agent selects and invokes tools such as SymPy, itertools, Fraction, Decimal, or Z3\. Tool requests, generated calls, returned results, and execution errors are retained to support subsequent adjudication and correction\. Different problems and model settings may run in parallel; concurrency only improves the processing efficiency of independent examples and does not alter the model configuration, input content, or maximum number of outer iterations for any individual example\.

### A\.5Answer Extraction and Unified Evaluation

Each method obtains a candidate answer from its final response using its predefined output format and extraction procedure\. Once extracted, every candidate is compared with the gold answer through the same three\-stage equivalence evaluation\. The first stage performs normalized exact\-string matching\. The second applies floating\-point comparison to numerically parseable answers with a tolerance of10−310^\{\-3\}\. If the first two stages are inconclusive, the third uses the same DeepSeek\-Flash evaluator at temperature0to determine whether the two final answers are mathematically equivalent\. For set\-valued, multi\-solution, and sequence answers, the evaluator also checks element completeness and ordering requirements; incomplete solution sets are not considered equivalent\. All methods use the same gold answers and evaluation rules\. Final accuracy is the proportion of correctly answered examples, and the cross\-dataset Avg is weighted by dataset size\.

##### Code and Data Availability\.

Code will be released athttps://github\.com/TicusFFF/mathematical\-self\-correction\.

## Appendix BSupplementary Results and Iteration\-Budget Analysis

### B\.1Supplementary Results on GPT and Gemini

This section reports detailed average accuracies for ProgCo, ProgCo\-Py, andAMTFVunder the GPT and Gemini settings, supporting the progressive architectural comparison in the main text\. Supplementary Tables[4](https://arxiv.org/html/2607.29549#A2.T4)and[5](https://arxiv.org/html/2607.29549#A2.T5)report results for bothmax\_turn=1\\texttt\{max\\\_turn\}=1andmax\_turn=3\\texttt\{max\\\_turn\}=3to show how each method behaves as the fixed iteration budget changes\.

Table 4:Supplementary results for verification\-enhanced methods on GPT models\. The table reports detailed results for ProgCo, ProgCo\-Py, andAMTFVwithmax\_turn=1\\texttt\{max\\\_turn\}=1andmax\_turn=3\\texttt\{max\\\_turn\}=3\. Avg denotes sample\-weighted average accuracy across the five datasets, and subscripts in the Avg columns show changes relative to Initial Score\.Table 5:Supplementary results for verification\-enhanced methods on Gemini models\. The table reports detailed results for ProgCo, ProgCo\-Py, andAMTFVwithmax\_turn=1\\texttt\{max\\\_turn\}=1andmax\_turn=3\\texttt\{max\\\_turn\}=3\. Avg denotes sample\-weighted average accuracy across the five datasets, and subscripts in the Avg columns show changes relative to Initial Score\.Overall, these supplementary results agree with the progressive architectural comparison in the main text:AMTFVachieves higher average accuracy than ProgCo and ProgCo\-Py under most GPT and Gemini settings, indicating that the observed gains of MTF\-driven verification and correction extend beyond the primary DeepSeek evaluations\. The magnitude of the gains varies across models and thinking/non\-thinking settings, suggesting that base\-model capability and reasoning mode can affect the practical effectiveness of multistep verification and correction\.

### B\.2Iteration Budget Analysis

AMTFVprogressively updates either the candidate answer or the verification workflow through a multistep verification–correction loop\. We analyze the effect of the maximum iteration countmax\_turn, focusing onmax\_turn=1\\texttt\{max\\\_turn\}=1andmax\_turn=3\\texttt\{max\\\_turn\}=3\. All methods are evaluated under the same maximum iteration count, so the results reflect their correction effectiveness under a fixed iteration budget\.

![Refer to caption](https://arxiv.org/html/2607.29549v1/x7.png)Figure 7:Verification–correction performance under different iteration budgets\. The three panels correspond to ProgCo, ProgCo\-Py, andAMTFV\. The horizontal axis shows sample\-weighted average accuracy \(%\) across the five datasets, and the vertical axis lists base\-model settings\. Each trajectory connects Initial Score,max\_turn=1\\texttt\{max\\\_turn\}=1, andmax\_turn=3\\texttt\{max\\\_turn\}=3\. Gain on the right denotes the absolute change from Initial Score tomax\_turn=3\\texttt\{max\\\_turn\}=3, in percentage points\.Figure[7](https://arxiv.org/html/2607.29549#A2.F7)shows the average\-accuracy trajectories of ProgCo, ProgCo\-Py, andAMTFVunder different iteration budgets\. Initial Score is the accuracy before additional correction, while Turn=1 and Turn=3 correspond tomax\_turn=1\\texttt\{max\\\_turn\}=1andmax\_turn=3\\texttt\{max\\\_turn\}=3, respectively\.

Frommax\_turn=1\\texttt\{max\\\_turn\}=1tomax\_turn=3\\texttt\{max\\\_turn\}=3,AMTFVimproves further under most base\-model settings; the largest additional gain is\+10\.0\+10\.0on DeepSeek\-Pro\. Additional iterations are not always monotonically beneficial: on GPT\-5\.4\-Mini,AMTFVdecreases slightly by−0\.6\-0\.6frommax\_turn=1\\texttt\{max\\\_turn\}=1tomax\_turn=3\\texttt\{max\\\_turn\}=3\. Multistep correction can therefore create new opportunities to fix errors but may also cause overcorrection in a small number of cases, motivating comparisons of actual correction quality under the same number of rounds\.

Combined with the overall average trajectories reported in the main paper, the results indicate thatAMTFVimproves by\+8\.8\+8\.8points on average from Initial Score tomax\_turn=3\\texttt\{max\\\_turn\}=3, exceeding the\+3\.4\+3\.4gain of ProgCo and the\+4\.7\+4\.7gain of ProgCo\-Py\.AMTFValso continues to improve frommax\_turn=1\\texttt\{max\\\_turn\}=1tomax\_turn=3\\texttt\{max\\\_turn\}=3, whereas the later gains of ProgCo and ProgCo\-Py are smaller\. Under these evaluated settings,AMTFVtherefore appears to convert additional verification–correction rounds into effective gains more successfully than the ProgCo family\.

## Appendix CVerification\-Complexity and Tool\-Type Analysis

### C\.1Empirical Difficulty and Verification Complexity

The main text uses the instance\-level number of MTF tool calls to define verification\-complexity bins\. We further analyze the relationship between problem\-level verification complexity and empirical difficulty to assess the interpretability of this proxy signal\.

Empirical difficulty is estimated from the initial\-answer accuracy across multiple base\-model settings:

Demp​\(q\)=1−1Mmodel​∑m=1Mmodel𝕀​\[am,q0=aq∗\],D\_\{\\mathrm\{emp\}\}\(q\)=1\-\\frac\{1\}\{M\_\{\\mathrm\{model\}\}\}\\sum\_\{m=1\}^\{M\_\{\\mathrm\{model\}\}\}\\mathbb\{I\}\[a^\{0\}\_\{m,q\}=a\_\{q\}^\{\*\}\],\(5\)
whereMmodelM\_\{\\mathrm\{model\}\}is the number of base\-model settings,am,q0a^\{0\}\_\{m,q\}is the initial candidate answer produced by settingmmfor problemqq, andaq∗a\_\{q\}^\{\*\}is the gold answer\. We define average problem\-level verification complexity as

Cver​\(q\)=1Mmodel​∑m=1Mmodellog⁡\(1\+ntool\(m,q\)\),C\_\{\\mathrm\{ver\}\}\(q\)=\\frac\{1\}\{M\_\{\\mathrm\{model\}\}\}\\sum\_\{m=1\}^\{M\_\{\\mathrm\{model\}\}\}\\log\\\!\\left\(1\+n\_\{\\mathrm\{tool\}\}^\{\(m,q\)\}\\right\),\(6\)
wherentool\(m,q\)n\_\{\\mathrm\{tool\}\}^\{\(m,q\)\}is the number of MTF tool calls produced byAMTFVfor model settingmmand problemqq\. The transformationlog⁡\(1\+ntool\(m,q\)\)\\log\(1\+n\_\{\\mathrm\{tool\}\}^\{\(m,q\)\}\)reduces the influence of extreme call counts on the problem\-level average\.

The instance\-level verification\-complexity bins are defined as

b​\(m,q\)=\{Low,ntool\(m,q\)≤1,Medium,2≤ntool\(m,q\)≤3,High,ntool\(m,q\)≥4\.b\(m,q\)=\\begin\{cases\}\\mathrm\{Low\},&n\_\{\\mathrm\{tool\}\}^\{\(m,q\)\}\\leq 1,\\\\ \\mathrm\{Medium\},&2\\leq n\_\{\\mathrm\{tool\}\}^\{\(m,q\)\}\\leq 3,\\\\ \\mathrm\{High\},&n\_\{\\mathrm\{tool\}\}^\{\(m,q\)\}\\geq 4\.\\end\{cases\}\(7\)
The correlation analysis in Figure[8](https://arxiv.org/html/2607.29549#A3.F8)aggregates over 170 problems\. Pearsonr=0\.67r=0\.67and Spearmanρ=0\.70\\rho=0\.70indicate that problems that are more difficult for the base models generally require more complex MTF verification\. This analysis does not treat tool\-call count as a human difficulty label; rather, it uses the count as a complexity signal from the perspective of the verification process\.

### C\.2MTF Tool\-Type Analysis

Figure[9](https://arxiv.org/html/2607.29549#A3.F9)shows the distribution of MTF call types inAMTFV\. Calls are concentrated primarily in the Enumeration and Symbolic categories, indicating that exhaustive enumeration and symbolic verification are common tool requirements in hard\-test mathematical tasks\. This pattern is consistent with our case analyses: many incorrect answers satisfy some local conditions but omit exhaustive enumeration, global minimality, exact computation, or symbolic\-equivalence checks\.

![[Uncaptioned image]](https://arxiv.org/html/2607.29549v1/x8.png)

Figure 8:Relationship between empirical difficulty and verification complexity\. The horizontal axis shows empirical difficultyDemp​\(q\)D\_\{\\mathrm\{emp\}\}\(q\), estimated from initial\-answer accuracy across seven base\-model settings; the vertical axis shows average problem\-level verification complexityCver​\(q\)C\_\{\\mathrm\{ver\}\}\(q\)\. Box plots show the distribution of problem\-level verification complexity at each empirical\-difficulty level, and red points and lines show the corresponding mean trend\.
![[Uncaptioned image]](https://arxiv.org/html/2607.29549v1/x9.png)

Figure 9:Distribution of MTF call types\. The vertical axis lists MTF tool\-call types, and the horizontal axis shows the corresponding call counts\. Percentages beside the bars indicate each type’s share of all MTF calls\.
These results further illustrate thatAMTFVis designed not simply to let the model generate an arbitrary program\. Instead, MTF organizes the verification target into an explicit mathematical tool\-call request: the model specifies the mathematical objects, constraints, and computational objective to be verified, while the backend performs the corresponding enumeration, symbolic simplification, or exact computation\.

## Appendix DCase Studies and Full Process Comparison

### D\.1Successful Case Study

To illustrate howAMTFVuses MTF and mathematical tool results for correction, we compare several representative successful cases\. In every case, the initial response is incorrect, neither ProgCo nor ProgCo\-Py corrects it, andAMTFVobtains the correct answer through MTF\-driven verification and correction\. Supplementary Table[6](https://arxiv.org/html/2607.29549#A4.T6)summarizes the key differences\. The next section presents the BRUMO25 exact double\-summation case in full as a direct illustration of howAMTFVmodels a mathematical verification target as an exact tool computation and uses structured tool results for candidate\-answer adjudication and revision\.

Table 6:Representative successful correction cases\. The table reports the initial answer, baseline outputs, andAMTFV’s final answer\.
AIME24 minimality verification\.The problem asks for the smallest value satisfying the given conditions\. The initial response gives 155, which satisfies some conditions but is not the required minimum; neither ProgCo nor ProgCo\-Py corrects it\. In contrast,AMTFVnot only checks feasibility but also constructs a minimality target and invokes mathematical tools through MTF to search for a smaller valid candidate\. The tool result supports rejecting 155, and the system ultimately revises the answer to 110\.

AIME25 combinatorial counting\.The initial response considers only a subset of the valid cases and returns 764; ProgCo and ProgCo\-Py retain the same incorrect answer\.AMTFVinstead expresses the counting target as an exhaustive MTF enumeration task, asking the backend to enumerate all combinations satisfying the original constraints\. The tool result exposes cases omitted by the initial reasoning, triggers answer revision, and yields the correct answer 16\.

AMO lattice\-point isosceles triangles\.The problem asks for the smallestnnsuch that every selection ofnnpoints from 15 triangular\-lattice points contains an isosceles triangle\. The initial response, ProgCo, and ProgCo\-Py all return77, relying primarily on the incorrect assumption that the largest isosceles\-free subset has size 6\.AMTFVrepresents the 15 lattice points as

P=\{\(i,j\):0≤j≤4,0≤i≤4−j\},P=\\\{\(i,j\):0\\leq j\\leq 4,\\ 0\\leq i\\leq 4\-j\\\},and exhaustively checks all 6\-point subsets\. The tool result shows that every 6\-point subset contains an isosceles triangle, while the following 5\-point counterexample exists:

\{\(0,0\),\(1,0\),\(2,0\),\(3,0\),\(4,0\)\},\\\{\(0,0\),\(1,0\),\(2,0\),\(3,0\),\(4,0\)\\\},Therefore, the largest isosceles\-free subset has size 5, and the smallest guaranteed number is66\. This case illustrates the role of MTF in exhaustive enumeration over a finite geometric structure and verification of a global guarantee\.

BRUMO25 exact double summation\.The initial response, ProgCo, and ProgCo\-Py all accept the candidate answer46084608; their common error is assuming that the sum of modular\-power residues is46564656for every fixednn\.AMTFVexpresses the verification target as an exact double\-summation task and asks the tool to return the total residueSS, exact valueAA, and rounded resultRR\. The tool returnsS=439312S=439312,A=439312/97A=439312/97, andR=4529R=4529, thereby rejecting 4608 and correcting the answer\.

These cases illustrate two characteristic advantages ofAMTFV\. First, MTF extends candidate verification to global constraints, including minimality, completeness, and feasible\-region coverage\. Second, it delegates enumeration, symbolic computation, and exact numerical computation—steps easily omitted in natural\-language reasoning—to the mathematical toolbox backend\. By writing tool results to the execution record, the system can further support subsequent adjudication, answer revision, and verification\-workflow revision\.

### D\.2Full Case Process Comparison: Exact Double\-Sum Verification

We examine a BRUMO25 exact double\-summation case to illustrate how Initial, ProgCo, ProgCo\-Py, andAMTFVdiffer in verification\-target construction, tool execution, and use of feedback\. The problem asks for

A=∑a=196∑n=196\{an97\}A=\\sum\_\{a=1\}^\{96\}\\sum\_\{n=1\}^\{96\}\\left\\\{\\frac\{a^\{n\}\}\{97\}\\right\\\}rounded to the nearest integer\. The gold answer is45294529, whereas Initial, ProgCo, and ProgCo\-Py all return46084608\.

The common error in the first three outputs is the following implicit assumption: for every fixednn, asaaranges from11to9696,

∑a=196\(anmod97\)=1\+2\+⋯\+96=4656\.\\sum\_\{a=1\}^\{96\}\(a^\{n\}\\bmod 97\)=1\+2\+\\cdots\+96=4656\.This assumption holds only whena↦an\(mod97\)a\\mapsto a^\{n\}\\pmod\{97\}is a permutation of\(ℤ/97​ℤ\)×\(\\mathbb\{Z\}/97\\mathbb\{Z\}\)^\{\\times\}, which requiresgcd⁡\(n,96\)=1\\gcd\(n,96\)=1\. Whengcd⁡\(n,96\)\>1\\gcd\(n,96\)\>1, the image is only a proper subgroup, so the inner sum need not equal46564656\. The central issue is therefore not a simple arithmetic error but an incorrect group\-structure assumption hidden in candidate verification\.

At the programmatic\-verification level, the methods differ primarily in how they organize the computational target and returned result\. ProgCo generates double\-loop verification code based on modular exponentiation, but its final feedback remains primarily a Boolean verdict\. ProgCo\-Py attempts to compute the fractional part ofan/97a^\{n\}/97directly, coupling tool execution with huge powers and floating\-point precision\.AMTFV, in contrast, explicitly represents the target as three mathematical objects,S,A,RS,A,R, and asks the tool to return exact results together with candidate\-matching status\. We next compare how the methods process this candidate answer\.

Problem, ground truth, and Initial response\.Problem\.ComputeA=∑a=196∑n=196\{an97\},A=\\sum\_\{a=1\}^\{96\}\\sum\_\{n=1\}^\{96\}\\left\\\{\\frac\{a^\{n\}\}\{97\}\\right\\\},where\{x\}\\\{x\\\}denotes the fractional part ofxx, and returnAArounded to the nearest integer\.Ground truth\.The gold answer is4529\.4529\.Initial extracted answer\.The final answer extracted from Initial is4608\.4608\.Generated solution\.Initial first rewrites each term as\{an97\}=anmod9797,\\left\\\{\\frac\{a^\{n\}\}\{97\}\\right\\\}=\\frac\{a^\{n\}\\bmod 97\}\{97\},and henceA=197​∑a=196∑n=196\(anmod97\)\.A=\\frac\{1\}\{97\}\\sum\_\{a=1\}^\{96\}\\sum\_\{n=1\}^\{96\}\(a^\{n\}\\bmod 97\)\.Initial then assumes that, for each fixednn, the values ofanmod97a^\{n\}\\bmod 97asaaranges from11to9696can be treated as either a permutation or equal repetitions of all nonzero residue classes1,2,…,961,2,\\ldots,96\. It therefore uses∑a=196\(anmod97\)=1\+2\+⋯\+96=4656\\sum\_\{a=1\}^\{96\}\(a^\{n\}\\bmod 97\)=1\+2\+\\cdots\+96=4656and obtainsA=96⋅465697=96⋅48=4608\.A=\\frac\{96\\cdot 4656\}\{97\}=96\\cdot 48=4608\.The final answer is4608\.\\boxed\{4608\}\.

Initial’s central error is failing to distinguishgcd⁡\(n,96\)=1\\gcd\(n,96\)=1fromgcd⁡\(n,96\)\>1\\gcd\(n,96\)\>1\. In the latter case,a↦an\(mod97\)a\\mapsto a^\{n\}\\pmod\{97\}is not a permutation of the nonzero residue classes, so the inner sum need not equal46564656\. The incorrect candidate46084608therefore arises from inadequate modeling of the mathematical object rather than an error in the final numerical simplification\.

ProgCo\.Final extracted answer\.4608\.4608\.Generated solution\.ProgCo’s final response retains the same central mathematical assumption as Initial\. It likewise writes the fractional part as\{an97\}=anmod9797,\\left\\\{\\frac\{a^\{n\}\}\{97\}\\right\\\}=\\frac\{a^\{n\}\\bmod 97\}\{97\},and assumes that, for each fixednn, the inner sum equals the sum of all nonzero residue classes:∑a=196\(anmod97\)=4656\.\\sum\_\{a=1\}^\{96\}\(a^\{n\}\\bmod 97\)=4656\.ProgCo therefore obtainsA=96⋅465697=4608,A=\\frac\{96\\cdot 4656\}\{97\}=4608,and returns the final answer4608\.\\boxed\{4608\}\.Generated verification code\.ProgCo further generates a verification function for the candidate answer46084608\. The function attempts to compute the original double sum directly:verify\_fractional\_part\_sum\(answer\): A = 0 for a in range\(1, 97\): for n in range\(1, 97\): remainder = pow\(a, n, 97\) A \+= remainder / 97 rounded\_A = round\(A\) return rounded\_A == answerThe verification code computes each remainder using modular exponentiation:remainder = pow\(a,n,97\)and accumulatesA \+= remainder / 97\.\\texttt\{A \+= remainder / 97\}\.Its intended computation isA=197​∑a=196∑n=196\(anmod97\),A=\\frac\{1\}\{97\}\\sum\_\{a=1\}^\{96\}\\sum\_\{n=1\}^\{96\}\(a^\{n\}\\bmod 97\),and then to compare whetherround⁡\(A\)\\operatorname\{round\}\(A\)equals the candidate answer46084608\.Returned verification feedback\.The retained verification feedback states that the96×96=921696\\times 96=9216double loop can be computed directly and claims that the code is independent of the original reasoning and will produce a result consistent with the candidate\. This round therefore returnsTrue,\\texttt\{True\},with feedbackverify passed\.\\texttt\{verify passed\}\.Notably, the feedback does not return the computed total residueSS, exact valueAA, or rounded resultRR; it accepts the candidate through a Boolean verdict\.

ProgCo’s process reflects program\-driven verification: beyond producing a candidate answer, it attempts to express verification as a finite\-summation program\. This design is more concrete than natural\-language reflection alone and seeks to turn answer verification into an executable process\.

In this case, however, ProgCo’s verification feedback does not explicitly return the key mathematical objects

S\\displaystyle S=∑a=196∑n=196\(anmod97\),\\displaystyle=\\sum\_\{a=1\}^\{96\}\\sum\_\{n=1\}^\{96\}\(a^\{n\}\\bmod 7\),A\\displaystyle A=S97,\\displaystyle=\\frac\{S\}\{97\},R\\displaystyle R=round⁡\(A\)\.\\displaystyle=\\operatorname\{round\}\(A\)\.Instead, the feedback only reportsverify passedand accepts46084608\. Although ProgCo generates an apparently direct verification function, its tool feedback does not expose the erroneous assumption in Initial as a traceable, exact mathematical result\.

ProgCo\-Py\.Final extracted answer\.4608\.4608\.Generated solution\.ProgCo\-Py’s final response likewise retains Initial’s core reasoning by transforming\{an97\}\\left\\\{\\frac\{a^\{n\}\}\{97\}\\right\\\}intoanmod9797,\\frac\{a^\{n\}\\bmod 97\}\{97\},and assuming that the inner sum for everynnis1\+2\+⋯\+96=4656\.1\+2\+\\cdots\+96=4656\.It therefore still obtainsA=96⋅465697=4608,A=\\frac\{96\\cdot 4656\}\{97\}=4608,and returns4608\.\\boxed\{4608\}\.Generated Python verification code\.ProgCo\-Py generates Python\-style direct\-computation code to verify46084608\. Unlike ProgCo’s modular\-power implementation, this code first attempts to computean/97a^\{n\}/97and then extract its fractional part:verify\_fractional\_part\_sum\(answer\): A = 0 for a in range\(1, 97\): for n in range\(1, 97\): value = \(a \*\* n\) / 97 fractional\_part = value \- int\(value\) A \+= fractional\_part rounded\_A = round\(A\) return rounded\_A == answerThat is, ProgCo\-Py’s verification code directly computesvalue = \(a \*\* n\) / 97and obtains the fractional part viafractional\_part = value \- int\(value\)\.Python execution and returned result\.The execution feedback notes that directly computingan/97a^\{n\}/97involves extremely large integersana^\{n\}, which may cause floating\-point overflow or severe precision loss; the direct floating\-point implementation is therefore unreliable\. The verification process then falls back to checking the mathematical reasoning in the original solution and again accepts the claim∑a=196\(anmod97\)=4656\\sum\_\{a=1\}^\{96\}\(a^\{n\}\\bmod 97\)=4656for allnn\. This round consequently retainsA=4608,A=4608,The verification result isTrue,\\texttt\{True\},with feedbackverify passed\.\\texttt\{verify passed\}\.

ProgCo\-Py’s process illustrates that adding Python\-tool feedback does not automatically ensure reliable verification\. The problem is not the absence of a tool call, but the continued coupling between tool implementation and the mathematical verification target\. The code computes the fractional part ofan/97a^\{n\}/97directly and is therefore vulnerable to huge powers and floating\-point precision; once direct execution is deemed infeasible, verification returns to the original incorrect assumption\. In other words, the tool call is not reliably converted into an exact mathematical\-object computation and thus fails to correct the candidate46084608\.

AMTFV\.Final extracted answer\.4529\.4529\.Initial candidate\.AMTFVstarts from the same initial candidate answer:4608\.4608\.MTF verification target\.Rather than asking the model to judge the plausibility of46084608directly or relying on the group\-theoretic assumption in the original solution, the verification agent expresses the problem requirement as an exact mathematical computation target:S\\displaystyle S=∑a=196∑n=196\(anmod97\),\\displaystyle=\\sum\_\{a=1\}^\{96\}\\sum\_\{n=1\}^\{96\}\(a^\{n\}\\bmod 7\),A\\displaystyle A=S97,\\displaystyle=\\frac\{S\}\{97\},R\\displaystyle R=round⁡\(A\)\.\\displaystyle=\\operatorname\{round\}\(A\)\.The candidate passes verification if and only ifR=4608\.R=4608\.The corresponding MTF request can be summarized as follows:<tool\_flow\> Let p = 97\. Compute S = sum\_\{a=1\}ˆ96 sum\_\{n=1\}ˆ96 \(aˆn mod p\)\. Compute A = S / p\. Compute R = round\(A\)\. Return S, A, R, and whether R == 4608\. </tool\_flow\>Compiled tool call and structured return\.The mathematical toolbox agent translates this MTF request into exact integer and rational arithmetic rather than direct computation with huge floating\-point values\. The mathematical toolbox backend accumulates integer residues using modular exponentiation:S=∑a=196∑n=196pow⁡\(a,n,97\),S=\\sum\_\{a=1\}^\{96\}\\sum\_\{n=1\}^\{96\}\\operatorname\{pow\}\(a,n,97\),It then computes, in exact rational form,A=S97\.A=\\frac\{S\}\{97\}\.The tool returns the following structured result:S\\displaystyle S=439312,\\displaystyle=39312,A\\displaystyle A=Fraction⁡\(439312,97\),\\displaystyle=\\operatorname\{Fraction\}\(39312,7\),R\\displaystyle R=4529,\\displaystyle=529,\(R=4608\)\\displaystyle\(R=608\)=False\.\\displaystyle=\\texttt\{False\}\.Tool execution result\.The tool result givesA=43931297=4528\+9697,A=\\frac\{439312\}\{97\}=4528\+\\frac\{96\}\{97\},and henceR=round⁡\(A\)=4529\.R=\\operatorname\{round\}\(A\)=4529\.The result also reportsR=4529≠4608\.R=4529\\neq 4608\.Therefore, the candidate answer46084608fails verification:False\.\\texttt\{False\}\.Feedback and answer revision\.Based on the tool result, the feedback identifies Initial’s key error: it assumes that for every fixednn, the mapa↦an\(mod97\)a\\mapsto a^\{n\}\\pmod\{97\}covers all nonzero residue classes\. In fact, this map is a permutation only whengcd⁡\(n,96\)=1\\gcd\(n,96\)=1; whengcd⁡\(n,96\)\>1\\gcd\(n,96\)\>1, its image is a proper subgroup and the inner sum need not equal46564656\.Using this feedback, the answer\-revision stage recomputes the double sum and obtainsA=43931297=4528\+9697\.A=\\frac\{439312\}\{97\}=4528\+\\frac\{96\}\{97\}\.The rounded result is therefore4529\.4529\.Final verification\.Final verification uses45294529as the candidate answer and invokes the same exact\-summation verification target again:S\\displaystyle S=∑a=196∑n=196\(anmod97\),\\displaystyle=\\sum\_\{a=1\}^\{96\}\\sum\_\{n=1\}^\{96\}\(a^\{n\}\\bmod 7\),A\\displaystyle A=S97,\\displaystyle=\\frac\{S\}\{97\},R\\displaystyle R=round⁡\(A\)\.\\displaystyle=\\operatorname\{round\}\(A\)\.The tool again returnsS=439312,R=4529\.S=439312,\\qquad R=4529\.Final verification therefore succeeds:True,verify passed\.\\texttt\{True\},\\qquad\\texttt\{verify passed\}\.AMTFVultimately returns4529\.\\boxed\{4529\}\.

A key advantage ofAMTFVin this case is that it neither asks the model to assess the original reasoning in natural language nor asks it to generate ad hoc code that determines how to compute the answer\. Instead, it first models the verification target explicitly as the exact mathematical objects

S\\displaystyle S=∑a=196∑n=196\(anmod97\),\\displaystyle=\\sum\_\{a=1\}^\{96\}\\sum\_\{n=1\}^\{96\}\(a^\{n\}\\bmod 7\),A\\displaystyle A=S97,\\displaystyle=\\frac\{S\}\{97\},R\\displaystyle R=round⁡\(A\)\.\\displaystyle=\\operatorname\{round\}\(A\)\.The mathematical toolbox backend then performs the finite summation, division by9797, rounding, and candidate comparison\. In this case, the process decouples mathematical modeling from concrete execution: the verification agent specifies*what to compute*, the backend performs*how to compute it*using exact arithmetic, and the returned results support candidate\-answer adjudication and revision\.

##### Discussion\.

The key distinction in this case is not whether code is used, but whether code or tool calls serve an explicit, traceable mathematical verification target\. ProgCo and ProgCo\-Py both attempt to program candidate verification, yet their feedback does not reliably produce exact mathematical objects that support adjudication and correction\. In contrast,AMTFVorganizes the target as an MTF request to the mathematical toolbox, causing the tool to returnSS,AA,RR, and whether the candidate matches\. The system can therefore directly identify the discrepancy between46084608and the true rounded result45294529, and revise the candidate to the correct answer\.