AMTFV: Agentic Mathematical Tool-Flow Verification for LLM Self-Correction Rui Zou1 , Yutao Zhu1 , Mengqi Wei2 , Ji-Rong Wen1∗ 1
2
Gaoling School of Artificial Intelligence, Renmin University of China National Engineering Research Center of Educational Big Data, Central China Normal University {zouruixyz, ytz, jrwen}@ruc.edu.cn, [email protected]
arXiv:2607.29549v1 [cs.AI] 31 Jul 2026
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 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 et al. 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). ∗
Corresponding author.
Existing backward-verification methods mainly follow two paths. The first revises outputs through natural-language selfreflection, 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 codegeneration 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 AMTFV1 (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 1
Code will be released at https://github.com/TicusFFF/mathematical-self-correction/tree/ main/S2-1_AMTFV.
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. 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 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 1: Comparison of natural-language reflection, direct code verification, and AMTFV for mathematical answer verification and correction.
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 multipath 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 SelfConsistency 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: S2 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 Pythonexecuted programs; Program-of-Thoughts separates numeri-
Figure 2: Overview of the AMTFV framework.
cal 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-toolboxoriented 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 and an initial candidate answer a0 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 verificationworkflow 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 Atool 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 Aver , Aans , and Aflow denote the verification, answerrevision, and verification-workflow revision agents, respectively. At iteration t, the system first invokes Aver : ′ (Vt , rt , Rt ) = Aver (q, yt , at ; Vt−1 ). (1) Here, yt is the current response and at its extracted can′ didate answer. The optional Vt−1 is a reference verification workflow; if unavailable, Aver reconstructs one from at . The
executed workflow, adjudication result, and execution record are Vt , rt ∈ {0, 1}, and Rt , respectively. The system returns at if rt = 1; otherwise, it proceeds to feedback and revision. Candidate Verification. At iteration t, Aver constructs Vt to determine whether at satisfies the constraints and objective of q. For steps requiring reliable execution, such as symbolic simplification, enumerative counting, exact computation, or constraint solving, it sends MTF requests to Atool . Returned results are written to Rt and used to produce rt . If verification at iteration t produces an MTF request τtver , the invocation is written as κver = Atool (τtver ; T), ztver = Run(κver t t ). Here, T is the set of tools exposed by the mathematical toolbox backend, κver the generated tool call, and ztver its t result. Answer Revision. When rt = 0, at fails verification and the system invokes Aans . Given the problem q, current response yt , verification workflow Vt , and execution record Rt , Aans produces feedback Ft and a revised response yt′ , from which the system extracts a′t : (Ft , yt′ ) = Aans (q, yt , Vt , Rt ),
(2) a′t = Extract(yt′ ). To recompute an expression, enumerate a candidate set, or check constraint feasibility during revision, the agent may produce τtans and invoke the backend through Atool : κans = Atool (τtans ; T), ztans = Run(κans t t ). The result ztans may be added to Rt and used to produce Ft and yt′ . If a′t ̸= at , 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 = at , the system invokes Aflow . Using the current workflow Vt and execution record Rt , Aflow diagnoses verification-target coverage, the mathematical objects, and computational evidence, then produces Vt′ : Vt′ = Aflow (q, yt , Vt , Rt ). (3) Verification-workflow revision improves checks insufficiently covered by Vt . 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 , the backend is again invoked through Atool : κflow = Atool (τtflow ; T), ztflow = Run(κflow ). t t flow The result zt may update Rt and guide construction of Vt′ , which serves as the next iteration’s reference workflow. Iteration Mechanism. The response and candidate for the next iteration are updated as follows: ′ ′ (yt , at ), a′t ̸= at , (yt+1 , at+1 ) = (4) (yt , at ), a′t = at . If a′t ̸= at , the next iteration verifies a′t ; otherwise, it retains at and uses Vt′ as its reference workflow. Iteration stops upon successful verification or at the preset iteration limit.
Mathematical Tool Invocation and Execution Module An MTF fragment τ is 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, τ = ⟨Γτ , Mτ , ρτ ⟩. Here, Γτ is the context, such as variables, domains, parameter assumptions, or known constraints; Mτ is the object to compute, construct, or verify, such as a set, expression, equation system, recurrence, or constraint system; and ρτ specifies the return operation on Mτ , such as cardinality, symbolic simplification, feasible solutions, a global optimum, or satisfiability. The tuple schema for τ 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 and a vanilla bar c + 2. Jamie buys one chocolate and three vanilla bars, while Kevin buys five chocolate bars. The candidate answer is 8c + 6. Let ∆(c) = c + 3(c + 2) + 5c − (8c + 6). The candidate passes verification if and only if Simplify(∆(c)) ≡ 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⟩. 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 returns zτ = c ̸≡ 0; hence the candidate fails verification and rt = 0. Here, ρτ = Simplify specifies symbolic verification. Counting, optimization, and constraint solving use the same template, replacing Mτ with a set, objective, or constraint system and ρτ 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 Atool translates it into an executable call. Through τ , the three agents specify the object and desired return; Atool selects a tool, generates a call, and dispatches it to the backend. Together, MTF and Atool 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 T = {Tsym , Tenum , Texact , Tsmt , . . .}. where Tsym , Tenum , Texact , and Tsmt support symbolic computation, enumeration, exact numerical computation, and constraint solving, respectively. Given τ and T, Atool generates an executable call κτ : κτ = Atool (τ ; T) = (Tj , uj ),
Tj ∈ T.
Here, Tj is the selected tool and uj its input. The agent selects Tj according to ρτ and constructs uj from Γτ and Mτ . The backend executes the call and returns zτ = Run(κτ ) = Tj (uj ). Here, zτ is the result specified by ρτ . The result zτ is enclosed in <result> and appended to execution record R: R ← Append R, (τ, Tj , uj , zτ ) . The three agents use results in 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 Atool .
Experiments We evaluate AMTFV for mathematical reasoning verification and correction against self-correction, reasoningenhanced, and verification-enhanced methods. We analyze its performance and gains through cross-model architectural comparisons, correction-state transitions, and verificationcomplexity 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-FlashThink, and DeepSeek-Pro to compare correction across nonthinking, 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.5Flash-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; SelfRefine (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 reasoningenhanced 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 ProgCoPy, 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 MTFbased 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 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 crossdataset Avg weighted by dataset size. The supplementary material details implementation and fairness settings (see Supplementary Tables 2 and 3). We also analyze correctionstate 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, DeepSeekFlash-Think from 88.8 to 89.4, and DeepSeek-Pro from 38.8 to 57.1: gains of +17.1, +0.6, and +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 av-
DeepSeek-Flash Method
A24 A25 B25 HMM AMO Avg
Initial Score 63.3 43.3 86.7 reflex 63.3 46.7 83.3 Self-Refine 66.7 60.0 86.7 Self-Refl. 63.3 46.7 86.7 CheckList 60.0 56.7 80.0 CoT-Tool 76.7 60.0 73.3 ProgCo 66.7 53.3 96.7 ProgCo-Py 66.7 60.0 90.0 AMTFV 80.0 66.7 93 .3
33.3 33.3 50.0 33.3 30.0 43.3 43.3 43.3 60.0
14.0 44.1 18.0 45.3 14.0 50.6 16.0 45.3 16.0 44.7 4.0 45.9 18.0 51.2 24.0 52.9 28.0 61.2
DeepSeek-Flash-Think A24
A25
B25 HMM AMO Avg
100.0 100.0 100.0 100.0 62.0 88.8 96.7 100.0 93.3 93.3 56.0 84.1 93.3 100.0 90.0 96.7 56.0 83.5 96.7 100.0 93.3 100.0 60.0 86.5 96.7 100.0 86.7 86.7 56.0 81.8 93.3 93.3 93.3 86.7 44.0 77.6 100.0 100.0 100.0 100.0 58.0 87.6 100.0 100.0 100.0 100.0 60.0 88.2 100.0 100.0 100.0 100.0 64.0 89.4
DeepSeek-Pro A24 A25 B25 HMM AMO Avg 63.3 53.3 60.0 26.7 60.0 63.3 70.0 40.0 66.7 66.7 86.7 56.7 66.7 60.0 73.3 40.0 66.7 53.3 70.0 40.0 56.7 43.3 43.3 23.3 66.7 60.0 66.7 40.0 80.0 60.0 73.3 43.3 76 .7 66.7 93.3 53 .3
10.0 38.8 10.0 44.1 16.0 53.5 8.0 44.7 16.0 45.3 6.0 31.2 12.0 44.7 14.0 49.4 20.0 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 secondhighest 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 max_turn = 3. Blue annotations report the absolute improvement of AMTFV over the better result between ProgCo and ProgCo-Py, in percentage points.
erage 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, +1.2, and +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 closedloop verification-workflow revision. Unless stated otherwise, max_turn = 3. Figure 3 compares average accuracy across all seven basemodel settings. AMTFV ranks highest in every setting, exceeding the better of ProgCo and ProgCo-Py by +0.6 to +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 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
Figure 4: Overall average-accuracy trajectories under different iteration budgets. The horizontal axis shows Initial Score, max_turn = 1, and max_turn = 3; the vertical axis shows average accuracy across seven base-model settings. Curve-end values denote absolute improvements from Initial Score to max_turn = 3, in percentage points.
Figure 5: Row-normalized correction-state transition matrices. Rows indicate initial correctness and columns indicate final correctness, where C denotes a correct answer and 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, while red borders and arrows highlight error-introducing transitions C → W .
complex interactions. Correction Behavior Analysis We characterize correction behavior with row-normalized transition matrices, where C and W denote correct and incorrect answers. W → C measures error correction, whereas C → W measures the risk of corrupting a correct answer. Figure 5 aggregates 7 × 170 = 1190 model–problem instances across seven base models. AMTFV’s W → C rate is 18.4%, versus 9.4% for ProgCo and 12.2% for ProgCoPy. Its C → 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 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
Figure 6: Normalized accuracy gains over Initial Score across verification-complexity bins. The horizontal axis reports (Final Score − Initial Score)/Initial Score, the accuracy gain normalized by initial accuracy. Low, Medium, and High bins are defined in the supplementary material. covers 7 × 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 and Spearman ρ = 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% and 84.6% in the Medium and High bins, exceeding ProgCo-Py by approximately 20.0 and 29.2 percentage points. Its advantage is therefore strongest when more verification interactions are required. The supplementary material provides the empiricaldifficulty–verification-complexity analysis and complexity definition. The supplementary material presents successful cases in minimality verification, combinatorial counting, latticepoint 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 doublesummation 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.
References Abedi Firouzjaei, H. 2025. Cogitator: A Python Toolkit for Chain-of-Thought Prompting. Boye, J.; and Moell, B. 2025. Large Language Models and Mathematical Reasoning Failures. arXiv:2502.11574. Chen, W.; Ma, X.; Wang, X.; and Cohen, W. W. 2023. Program of Thoughts Prompting: Disentangling Computation from Reasoning for Numerical Reasoning Tasks. Transactions on Machine Learning Research. Chen, W.; Su, Y.; Zuo, J.; Yang, C.; Yuan, C.; Chan, C.-M.; Yu, H.; Lu, Y.; Hung, Y.-H.; Qian, C.; Qin, Y.; Cong, X.; Xie, R.; Liu, Z.; Sun, M.; and Zhou, J. 2024. AgentVerse: Facilitating Multi-Agent Collaboration and Exploring Emergent Behaviors. In The Twelfth International Conference on Learning Representations. Cobbe, K.; Kosaraju, V.; Bavarian, M.; Chen, M.; Jun, H.; Kaiser, L.; Plappert, M.; Tworek, J.; Hilton, J.; Nakano, R.; Hesse, C.; and Schulman, J. 2021. Training Verifiers to Solve Math Word Problems. arXiv:2110.14168. Cook, J.; Rocktäschel, T.; Foerster, J.; Aumiller, D.; and Wang, A. 2024. TICKing All the Boxes: Generated Checklists Improve LLM Evaluation and Generation. In NeurIPS 2024 Workshop on Language Gamification. DeepSeek. 2026. DeepSeek V4 Preview Release. https://apidocs.deepseek.com/news/news260424. Accessed: 2026-0722. Gao, L.; Madaan, A.; Zhou, S.; Alon, U.; Liu, P.; Yang, Y.; Callan, J.; and Neubig, G. 2023. PAL: Program-aided Language Models. In Proceedings of the 40th International Conference on Machine Learning, volume 202 of Proceedings of Machine Learning Research, 10764–10799. PMLR. Google AI for Developers. 2026a. Gemini 2.5 FlashLite. https://ai.google.dev/gemini-api/docs/models/gemini2.5-flash-lite. Accessed: 2026-07-22. Google AI for Developers. 2026b. Gemini API OpenAI Compatibility. https://ai.google.dev/gemini-api/docs/ openai. Accessed: 2026-06-05. Gou, Z.; Shao, Z.; Gong, Y.; Shen, Y.; Yang, Y.; Huang, M.; Duan, N.; and Chen, W. 2024. ToRA: A Tool-Integrated Reasoning Agent for Mathematical Problem Solving. In The Twelfth International Conference on Learning Representations. Guo, D.; et al. 2025. DeepSeek-R1 Incentivizes Reasoning in LLMs through Reinforcement Learning. Nature, 645: 633–638. Hochlehnert, A.; Bhatnagar, H.; Udandarao, V.; Albanie, S.; Prabhu, A.; and Bethge, M. 2025. A Sober Look at Progress in Language Model Reasoning: Pitfalls and Paths to Reproducibility. In Second Conference on Language Modeling. Dataset page: https://huggingface.co/datasets/ bethgelab/sober_reasoning. Hong, S.; Zhuge, M.; Chen, J.; Zheng, X.; Cheng, Y.; Wang, J.; Zhang, C.; Wang, Z.; Yau, S. K. S.; Lin, Z.; Zhou, L.; Ran, C.; Xiao, L.; Wu, C.; and Schmidhuber, J. 2024. MetaGPT: Meta Programming for A Multi-Agent Collaborative Framework. In The Twelfth International Conference on Learning Representations.
Huang, J.; Chen, X.; Mishra, S.; Zheng, H. S.; Yu, A. W.; Song, X.; and Zhou, D. 2024. Large Language Models Cannot Self-Correct Reasoning Yet. In The Twelfth International Conference on Learning Representations. Kamoi, R.; Zhang, Y.; Zhang, N.; Han, J.; and Zhang, R. 2024. When Can LLMs Actually Correct Their Own Mistakes? A Critical Survey of Self-Correction of LLMs. Transactions of the Association for Computational Linguistics, 12: 1417–1440. Liu, J.; An, S.; Zhou, S.; Ma, D.; Lin, Y.; Lv, X.; Wang, X.; Li, X.; Wang, Z.; Cao, X.; and Cai, X. 2026a. AMO-Bench: Large Language Models Still Struggle in High School Math Competitions. In Findings of the Association for Computational Linguistics: ACL 2026, 2120–2137. San Diego, California, United States: Association for Computational Linguistics. Liu, Y.; Chen, Y.; Zhou, J.; Hao, Y.; Wang, J.; Zhang, Y.; Li, N.; and Fan, C. 2026b. R1-Code-Interpreter: LLMs Reason with Code via Supervised and Multi-stage Reinforcement Learning. In The Fourteenth International Conference on Learning Representations. Luo, H.; Feng, H.; Sun, Q.; Xu, C.; Zheng, K.; Wang, Y.; Yang, T.; Hu, H.; and Tang, Y. 2026. AgentMath: Empowering Mathematical Reasoning for Large Language Models via Tool-Augmented Agent. In The Fourteenth International Conference on Learning Representations. Ma, R.; Wang, P.; Liu, C.; Liu, X.; Chen, J.; Zhang, B.; Zhou, X.; Du, N.; and Li, J. 2025. S2 R: Teaching LLMs to Self-verify and Self-correct via Reinforcement Learning. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), 22632–22654. Vienna, Austria: Association for Computational Linguistics. Madaan, A.; Tandon, N.; Gupta, P.; Hallinan, S.; Gao, L.; Wiegreffe, S.; Alon, U.; Dziri, N.; Prabhumoye, S.; Yang, Y.; Gupta, S.; Majumder, B. P.; Hermann, K.; Welleck, S.; Yazdanbakhsh, A.; and Clark, P. 2023. Self-Refine: Iterative Refinement with Self-Feedback. In Advances in Neural Information Processing Systems, volume 36, 46534–46594. Meurer, A.; Smith, C. P.; Paprocki, M.; Čertík, O.; Kirpichev, S. B.; Rocklin, M.; Kumar, A.; Ivanov, S.; Moore, J. K.; Singh, S.; Rathnayake, T.; Vig, S.; Granger, B. E.; Muller, R. P.; Bonazzi, F.; Gupta, H.; Vats, S.; Johansson, F.; Pedregosa, F.; Curry, M. J.; Terrel, A. R.; Roučka, S.; Saboo, A.; Fernando, I.; Kulal, S.; Cimrman, R.; and Scopatz, A. 2017. SymPy: Symbolic Computing in Python. PeerJ Computer Science, 3: e103. OpenAI. 2026. GPT-5.4 mini Model. https://developers. openai.com/api/docs/models/gpt-5.4-mini. Accessed: 202607-22. Pan, L.; Saxon, M.; Xu, W.; Nathani, D.; Wang, X.; and Wang, W. Y. 2024. Automatically Correcting Large Language Models: Surveying the Landscape of Diverse Automated Correction Strategies. Transactions of the Association for Computational Linguistics, 12: 484–506. Pei, Q.; Pan, Z.; Lin, H.; Gao, X.; Li, Y.; Tang, Z.; He, C.; Yan, R.; and Wu, L. 2025. ScaleDiff: Scal-
ing Difficult Problems for Advanced Mathematical Reasoning. Dataset page: https://huggingface.co/datasets/QizhiPei/ ScaleDiff-Math, arXiv:2509.21070. Qiao, S.; Gui, H.; Lv, C.; Jia, Q.; Chen, H.; and Zhang, N. 2024. Making Language Models Better Tool Learners with Execution Feedback. In Proceedings of the 2024 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies (Volume 1: Long Papers), 3550–3568. Mexico City, Mexico: Association for Computational Linguistics. Schick, T.; Dwivedi-Yu, J.; Dessì, R.; Raileanu, R.; Lomeli, M.; Hambro, E.; Zettlemoyer, L.; Cancedda, N.; and Scialom, T. 2023. Toolformer: Language Models Can Teach Themselves to Use Tools. In Advances in Neural Information Processing Systems, volume 36, 68539–68551. Shinn, N.; Cassano, F.; Gopinath, A.; Narasimhan, K.; and Yao, S. 2023. Reflexion: Language Agents with Verbal Reinforcement Learning. In Advances in Neural Information Processing Systems, volume 36, 8634–8652. Song, X.; Wu, Y.; Wang, W.; Liu, J.; Su, W.; and Zheng, B. 2025. ProgCo: Program Helps Self-Correction of Large Language Models. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 2: Short Papers), 944–959. Vienna, Austria: Association for Computational Linguistics. Tyen, G.; Mansoor, H.; Carbune, V.; Chen, P.; and Mak, T. 2024. LLMs Cannot Find Reasoning Errors, but Can Correct Them Given the Error Location. In Findings of the Association for Computational Linguistics: ACL 2024, 13894– 13908. Bangkok, Thailand: Association for Computational Linguistics. Wang, X.; Wei, J.; Schuurmans, D.; Le, Q. V.; Chi, E. H.; Narang, S.; Chowdhery, A.; and Zhou, D. 2023. SelfConsistency Improves Chain of Thought Reasoning in Language Models. In International Conference on Learning Representations. Wei, J.; Wang, X.; Schuurmans, D.; Bosma, M.; Ichter, B.; Xia, F.; Chi, E. H.; Le, Q. V.; and Zhou, D. 2022. Chainof-Thought Prompting Elicits Reasoning in Large Language Models. In Advances in Neural Information Processing Systems, volume 35, 24824–24837. Wu, Q.; Bansal, G.; Zhang, J.; Wu, Y.; Li, B.; Zhu, E.; Jiang, L.; Zhang, X.; Zhang, S.; Liu, J.; Awadallah, A. H.; White, R. W.; Burger, D.; and Wang, C. 2024. AutoGen: Enabling Next-Gen LLM Applications via Multi-Agent Conversations. In First Conference on Language Modeling. Yang, A.; Zhang, B.; Hui, B.; Gao, B.; Yu, B.; Li, C.; Liu, D.; Tu, J.; Zhou, J.; Lin, J.; Lu, K.; Xue, M.; Lin, R.; Liu, T.; Ren, X.; and Zhang, Z. 2024. Qwen2.5-Math Technical Report: Toward Mathematical Expert Model via Self-Improvement. arXiv:2409.12122. Yao, S.; Zhao, J.; Yu, D.; Du, N.; Shafran, I.; Narasimhan, K.; and Cao, Y. 2023. ReAct: Synergizing Reasoning and Acting in Language Models. In International Conference on Learning Representations. Zhan, S.; Lai, Y.; Lu, Z.; Lin, D.; Yang, Z.; and Tan, F. 2026. MathSmith: Towards Extremely Hard Mathematical
Reasoning by Forging Synthetic Problems with a Reinforced Policy. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 40, 34602–34610. Zhao, X.; Xu, T.; Wang, X.; Chen, Z.; Jin, D.; Tan, L.; Lin, Y.-T.; Yu, Z.; Zhao, Z.; He, Y.; Wang, S.; Fang, H.; Chandar, S.; and Zhu, C. 2025. Boosting LLM Reasoning via Spontaneous Self-Correction. In Second Conference on Language Modeling.
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 document AMTFV’s evaluation protocol, cross-model performance, runtime behavior, verification-complexity signal, distribution of tool calls, and verification–correction process.
A
Implementation 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.1
Base Models and Reasoning Configurations
Table 2 lists the model settings used in this paper and their corresponding official model identifiers. Names with the -Think suffix 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; OpenAI 2026; Google AI for Developers 2026a,b). Model setting DeepSeek-Flash DeepSeek-Flash-Think DeepSeek-Pro GPT-5.4-Mini GPT-5.4-Mini-Think Gemini-2.5-Flash-Lite Gemini-2.5-Flash-Lite-Think
Official model identifier deepseek-v4-flash deepseek-v4-flash deepseek-v4-pro gpt-5.4-mini gpt-5.4-mini gemini-2.5-flash-lite gemini-2.5-flash-lite
Reasoning configuration Non-Thinking Thinking enabled, reasoning effort: high Non-Thinking Reasoning effort: none Reasoning effort: low Thinking disabled Thinking enabled
Table 2: Base models and reasoning configurations. -Think denotes an experimental setting in which the corresponding reasoning mode is enabled.
A.2
Shared 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, and AMTFV all 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.3
Generation Parameters and Method Budgets
Model requests use a common OpenAI-compatible Chat Completions format. Whenever the parameter is supported, temperature is set to 0. 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 evaluates max_turn ∈ {1, 3}, while the main experiments use 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 to max_turn = 3. Following its multi-path consistency procedure, CoT-Tool independently generates and selects among 3 reasoning paths. Table 3 summarizes the outer reasoning budget for each method. Thus, every iterative method runs for at most 3 rounds; 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. Method Initial Score reflex / Self-Refine / Self-Refl. / CheckList ProgCo / ProgCo-Py / AMTFV CoT-Tool
Outer reasoning budget No additional correction At most 3 correction rounds At most 3 verification–correction rounds 3 independent reasoning paths
Table 3: Outer reasoning budgets used by different methods.
A.4
Mathematical Tool Execution
Both ProgCo-Py and AMTFV can receive Python execution feedback, but each organizes tool use according to its own method definition. AMTFV uses 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.5
Answer 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 of 10−3 . If the first two stages are inconclusive, the third uses the same DeepSeek-Flash evaluator at temperature 0 to 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.
B B.1
Code will be released at https://github.com/TicusFFF/mathematical-self-correction.
Supplementary Results and Iteration-Budget Analysis
Supplementary Results on GPT and Gemini
This section reports detailed average accuracies for ProgCo, ProgCo-Py, and AMTFV under the GPT and Gemini settings, supporting the progressive architectural comparison in the main text. Supplementary Tables 4 and 5 report results for both max_turn = 1 and max_turn = 3 to show how each method behaves as the fixed iteration budget changes. Turn Method
1
3
GPT-5.4-Mini A24 A25 B25 HMM AMO Avg ProgCo 40.0 26.7 43.3 13.3 8.0 24.1+1.2 ProgCo-Py 46.7 26.7 43.3 13.3 4.0 24.1+1.2 AMTFV 50.0 43.3 53.3 16.7 4 .0 30.0+7.1 ProgCo 40.0 30.0 43.3 16.7 6.0 24.7+1.8 ProgCo-Py 46.7 26.7 43.3 13.3 6.0 24.7+1.8 AMTFV 53.3 40.0 50.0 20.0 2 .0 29.4+6.5
A24 A25 70.0 80.0 73.3 73.3 86.7 76 .7 73.3 83.3 76.7 73.3 86.7 83.3
GPT-5.4-Mini-Think B25 HMM AMO Avg 76.7 53.3 22.0 55.9+5.3 80.0 56.7 26.0 57.6+7.0 76 .7 53 .3 14.0 55 .9 +5.3 76.7 53.3 24.0 57.6+7.0 80.0 60.0 28.0 59.4+8.8 83.3 60.0 20.0 61.2+10.6
Table 4: Supplementary results for verification-enhanced methods on GPT models. The table reports detailed results for ProgCo, ProgCo-Py, and AMTFV with max_turn = 1 and 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.
Turn Method
1
3
Gemini-2.5-Flash-Lite A24 A25 B25 HMM AMO Avg ProgCo 63.3 50.0 63.3 30.0 6.0 38.2+1.7 ProgCo-Py 63.3 46.7 63.3 36.7 6.0 38.8+2.3 AMTFV 66.7 50.0 56 .7 33 .3 8.0 38.8+2.3 ProgCo 63.3 50.0 63.3 33.3 2.0 37.6+1.1 ProgCo-Py 53.3 46.7 56.7 33.3 8.0 35.9−0.6 AMTFV 66.7 53.3 60 .0 33.3 8.0 40.0+3.5
A24 56.7 60.0 60.0 60.0 66.7 63 .3
Gemini-2.5-Flash-Lite-Think A25 B25 HMM AMO Avg 46.7 60.0 43.3 8.0 38.8+1.2 40.0 66.7 40.0 8.0 38.8+1.2 50.0 66.7 33.3 8.0 39.4+1.8 46.7 63.3 43.3 8.0 40.0+2.4 46.7 70.0 40.0 8.0 41.8+4.2 53.3 73.3 33.3 10.0 42.4+4.8
Table 5: Supplementary results for verification-enhanced methods on Gemini models. The table reports detailed results for ProgCo, ProgCo-Py, and AMTFV with max_turn = 1 and 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: AMTFV achieves 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.2
Iteration Budget Analysis
AMTFV progressively updates either the candidate answer or the verification workflow through a multistep verification– correction loop. We analyze the effect of the maximum iteration count max_turn, focusing on max_turn = 1 and 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.
Figure 7: Verification–correction performance under different iteration budgets. The three panels correspond to ProgCo, ProgCoPy, and AMTFV. 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, and max_turn = 3. Gain on the right denotes the absolute change from Initial Score to max_turn = 3, in percentage points. Figure 7 shows the average-accuracy trajectories of ProgCo, ProgCo-Py, and AMTFV under different iteration budgets. Initial Score is the accuracy before additional correction, while Turn=1 and Turn=3 correspond to max_turn = 1 and max_turn = 3, respectively.
From max_turn = 1 to max_turn = 3, AMTFV improves further under most base-model settings; the largest additional gain is +10.0 on DeepSeek-Pro. Additional iterations are not always monotonically beneficial: on GPT-5.4-Mini, AMTFV decreases slightly by −0.6 from max_turn = 1 to 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 that AMTFV improves by +8.8 points on average from Initial Score to max_turn = 3, exceeding the +3.4 gain of ProgCo and the +4.7 gain of ProgCo-Py. AMTFV also continues to improve from max_turn = 1 to max_turn = 3, whereas the later gains of ProgCo and ProgCo-Py are smaller. Under these evaluated settings, AMTFV therefore appears to convert additional verification–correction rounds into effective gains more successfully than the ProgCo family.
C C.1
Verification-Complexity and Tool-Type Analysis
Empirical 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 −
1
MX model
Mmodel
m=1
I[a0m,q = a∗q ],
(5)
where Mmodel is the number of base-model settings, a0m,q is the initial candidate answer produced by setting m for problem q, and a∗q is the gold answer. We define average problem-level verification complexity as
Cver (q) =
1
MX model
Mmodel
m=1
(m,q) log 1 + ntool ,
(6)
(m,q)
where ntool is the number of MTF tool calls produced by AMTFV for model setting m and problem q. The transformation (m,q) log(1 + ntool ) reduces the influence of extreme call counts on the problem-level average. The instance-level verification-complexity bins are defined as (m,q) ntool ≤ 1, Low, b(m, q) = Medium, 2 ≤ n(m,q) tool ≤ 3, (m,q) High, ntool ≥ 4.
(7)
The correlation analysis in Figure 8 aggregates over 170 problems. Pearson r = 0.67 and Spearman ρ = 0.70 indicate 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.2
MTF Tool-Type Analysis
Figure 9 shows the distribution of MTF call types in AMTFV. Calls are concentrated primarily in the Enumeration and Symbolic categories, indicating that exhaustive enumeration and symbolic verification are common tool requirements in hardtest 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.
Figure 8: Relationship between empirical difficulty and verification complexity. The horizontal axis shows empirical difficulty Demp (q), estimated from initial-answer accuracy across seven base-model settings; the vertical axis shows average problem-level verification complexity Cver (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.
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 that AMTFV is 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.
D D.1
Case Studies and Full Process Comparison
Successful Case Study
To illustrate how AMTFV uses 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, and AMTFV obtains the correct answer through MTF-driven verification and correction. Supplementary Table 6 summarizes the key differences. The next section presents the BRUMO25 exact double-summation case in full as a direct illustration of how AMTFV models a mathematical verification target as an exact tool computation and uses structured tool results for candidate-answer adjudication and revision. Case
Initial ProgCo ProgCo-Py AMTFV Key MTF role
AIME24 minimality AIME25 counting AMO lattice triangles BRUMO25 exact double sum
155 764 7 4608
155 764 7 4608
155 764 7 4608
110 16 6 4529
Verify global minimality Exhaustively enumerate valid cases Enumerate 15 points; maximum isosceles-free subset: 5 Compute the exact sum and return S, A, R
Table 6: Representative successful correction cases. The table reports the initial answer, baseline outputs, and AMTFV’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, AMTFV not 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. AMTFV instead 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 smallest n such that every selection of n points from 15 triangular-lattice points contains an isosceles triangle. The initial response, ProgCo, and ProgCo-Py all return 7, relying primarily on the incorrect assumption that the largest isosceles-free subset has size 6. AMTFV represents the 15 lattice points as P = {(i, j) : 0 ≤ j ≤ 4, 0 ≤ i ≤ 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)}, Therefore, the largest isosceles-free subset has size 5, and the smallest guaranteed number is 6. 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 answer 4608; their common error is assuming that the sum of modular-power residues is 4656 for every fixed n. AMTFV expresses the verification target as an exact double-summation task and asks the tool to return the total residue S, exact value A, and rounded result R. The tool returns S = 439312, A = 439312/97, and R = 4529, thereby rejecting 4608 and correcting the answer. These cases illustrate two characteristic advantages of AMTFV. 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.2
Full Case Process Comparison: Exact Double-Sum Verification
We examine a BRUMO25 exact double-summation case to illustrate how Initial, ProgCo, ProgCo-Py, and AMTFV differ in verification-target construction, tool execution, and use of feedback. The problem asks for 96 X 96 n X a A= 97 a=1 n=1 rounded to the nearest integer. The gold answer is 4529, whereas Initial, ProgCo, and ProgCo-Py all return 4608. The common error in the first three outputs is the following implicit assumption: for every fixed n, as a ranges from 1 to 96, 96 X
(an mod 97) = 1 + 2 + · · · + 96 = 4656.
a=1
This assumption holds only when a 7→ an (mod 97) is a permutation of (Z/97Z)× , which requires gcd(n, 96) = 1. When gcd(n, 96) > 1, the image is only a proper subgroup, so the inner sum need not equal 4656. 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 of an /97 directly, coupling tool execution with huge powers and floating-point precision. AMTFV, in contrast, explicitly represents the target as three mathematical objects, S, 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. Compute A=
96 X 96 n X a a=1 n=1
97
,
where {x} denotes the fractional part of x, and return A rounded to the nearest integer. Ground truth. The gold answer is 4529. Initial extracted answer. The final answer extracted from Initial is 4608. Generated solution. Initial first rewrites each term as n an mod 97 a = , 97 97 and hence
96
A=
96
1 XX n (a mod 97). 97 a=1 n=1
Initial then assumes that, for each fixed n, the values of an mod 97 as a ranges from 1 to 96 can be treated as either a permutation or equal repetitions of all nonzero residue classes 1, 2, . . . , 96. It therefore uses 96 X (an mod 97) = 1 + 2 + · · · + 96 = 4656 a=1
and obtains A=
96 · 4656 = 96 · 48 = 4608. 97
The final answer is 4608 .
Initial’s central error is failing to distinguish gcd(n, 96) = 1 from gcd(n, 96) > 1. In the latter case, a 7→ an (mod 97) is not a permutation of the nonzero residue classes, so the inner sum need not equal 4656. The incorrect candidate 4608 therefore arises from inadequate modeling of the mathematical object rather than an error in the final numerical simplification. ProgCo. Final extracted answer. 4608. Generated solution. ProgCo’s final response retains the same central mathematical assumption as Initial. It likewise writes the fractional part as n a an mod 97 = , 97 97 and assumes that, for each fixed n, the inner sum equals the sum of all nonzero residue classes: 96 X
(an mod 97) = 4656.
a=1
ProgCo therefore obtains A=
96 · 4656 = 4608, 97
and returns the final answer 4608 . Generated verification code. ProgCo further generates a verification function for the candidate answer 4608. 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 == answer The verification code computes each remainder using modular exponentiation: remainder = pow(a,n,97) and accumulates A += remainder / 97. Its intended computation is 96
A=
96
1 XX n (a mod 97), 97 a=1 n=1
and then to compare whether round(A) equals the candidate answer 4608. Returned verification feedback. The retained verification feedback states that the 96 × 96 = 9216 double 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 returns True,
with feedback verify passed. Notably, the feedback does not return the computed total residue S, exact value A, or rounded result R; 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 96 X 96 X S= (an mod 97), a=1 n=1
S , 97 R = round(A). Instead, the feedback only reports verify passed and accepts 4608. 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. A=
ProgCo-Py. Final extracted answer. 4608. Generated solution. ProgCo-Py’s final response likewise retains Initial’s core reasoning by transforming n a 97 into
an mod 97 , 97
and assuming that the inner sum for every n is 1 + 2 + · · · + 96 = 4656. It therefore still obtains A=
96 · 4656 = 4608, 97
and returns 4608 . Generated Python verification code. ProgCo-Py generates Python-style direct-computation code to verify 4608. Unlike ProgCo’s modular-power implementation, this code first attempts to compute an /97 and 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 == answer That is, ProgCo-Py’s verification code directly computes value = (a ** n) / 97 and obtains the fractional part via fractional_part = value - int(value) . Python execution and returned result. The execution feedback notes that directly computing an /97 involves extremely large integers an , 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 96 X (an mod 97) = 4656 a=1
for all n. This round consequently retains A = 4608, The verification result is True, with feedback 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 of an /97 directly 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 candidate 4608. AMTFV. Final extracted answer. 4529. Initial candidate. AMTFV starts from the same initial candidate answer: 4608. MTF verification target. Rather than asking the model to judge the plausibility of 4608 directly or relying on the group-theoretic assumption in the original solution, the verification agent expresses the problem requirement as an exact mathematical computation target: 96 X 96 X S= (an mod 97), a=1 n=1
S , 97 R = round(A). A=
The candidate passes verification if and only if 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: 96 X 96 X S= pow(a, n, 97), a=1 n=1
It then computes, in exact rational form, A=
S . 97
The tool returns the following structured result: S = 439312, A = Fraction(439312, 97), R = 4529, (R = 4608) = False. Tool execution result. The tool result gives A=
439312 96 = 4528 + , 97 97
and hence R = round(A) = 4529. The result also reports R = 4529 ̸= 4608. Therefore, the candidate answer 4608 fails verification: False. Feedback and answer revision. Based on the tool result, the feedback identifies Initial’s key error: it assumes that for every fixed n, the map a 7→ an (mod 97) covers all nonzero residue classes. In fact, this map is a permutation only when gcd(n, 96) = 1; when gcd(n, 96) > 1, its image is a proper subgroup and the inner sum need not equal 4656. Using this feedback, the answer-revision stage recomputes the double sum and obtains A=
439312 96 = 4528 + . 97 97
The rounded result is therefore 4529. Final verification. Final verification uses 4529 as the candidate answer and invokes the same exact-summation verification target again: S=
96 96 X X
(an mod 97),
a=1 n=1
S , 97 R = round(A). A=
The tool again returns S = 439312,
R = 4529.
Final verification therefore succeeds: True,
verify passed.
AMTFV ultimately returns 4529 .
A key advantage of AMTFV in 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 96 96 X X (an mod 97), S= a=1 n=1
S , 97 R = round(A). A=
The mathematical toolbox backend then performs the finite summation, division by 97, 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, AMTFV organizes the target as an MTF request to the mathematical toolbox, causing the tool to return S, A, R, and whether the candidate matches. The system can therefore directly identify the discrepancy between 4608 and the true rounded result 4529, and revise the candidate to the correct answer.