VeryTrace: Verifying Reasoning Traces through Compilable Formalism and Structured Verification

# VeryTrace: Verifying Reasoning Traces through Compilable Formalism and Structured Verification
Source: [https://arxiv.org/html/2606.24124](https://arxiv.org/html/2606.24124)
###### Abstract

Multi\-step reasoning with Chain\-of\-Thought \(CoT\) prompting remains fragile: logical errors or hallucinations in early steps silently propagate, producing confident but incorrect conclusions\. This paper presentsVeryTrace, a zero\-shot verification\-and\-repair framework that formalizes natural\-language reasoning traces into a structured, compilable representation\. VeryTrace introduces a Domain\-Specific Language \(DSL\) that: \(i\) makes step dependencies explicit, \(ii\) mechanizes quantitative content as executable expressions, and \(iii\) structures semantic inferences via deduction schemas\. Our hybrid verifier combines deterministic checks for computational correctness, dependency resolution, & constraint satisfaction with targeted LLM audits for non\-mechanizable semantic judgments, enabling step\-level error localization and repair\.

Across three diverse domains—competition mathematics \(AIME 2025\), robotics planning \(LLM\-BabyBench\), and kinship reasoning \(CLUTRR\)— VeryTrace improves accuracy over zero\-shot baselines on state\-of\-the\-art LLMs without requiring domain\-specific training or in\-context examples, demonstrating that formalized trace verification achieves both precision and generalization\.

Chain of Thought, Reasoning Traces, Domain Specific Languages \(DSLs\), Auditing Models, Large Language Models

## 1Introduction

Chain\-of\-Thought \(CoT\) prompting has transformed how Large Language Models \(LLMs\) handle complex reasoning tasks, enabling multi\-step derivations that outperform single\-shot predictions\. However, this capability remains fundamentally brittle\. A single arithmetic error, unstated assumption, or logical fallacy at stepkkcan cascade through stepsk\+1,k\+2,…k\+1,k\+2,\\ldots, producing a coherent\-sounding but incorrect conclusion\. This error propagation problem intensifies in domains requiring strict correctness: competition mathematics demands precise symbolic manipulation, planning tasks require invariant satisfaction at every step, and relational reasoning depends on consistent inference chains\.

Existing mitigation strategies face a fundamental trade\-off: End\-to\-end verification evaluates only final answers, providing no diagnostic granularity when traces fail\. Self\-consistency and voting approaches require multiple expensive samples without diagnosing*why*individual traces fail\. At the other extreme, formal theorem provers \(Lean, Coq, Isabelle\) offer rigorous verification but demand domain\-specific formalization, expert\-level syntax, and extensive manual effort, requirements that do not transfer across problem types\. What is missing is a framework that provides step\-level verification granularity while maintaining domain\-agnostic generalization — one that verifies the*process*of reasoning, not just the outcomes\.

We presentVeryTrace, a framework that treats reasoning traces as compilable programs that can be verified step\-by\-step\. Drawing inspiration from tactic\-style theorem proving \(Lean, Isabelle\), VeryTrace models reasoning as a sequence of state transitions: each step declares its dependencies, applies a computation or deduction schema, and produces an updated reasoning state containing variable bindings and active constraints\. This representation enables two critical capabilities: \(i\) mechanized verification of the parts of reasoning that*can*be formalized \(arithmetic, symbolic evaluation, dependency ordering\), and \(ii\) structured LLM audits for the semantic parts that*cannot*be formalized \(natural language constraints, commonsense inferences\)\. Crucially, formalization logic and verification pipeline apply across domains without specialized handlers\.

![Refer to caption](https://arxiv.org/html/2606.24124v1/x1.png)Figure 1:Illustrations of the VeryTrace Framework\. The process begins with the user prompt, which is provided into the User LLM to produce a Chain of Thought, or natural language reasoning trace𝒯NL\\mathcal\{T\}\_\{\\text\{NL\}\}\. The Context Extraction module queries an LLM to extract formalized context𝒦\\mathcal\{K\}\(initial factsFF, assumptionsAA, invariant constraintsCinvC\_\{\\text\{inv\}\}and goal constraintsCgoalC\_\{\\text\{goal\}\}\), without seeing the reasoning trace𝒯NL\\mathcal\{T\}\_\{\\text\{NL\}\}\. This separation prevents the model from hallucinating context to justify incorrect steps\. The Chain of Thought, formalized context, alongside the user prompt are processed by a Translation LLM to produce a compilable DSL trace𝒯DSL\\mathcal\{T\}\_\{\\text\{DSL\}\}\. This formalized trace enters the Hybrid Verification pipeline, which verifies inference structure, constraint satisfaction, computation and deduction correctness in reasoning steps, and final conclusion consistency\. If the trace is invalid, the verifier generates an error report and feedback for the USER LLM to iteratively repair the reasoning trace\.##### A compilable DSL for reasoning traces\.

VeryTrace’s Domain\-Specific Language makes step dependencies explicit and maximally mechanizes quantitative content\. Rather than treating “computex=2×15x=2\\times 15” as unstructured text, the DSL represents it asCOMPUTE\(x, "2 \* 15", deps=\[\.\.\.\]\), making the computational content executable and the dependency structure verifiable\. For semantic inferences that resist mechanization, the DSL constrains reasoning to a small library of deduction schemas \(direct entailment, modus ponens, transitivity, case analysis\), ensuring even “soft” steps have explicit form and declared premises\.

##### Hybrid verification: mechanical checks plus structured LLM audits\.

The verifier separates deterministic checks from semantic judgments\. Deterministic checks validate: \(i\) dependency resolution \(no forward references\), \(ii\) computational correctness \(evaluate the right\-hand side, verify state update\), \(iii\) mechanizable constraint satisfaction, and \(iv\) conclusion consistency with declared goals\. For non\-mechanizable parts such as natural language constraints and underspecified commonsense, VeryTrace triggers structured LLM audits scoped to a specific step, deduction schema, and state snapshots\. This division mirrors the principle: “verify mechanically wherever possible, semantically only where necessary\.”

##### Verification\-driven repair\.

Step\-level verification produces actionable diagnostics: not “the answer is wrong,” but “Step 7 violates constraintccunder states6s\_\{6\}” or “Step 12’s computation yields 42, but the state declaresx=35x=35\.” This enables targeted repair: an LLM can revise the problematic region rather than regenerating the entire trace\. VeryTrace implements this as an iterative loop: generate CoT→\\rightarrowformalize to DSL→\\rightarrowverify→\\rightarrowif invalid, return localized errors and request correction→\\rightarrowre\-verify\.

##### Zero\-shot transfer across domains\.

We evaluate VeryTrace on three domains chosen to stress different reasoning modes: pure symbolic manipulation \(AIME 2025 competition mathematics\), hybrid quantitative\-semantic reasoning \(LLM\-BabyBench robotics planning\), and relational inference over natural language \(CLUTRR kinship reasoning\)\. Across state\-of\-the\-art open\-sourced LLMs, VeryTrace improves accuracy over strong zero\-shot baselines without any domain\-specific training or in\-context examples, demonstrating that formalized trace verification can generalize across heterogeneous reasoning types\.

##### Contributions\.

In summary, this paper makes the following contributions:

1. 1\.A domain\-agnostic DSL for reasoning traces\.We propose a compilable representation that makes step dependencies explicit, mechanizes quantitative content, and structures semantic inferences via universal deduction schemas\.
2. 2\.A hybrid state\-transition verifier\.We develop a step\-wise verification pipeline that combines deterministic checks with structured LLM audits, propagating the reasoning state through each step\.
3. 3\.A verification\-driven repair framework\.We show how step\-level error diagnostics enable targeted correction and iterative improvement of traces without training or domain\-specific demonstrations\.
4. 4\.Cross\-domain evaluation\.We demonstrate consistent gains over zero\-shot baselines on AIME 2025, LLM\-BabyBench, and CLUTRR across multiple state\-of\-the\-art LLMs\.

## 2Related Work

##### Chain\-of\-Thought Reasoning and Verification Approaches\.

Chain\-of\-Thought \(CoT\) prompting\(Weiet al\.,[2022](https://arxiv.org/html/2606.24124#bib.bib18); Kojimaet al\.,[2022](https://arxiv.org/html/2606.24124#bib.bib19)\)has established itself as the dominant paradigm for complex reasoning in LLMs, with extensions including Tree\-of\-Thoughts\(Yaoet al\.,[2023](https://arxiv.org/html/2606.24124#bib.bib20)\), Graph\-of\-Thoughts\(Bestaet al\.,[2024](https://arxiv.org/html/2606.24124#bib.bib21)\), and least\-to\-most prompting\(Zhouet al\.,[2023b](https://arxiv.org/html/2606.24124#bib.bib22)\)\. However, these approaches fundamentally lack error detection mechanisms: a single mistake propagates uncorrected through subsequent steps\. Self\-consistency methods\(Wanget al\.,[2023](https://arxiv.org/html/2606.24124#bib.bib24)\)address this through majority voting over multiple samples, but require expensive generation without diagnosing*why*individual traces fail\. Prompt\-based verification approaches attempt to mitigate this: Self\-Refine\(Madaanet al\.,[2023](https://arxiv.org/html/2606.24124#bib.bib12)\)and Chain\-of\-Verification\(Dhuliawalaet al\.,[2024](https://arxiv.org/html/2606.24124#bib.bib1)\)enable iterative refinement through self\-generated feedback, while Natural Program\(Linget al\.,[2023](https://arxiv.org/html/2606.24124#bib.bib2)\)structures reasoning as verifiable deductive steps\. Recent work explores spontaneous self\-correction\(Zhaoet al\.,[2025a](https://arxiv.org/html/2606.24124#bib.bib8)\)and token\-probability\-based verification\(Chowdhury and Caragea,[2025](https://arxiv.org/html/2606.24124#bib.bib4)\)\. Process reward models\(Lightmanet al\.,[2023](https://arxiv.org/html/2606.24124#bib.bib28); Uesatoet al\.,[2022](https://arxiv.org/html/2606.24124#bib.bib27)\)and step\-level verifiers\(Liet al\.,[2023](https://arxiv.org/html/2606.24124#bib.bib13); Cobbeet al\.,[2021](https://arxiv.org/html/2606.24124#bib.bib26)\)learn to score reasoning steps but require substantial training data and remain domain\-specific\. VeryTrace differs fundamentally by introducing a domain\-agnostic DSL that makes reasoning steps*mechanically verifiable*wherever possible, providing precise error localization without requiring trained verifiers or multiple sampling\.

##### Formal Methods and Solver\-Integrated Reasoning\.

At the opposite end of the verification spectrum, formal proof assistants \(Lean\(de Mouraet al\.,[2015](https://arxiv.org/html/2606.24124#bib.bib30)\), Isabelle\(Paulson,[1994](https://arxiv.org/html/2606.24124#bib.bib31)\), Coq\(Bertot and Castéran,[2013](https://arxiv.org/html/2606.24124#bib.bib32)\)\) offer rigorous correctness guarantees through typed calculi and tactics\. Recent work has explored LLM integration with these systems: autoformalization\(Wuet al\.,[2022](https://arxiv.org/html/2606.24124#bib.bib39)\)translates informal mathematics to formal statements, proof artifact co\-training\(Hanet al\.,[2022](https://arxiv.org/html/2606.24124#bib.bib35)\)leverages intermediate proof states, and retrieval\-augmented approaches\(Yanget al\.,[2023](https://arxiv.org/html/2606.24124#bib.bib36)\)enable large\-scale theorem proving\. Draft\-Sketch\-Prove\(Jianget al\.,[2023](https://arxiv.org/html/2606.24124#bib.bib38)\)and related hybrid methods\(Polu and Sutskever,[2020](https://arxiv.org/html/2606.24124#bib.bib34); Trinhet al\.,[2024](https://arxiv.org/html/2606.24124#bib.bib54)\)use informal proofs to guide formal verification\. Domain\-specific systems include Safe\(Liuet al\.,[2025](https://arxiv.org/html/2606.24124#bib.bib10)\), which translates mathematical reasoning into Lean for retrospective verification, and Typed Chain\-of\-Thought\(Perrier,[2025](https://arxiv.org/html/2606.24124#bib.bib11)\), which applies type\-theory principles to structure reasoning\. Logic\.py\(Kesseliet al\.,[2025](https://arxiv.org/html/2606.24124#bib.bib3)\)and LELMA\(Mensfeltet al\.,[2025](https://arxiv.org/html/2606.24124#bib.bib5)\)bridge natural language reasoning with constraint solvers, while SMT solvers\(Bermanet al\.,[2024](https://arxiv.org/html/2606.24124#bib.bib6)\)rigorously verify constraint\-heavy problems\. While these approaches achieve remarkable results, they face critical limitations: \(i\) formalization requires expert knowledge of proof assistant syntax, \(ii\) the verification machinery is domain\-specific, and \(iii\) complete formalization is often impractical for problems involving natural language constraints\. VeryTrace adopts the*spirit*of tactic\-based proving—explicit state transitions, declared dependencies, structured inference rules—while remaining domain\-agnostic through a lightweight DSL and hybrid verification strategy that mechanizes what it can and audits what it cannot\.

##### Neuro\-Symbolic Methods and Learned Verifiers\.

Neuro\-symbolic systems\(Garcezet al\.,[2019](https://arxiv.org/html/2606.24124#bib.bib45); Maoet al\.,[2019](https://arxiv.org/html/2606.24124#bib.bib46); Yiet al\.,[2018](https://arxiv.org/html/2606.24124#bib.bib47)\)combine neural perception with symbolic reasoning, often for visual question answering, but do not address multi\-step reasoning verification in language models\. Work on program synthesis\(Chenet al\.,[2021](https://arxiv.org/html/2606.24124#bib.bib40); Nijkampet al\.,[2023](https://arxiv.org/html/2606.24124#bib.bib41)\)and verification\(Solar\-Lezama,Armando,[2008](https://arxiv.org/html/2606.24124#bib.bib42); Polikarpovaet al\.,[2016](https://arxiv.org/html/2606.24124#bib.bib43)\)provides techniques for validating executable code but assumes well\-defined programming language semantics\. LLM\-P\(Liuet al\.,[2023](https://arxiv.org/html/2606.24124#bib.bib49)\)and similar planning approaches\(Valmeekamet al\.,[2023](https://arxiv.org/html/2606.24124#bib.bib48); Songet al\.,[2023](https://arxiv.org/html/2606.24124#bib.bib58)\)integrate LLMs with classical planners requiring domain\-specific planning languages \(PDDL\)\. Learned verification approaches train specialized models to assess reasoning quality: Math\-Shepherd\(Wanget al\.,[2024](https://arxiv.org/html/2606.24124#bib.bib61)\)and ThinkPRM\(Khalifaet al\.,[2025](https://arxiv.org/html/2606.24124#bib.bib9)\)advance Process Reward Models \(PRMs\) where trained verifiers score individual steps, DiVeRSe\(Liet al\.,[2023](https://arxiv.org/html/2606.24124#bib.bib13)\)employs step\-aware verifiers with voting mechanisms, and S2R\(Maet al\.,[2025](https://arxiv.org/html/2606.24124#bib.bib14)\)uses reinforcement learning to train critics for self\-verification\. Recent work\(Zhaoet al\.,[2025b](https://arxiv.org/html/2606.24124#bib.bib7)\)proposes verification via computational graph analysis\. Code\-based verification methods\(Zhouet al\.,[2023a](https://arxiv.org/html/2606.24124#bib.bib69)\)demonstrate the value of executable representations for mathematical reasoning but remain specialized to arithmetic domains\. In contrast to these methods, which typically require extensive training data, domain\-specific solvers, or full formalization, VeryTrace generalizes by treating reasoning traces as programs expressed in a universal DSL, enabling mechanized verification of quantitative content while using structured LLM audits for semantic content that resists formalization\. This hybrid approach allows VeryTrace to transfer zero\-shot across heterogeneous domains—from pure mathematics to robotics planning to relational reasoning—without domain\-specific compilation, solvers, or training data, filling a critical gap between brittle end\-to\-end verification and impractical full formalization\.

## 3DSL for Reasoning Trace Formalization

VeryTrace formalizes free\-form reasoning as a sequence of state transitions governed by a*compilable*DSL\. Such a formalization \(a\) makes step dependencies explicit, \(b\) mechanizes as much content as possible into executable expressions, and \(c\) structures the remaining semantic inferences via a small library of universal deduction schemas\.

### 3\.1Reasoning State

We formalize a reasoning trace as state transitions over an explicit*reasoning state space*\.

Let𝒮\\mathcal\{S\}denote a reasoning state space\. A reasoning states∈𝒮s\\in\\mathcal\{S\}is a partial binding

s:𝒱→𝒟,s:\\;\\mathcal\{V\}\\to\\mathcal\{D\},mapping variable names𝒱\\mathcal\{V\}\(e\.g\.,money,position\) to typed values in a domain𝒟\\mathcal\{D\}\(e\.g\., numbers, strings, tuples, lists\)\. The DSL state is designed to be domain\-agnostic\.

### 3\.2Formalizing Problem Context

We explicitly decouple the problem context from the reasoning trajectory\. We formalize the problem context as𝒦=\(F,A,Cinv,Cgoal\)\\mathcal\{K\}=\(F,A,C\_\{\\text\{inv\}\},C\_\{\\text\{goal\}\}\), consisting of initial facts, assumptions, and constraints\.

Initial Facts \(FF\)\.We defineF=\{f1,f2,…,fM\}F=\\\{f^\{1\},f^\{2\},\\dots,f^\{M\}\\\}as a set ofMMindisputable premises derived explicitly from the problem statement\. Each initial factfif^\{i\}is a proposition that seeds the first reasoning states1s\_\{1\}\(e\.g\.,“Betty initially has $50”,“Robot starts at\(3,4\)\(3,4\)facing East”\)\. These serve as the roots of the dependency graph, providing ground truth for anchoring subsequent inferences\.

Assumptions \(AA\)\.We defineA=\{a1,a2,…,aK\}A=\\\{a^\{1\},a^\{2\},\\dots,a^\{K\}\\\}as a set ofKKdomain knowledge from the context for all reasoning steps\. Some assumptions may be explicitly stated \(e\.g\.,”Assume all divisions in this context to be integer divisions”\), while others are implied \(e\.g\.,”moving North increases the y\-coordinate in standard coordinate systems”\)\. By formalizing these as explicit DSL assumptions, we reduce the LLM’s tendency to hallucinate convenient facts when justifying incorrect steps\.

Constraints \(CC\)\.To enforce safety and reliability, we define constraintsC=\{c1,…,cN\}C=\\\{c\_\{1\},\\ldots,c\_\{N\}\\\}as conditions that must hold for valid reasoning\. Each constraintci∈Cc\_\{i\}\\in Cis modeled as a Boolean predicate over reasoning states:

ci:𝒮→\{true,false\}\.c\_\{i\}:\\mathcal\{S\}\\to\\\{\\text\{true\},\\text\{false\}\\\}\.whereci​\(st\)c\_\{i\}\(s\_\{t\}\)evaluates to true if and only if the reasoning statests\_\{t\}satisfies the constraint\.

VeryTrace distinguishes between two constraint scopes:

- •Invariant constraintsCinvC\_\{\\mathrm\{inv\}\}must hold at*every*state along the trace \(e\.g\., “the agent never visits a forbidden cell”\)\.
- •Goal constraintsCgoalC\_\{\\mathrm\{goal\}\}must hold only at the*final*state \(e\.g\., “the agent reaches the target”, “the final numerical answer matches the required format”\)\.

This separation enables more precise definitions of reasoning constraints\.

### 3\.3Typed Reasoning Step

We formalize a natural language reasoning trace𝒯NL\\mathcal\{T\}\_\{\\text\{NL\}\}as a DSL trace𝒯DSL\\mathcal\{T\}\_\{\\text\{DSL\}\}in the form of a sequence of state transitions through typed reasoning steps\. Each reasoning step consumes a set of premises, advances the reasoning state and produces an intermediate claim\.

Letσt\\sigma\_\{t\}be a reasoning step that advances a reasoning statests\_\{t\}tost\+1s\_\{t\+1\}and produces an intermediate claimφt\+1\\varphi\_\{t\+1\}\. A*claim*φt\+1\\varphi\_\{t\+1\}is an atomic assertion or proposition derived from the stepσt\\sigma\_\{t\}\. We further denote the set of premises referenced byσt\\sigma\_\{t\}asPtP\_\{t\}\. Each*premise*p∈Ptp\\in P\_\{t\}is either \(i\) an initial factf∈Ff\\in F, \(ii\) an assumptiona∈Aa\\in Afrom the context, or \(iii\) a prior claimφk,\\varphi\_\{k\},wherek<tk<t\.

As such, a valid reasoning state transition is defined as:

σt​\(typet,st,Pt\)=\(st\+1,φt\+1\)\\sigma\_\{t\}\(\\texttt\{type\}\_\{t\},s\_\{t\},P\_\{t\}\)=\(s\_\{t\+1\},\\varphi\_\{t\+1\}\)\(1\)wheretypet\\texttt\{type\}\_\{t\}indicates the step’s inference type, determining its verification method\. VeryTrace defines three inference types for reasoning steps: COMPUTE, ASSUME, DEDUCE, and CONCLUDE\.

COMPUTE step\.The step must provide one or more executable assignment expressions to some state variables \(e\.g\.,x=sin⁡θ\+kx=\\sin\{\\theta\}\+k\) alongside anupdatefield defining the state change\. This enables deterministic verification: the verifier checks whetherst\+1s\_\{t\+1\}matches evaluatingσt\\sigma\_\{t\}’s expression understs\_\{t\}, eliminating arithmetic hallucinations\.

ASSUME step\.The step declares a premise from the context𝒦\\mathcal\{K\}\. It links the trace explicitly to the static context\.

DEDUCE step\.The step performs logical inference\. To structure semantic reasoning, we requireDeducesteps to instantiateDeduction Schemasfrom a fixed library\. This enforces a structured representation of natural language deductions, enabling rigorous audits\.

The VeryTrace deduction library includes:

- •Modus Ponens: GivenA→BA\\to BandA=trueA=\\text\{true\}, inferBB\.
- •Conjunction: GivenA=trueA=\\text\{true\}andB=trueB=\\text\{true\}, thenA∧B=trueA\\land B=\\text\{true\}\.
- •Transitivity: Givenx=yx=yandy=zy=z, inferx=zx=z\.
- •Direct Deduction: To ensure flexibility, this schema is an unstructured fallback when other structured schemas are too restrictive\.

CONCLUDE step\.This step produces the final reasoning state and declares the final conclusion, denoted asω\\omega\.

Finally, we formally define a DSL trace𝒯D​S​L\\mathcal\{T\}\_\{DSL\}as a trajectory of reasoning state transitions with a sequence of intermediate claims, seeded with the problem context𝒦=\(F,A,Cinv,Cgoal\)\\mathcal\{K\}=\(F,A,C\_\{\\text\{inv\}\},C\_\{\\text\{goal\}\}\), arriving at a final conclusionω\\omega:

𝒯DSL:=\(𝒦,\{st\}t=1T,\{σt\}t=1T−1,\{φt\}t=2T,ω\)\\mathcal\{T\}\_\{\\text\{DSL\}\}:=\\Big\(\\mathcal\{K\},\\;\\\{s\_\{t\}\\\}\_\{t=1\}^\{T\},\\;\\\{\\sigma\_\{t\}\\\}\_\{t=1\}^\{T\-1\},\\;\\\{\\varphi\_\{t\}\\\}\_\{t=2\}^\{T\},\\omega\\Big\)\(2\)
𝒯DSL\\mathcal\{T\}\_\{\\text\{DSL\}\}is*compilable*because \(i\) computational expressions and executable constraints can be parsed and evaluated against the evolving state, and \(ii\) semantic components have a standardized structure \(premises, claims, schema arguments\) enabling structured audits\. In the following section, we present the verification pipeline, which determines whether a given trace𝒯DSL\\mathcal\{T\}\_\{\\text\{DSL\}\}is valid\.

## 4Structured Verification

![Refer to caption](https://arxiv.org/html/2606.24124v1/x2.png)Figure 2:Illustrations of Structured Verification Pipeline\. Given a compiled DSL trace𝒯DSL\\mathcal\{T\}\_\{\\text\{DSL\}\}, the verification pipeline applies four stages of logical verifications\.\(1\) Structural Verificationchecks for backward references and circular dependencies\.\(2\) Constraint Verificationverifies each reasoning state on constraint satisfactions\.\(3\) Step Verificationverifies the computation in COMPUTE step, and logical deduction validity from DEDUCE and ASSUME steps\. Finally,\(4\) Conclusion Verificationverifies whether the final conclusion follows logically from the established claims\.We now present a verification pipeline operating on the formalism defined in Sec\.[3](https://arxiv.org/html/2606.24124#S3)\. As illustrated in Fig\.[1](https://arxiv.org/html/2606.24124#S1.F1), the pipeline implements aGenerate\-Verify\-Repairloop: the user LLM generates a reasoning trace, which is compiled into the VeryTrace DSL, verified for correctness, and if invalid, returned to the model with precise, step\-level diagnostics for repair\. This section details two critical components: bias\-mitigating DSL conversion and hybrid verification logic\.

### 4\.1Two\-stage DSL conversion

The conversion from the promptQQand the natural language reasoning trace𝒯NL\\mathcal\{T\}\_\{\\text\{NL\}\}to a DSL trace𝒯DSL\\mathcal\{T\}\_\{\\text\{DSL\}\}is itself critical: verification quality depends on correctly extracting problem context and reasoning step structure\. If the translation model conditions on the reasoning trace, it may overlook errors to maintain consistency with the provided reasoning\(Holtzmanet al\.,[2020](https://arxiv.org/html/2606.24124#bib.bib15)\)\. For example, if a trace violates a constraint from the prompt, a naive translator might omit that constraint from the DSL to make the trace appear valid\. Therefore, we use a 2\-stage conversion:

##### Stage 1: context extraction\.

A*context\-extraction LLM*reads only the user promptQQand produces a formalized problem context𝒦\\mathcal\{K\}\. Crucially, it does*not*see the trace𝒯NL\\mathcal\{T\}\_\{\\text\{NL\}\}, preventing missing or hallucinated context from propagating to the DSL representation\.

##### Stage 2: trace translation\.

A*translation LLM*then receives\(Q,𝒦,𝒯NL\)\(Q,\\mathcal\{K\},\\mathcal\{T\}\_\{\\text\{NL\}\}\)and produces the DSL trace𝒯DSL\\mathcal\{T\}\_\{\\text\{DSL\}\}\. The translation prompt encourages maximal mechanization: constraints and computations should use executable expressions \(e\.g\., arithmetic, equality/inequality, membership tests\) whenever possible, enabling deterministic verification over LLM audits\.

Our Ablation study \(Sec\.[5\.4](https://arxiv.org/html/2606.24124#S5.SS4)\) suggests that this separation benefits tasks involving longer reasoning chains and mathematical reasoning where explicitly stated context is needed\. We further evaluate the quality of the translation and its impact to the downstream performance in Appendix[C](https://arxiv.org/html/2606.24124#A3)\.

### 4\.2Hybrid verification pipeline

Given a compiled𝒯DSL\\mathcal\{T\}\_\{\\text\{DSL\}\}from Eq\.[2](https://arxiv.org/html/2606.24124#S3.E2), the verifier performs a sequence of verifications that combines mechanical validations with structured LLM audits only where needed\. Mechanical validations provide guarantees and reliability, while LLM\-audits enable greater flexibility\. The complementary nature of mechanical and LLM\-based verification are further analyzed and highlighted in Appendix[B](https://arxiv.org/html/2606.24124#A2)and[D](https://arxiv.org/html/2606.24124#A4)\.

#### 4\.2\.1structural Verification \(VstrV\_\{\\mathrm\{str\}\}\)

Before evaluating content, we verify the structural integrity of the DSL trace\. This verification first checks that each step contains the required fields for its inference type \(e\.g\., COMPUTE steps provide executable expressions; DEDUCE steps instantiate deduction schemas\)\. Further, we verify that every premisep∈ptp\\in p\_\{t\}referenced in stepσt\\sigma\_\{t\}refers to a claim established at a prior steptt\. This mechanically detects forward & backward references and circular dependencies\. We denote this verification result asVp​r​e​\(𝒯DSL\)∈\{true, false\}V\_\{pre\}\(\\mathcal\{T\}\_\{\\text\{DSL\}\}\)\\in\\\{\\text\{true, false\}\\\}\.

#### 4\.2\.2constraint Verification \(VcstV\_\{\\mathrm\{cst\}\}\)

We verify that the reasoning trajectory respects the problem constraints defined in the context\. Given the reasoning trace𝒯DSL:=\(𝒦,\{st\}t=1T,\{σt\}t=1T−1,\{φt\}t=2T,ω\)\\mathcal\{T\}\_\{\\text\{DSL\}\}:=\(\\mathcal\{K\},\\;\\\{s\_\{t\}\\\}\_\{t=1\}^\{T\},\\;\\\{\\sigma\_\{t\}\\\}\_\{t=1\}^\{T\-1\},\\;\\\{\\varphi\_\{t\}\\\}\_\{t=2\}^\{T\},\\omega\), and letCinvC\_\{\\mathrm\{inv\}\}andCgoalC\_\{\\mathrm\{goal\}\}be invariant and goal constraints from context𝒦\\mathcal\{K\}\. We strictly enforce that all invariant constraints hold at every state, and that goal constraints hold at the final state\. Formally, we define the constraint verification resultVc​s​t​\(𝒯DSL\)∈\{true,false\}V\_\{cst\}\(\\mathcal\{T\}\_\{\\text\{DSL\}\}\)\\in\\\{\\text\{true\},\\text\{false\}\\\}as:

Vc​s​t​\(𝒯DSL\)=\(⋀t=1T⋀c∈Ci​n​vc​\(st\)\)∧\(⋀c∈Cgoalc​\(sT\)\)V\_\{cst\}\(\\mathcal\{T\}\_\{\\text\{DSL\}\}\)=\\left\(\\bigwedge\_\{t=1\}^\{T\}\\bigwedge\_\{c\\in C\_\{inv\}\}c\(s\_\{t\}\)\\right\)\\land\\left\(\\bigwedge\_\{c\\in C\_\{\\text\{goal\}\}\}c\(s\_\{T\}\)\\right\)\(3\)
Not all constraints admit an executable predicate form \(e\.g\., natural\-language constraints like“in the game, rule5 takes higher precedence over rule1”\)\. Hence, to evaluate Eq\.[3](https://arxiv.org/html/2606.24124#S4.E3), we employ a hybrid strategy: If a constraintccis expressed as a boolean predicate \(e\.g\.,p​o​s​i​t​i​o​n≠\[2,3\]position\\neq\[2,3\]\), it is evaluated deterministically against the statests\_\{t\}\. For all remaining constraintsccthat represent semantic constraints, we batch these constraints into a prompt and query an Audit LLM\. This audit LLM verifies whether the statests\_\{t\}satisfies the natural language specification ofcc\.

#### 4\.2\.3computation Verification

For COMPUTE steps, we perform deterministic verification\. The verifier extracts the executable math expressions \(possibly multiple\), evaluates them using the values from the prior statests\_\{t\}, and compares the results to the claimed update inst\+1s\_\{t\+1\}\. Discrepancies trigger verification failures\. This verification detects arithmetic hallucinations, ensuring mathematically sound quantitative updates\.

#### 4\.2\.4assumption and deduction Verification

ForAssumeandDeducesteps, mechanical verification is insufficient as they often involve natural language entailment\. Instead, we useStructured LLM Audits\. For each deduction step, we construct a verification prompt containing explicit premisesptp\_\{t\}, the declared deduction schema, and the derived claimϕt\+1\\phi\_\{t\+1\}\. The Audit LLM is tasked with a single, highly focused judgment:Does the claim logically follow from the premises using the specified rule?

For ASSUME steps, the verifier audits whether the claimed assumption is consistent with problem context K\.

##### Step\-wise validity\.

LetVstep​\(𝒯DSL\)∈\{true,false\}V\_\{\\mathrm\{step\}\}\(\\mathcal\{T\}\_\{\\text\{DSL\}\}\)\\in\\\{\\text\{true\},\\text\{false\}\\\}denote the step\-wise validity verification result of the trace𝒯DSL\\mathcal\{T\}\_\{\\text\{DSL\}\}, defined as:

Vstep​\(𝒯DSL\)=⋀t=1T−1Vt,V\_\{\\mathrm\{step\}\}\(\\mathcal\{T\}\_\{\\text\{DSL\}\}\)\\;=\\;\\bigwedge\_\{t=1\}^\{T\-1\}V\_\{t\},\(4\)whereVtV\_\{t\}is computed by \(Sec\.[4\.2\.3](https://arxiv.org/html/2606.24124#S4.SS2.SSS3)\) deterministic execution and verification for COMPUTE steps, and \(Sec\.[4\.2\.4](https://arxiv.org/html/2606.24124#S4.SS2.SSS4)\) structured audits for DEDUCE and ASSUME steps\.

#### 4\.2\.5conclusion verification \(VconcV\_\{\\mathrm\{conc\}\}\)

Local step checks do not guarantee that the final conclusionω\\omegafollows from established claims\. We therefore employ an Audit LLM to verify that the final conclusionω\\omegafollows from established reasoning\. The audit prompt includes the problem context𝒦=\(F,A,Cinv,Cgoal\)\\mathcal\{K\}=\(F,A,C\_\{\\text\{inv\}\},C\_\{\\text\{goal\}\}\), and the sequence of established claims\{φt\}\\\{\\varphi\_\{t\}\\\}\. The LLM assumes all prior claims are valid and all constraints are satisfied, then verifies whether the conclusionω\\omegafollows\. This detects cases where intermediate reasoning is sound but the final answer is inconsistent\.

Finally, the validity of a given DSL trace𝒯DSL\\mathcal\{T\}\_\{\\text\{DSL\}\}is the conjunction of all verification components:

V​\(𝒯DSL\)=\\displaystyle V\(\\mathcal\{T\}\_\{\\text\{DSL\}\}\)\\;=Vstr​\(𝒯DSL\)∧Vcst​\(𝒯DSL\)\\displaystyle V\_\{\\mathrm\{str\}\}\(\\mathcal\{T\}\_\{\\text\{DSL\}\}\)\\wedge V\_\{\\mathrm\{cst\}\}\(\\mathcal\{T\}\_\{\\text\{DSL\}\}\)\(5\)∧Vstep​\(𝒯DSL\)∧Vconc​\(𝒯DSL\)\.\\displaystyle\\wedge V\_\{\\mathrm\{step\}\}\(\\mathcal\{T\}\_\{\\text\{DSL\}\}\)\\wedge V\_\{\\mathrm\{conc\}\}\(\\mathcal\{T\}\_\{\\text\{DSL\}\}\)\.

### 4\.3Verification\-driven repair

WhenV​\(𝒯DSL\)=falseV\(\\mathcal\{T\}\_\{\\text\{DSL\}\}\)=\\text\{false\}, the verifier returns structured diagnostics containing: step index, error type or violated constraint, and explanation\. Because errors are localized \(e\.g\.,“State 7 violates invariant constraintcc”or“Step 12’s computation disagrees with its claimed values”\), the user LLM can revise the problematic region instead of regenerating the full trace\. The verification feedback loop terminates when a valid trace is produced or a maximum iteration countRmaxR\_\{\\text\{max\}\}is reached\. The overall algorithm is presented in Alg\.[1](https://arxiv.org/html/2606.24124#alg1)\.

Algorithm 1VeryTrace Verification Feedback Loop1:Input:user prompt

QQ, max iteration

RmaxR\_\{\\text\{max\}\}
2:Output:Verified answer

ω\\omega
3:

ω,𝒯NL←\\omega,\\mathcal\{T\}\_\{\\text\{NL\}\}\\leftarrowLLM

\(Q\)\(Q\)
4:for

i=1i=1to

RmaxR\_\{\\text\{max\}\}do

5:

𝒦←\\mathcal\{K\}\\leftarrowExtractContext

\(Q\)\(Q\)
6:

𝒯DSL←\\mathcal\{T\}\_\{\\text\{DSL\}\}\\leftarrowTranslateDSL

\(Q,𝒦,𝒯NL\)\(Q,\\mathcal\{K\},\\mathcal\{T\}\_\{\\text\{NL\}\}\)
7:

Vpre​\(𝒯DSL\)←V\_\{\\mathrm\{pre\}\}\(\\mathcal\{T\}\_\{\\text\{DSL\}\}\)\\leftarrowStructural Verification

8:

Vcst​\(𝒯DSL\)←V\_\{\\mathrm\{cst\}\}\(\\mathcal\{T\}\_\{\\text\{DSL\}\}\)\\leftarrowConstraint Verification

9:

Vstep​\(𝒯DSL\)←V\_\{\\mathrm\{step\}\}\(\\mathcal\{T\}\_\{\\text\{DSL\}\}\)\\leftarrowStep\-wise Validity Verification

10:

Vconc​\(𝒯DSL\)←V\_\{\\mathrm\{conc\}\}\(\\mathcal\{T\}\_\{\\text\{DSL\}\}\)\\leftarrowConclusion Verification

11:

V​\(𝒯DSL\)=Vstr​\(𝒯DSL\)∧Vcst​\(𝒯DSL\)∧Vstep​\(𝒯DSL\)∧Vconc​\(𝒯DSL\)\.\\begin\{aligned\} V\(\\mathcal\{T\}\_\{\\text\{DSL\}\}\)\\;=\\;&V\_\{\\mathrm\{str\}\}\(\\mathcal\{T\}\_\{\\text\{DSL\}\}\)\\wedge V\_\{\\mathrm\{cst\}\}\(\\mathcal\{T\}\_\{\\text\{DSL\}\}\)\\\\ &\\wedge V\_\{\\mathrm\{step\}\}\(\\mathcal\{T\}\_\{\\text\{DSL\}\}\)\\wedge V\_\{\\mathrm\{conc\}\}\(\\mathcal\{T\}\_\{\\text\{DSL\}\}\)\.\\end\{aligned\}
12:if

V\(𝒯DSL\)==trueV\(\\mathcal\{T\}\_\{\\text\{DSL\}\}\)==\\text\{true\}then

13:return

ω\\omega
14:else

15:

ϵ←\\epsilon\\leftarrowgenerate logical error feedback

16:

ω,𝒯NL←\\omega,\\mathcal\{T\}\_\{\\text\{NL\}\}\\leftarrowLLM

\(Q,ϵ\)\(Q,\\epsilon\)
17:endif

18:endfor

19:return

ω\\omega

## 5Evaluation

We evaluate VeryTrace to assess whether formalizing natural language reasoning and applying hybrid verification improve the reliability of LLM reasoning\. We aim to answer three key questions: \(1\) Does VeryTrace improve performance across diverse reasoning domains compared to strong zero\-shot baselines? \(2\) Does the structured verification framework prevent error propagation in long\-horizon reasoning tasks? \(3\) Are the deterministic mechanical checks and the two\-stage DSL conversion process necessary for accurate verification?

### 5\.1Experimental Setup

Models\.We employ state\-of\-the\-art open\-weights models for both the reasoning agents and the underlying components of the VeryTrace pipeline\. For the user LLM, we test Llama\-3\.3\-70B\-Instruct \(L3\.3\-70b\-I\), Qwen3\-Next\-80B\-A3B\-Instruct \(Q3\-80b\-I\), and the reasoning\-specialized Qwen3\-Next\-80B\-A3B\-Thinking \(Q3\-80b\-T\)\. For the VeryTrace pipeline \(Context Extraction, Translation, and Audit\), we uniformly utilize Qwen3\-Next\-80B\-Thinking to ensure high\-quality formalization and semantic auditing\. For all experiments, we set the maximum repair budgetRm​a​x=5R\_\{max\}=5\. All methods are evaluated in a zero\-shot setting without task\-specific fine\-tuning\.

##### Baselines\.

We compare against two established prompt\-based verification baselines: \(1\)Chain\-of\-Verification \(CoVe\)\(Dhuliawalaet al\.,[2024](https://arxiv.org/html/2606.24124#bib.bib1)\), a prompt\-based method where the model drafts verification questions to self\-correct hallucinations; and \(2\)Natural Program \(NP\)\(Linget al\.,[2023](https://arxiv.org/html/2606.24124#bib.bib2)\), which encourages the generation of deductive steps verified against problem premises\. We also include the base model \(Vanilla\) as a baseline, which generates answers via standard Chain\-of\-Thought prompting without verification\.

Domains and Metrics\.We select three datasets to stress\-test different reasoning modalities\. First, for symbolic and quantitative reasoning, we use 30 problems from theAIME 2025competition\. This domain tests arithmetic precision and symbolic manipulation in reasoning traces\. Second, for the mixed quantitative\-semantic reasoning domain, we utilize planning tasks fromLLM\-BabyBench\(Choukraniet al\.,[2025](https://arxiv.org/html/2606.24124#bib.bib16)\)\. Models must plan action sequences that navigate a robot through a gridworld from an initial position to a goal while avoiding obstacles\. This task tests the pipeline’s ability to maintain state consistency \(position, direction\) and respect constraints over long horizons\. We run LLM\-BabyBench under three difficulty levels \(small/medium/large\) that vary world size and thus plan horizon\. We evaluate 100 trials per difficulty \(300 total\)\. Finally, for semantic reasoning, we use the test split \(1048 queries\) of theCLUTRRbenchmark\(Sinhaet al\.,[2019](https://arxiv.org/html/2606.24124#bib.bib59)\)to test the semantic inference of kinship relations from given stories\.

For AIME 2025 and CLUTRR, we reportaccuracyvia exact match against ground truth answers\. For LLM\-BabyBench Planning, where multiple feasible paths exist, we report thesuccess rateby executing the predicted action sequence in a simulated grid world using Gymnasium\(Towerset al\.,[2024](https://arxiv.org/html/2606.24124#bib.bib17)\)and checking whether it reaches a terminal state that satisfies the task completion condition \(agent ends adjacent to the target cell while facing it\)\.

### 5\.2Main Results and Discussion

Table 1:Performance comparison of our method against baselines across three domains and three models\.Table[1](https://arxiv.org/html/2606.24124#S5.T1)reports performance across all domains and models\. The per\-difficulty breakdown for LLM\-BabyBench Planning is presented in Fig\.[3](https://arxiv.org/html/2606.24124#S5.F3)\.

VeryTrace generally achieves the highest accuracy, demonstrating that formalizing the reasoning process yields gains regardless of the underlying model architecture\.

A key finding is the performance impact on reasoning\-specialized models\. VeryTrace significantly improves the performance of Qwen3\-Next\-80B\-A3B\-Thinking \(Q3\-80b\-T\)\. While Q3\-80b\-T achieves a strong baseline of 83\.33% on AIME 2025, applying VeryTrace boosts this to 90\.00%\. This result suggests that even specialized models for complex reasoning tasks benefit from the externalized, rigid reasoning state tracking provided by our DSL\. The deterministic checks in VeryTrace \(Vc​s​tV\_\{cst\}and mechanicalCOMPUTEverification\) potentially act as a hard runtime monitor that purely neural self\-correction cannot replicate\.

Furthermore, these gains largely generalize across domains, but the margin over CoVe shrinks on CLUTRR with Q3\-80B\-T\. We hypothesize that given the CLUTRR benchmark is purely semantic reasoning, VeryTrace has fewer opportunities to exploit mechanical verification\. This suggests that VeryTrace overall generalizes across domains, with the strongest benefits likely in math and symbolic reasoning\.

### 5\.3Reasoning in Varying Planning Horizons

![Refer to caption](https://arxiv.org/html/2606.24124v1/x3.png)Figure 3:LLM\-BabyBench Planning Results Across World SizesWe further analyze VeryTrace under increasing reasoning horizons by evaluating LLM\-BabyBench as the world size \(and hence planning horizon\) scales fromSmalltoLarge\. Figure[3](https://arxiv.org/html/2606.24124#S5.F3)reports the corresponding success rates\. We present results for two models, Qwen3\-Next\-80B\-A3B\-Thinking and Llama\-3\.3\-70B\-Instruct; results for Qwen3\-Next\-80B\-A3B\-Instruct are deferred to Appendix[A](https://arxiv.org/html/2606.24124#A1)\.

As expected, performance for all methods degrades as difficulty increases\. VeryTrace outperforms all other methods in all sizes, indicating its ability for long\-horizon reasoning\.

For experiments using Qwen3\-Next\-80B\-A3B\-Thinking \(Figure[3](https://arxiv.org/html/2606.24124#S5.F3)left\), we implement Vanilla, CoVe, and Natural Program using the same underlying model as VeryTrace, since VeryTrace also uses Qwen3\-Next\-80B\-A3B\-Thinking for all components\. The resulting gains therefore reflect the DSL formalization and structured verification, rather than benefits from selecting different audit LLMs\.

### 5\.4Ablation Study: Two\-stage Translation

VeryTrace uses a two\-stage DSL translation to reduce translator bias \(Sec\.[4\.1](https://arxiv.org/html/2606.24124#S4.SS1)\)\. To test whether this separation matters, we compare against a variant withdirecttranslation \(Direct\), which collapses the two steps into a single call that directly maps\(Q,TNL\)→TDSL\(Q,T\_\{\\mathrm\{NL\}\}\)\\rightarrow T\_\{\\mathrm\{DSL\}\}, while keeping the rest of the VeryTrace verification pipeline unchanged\. We evaluateTwo\-Stagevs\.Directon the AIME 2025 dataset, as well as two 150\-instance subsets: LLM\-BabyBench Planning \(Small\) and CLUTRR\. The results are shown in Table[2](https://arxiv.org/html/2606.24124#S5.T2)\.

Table 2:Directtranslation vs\.Two\-StagetranslationTable[2](https://arxiv.org/html/2606.24124#S5.T2)suggests that two\-stage translation is beneficial in AIME 2025 and Planning, but underperformsDirecton CLUTRR\. We hypothesize this difference reflects the fact that AIME and Planning are constraint and computation\-heavy, where isolating𝒦\\mathcal\{K\}before seeingTNLT\_\{\\mathrm\{NL\}\}can better preserve a strict problem specification for verification\. In contrast, CLUTRR relies more on purely semantic inference with fewer explicit constraints to extract; in this setting, a separate context pass may instead introduce noise\. We leave a broader ablation across additional semantic datasets and larger CLUTRR slices to future work\.

## 6Conclusion

We presentedVeryTrace, a reasoning formalization and structured verification framework that compiles natural\-language reasoning traces into explicit state transitions and verifiable claims\. VeryTrace combines deterministic checks with LLM audits, producing localized error reports for iterative repair\. Across AIME 2025, LLM\-BabyBench planning, and CLUTRR benchmarks, VeryTrace improves performance over strong prompt\-based baselines and yields gains for reasoning\-specialized models, suggesting that formalizing reasoning traces and structured verifications provide a robust framework for validating logical reasoning\.

## Impact Statement

This work aims to improve the reliability and verifiability of Large Language Model reasoning, reducing hallucinations and error propagation in multi\-step reasoning tasks\. By enabling more transparent and auditable reasoning traces, VeryTrace aims to enhance trust and safety in LLM deployment for potentially high\-stakes applications\.

The computational overhead of our verification pipeline may limit accessibility, potentially concentrating benefits among well\-resourced actors\. Future work should address efficiency to democratize access to verified reasoning\.

## References

- S\. Berman, K\. McKeown, and B\. Ray \(2024\)Solving zebra puzzles using constraint\-guided multi\-agent systems\.arXiv preprint arXiv:2407\.03956\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px2.p1.1)\.
- Y\. Bertot and P\. Castéran \(2013\)Interactive theorem proving and program development: coq’art: the calculus of inductive constructions\.InSpringer Science & Business Media,Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px2.p1.1)\.
- M\. Besta, N\. Blach, A\. Kubicek, R\. Gerstenberger, L\. Gianinazzi, J\. Gajda, T\. Lehmann, M\. Podstawski, H\. Niewiadomski, P\. Nyczyk,et al\.\(2024\)Graph of thoughts: solving elaborate problems with large language models\.Proceedings of the AAAI Conference on Artificial Intelligence38\(16\),pp\. 17682–17690\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px1.p1.1)\.
- M\. Chen, J\. Tworek, H\. Jun, Q\. Yuan, H\. P\. d\. O\. Pinto, J\. Kaplan, H\. Edwards, Y\. Burda, N\. Joseph, G\. Brockman,et al\.\(2021\)Evaluating large language models trained on code\.arXiv preprint arXiv:2107\.03374\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px3.p1.1)\.
- O\. Choukrani, I\. Malek, D\. Orel, Z\. Xie, Z\. Iklassov, M\. Takáč, and S\. Lahlou \(2025\)LLM\-babybench: understanding and evaluating grounded planning and reasoning in llms\.arXiv preprint arXiv:2505\.12135\.Cited by:[§5\.1](https://arxiv.org/html/2606.24124#S5.SS1.SSS0.Px1.p2.1)\.
- J\. R\. Chowdhury and C\. Caragea \(2025\)Zero\-shot verification\-guided chain of thoughts\.arXiv preprint arXiv:2501\.13122\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px1.p1.1)\.
- K\. Cobbe, V\. Kosaraju, M\. Bavarian, M\. Chen, H\. Jun, L\. Kaiser, M\. Plappert, J\. Tworek, J\. Hilton, R\. Nakano,et al\.\(2021\)Training verifiers to solve math word problems\.arXiv preprint arXiv:2110\.14168\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px1.p1.1)\.
- L\. de Moura, S\. Kong, J\. Avigad, F\. Van Doorn, and J\. von Raumer \(2015\)The lean theorem prover \(system description\)\.InInternational Conference on Automated Deduction,pp\. 378–388\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px2.p1.1)\.
- S\. Dhuliawala, M\. Komeili, J\. Xu, R\. Raileanu, X\. Li, A\. Celikyilmaz, and J\. Weston \(2024\)Chain\-of\-verification reduces hallucination in large language models\.InFindings of the association for computational linguistics: ACL 2024,pp\. 3563–3578\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px1.p1.1),[§5\.1](https://arxiv.org/html/2606.24124#S5.SS1.SSS0.Px1.p1.1)\.
- A\. d\. Garcez, M\. Gori, L\. C\. Lamb, L\. Serafini, M\. Spranger, and S\. N\. Tran \(2019\)Neural\-symbolic computing: an effective methodology for principled integration of machine learning and reasoning\.Journal of Applied Logics6\(4\),pp\. 611–632\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px3.p1.1)\.
- J\. M\. Han, J\. Rute, Y\. Wu, E\. W\. Ayers, and S\. Polu \(2022\)Proof artifact co\-training for theorem proving with language models\.arXiv preprint arXiv:2102\.06203\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px2.p1.1)\.
- A\. Holtzman, J\. Buys, L\. Du, M\. Forbes, and Y\. Choi \(2020\)The curious case of neural text degeneration\.InInternational Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=rygGQyrFvH)Cited by:[§4\.1](https://arxiv.org/html/2606.24124#S4.SS1.p1.3)\.
- A\. Q\. Jiang, S\. Welleck, J\. P\. Zhou, W\. Li, J\. Liu, M\. Jamnik, T\. Lacroix, Y\. Wu, and G\. Lample \(2023\)Draft, sketch, and prove: guiding formal theorem provers with informal proofs\.arXiv preprint arXiv:2210\.12283\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px2.p1.1)\.
- P\. Kesseli, P\. O’Hearn, and R\. S\. Cabral \(2025\)Logic\. py: bridging the gap between llms and constraint solvers\.arXiv preprint arXiv:2502\.15776\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px2.p1.1)\.
- M\. Khalifa, R\. Agarwal, L\. Logeswaran, J\. Kim, H\. Peng, M\. Lee, H\. Lee, and L\. Wang \(2025\)Process reward models that think\.arXiv preprint arXiv:2504\.16828\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px3.p1.1)\.
- T\. Kojima, S\. S\. Gu, M\. Reid, Y\. Matsuo, and Y\. Iwasawa \(2022\)Large language models are zero\-shot reasoners\.Advances in Neural Information Processing Systems35,pp\. 22199–22213\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px1.p1.1)\.
- Y\. Li, Z\. Lin, S\. Zhang, Q\. Fu, B\. Chen, J\. Lou, and W\. Chen \(2023\)Making language models better reasoners with step\-aware verifier\.InProceedings of the 61st Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\),A\. Rogers, J\. Boyd\-Graber, and N\. Okazaki \(Eds\.\),Toronto, Canada,pp\. 5315–5333\.External Links:[Link](https://aclanthology.org/2023.acl-long.291/),[Document](https://dx.doi.org/10.18653/v1/2023.acl-long.291)Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px1.p1.1),[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px3.p1.1)\.
- H\. Lightman, V\. Kosaraju, Y\. Burda, H\. Edwards, B\. Baker, T\. Lee, J\. Leike, J\. Schulman, I\. Sutskever, and K\. Cobbe \(2023\)Let’s verify step by step\.arXiv preprint arXiv:2305\.20050\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px1.p1.1)\.
- Z\. Ling, Y\. Fang, X\. Li, Z\. Huang, M\. Lee, R\. Memisevic, and H\. Su \(2023\)Deductive verification of chain\-of\-thought reasoning\.Advances in Neural Information Processing Systems36,pp\. 36407–36433\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px1.p1.1),[§5\.1](https://arxiv.org/html/2606.24124#S5.SS1.SSS0.Px1.p1.1)\.
- B\. Liu, Y\. Jiang, X\. Zhang, Q\. Liu, S\. Zhang, J\. Biswas, and P\. Stone \(2023\)Llm\+ p: empowering large language models with optimal planning proficiency\.arXiv preprint arXiv:2304\.11477\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px3.p1.1)\.
- C\. Liu, Y\. Yuan, Y\. Yin, Y\. Xu, X\. Xu, Z\. Chen, Y\. Wang, L\. Shang, Q\. Liu, and M\. Zhang \(2025\)Safe: enhancing mathematical reasoning in large language models via retrospective step\-aware formal verification\.arXiv preprint arXiv:2506\.04592\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px2.p1.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\),W\. Che, J\. Nabende, E\. Shutova, and M\. T\. Pilehvar \(Eds\.\),Vienna, Austria,pp\. 22632–22654\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px3.p1.1)\.
- A\. Madaan, N\. Tandon, P\. Gupta, S\. Hallinan, L\. Gao, S\. Wiegreffe, U\. Alon, N\. Dziri, S\. Prabhumoye, Y\. Yang,et al\.\(2023\)Self\-refine: iterative refinement with self\-feedback\.Advances in Neural Information Processing Systems36,pp\. 46534–46594\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px1.p1.1)\.
- J\. Mao, C\. Gan, P\. Kohli, J\. B\. Tenenbaum, and J\. Wu \(2019\)The neuro\-symbolic concept learner: interpreting scenes, words, and sentences from natural supervision\.arXiv preprint arXiv:1904\.12584\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px3.p1.1)\.
- A\. Mensfelt, K\. Stathis, and V\. Trencsenyi \(2025\)Towards logically sound natural language reasoning with logic\-enhanced language model agents\.In2025 IEEE 37th International Conference on Tools with Artificial Intelligence \(ICTAI\),pp\. 838–842\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px2.p1.1)\.
- E\. Nijkamp, B\. Pang, H\. Hayashi, L\. Tu, H\. Wang, Y\. Zhou, S\. Savarese, and C\. Xiong \(2023\)Codegen: an open large language model for code with multi\-turn program synthesis\.arXiv preprint arXiv:2203\.13474\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px3.p1.1)\.
- L\. C\. Paulson \(1994\)Isabelle: a generic theorem prover\.InLecture Notes in Computer Science,Vol\.828\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px2.p1.1)\.
- E\. Perrier \(2025\)Typed chain\-of\-thought: a curry\-howard framework for verifying llm reasoning\.arXiv preprint arXiv:2510\.01069\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px2.p1.1)\.
- N\. Polikarpova, I\. Kuraj, and A\. Solar\-Lezama \(2016\)Program synthesis from polymorphic refinement types\.ACM SIGPLAN Notices51\(6\),pp\. 522–538\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px3.p1.1)\.
- S\. Polu and I\. Sutskever \(2020\)Generative language modeling for automated theorem proving\.arXiv preprint arXiv:2009\.03393\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px2.p1.1)\.
- K\. Sinha, S\. Sodhani, J\. Dong, J\. Pineau, and W\. L\. Hamilton \(2019\)CLUTRR: a diagnostic benchmark for inductive reasoning from text\.arXiv preprint arXiv:1908\.06177\.Cited by:[§5\.1](https://arxiv.org/html/2606.24124#S5.SS1.SSS0.Px1.p2.1)\.
- Solar\-Lezama,Armando \(2008\)Program synthesis by sketching\.Ph\.D\. Thesis\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px3.p1.1)\.
- C\. H\. Song, J\. Wu, C\. Washington, B\. M\. Sadler, W\. Chao, and Y\. Su \(2023\)Llm\-planner: few\-shot grounded planning for embodied agents with large language models\.Proceedings of the IEEE/CVF International Conference on Computer Vision,pp\. 2998–3009\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px3.p1.1)\.
- M\. Towers, A\. Kwiatkowski, J\. Terry, J\. U\. Balis, G\. De Cola, T\. Deleu, M\. Goulão, A\. Kallinteris, M\. Krimmel, A\. KG,et al\.\(2024\)Gymnasium: a standard interface for reinforcement learning environments\.arXiv preprint arXiv:2407\.17032\.Cited by:[§5\.1](https://arxiv.org/html/2606.24124#S5.SS1.SSS0.Px1.p3.1)\.
- T\. H\. Trinh, Y\. Wu, Q\. V\. Le, H\. He, and T\. Luong \(2024\)Solving olympiad geometry without human demonstrations\.Nature625\(7995\),pp\. 476–482\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px2.p1.1)\.
- J\. Uesato, N\. Kushman, R\. Kumar, F\. Song, N\. Siegel, L\. Wang, A\. Creswell, G\. Irving, and I\. Higgins \(2022\)Solving math word problems with process\-and outcome\-based feedback\.arXiv preprint arXiv:2211\.14275\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px1.p1.1)\.
- K\. Valmeekam, M\. Marquez, A\. Olmo, S\. Sreedharan, and S\. Kambhampati \(2023\)Planbench: an extensible benchmark for evaluating large language models on planning and reasoning about change\.Advances in Neural Information Processing Systems36,pp\. 38975–38987\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px3.p1.1)\.
- P\. Wang, L\. Li, Z\. Shao, R\. Xu, D\. Dai, Y\. Li, D\. Chen, Y\. Wu, and Z\. Sui \(2024\)Math\-shepherd: verify and reinforce llms step\-by\-step without human annotations\.InProceedings of the 62nd Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\),pp\. 9426–9439\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px3.p1.1)\.
- X\. Wang, J\. Wei, D\. Schuurmans, Q\. Le, E\. Chi, S\. Narang, A\. Chowdhery, and D\. Zhou \(2023\)Self\-consistency improves chain of thought reasoning in language models\.arXiv preprint arXiv:2203\.11171\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px1.p1.1)\.
- J\. Wei, X\. Wang, D\. Schuurmans, M\. Bosma, F\. Xia, E\. Chi, Q\. V\. Le, and D\. Zhou \(2022\)Chain\-of\-thought prompting elicits reasoning in large language models\.Advances in Neural Information Processing Systems35,pp\. 24824–24837\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px1.p1.1)\.
- Y\. Wu, A\. Q\. Jiang, W\. Li, M\. N\. Rabe, C\. Staats, M\. Jamnik, and C\. Szegedy \(2022\)Autoformalization with large language models\.Advances in Neural Information Processing Systems35,pp\. 32353–32368\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px2.p1.1)\.
- K\. Yang, A\. M\. Swope, A\. Gu, R\. Chalamala, P\. Song, S\. Yu, S\. Godil, R\. Prenger, and A\. Anandkumar \(2023\)Leandojo: theorem proving with retrieval\-augmented language models\.Advances in Neural Information Processing Systems36\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px2.p1.1)\.
- S\. Yao, D\. Yu, J\. Zhao, I\. Shafran, T\. Griffiths, Y\. Cao, and K\. Narasimhan \(2023\)Tree of thoughts: deliberate problem solving with large language models\.Advances in Neural Information Processing Systems36\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px1.p1.1)\.
- K\. Yi, J\. Wu, C\. Gan, A\. Torralba, P\. Kohli, and J\. Tenenbaum \(2018\)Neural\-symbolic vqa: disentangling reasoning from vision and language understanding\.Advances in Neural Information Processing Systems31\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px3.p1.1)\.
- X\. Zhao, T\. Xu, X\. Wang, Z\. Chen, D\. Jin, L\. Tan, Z\. Yu, Z\. Zhao, Y\. He, S\. Wang,et al\.\(2025a\)Boosting llm reasoning via spontaneous self\-correction\.arXiv preprint arXiv:2506\.06923\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px1.p1.1)\.
- Z\. Zhao, Y\. Koishekenov, X\. Yang, N\. Murray, and N\. Cancedda \(2025b\)Verifying chain\-of\-thought reasoning via its computational graph\.arXiv preprint arXiv:2510\.09312\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px3.p1.1)\.
- C\. Zheng, Z\. Zhang, B\. Zhang, R\. Lin, K\. Lu, B\. Yu, D\. Liu, J\. Zhou, and J\. Lin \(2025\)Processbench: identifying process errors in mathematical reasoning\.InProceedings of the 63rd Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\),pp\. 1009–1024\.Cited by:[Table 6](https://arxiv.org/html/2606.24124#A5.T6),[Table 6](https://arxiv.org/html/2606.24124#A5.T6.4.2),[Appendix E](https://arxiv.org/html/2606.24124#A5.p1.1)\.
- A\. Zhou, K\. Wang, Z\. Lu, W\. Shi, S\. Luo, Z\. Qin, S\. Lu, A\. Jia, L\. Song, M\. Zhan,et al\.\(2023a\)Solving challenging math word problems using gpt\-4 code interpreter with code\-based self\-verification\.arXiv preprint arXiv:2308\.07921\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px3.p1.1)\.
- D\. Zhou, N\. Schärli, L\. Hou, J\. Wei, N\. Scales, X\. Wang, D\. Schuurmans, C\. Cui, O\. Bousquet, Q\. Le,et al\.\(2023b\)Least\-to\-most prompting enables complex reasoning in large language models\.arXiv preprint arXiv:2205\.10625\.Cited by:[§2](https://arxiv.org/html/2606.24124#S2.SS0.SSS0.Px1.p1.1)\.

## Appendix AReasoning in Varying Planning Horizons with Qwen3\-Next\-80B\-A3B\-Instruct

Here we present the evaluation results under LLM\-BabyBench Planning in varying planning horizons with all three tested LLM models: Qwen3\-Next\-80B\-A3B\-Thinking, Qwen3\-Next\-80B\-A3B\-Instruct, and Llama\-3\.3\-70B\-Instruct\. The results are presented in Fig\.[4](https://arxiv.org/html/2606.24124#A1.F4), which is consistent with the analysis from Sec\.[5\.3](https://arxiv.org/html/2606.24124#S5.SS3)\.

In particular, Fig\.[4](https://arxiv.org/html/2606.24124#A1.F4)shows that while all methods degrade as the planning horizon grows, VeryTrace remains the strongest method across all world sizes\. The advantage is especially clear for weaker planning backbones \(Qwen3\-Next\-80B\-A3B\-Instruct and Llama\-3\.3\-70B\-Instruct\), where VeryTrace retains substantially higher success rates under Medium and Large worlds\.

![Refer to caption](https://arxiv.org/html/2606.24124v1/x4.png)Figure 4:LLM\-BabyBench Planning Results Across World Sizes
## Appendix BAblation Study on Mechanical Verifications

To further analyze the effectiveness of the hybrid verification pipeline, namely the inclusion of mechanical verifications in comparison with purely an LLM\-as\-a\-judge pipeline, we developed a variant of VeryTrace, termed VeryTrace\-LLM, where all the mechanical verifications are replaced by LLM\-audits\. Specifically, this involves replacing constraint verification \(Sec\.[4\.2\.2](https://arxiv.org/html/2606.24124#S4.SS2.SSS2)\) and COMPUTE step verification \(Sec\.[4\.2\.3](https://arxiv.org/html/2606.24124#S4.SS2.SSS3)\) with LLM audits\. We ran a ablation study between VeryTrace and VeryTrace\-LLM using the Qwen3\-Next\-80B\-A3B\-Thinking model\. We ran the ablation study on AIME 2025, BabyBench Planning \(100 trials each for small, medium, and large\), and CLUTRR\. The results are presented in Table[3](https://arxiv.org/html/2606.24124#A2.T3)\.

Table 3:Ablation study between VeryTrace and purely LLM\-audit variant VeryTrace\-LLMAs shown, VeryTrace generally outperforms the VeryTrace\-LLM variant, especially under the AIME and BabyBench Planning benchmarks and with increased reasoning horizons\. This suggests that the mechanical verifications provide reliable audits overall, and particularly for planning and math related tasks\.

## Appendix CAssessment on Translation Quality Impact

To directly probe translation quality and its impact on downstream verification performance, we added a faithfulness analysis\. Given a natural\-language CoT and its translated DSL trace, we ask an audit LLM to rate translation faithfulness on a 1–10 scale using an explicit rubric \(see App\.[G\.2](https://arxiv.org/html/2606.24124#A7.SS2)\)\. We then compare faithfulness for cases where verification is correct vs\. incorrect\. The correctness of verification is obtained by comparing the verification output against the ground truth correctness of the reasoning\. For this analysis, we ran VeryTrace on 400 trials from BabyBench Planning \(Large\)\. The results are in Table[4](https://arxiv.org/html/2606.24124#A3.T4)\.

Table 4:Translation faithfulness analysisWe note that the gap is modest but directionally consistent\. Better translation quality \(higher mean faithfulness with lower standard deviation\) is associated with more reliable verification\. This observation suggests that the translation quality is directly associated with verification performance\.

## Appendix DSplit between mechanical verifications and LLM\-audits

VeryTrace uses hybrid verification approaches for both the constraint verification \(Sec\.[4\.2\.2](https://arxiv.org/html/2606.24124#S4.SS2.SSS2)\) and COMPUTE step verification \(Sec\.[4\.2\.3](https://arxiv.org/html/2606.24124#S4.SS2.SSS3)\)\. Namely, both mechanical and LLM\-based verifications are used for these components\. To directly assess how much the mechanical verification contribute in practice, here we complement the main evaluation results from Sec\.[5](https://arxiv.org/html/2606.24124#S5)by reporting the split between mechanical and LLM\-based verifications we observed\. In Table[5](https://arxiv.org/html/2606.24124#A4.T5), we report the split under the evaluation trials with Qwen3\-Next\-80B\-A3B\-Thinking model across all benchmarks\.

Table 5:Split between mechanical and LLM\-based verifications across all benchmarks\.We note that mechanical verification is used heavily where executable structure exists \(especially AIME and BabyBench\), while CLUTRR is largely semantic and therefore relies more on LLM audits\. This matches the observation outlined in our manuscript where the largest gains are observed in math and planning, with a smaller margin on CLUTRR\. Further, notice that given the low mechanical verification percentage in CLUTRR, VeryTrace still performed competitively against other baselines\. This suggests despite heavily relying on LLM\-audits on domains like CLUTRR, VeryTrace still benefits from the structure introduced by the DSL\.

## Appendix EEvaluation of VeryTrace’s standalone verification capability on ProcessBench

The verifier quality of VeryTrace directly impact the downstream performance\. We further provide a standalone verifier evaluation using the ProcessBench\(Zhenget al\.,[2025](https://arxiv.org/html/2606.24124#bib.bib70)\)under the GSM8K split\. This small\-scale verification is to show how well the verifier performs on a benchmark outside ones from the main evaluation as a standalone component\. We report the results in Table[6](https://arxiv.org/html/2606.24124#A5.T6)\.

Table 6:VeryTrace’s verifier performance on ProcessBench\(Zhenget al\.,[2025](https://arxiv.org/html/2606.24124#bib.bib70)\)\.We note that VeryTrace’s verifier achieves a competitive false accept rate \(9\.7%\) and false reject rate \(11\.4%\), presenting itself as a strong verification mechanism\.

## Appendix FLimitations and Future Work

##### Verification cost and scalability\.

A primary limitation of our step\-level hybrid verification is runtime and resource usage\. Since structural and constraint checks are performed*per step*, the total number of verification calls scales linearly with the number of steps in the trace \(see Sec\.[4\.2\.3](https://arxiv.org/html/2606.24124#S4.SS2.SSS3)and Sec\.[4\.2\.4](https://arxiv.org/html/2606.24124#S4.SS2.SSS4)\)\. This scaling is acceptable for moderately sized traces, but can become costly for extremely long traces or iterative feedback loops that require multiple conversion–verification rounds\.

##### Dependence on semantic auditing for deductive steps\.

While mostcomputesteps can be verified efficiently by deterministically executing \(or re\-evaluating\) the extracted mathematical expressions,deducesteps often involve semantic transformations that are difficult to validate purely with symbolic execution\. In our current pipeline, such steps may require an LLM\-based audit or other semantic checker, which increases cost and can introduce stochasticity into verification outcomes\.

##### Expressiveness of the inference schema library\.

Our current set of structured inference schema is intentionally small to keep compilation and verification tractable\. As a consequence, certain forms of reasoning may be forced into coarsededucesteps \(or into underspecified natural\-language explanations\), reducing the granularity of verifiable structure\. Extending the schema library to cover richer algebraic transformations, case analysis, induction, and domain\-specific semantic operators is an important direction for increasing task coverage and reducing reliance on black\-box semantic auditing\.

##### Future work\.

We plan to \(i\) improve efficiency via caching, incremental verification, and selective checking policies \(e\.g\., prioritizing steps that affect constraints or goal satisfaction\); \(ii\) integrate stronger formal back\-ends such as SMT solvers and/or Lean\-style provers to formalize and discharge a larger fraction of semantic deductions; and \(iii\) grow the DSL and deduction schema set while maintaining a clean compilation interface, enabling broader task coverage and finer\-grained error localization\.

## Appendix GPrompt Templates

For reproducibility, we document the*exact*prompt templates used in our experiments for the three LLM\-facing stages of the VeryTrace pipeline: \(B\.1\) the*user LLM*that produces a structured, step\-decomposed reasoning trace; \(B\.2\) the*context extractor*that reads*only*the original problem statement and outputs a structured context \(facts/assumptions/constraints/state/goal\); and \(B\.3\) the*DSL converter*that combines prompt\-derived context with the chain\-of\-thought to emit a ReasonLang JSON trace\.

All templates below contain placeholders \(e\.g\.,\{problem\},\{prompt\_text\},\{cot\_text\}\) that are filled at runtime\.

### G\.1User LLM Prompt

We standardize the user LLM output to facilitate deterministic parsing and downstream conversion\. In particular, we enforce \(i\) explicit*premises*per step, \(ii\) explicit*assumptions used*, and \(iii\) explicit*state updates*when variables change\. We also request an*atomic*decomposition into small steps to improve step\-level localization during verification\.

Youareacarefulreasonersolvingcomplexmathcompetitionproblems\.

YouwillbegivenaproblemfromtheAIME2025competitionthatrequiresstep\-by\-stepreasoningtosolve\.

Problem:

\{problem\}

YouMUSTformatyourreasoningaccordingtothefollowingrulesandexactformat:

\-First,writedownthefollowingintheexactformat:

PROBLEMSTATEMENT:\.\.\.

GIVENFACTSANDVARIABLES:\.\.\.

ALLASSUMPTIONS:\.\.\.

CONSTRAINTS\(IFANY\):\.\.\.

UNKNOWNS:\.\.\.

\-Reasonstepbystep\.Eachstepmustbeexplicitlynumberedandmustlistoutthefollowingintheexactformat:

Step<step\_number\>:

PREMISES:fact1,fact2,\.\.\.,factn

CALCULATION/REASONING:\.\.\.

ASSUMPTIONSUSED\(IFANY\):\.\.\.

UPDATEINREASONINGVARIABLES\(IFANY\):\.\.\.

\-\*\*BEATOMIC\*\*:breakdownreasoningintosmallestatomicsteps,themoregranulardecompositionthebetter\.

Attheend,outputthefinalansweronitsownlineintheexactformat:

FINAL\_ANSWER:<integer\>

Note:Theanswermustbeaninteger\(nodecimals,nofractions\)\.

TheFINAL\_ANSWERlinemustbethelastlineofyouranswer\.

### G\.2Context Extraction Prompt

To reduce confirmation bias in the conversion stage, we first extract context from the problem statement*without*giving the model access to the chain\-of\-thought\. The extractor is instructed to not solve the problem, but instead produce a complete context bundle: initial facts, persistent assumptions, verifiable constraints \(with mathematical expressions whenever possible\), an initial state for tracked variables, and a precise goal\.

Youareareasoningcontextanalyzer\.YourjobistoextractALLrelevantcontextfromaproblemstatementthatwouldbeneededforreasoning\.

\*\*CRITICAL\*\*:YouaregivenONLYtheproblemstatement\.DONOTtrytosolvetheproblem\.YourgoalistoextractcontextthatwouldbeneededforANYreasoningapproach\.

\*\*ProblemStatement:\*\*

\{prompt\_text\}

\*\*YourTask:\*\*

ExtractallrelevantcontextfromtheproblemstatementaboveintoastructuredJSONformat:

‘‘‘json

\{\{

"initial\_facts":\[

\{\{"id":"fact\_1","content":"\.\.\.","entities":\[\.\.\.\]\}\}

\],

"assumptions":\[

\{\{"id":"a\_1","content":"\.\.\."\}\}

\],

"constraints":\[

\{\{

"id":"c1",

"description":"Naturallanguagedescription",

"constraint\_expr":"Mathematicalexpression\(ifapplicable\)",

"scope":"invariant\|goal"

\}\}

\],

"initial\_state":\{\{

"variable\_name":value

\}\},

"goal":"\.\.\."

\}\}

‘‘‘

\*\*CRITICALDEFINITIONS\-Readthesecarefully:\*\*

1\.\*\*initial\_facts\*\*:GivenfactsthatdescribetheINITIALorSTARTINGconditions\.

\-Thesearefactsthatmayonlyholdatthebeginningandcanchangeduringreasoning\.

\-Examples:"Bettystartswith$50","Robotisatposition\(0,0\)","Johnhas5applesinitially"

\-Ifavariableisassociatedordefinedwithafactstatement,itshouldalsobeincludedinthecontext\.Example:"a:5isanoddnumber",theentiredefinitionandstatementshouldbeincluded\.

\-Format:\{\{"id":"fact\_1","content":"\.\.\.","entities":\[\.\.\.\]\}\}

2\.\*\*assumptions\*\*:FactsassumedtobetrueTHROUGHOUTALLreasoningsteps\.

\-Thesearepersistenttruthsthatdon’tchange,unlikeinitial\_facts\.

\-Thesearefactstakenasgiven,NOTconditionstoverify\(thoseareconstraints\)\.

\-LookforbothEXPLICITassumptions\(statedintheproblem\)andIMPLICITassumptions\(impliedbytheproblemcontext\)\.

\-Examples:

\*"Allapplesarewholeapples\(nofractions\)"\-assumptionaboutthenatureofobjects

\*"Therobotcanonlymoveonestepatatime"\-assumptionaboutcapabilities

\*"Timeprogresseslinearly"\-assumptionabouttheenvironment

\*"Thecoordinatesystemhasy\-axispointingnorth"\-assumptionaboutthereferenceframe

\*"Operationsareperformedleft\-to\-right"\-assumptionaboutexecutionorder

\-Format:\{\{"id":"a\_1","content":"\.\.\."\}\}

\-\*\*BETHOROUGH\*\*:ExtractALLassumptions,bothexplicitandimplicit,thatunderpinanyreasoningapproach\.

3\.\*\*constraints\*\*:ConditionsthatmustbeVERIFIEDorSATISFIEDduringreasoning\.

\-TheseareNOTassumptions\(factstakenasgiven\),butconditionstoCHECK\.

\-Eachconstrainthas:

\*"description":Naturallanguageexplanation

\*"constraint\_expr":MathematicalexpressionMUSTusesvariablesfrominitial\_state\(e\.g\.,"x<10","position\[0\]\!=2"\)

\-Leaveemptyifcannotbeexpressedmathematically

\*"scope":"invariant"\(mustholdatALLsteps\)or"goal"\(mustholdonlyatFINALstep\)

\-Examples:"Theagentcannotgotoposition\(2,3\)","Totalmustnotexceed100"

\-Format:\{\{"id":"c1","description":"\.\.\.","constraint\_expr":"\.\.\.","scope":"invariant\|goal"\}\}

4\.\*\*initial\_state\*\*:Initialvaluesofvariablesmentionedintheproblem\.

\-Extractstartingvaluesforquantitativereasoning\.

\-Examples:\{\{"position":\[0,0\],"money":50,"direction":0\}\}

5\.\*\*goal\*\*:Thequestionorgoaltobeanswered\.

\*\*CRITICALINSTRUCTIONS:\*\*

\-\*\*ExtractEVERYTHING\*\*:Bethorough\-extractallfacts,assumptions,andconstraintsthatmightberelevant\.

\-\*\*DoNOTsolve\*\*:YouareNOTsolvingtheproblem,justextractingcontext\.

\-\*\*Lookforimplicitassumptions\*\*:Don’tjustextractwhat’sexplicitlystated\-alsoidentifyimplicitassumptionstheproblemmakes\.

\-\*\*Differentiatecarefully\*\*:

\*initial\_facts=startingconditionsthatmaychange

\*assumptions=persistenttruthsthroughoutreasoning

\*constraints=conditionstoverify/satisfy

\-\*\*Usemathematicalexpressions\*\*:Forconstraints,maximizeuseofmathematicalexpressionsinconstraint\_exprfieldusingvariablesfrominitial\_state\.

\-\*\*Constraint\_exprvariablesMUSTbefrominitial\_state\*\*:Allconstraint\_exprmustusevariablesfrominitial\_state\.

\-Constraint\_exprmustbeabooleanexpressionthatistrueifsatisfied\.

\*\*Extractgoalprecisely\*\*:Captureexactlywhattheproblemisaskingfor\.

OutputONLYtheJSONstructure,noothertext\.

\*\*IMPORTANT\*\*:YourfinaloutputMUSTstartwith‘‘‘jsonandendwith‘‘‘\.

### G\.3DSL Conversion Prompt

Given the pre\-extracted context and the original chain\-of\-thought, the converter \(i\) takes the*union*of prompt\-derived context and any additional assumptions/constraints introduced in the trace, \(ii\) decomposes the trace into atomic DSL steps with explicit premises, and \(iii\) emits a structured JSON trace suitable for subsequent structural and constraint verification\.

Youareareasoningtraceanalyzer\.Yourjobistoconvertanaturallanguagechain\-of\-thought\(COT\)reasoningtraceintoastructuredJSONformat\.

\*\*OriginalProblem/Prompt:\*\*

\{prompt\_text\}

\*\*Pre\-ExtractedContextfromPrompt:\*\*

Thefollowingcontexthasbeenextractedfromtheproblemstatementbyanalyzingitindependently\(withoutlookingattheCOT\):

\{extracted\_context\}

\*\*Chain\-of\-ThoughtReasoning:\*\*

\{cot\_text\}

\*\*YourTask:\*\*

ConvertthereasoningtraceintoastructuredJSONformatwiththefollowingstructure:

‘‘‘json

\{\{

"context":\{\{

"initial\_facts":\[

\{\{"id":"fact\_1","content":"\.\.\.","entities":\[\.\.\.\]\}\}

\],

"goal":"\.\.\.",

"constraints":\[

\{\{

"id":"c1",

"description":"Naturallanguagedescription",

"constraint\_expr":"Mathematicalexpressionlike’x<10’or’position\[0\]\!=2’",

"scope":"invariant\|goal"

\}\}

\],

"assumptions":\[

\{\{"id":"a\_1","content":"\.\.\."\}\}

\],

"initial\_state":\{\{

"variable\_name":value,

"another\_variable":\[x,y\]

\}\}

\}\},

"steps":\[

\{\{

"step\_number":1,

"inference\_type":"assume\|deduce\|compute\|conclude",

"claim":"\.\.\.",

"premises":\["fact\_1","step\_2"\],

"reasoning":"\.\.\.",

"assumptions":\["\.\.\.",\.\.\.\],

"updates":\{\{"variable\_name":new\_value,\.\.\.\}\},

"compute\_expr":"expressionforcomputesteps",

"deduction\_rule":"modus\_ponens\|direct\|transitivity\|\.\.\.",

"deduction\_args":\{\{"arg1":"\.\.\.","arg2":"\.\.\."\}\}fordeducesteps,

"is\_final":false

\}\}

\],

"conclusion":\{\{

"content":"\.\.\."

\}\}

\}\}

‘‘‘

\*\*CRITICALINSTRUCTIONSFORCOMBININGCONTEXT:\*\*

Thepre\-extractedcontextabovewascreatedbyanalyzingthepromptONLY\(withoutseeingtheCOT\)\.TheCOTmayalsomentionorusesomefacts,assumptions,orconstraints\.

Yourjobisto\*\*taketheUNION\*\*of:

1\.Contextextractedfromtheprompt\(providedabove\)

2\.AnyadditionalcontextmentionedorusedintheCOT

\*\*Howtocombine:\*\*

\-\*\*initial\_facts\*\*:Usetheonesfrompre\-extractedcontext\.TheCOTtypicallydoesn’taddnewinitialfacts\.

\-\*\*assumptions\*\*:COMBINE\(union\)assumptionsfrompre\-extractedcontextANDanyadditionalassumptionsmentionedintheCOT\.

\-IftheCOTexplicitlystatesanassumptionnotinthepre\-extractedcontext,ADDit\.

\-Ifanassumptionappearsinboth,keepitonce\(noduplicates\)\.

\-PreserveIDsfrompre\-extractedcontext;assignnewIDs\(a\_N\+1,a\_N\+2,\.\.\.\)fornewassumptionsfromCOT\.

\-\*\*constraints\*\*:COMBINE\(union\)constraintsfrompre\-extractedcontextANDanyconstraintsmentionedintheCOT\.

\-Samerulesasassumptions:addnewones,avoidduplicates\.

\-PreserveIDsfrompre\-extractedcontext;assignnewIDsfornewconstraints\.

\-\*\*initial\_state\*\*:Usefrompre\-extractedcontext,orenhanceifCOTprovidesadditionalvariablevalues\.

\-\*\*goal\*\*:Usefrompre\-extractedcontext\.

\*\*Instructions:\*\*

1\.Useinitial\_factsfrompre\-extractedcontextwithIDslike"fact\_1","fact\_2",etc\.

2\.\*\*Useinitial\_statefrompre\-extractedcontext\*\*:Theinitialstatevariableshavebeenextractedfromtheproblemstatement\.

3\.Usegoalfrompre\-extractedcontext\.

4\.\*\*DecomposeCOTintoatomicsteps\*\*:

\-Eachstepshouldbeasingleinference,calculation,ordeduction\.

\-IftheoriginalCOTcombinesmultiplereasoningoperationsinonestep,SPLITthemintoseparatesteps\.

\-Examplesofwhattosplit:

\*"CalculateXandthenuseittodetermineY"\-\-\>Splitinto:Step1\(calculateX\),Step2\(determineYusingX\)

\*"FromAandB,weconcludeCandD"\-\-\>Splitinto:Step1\(fromAandBconcludeC\),Step2\(fromCconcludeD\)

\*Multiplecalculationsinsequence\-\-\>Eachcalculationisaseparatestep

5\.\*\*COMBINEconstraints\*\*frompre\-extractedcontextandCOT:

\-Thepre\-extractedcontextalreadyhasconstraintswithmathematicalexpressionswherepossible

\-IftheCOTmentionsadditionalconstraintsnotinpre\-extractedcontext,ADDthem

\-Fornewconstraints:

\*\*\*MAXIMALLYUSEMATHEMATICALEXPRESSIONS\*\*:ThisistheMOSTIMPORTANTrequirement

\*ForEACHconstraint,trytoexpressitasamathematicalexpressionusing:

\-Comparisonoperators:<,\>,==,\!=,<=,\>=

\-Logicaloperators:and,or,not

\-Arithmetic:\+,\-,\*,/

\-Array/tupleindexing:position\[0\],position\[1\]

\-Variablenamesthatwillbetrackedinreasoningstate

\*\*\*constraint\_exprfield\*\*:mathematicalexpressionMUSTusesvariablesfrominitial\_state

\*\*\*descriptionfield\*\*:Naturallanguageexplanationoftheconstraint

\*ONLYusenaturallanguage\(leaveconstraint\_exprempty\)iftheconstraintCANNOTbeexpressedmathematically

\-\*\*Constraintstructure\*\*:

\*GiveeachconstraintauniqueID:useIDsfrompre\-extractedcontext,assignnewIDslike"c\_N\+1"foradditions

\*Giveeachconstraintascope:"invariant"or"goal"

\-"invariant":MustbesatisfiedatALLreasoningsteps

\-"goal":MustbesatisfiedonlyattheFINALreasoningstep\(successcriteria\)

\*\*\*BESPECIFIC\*\*:Useactualvalues,notplaceholders\(e\.g\.,"position\[0\]\!=2"not"position\[0\]\!=x"\)

\*\*\*BEATOMIC\*\*:Eachconstraintmustbeasinglecondition

\*\*\*USEVARIABLESFROMTHEREASONINGSTATE\*\*:variablesinconstraint\_exprMUSTbefromtheinitial\_state

6\.\*\*COMBINEassumptions\*\*frompre\-extractedcontextandCOT:

\-Thepre\-extractedcontextalreadyhasassumptions

\-IftheCOTexplicitlymentionsorreliesonadditionalassumptionsnotinpre\-extractedcontext,ADDthem

\-Format:\{\{"id":"a\_N\+1","content":"\.\.\."\}\}

\-PreserveIDsfrompre\-extractedcontext;assignnewsequentialIDsforadditions

7\.Foreachreasoningstep:

\-\*\*inference\_type\*\*:Classifythestepasoneof:

\*"assume"\-Establishingafactfromcontext/premises

\*"deduce"\-Logicaldeductionorinference\(MUSTprovidededuction\_ruleanddeduction\_args\)frompremises

\*"compute"\-Performingcalculations\(MUSTprovidecompute\_exprandupdates\)

\*"conclude"\-Finalconclusion

\-\*\*claim\*\*:Themainassertionbeingmadeinthisstep

\-\*\*premises\*\*:CRITICAL\-ListtheIDsoffacts/stepsthisdependsonusingONLYtheseformats:

\*"fact\_1","fact\_2",etc\.forinitialfactsfromcontext

\*"step\_1","step\_2",etc\.forpreviousreasoningsteps

\*Example:\["fact\_1","step\_2"\]meansthisstepusesfact\_1andtheresultfromstep\_2

\*DONOTwritenaturallanguagedescriptions\-ONLYuse"fact\_\#"or"step\_\#"format

\-\*\*reasoning\*\*:Naturallanguageexplanationofwhythisstepfollows

\-\*\*assumptions\*\*:Anyassumptionsmade\(canreferenceassumptionIDsfromcontext\)

\-\*\*FORCOMPUTESTEPSONLY\-BOTHREQUIRED\*\*:

\*\*\*compute\_expr\*\*:AnASSIGNMENTexpressionintheform"variable=expression"

\-MUSTcontainanequalssign\(assignmentoperator\)

\-TheRHSexpressionmustuseONLYvariablesfromthecurrentreasoningstate

\-Examples:

\*"position=\[position\[0\]\+1,position\[1\]\]"\(updatesentirevariable\)

\*"x=x\+1"\(updatesexistingvariable\)

\*"new\_x=position\[0\]\+1"\(createsnewvariable\)

\-INVALID:"position\[0\]\+1"\(missingassignment\)

\-INVALID:"x\+1"\(missingassignment\)

\*\*\*updates\*\*:Theresultingvariablechangesaftertheassignment

\-Examples:\{\{"position":\[4,3\]\}\},\{\{"x":2\}\},\{\{"new\_x":4\}\}

\-MustintroducenewvariablesORupdateexistingones

\-Theupdatesmustreflectthestatechangesfromtheassignment

\-\*\*FORDEDUCESTEPSONLY\*\*:

\*MUSTprovideatleastonepremise\.

\*\*\*deduction\_rule\*\*:Thelogicalrulebeingapplied,oneof:

\-"modus\_ponens"\-A\-\>B,A=\>B

\-"conjunction"\-A,B=\>AandB

\-"direct"\-Conclusionfollowsdirectlyfrompremises

\-"transitivity"\-A=B,B=C=\>A=C

\*\*\*deduction\_args\*\*:Structuredargumentsforthedeductionrule

\-For"modus\_ponens":\{\{"conditional":"ifAthenB","antecedent":"A","consequent":"B"\}\}

\-For"direct":\{\{"premise\_content":"\.\.\.","conclusion":"\.\.\."\}\}

\-For"transitivity":\{\{"first\_equality":"A=B","second\_equality":"B=C","conclusion":"A=C"\}\}

\-Adaptformatbasedonthedeductionrule

\*\*\*updates\*\*:MUSTprovideupdatesthatintroducenewvariablesormodifyexistingones

\-\*\*is\_final\*\*:trueonlyforthelaststep

8\.Extractthefinalconclusion

\-\*\*content\*\*:Thecontentmusthaveenoughinformationtofullyanswertheoriginalproblem\.

\-\*\*BETHOROUGH\*\*:Thecontentmustbethoroughandcomplete\.Avoidasingle\-wordanswer\.

\*\*CRITICALRULESFORPREMISES:\*\*

\-ALWAYSuse"step\_\#"toreferenceprevioussteps\(e\.g\.,"step\_1","step\_2"\)

\-ALWAYSuse"fact\_\#"toreferenceinitialfacts\(e\.g\.,"fact\_1","fact\_2"\)

\-NEVERwritenaturallanguageinpremiseslike"InitialstateisX"or"Bettyhas$50"

\-EachpremiseMUSTbeexactly"step\_\#"or"fact\_\#"

\-Deducestepsmusthaveatleastonepremise\.

\*\*CRITICALRULESFORINFERENCE\_TYPE:\*\*

\-Use"compute"ONLYwhenthestepdirectlyevaluatesamathematicalexpression:

\*A"compute"stepMUSTprovideBOTH"compute\_expr"\(executableexpression\)AND"updates"\(results\)

\*Thecompute\_exprmustuseONLYvariablesfromthereasoningstate

\*TheupdatesmustintroducenewvariablesORmodifyexistingones

\*Examples:"position\[0\]\+1","total\-15","\[x,y\+1\]"

\-Use"deduce"forlogicalreasoning,includingreasoningabouttransformations:

\*A"deduce"stepMUSTprovideBOTH"deduction\_rule"AND"deduction\_args"

\*A"deduce"stepSHOULDprovide"updates"whenitmodifiesreasoningstate

\*Updatesareoptionalforintermediatelogicalconclusions

\*Use"deduce"whenthestepinvolvesunderstandingsemanticsorrules

\-Use"assume"forestablishingfactsfromtheproblemstatement

\-Use"conclude"forthefinalanswer

\*\*KEYDISTINCTION:\*\*

\-"compute":Directcalculationwithexistingvalues\-\-\>"position\[0\]\+1"

\-"deduce":Reasoningaboutwhattransformationapplies\-\-\>"turningleftfromeastmeansfacingnorth,sonewdirectionis3"

\-MAXIMALLYuse"compute"stepswhenmathisinvolved\.

\*\*CRITICALRULESFORCOMPUTESTEPS:\*\*

\-MUSTinclude"compute\_expr":anASSIGNMENTexpressionwithformat"variable=expression"

\-MUSTinclude"updates":theresultingvariablechanges

\-Thecompute\_exprMUSTcontainanequalssign\(=\)forassignment

\-TheRHSoftheassignmentmustreferenceONLYexistingstatevariables

\-ExamplesofVALIDexpressions:

\*"x=x\+1"\(ifxexistsinstate\)

\*"position=\[position\[0\]\+1,position\[1\]\]"\(ifpositionexists\)

\*"new\_total=old\_total\+amount"\(ifold\_totalandamountexist\)

\-ExamplesofINVALIDexpressions:

\*"position\[0\]\+1"\(missingassignment\-whichvariabledoesthisupdate?\)

\*"y=z\+1"\(ifzdoesn’texistinstate\)

\*\*CRITICALRULESFORDEDUCESTEPS:\*\*

\-MUSTinclude"deduction\_rule":oneofthedefinedlogicalrules

\-MUSTinclude"deduction\_args":structuredargumentsforthatrule

\-SHOULDinclude"updates":statechangesfromthededuction\(optionalforintermediatesteps\)

\-Thededuction\_argsmustclearlyspecifythelogicalstructure

\-Use"direct"ruleforstraightforwardlogicalconclusions

\-Examples:

\*Fororientationchanges:\{\{"deduction\_rule":"direct","deduction\_args":\{\{"premise\_content":"agentfaceseast\(direction=0\),turningleftrotatescounter\-clockwise","conclusion":"agentnowfacesnorth\(direction=3\)"\}\},"updates":\{\{"direction":3\}\}\}\}

\*Formovement:\{\{"deduction\_rule":"direct","deduction\_args":\{\{"premise\_content":"agentat\(3,4\)facingwest,movingforwardgoeswest","conclusion":"agentmovesto\(2,4\)"\}\},"updates":\{\{"position":\[2,4\]\}\}\}\}

\*Forintermediatelogic:\{\{"deduction\_rule":"direct","deduction\_args":\{\{"premise\_content":"targetiseastofagent","conclusion":"agentneedstoturntofaceeast"\}\},"updates":\{\{\}\}\}\}

\*Formodus\_ponens:\{\{"deduction\_rule":"modus\_ponens","deduction\_args":\{\{"conditional":"ifagentfaceseastandturnsleftthenagentfacesnorth","antecedent":"agentfaceseastandturnsleft","consequent":"agentfacesnorth"\}\},"updates":\{\{"direction":3\}\}\}\}

\*\*IMPORTANT:\*\*

\-\*\*COMBINEcontext\*\*:Takeunionofpre\-extractedcontextandanyadditionalcontextfromCOT

\-\*\*Avoidduplicates\*\*:Ifthesameassumption/constraintappearsinboth,keepitonce

\-\*\*PreserveIDs\*\*:KeepIDsfrompre\-extractedcontext;assignnewsequentialIDsforadditions

\-\*\*ExtractconstraintswithACTUALvalues\*\*:Usespecificvaluesfromtheproblem

\-\*\*NoMagicConstraintVariables\*\*:Donotusevariablesthatarenotintheinitial\_stateintheconstraint\_expr

\-\*\*Trackstatethroughupdates\*\*:Everyvariableintroduction/changeshouldbein"updates"

\-\*\*Payspecialattention\*\*toconstraintsintheoriginalpromptthattheCOTmighthaveignored

\-Classifyconstraintscopecorrectly\(invariantvsgoal\)

\-Inthe"updates"field,useJSONarrays\[x,y\]nottuples\(x,y\)

\-Fornestedstructures,usearrays:\[\[1,2\],3\]not\(\(1,2\),3\)

FinalNote:OutputONLYtheJSONstructure,noothertext\.

### G\.4Translation faithfulness evaluation prompt template

Given the natural language CoT and the translated formal DSL, we use the following prompt template to query the LLM to evaluate the faithfulness of the translation based on a score from 1 to 10\.

YouareanexpertevaluatorassessingthefaithfulnessofaformalDSL\(Domain\-SpecificLanguage\)translationofanatural\-languagechain\-of\-thought\(COT\)reasoningtrace\.

Important:TheDSLhasalreadypassedsyntaxvalidation\.itisstructurallywell\-formed\.YourtaskisNOTtocheckforsyntaxerrors\.Instead,youmustevaluatewhethertheDSLisa\*\*faithfulsemantictranslation\*\*oftheoriginalNLCOT,regardlessofwhethertheoriginalNLCOTitselfislogicallycorrect\.

\*\*BriefDSLschemaoverview\(forreferenceonly\):\*\*

TheDSLisaJSONobjectwiththesekeysections:

\-\*\*"initial\_facts"\*\*:Alistoffactsextractedfromtheproblemstatement/NLCOTpreamble\.Eachhasan"id"and"content"\.

\-\*\*"assumptions"\*\*:Alistofassumptionsthereasonerstatedorreliedon\.Eachhasan"id"and"content"\.

\-\*\*"constraints"\*\*:Alistofconstraintsthatthereasoningshouldrespect\.Eachhasa"description"andoptional"constraint\_expr"\.

\-\*\*"initial\_state"\*\*:Thestartingstateofthereasoning\(e\.g\.,position,direction\)\.

\-\*\*"goal"\*\*:Thegoalthereasoneristryingtoachieve\.

\-\*\*"steps"\*\*:Alistofreasoningsteps\.Eachstephas:

\-"step\_number":ordinalindex

\-"inference\_type":oneof"compute","deduction","observation",etc\.

\-"claim":whatthestepasserts

\-"premises":referencestopriorstepsorfactsused

\-"reasoning":thereasoningorcalculationperformed

\-"assumptions":assumptionsreferenced

\-"compute\_expr"\(ifapplicable\):aformalizedexpressionofthecomputation

\-"updates":statechangesproducedbythisstep

\-\*\*"conclusion"\*\*:Thefinalconclusionofthereasoning\.

\*\*OriginalProblem/Prompt:\*\*

\{prompt\_text\}

\*\*OriginalNatural\-LanguageCOT:\*\*

\{nl\_cot\}

\*\*TranslatedDSL:\*\*

\{dsl\_json\_str\}

\*\*YourEvaluationTask:\*\*

AssesswhethertheDSLisafaithfultranslationoftheoriginalNLCOT\."Faithful"meanstheDSLaccuratelycaptureswhattheNLCOTsays\-notwhethertheNLCOTiscorrect\.Specifically:

\*\*FaithfulnessScore\(1\-10\):\*\*HowwelldoestheDSLcapturethecontentandreasoningoftheoriginalNLCOT?

1\-2:TheDSLbearslittleresemblancetotheNLCOT\.

3\-4:MajorportionsoftheNLCOTaremissing,distorted,orfabricatedintheDSL\.

5\-6:TheDSLcapturesthegeneralapproachbuthasnotableomissionsoradditions\.

7\-8:TheDSLismostlyfaithfulwithminoromissions,additions,orrephrasings\.

9\-10:TheDSLisanear\-perfectorperfecttranslationoftheNLCOT\.

RespondinEXACTLYthisformat\(noothertext\):

FAITHFULNESS\_SCORE:<integer1\-10\>