LogicTrack：使用形式化逻辑求解器审计大型语言模型的推理轨迹

# Auditing Reasoning Trajectories of Large Language Models with Formal Logic Solvers
Source: [https://arxiv.org/html/2609.21492](https://arxiv.org/html/2609.21492)
###### Abstract

Chain\-of\-Thought \(CoT\) reasoning has been shown to improve the performance of large language models \(LLMs\), yet existing optimization methods largely rely on outcome\-based feedback, leaving the logical validity of intermediate reasoning steps largely unverified\. To address the gap whereby LLMs arrive at correct final answers through logically flawed intermediate reasoning chains, we propose LogicTrack, a neuro\-symbolic framework that audits reasoning trajectories by auto\-formalizing each reasoning step into symbolic representations and verifying it with automated theorem provers\. LogicTrack introduces Solver\-Based Backtracking Reward \(SBR\), a step\-wise scoring mechanism that quantifies logical soundness and guides backtracking tree search at inference time\. We further extend LogicTrack to construct supervised fine\-tuning \(SFT\) data with backtracking traces from its trajectories, enabling fine\-tuned models to internalize step\-wise auditing as an intrinsic capability\. Extensive experiments across 8 reasoning benchmarks and 7 LLMs demonstrate that LogicTrack effectively improves both the verifiability of reasoning chains and final answer pass rate, thereby enhancing overall CoT quality and trustworthiness in high\-stakes domains\.

1University of Bristol

2King Abdullah University of Science and Technology

## 1Introduction

Reasoning chains have greatly advanced the capacity of large language models \(LLMs\) to tackle complex tasks in coding\([Gao et al\. 2023](https://arxiv.org/html/2609.21492#bib.bib46)\), question answering\([Lu et al\. 2022](https://arxiv.org/html/2609.21492#bib.bib47)\), and logical reasoning\([Xu et al\. 2024](https://arxiv.org/html/2609.21492#bib.bib12)\)\. Recent models such as OpenAI\-o1\([Jaech et al\. 2024](https://arxiv.org/html/2609.21492#bib.bib34)\)and DeepSeek\-R1\([Guo et al\. 2025](https://arxiv.org/html/2609.21492#bib.bib35)\)further improve performance by encouraging the model to verbalize and extend its thinking trajectory before generating a final answer\. However, producing a correct final answer is not sufficient on its own\. If the intermediate reasoning steps contain logically invalid operations, users in high\-stakes domains such as legal and scientific reasoning cannot trust its conclusions, even when the final answer happens to be correct\([Turpin et al\. 2023](https://arxiv.org/html/2609.21492#bib.bib48);[Huang and Chang 2023](https://arxiv.org/html/2609.21492#bib.bib51)\)\. This concern is especially important as most current methods use outcome\-driven training, which does not guarantee that the reasoning path itself is sound\.

This concern has motivated a growing body of research focused on the quality of intermediate reasoning steps\. Existing work can be broadly divided into two categories\. The first is training\-free test\-time self\-refinement, where the LLM generates a response, receives feedback through a critic model or retrieval mechanism, and applies a search algorithm to regenerate the response based on that feedback\([Yao et al\. 2023a](https://arxiv.org/html/2609.21492#bib.bib53);[Xie et al\. 2023](https://arxiv.org/html/2609.21492#bib.bib50)\)\. The second is training\-based process supervision, where process reward models \(PRMs\) are trained to evaluate the quality of individual reasoning steps, typically using human\-annotated or model\-generated step\-level labels\([Lightman et al\. 2023](https://arxiv.org/html/2609.21492#bib.bib23);[Khalifa et al\. 2023](https://arxiv.org/html/2609.21492#bib.bib52)\)\. However, methods in both categories ultimately rely on human feedback or LLM\-based judges to produce feedback and reward signals\. Such signals are non\-deterministic for logical correctness, prone to inconsistency, and difficult to scale reliably across diverse domains\.

![Refer to caption](https://arxiv.org/html/2609.21492v1/img1_workflow.png)Figure 1:Overview of the LogicTrack workflow\. Each NL reasoning step is decomposed, formalized into a solver\-executable specification, verified, assigned an SBR score, and either forwarded \[FW\] to the next step or backtracked \[BT\] for regeneration\. These generated trajectories can be used for backtracking fine\-tuning\.More recent efforts have turned to neuro\-symbolic approaches to make verification more reliable\. These include using formal tools for symbolic checking of LLM outputs\([Olausson et al\. 2023](https://arxiv.org/html/2609.21492#bib.bib13);[Pan et al\. 2023](https://arxiv.org/html/2609.21492#bib.bib14)\), auto\-formalization of natural language reasoning into solver\-verifiable logic, and self\-refinement guided by solver feedback\([Quan et al\. 2024](https://arxiv.org/html/2609.21492#bib.bib18);[Singh et al\. 2026](https://arxiv.org/html/2609.21492#bib.bib45)\)\. Step\-wise formal verification for natural language reasoning remains underexplored\. Recent LogicReward\([Xu et al\. 2025b](https://arxiv.org/html/2609.21492#bib.bib43)\)and VeriCoT\([Feng et al\. 2025](https://arxiv.org/html/2609.21492#bib.bib44)\)represent important initial steps in this direction\. Concretely, both methods first generate a complete response and then apply solver\-based step verification retroactively, constructing SFT and DPO training data from the verified traces\.

However, both methods perform step verification in a post\-hoc way\. They require a complete reasoning chain and final answer to be generated first, and then audit each step retroactively\. This paradigm has two limitations\. First, once the full response has been produced, delayed verification raises safety concerns as flawed reasoning may have already been presented to or acted upon by users\. Second, a logical error in an intermediate step can propagate through and corrupt subsequent reasoning steps, making after\-the\-fact correction both more difficult and less reliable\.

These limitations naturally raise the question of whether we can*audit LLMs’ reasoning trajectories during generation and intervene with timely backtracking to regenerate from the point of failure\.*To address this question, we introduceLogicTrack, a neuro\-symbolic framework for generation\-time auditing and improvement of CoT reasoning through a formally defined verification reward\. Specifically, LogicTrack decomposes each NL reasoning step into premises, explanations, and conclusions, auto\-formalizes them into logic specifications, and uses the solver for verification\. We defineSolver\-based Backtracking Reward \(SBR\), a fine\-grained step\-level signal that combines premise fidelity with solver verification\. LogicTrack enables a reward\-guided backtracking search at inference time\. When SBR of a step falls below a predefined threshold, the model triggers a backtrack and regenerates the reasoning from that step onward\.

Beyond inference\-time auditing, we further extend the application of LogicTrack toself\-backtracking supervised fine\-tuning \(SFT\)\. Unlike prior self\-correction methods that rely on synthetically injected errors to construct backtracking datasets\([Yang et al\. 2025b](https://arxiv.org/html/2609.21492#bib.bib49)\), LogicTrack pairs real model\-generated flawed trajectories with solver\-verified corrections\. Fine\-tuning on these trajectories with a dedicated backtrack token<backtrack\>allows the model to internalize step\-wise verification behavior, and we show that this benefit generalizes across multiple benchmarks and models\.

Overall, our main contributions are as follows:

- •We propose LogicTrack, a neuro\-symbolic framework that audits NL reasoning trajectories via autoformalization and solver verification at inference time\. LogicTrack includes a reward\-guided backtracking mechanism that uses Solver\-based Backtracking Reward to audit and guide model step\-wise reasoning\.
- •We evaluate LogicTrack on eight reasoning benchmarks across seven models, showing consistent improvements in both final\-answer correctness and intermediate\-step validity\. Further ablation studies and diverse variants of the search strategy confirm the generalizability of LogicTrack\.
- •We show that LogicTrack can be extended to construct high\-quality backtracking SFT data\. By introducing a dedicated backtrack token, the fine\-tuned model internalizes step\-wise verification behavior and achieves self\-backtracking in reasoning\.

## 2Methodology of LogicTrack

Figure[1](https://arxiv.org/html/2609.21492#S1.F1)illustrates the overall workflow of LogicTrack, which proceeds in three parts: decomposition and formal verification, reward\-guided search with backtracking, and the extended application of LogicTrack as higher\-quality training data for self\-backtracking supervised fine\-tuning\.

#### Preliminaries\.

When models use natural language to infer logical reasoning tasks, their goal is to determine the logical relationship between a set of given premisesP=\{p1,…,pn\}P=\\\{p\_\{1\},\\ldots,p\_\{n\}\\\}and a queryQQ\. Each data sample is a triplex=\(P,Q,y\)x=\(P,Q,y\), wherey∈𝒴y\\in\\mathcal\{Y\}is the ground\-truth label from a dataset\-specific label set𝒴\\mathcal\{Y\}\. Although label names \(e\.g\.,entailment/contradiction,yes/no/uncertain\) differ across datasets, each𝒴\\mathcal\{Y\}corresponds to one of three underlying logical relations:P⊧QP\\models Q,P⊧¬QP\\models\\neg Q, or neither\. Given a samplexx, the model response is an ordered sequence ofTTreasoning steps\(s1,s2,…,sT\)\(s\_\{1\},s\_\{2\},\\ldots,s\_\{T\}\)followed by a final predictiony^\\hat\{y\}\. To ensure the quality of both the final prediction and the intermediate reasoning trajectories, we propose LogicTrack to audit the logical validity of each intermediate step and trigger backtracking when necessary\.

### 2\.1Decomposition and Formal Verification

#### Step Decomposition

We specify in the LLM response format that each reasoning step needs to present new conclusion\(s\) derived from contextCiC\_\{i\}and explanationEiE\_\{i\}, and the details are explained below\. Let𝒦i=\{q1,…,qi\}\\mathcal\{K\}\_\{i\}=\\\{q\_\{1\},\\ldots,q\_\{i\}\\\}denote the set of derived conclusions from the firstiiverified reasoning steps \(𝒦0=∅\\mathcal\{K\}\_\{0\}=\\emptyset\)\. Specifically, the stepsis\_\{i\}can be decomposed into three componentssi=\(Ci,Ei,qi\)s\_\{i\}=\(C\_\{i\},E\_\{i\},q\_\{i\}\), defined as below\. With bothCiC\_\{i\}andEiE\_\{i\}stated explicitly, the conclusionqiq\_\{i\}should follow by logical entailment alone\. The verifiedqiq\_\{i\}is then incorporated into𝒦i\\mathcal\{K\}\_\{i\}, making it available as context for subsequent steps\.

- •ContextCiC\_\{i\}: the premises fromPPand prior verified conclusions relevant to this step, i\.e\.,Ci⊆P∪𝒦i−1C\_\{i\}\\subseteq P\\cup\\mathcal\{K\}\_\{i\-1\}\.
- •ExplanationEiE\_\{i\}: implicit assumptions and background knowledge that the step relies on but does not state, e\.g\., “a father is a parent”\.
- •Conclusionqiq\_\{i\}: the new claim derived fromCiC\_\{i\}andEiE\_\{i\}\.

#### Autoformalization and Verification

Unlike post\-hoc verification methods that check the entire reasoning chain after the response is fully generated, LogicTrack performs verification during reasoning in a step\-wise autoregressive way\. Starting from thei−1i\{\-\}1verified steps\(s1,…,si−1\)\(s\_\{1\},\\ldots,s\_\{i\-1\}\)and knowledge base𝒦i−1\\mathcal\{K\}\_\{i\-1\}, the reasoning LLM generates the next candidate stepsis\_\{i\}, conditioned on\(P,Q,s1,…,si−1\)\(P,Q,s\_\{1\},\\ldots,s\_\{i\-1\}\)\. The candidate is then decomposed, formalized and verified by the logic solver\.

For each candidate stepsis\_\{i\}, the formalization model receives components\(Ci,Ei,qi\)\(C\_\{i\},E\_\{i\},q\_\{i\}\)and formalizes them into an executable logic specificationFiF\_\{i\}in SMT\-LIB format\. The context and explanations are jointly formalized as a conjunction of solver assertionsΦi\\Phi\_\{i\}, i\.e\.,Φi\\Phi\_\{i\}encodesCi∪EiC\_\{i\}\\cup E\_\{i\}\. The conclusionqiq\_\{i\}is encoded as the proof goal, yieldingFi=\(Φi,qi\)F\_\{i\}=\(\\Phi\_\{i\},\\,q\_\{i\}\), so that verification reduces to checking ifΦi⊧qi\\Phi\_\{i\}\\models q\_\{i\}\. GivenFi=\(Φi,qi\)F\_\{i\}=\(\\Phi\_\{i\},\\,q\_\{i\}\), LogicTrack verifies whether the candidate step is well\-formed and logically justified\. The solver first checks syntactic validity of the generated formalization; if the specification is malformed, the autoformalization module is re\-invoked up toMMtimes\. Once a valid specification is obtained, the solver tests whetherΦi⊧qi\\Phi\_\{i\}\\models q\_\{i\}via proof by refutation, that is, it checks whetherΦi∪\{¬qi\}\\Phi\_\{i\}\\cup\\\{\\neg q\_\{i\}\\\}is unsatisfiable, and also records diagnostic signals such as contradiction or undecidability\. These verification outcomes, together with the judge’s assessment of explanation grounding, are stored as a step\-level audit log and converted into the scalar reward used by the search controller\.

### 2\.2Reward\-Guided Backtracking Search

We consider two aspects of effective reasoning\. The model must ground its reasoning in the given premises, and each inference must be logically sound\. We design a reward function called the Solver\-based Backtracking Reward \(SBR\) to quantify both aspects\. LogicTrack assigns each stepsis\_\{i\}a composite rewardSBR⁡\(si\)=λ⋅Rfidelity​\(Φi,P\)\+\(1−λ\)⋅Rverify​\(Fi\)\\mathrm\{SBR\}\(s\_\{i\}\)=\\lambda\\cdot R^\{\\mathrm\{fidelity\}\}\(\\Phi\_\{i\};\\,P\)\+\(1\-\\lambda\)\\cdot R^\{\\mathrm\{verify\}\}\(F\_\{i\}\)\.

- •Fidelity rewardRfidelity​\(Φi,P\)R^\{\\mathrm\{fidelity\}\}\(\\Phi\_\{i\};\\,P\): Checks the consistency ofΦi\\Phi\_\{i\}, including if each assertion is grounded in the original premisesPP\(not sourced from the queryQQ\), if introduced commonsense is acceptable, and ifΦi\\Phi\_\{i\}is jointly satisfiable\. We defineRfidelity​\(Φi,P\)=1R^\{\\mathrm\{fidelity\}\}\(\\Phi\_\{i\};\\,P\)=1if all checks pass, and00otherwise\.
- •Verification rewardRVerify​\(Fi\)R^\{\\mathrm\{Verify\}\}\(F\_\{i\}\): The verification score is set to11if the specificationFiF\_\{i\}is syntactically correct and the step is logically valid \(Φi⊧qi\\Phi\_\{i\}\\models q\_\{i\}\)\. IfFiF\_\{i\}is syntactically invalid, autoformalization will be regenerated up toMMtimes before the step is marked as unverifiable andRVerify​\(Fi\)=0R^\{\\mathrm\{Verify\}\}\(F\_\{i\}\)=0\. We also setRVerify​\(Fi\)=0R^\{\\mathrm\{Verify\}\}\(F\_\{i\}\)=0if the solver actively refutes the step \(Φi⊧¬qi\\Phi\_\{i\}\\models\\neg q\_\{i\}\)\. For undecided steps, the verifier assigns partial creditRVerify​\(Fi\)=αR^\{\\mathrm\{Verify\}\}\(F\_\{i\}\)=\\alpha, whereα∈\(0,1\)\\alpha\\in\(0,1\)is a discounting constant, since these steps may simply exceed the solver’s decision procedure without being logically wrong\.

LogicTrack builds the verified reasoning chain via reward\-guided backtracking search to decide whether to forward or backtrack on each candidate step\. At each steptt, the search maintains a verified prefix\(s1,…,st−1\)\(s\_\{1\},\\ldots,s\_\{t\-1\}\)and evaluates a new candidatests\_\{t\}against two quality criteria: the step\-level rewardSBR⁡\(st\)\\mathrm\{SBR\}\(s\_\{t\}\)and running mean over all verified stepsSBR¯​\(t\)=1t​∑i=1tSBR⁡\(si\)\\overline\{\\mathrm\{SBR\}\}\(t\)=\\frac\{1\}\{t\}\\sum\_\{i=1\}^\{t\}\\mathrm\{SBR\}\(s\_\{i\}\)\. The search starts from an empty prefix and proceeds one step at a time\. A candidatests\_\{t\}is forwarded ifSBR⁡\(st\)≥θstepandSBR¯​\(t\)≥θavg\\mathrm\{SBR\}\(s\_\{t\}\)\\geq\\theta\_\{\\mathrm\{step\}\}\\quad\\text\{and\}\\quad\\overline\{\\mathrm\{SBR\}\}\(t\)\\geq\\theta\_\{\\mathrm\{avg\}\}\. In that case,sts\_\{t\}is appended to the verified prefix and𝒦t−1\\mathcal\{K\}\_\{t\-1\}is updated to𝒦t\\mathcal\{K\}\_\{t\}\.

When triggering backtracking, LogicTrack collects the audit logs forsts\_\{t\}and re\-prompts the model with the verified prefix\(s1,…,st−1\)\(s\_\{1\},\\ldots,s\_\{t\-1\}\)along with concise failure feedback derived from error logs\. The model then regenerates from positionttonward\. This backtracking process repeats until a viable solution is found\. We provide implementation details and discussion of other backtracking strategies like Beam search and MCTS in Appendix A\.1[A\.1](https://arxiv.org/html/2609.21492#A1.SS1)\.

### 2\.3LogicTrack with Backtracking\-SFT

![Refer to caption](https://arxiv.org/html/2609.21492v1/misc/imgs/test_cast.png)Figure 2:An example of LogicTrack\-SFT training data construction with backtracking trajectories\.We introduce LogicTrack\-SFT, an extension of LogicTrack that converts its backtracking trajectories into supervised fine\-tuning data, allowing the model to internalize step\-level auditing as an intrinsic capability\.

Recent work has shown that training on explicit error\-correction trajectories can teach models to revise flawed reasoning\. An et al\.\([An et al\. 2023](https://arxiv.org/html/2609.21492#bib.bib9)\)construct mistake\-correction pairs; Ye et al\.\([Ye et al\. 2024](https://arxiv.org/html/2609.21492#bib.bib10)\)show that retry data with erroneous steps immediately followed by corrections improves reasoning; and Self\-Backtracking\([Yang et al\. 2025a](https://arxiv.org/html/2609.21492#bib.bib11)\)further introduces a dedicated backtracking token to learn when and where to revise a partial trajectory\. However, the supervision signals in these methods are largely synthesized from artificially injected or sampled errors in mathematical settings, where correctness is straightforward to verify\. We build on the same backtracking intuition but focus on a harder setting: using LogicTrack to construct verifier\-grounded backtracking steps for NL logic reasoning\.

Specifically, SFT training data is constructed from LogicTrack’s backtracking trajectories\. We treat the verified correct path from the search tree ass\+s^\{\+\}and the backtracked steps that triggered backtracking events ass−s^\{\-\}\. A training trajectory with backtrack at positionkkis assembled by concatenating the correct prefixes, the backtracked stepsk−s\_\{k\}^\{\-\}, a special backtrack token, and the verified correct continuation:\{s1\+⋯sk−1\+sk−<backtrack\>sk\+⋯sn\+\}\\\{s\_\{1\}^\{\+\}\\cdots s\_\{k\-1\}^\{\+\}\\;\\;s\_\{k\}^\{\-\}\\;\\;\\texttt\{<backtrack\>\}\\;\\;s\_\{k\}^\{\+\}\\cdots s\_\{n\}^\{\+\}\\\}\. For example, one possible training trajectory with backtracking in the workflow demo in Figure[1](https://arxiv.org/html/2609.21492#S1.F1)is\{s1,s2,s3,s4,<backtrack\>,s4′′,s5′′,s6′\}\\\{s\_\{1\},s\_\{2\},s\_\{3\},s\_\{4\},\\texttt\{<backtrack\>\},s^\{\\prime\\prime\}\_\{4\},s^\{\\prime\\prime\}\_\{5\},s^\{\\prime\}\_\{6\}\\\}\. Figure[2](https://arxiv.org/html/2609.21492#S2.F2)presents a more intuitive example, where we aim to determine whether Alex is cold based on the given premises, such as ‘Alex is Tumpus’ and ‘dompus is zumpus’\. We consider both single\-round and multi\-round backtracking during the synthetic stage, resulting in a set of∼\\sim6,000 samples for training\. Given the constructed trajectory𝐬\\mathbf\{s\}, LogicTrack\-SFT minimizes the standard autoregressive negative log\-likelihoodℒSFT\(θ\)=−∑t=1nlogpθ\(st∣P,Q,s<t\)\\mathcal\{L\}\_\{\\mathrm\{SFT\}\}\(\\theta\)=\-\\sum\_\{t=1\}^\{n\}\\log p\_\{\\theta\}\\left\(s\_\{t\}\\mid P,Q,s\_\{<t\}\\right\)\. The backtrack token<backtrack\>is added to the model vocabulary and trained end\-to\-end, teaching the model to recognize flawed steps and self\-correct without external critics\. The detailed implementations can be found in Appendix A\.2[A\.2](https://arxiv.org/html/2609.21492#A1.SS2)\.

## 3Experiments and Results

This section presents the experimental setup and the discussions of overall performance, ablation studies, and LogicTrack’s extended application to SFT self\-backtracking\.

Table 1:Benchmark\-level Performance Comparison of VWA%, OA%, and UR% between BASE and LogicTrack \(Ours\) across Eight Reasoning Data Benchmarks and Seven Models\.### 3\.1Experimental Setup

#### Datasets and Baselines\.

We evaluate on a diverse collection of natural\-language reasoning benchmarks including e\-SNLI\([Camburu et al\. 2018](https://arxiv.org/html/2609.21492#bib.bib1)\), FOLIO\([Han et al\. 2024](https://arxiv.org/html/2609.21492#bib.bib2)\), LogiQA\([Liu et al\. 2020](https://arxiv.org/html/2609.21492#bib.bib3)\), ProntoQA\([Saparov and He 2023](https://arxiv.org/html/2609.21492#bib.bib7)\), ProofWriter\([Tafjord et al\. 2021](https://arxiv.org/html/2609.21492#bib.bib4)\), QASC\([Khot et al\. 2020](https://arxiv.org/html/2609.21492#bib.bib5)\), SARA\([Holzenberger et al\. 2020](https://arxiv.org/html/2609.21492#bib.bib6)\), and SemEval\([SemEval\-2026 Team 2026](https://arxiv.org/html/2609.21492#bib.bib8)\)\.

Each dataset is split into train and test set following\([Xu et al\. 2025b](https://arxiv.org/html/2609.21492#bib.bib43)\)\. The evaluation covers seven large language models with varying architectures and scales, including three proprietary models \(Gemini\-2\.5\([Comanici et al\. 2025](https://arxiv.org/html/2609.21492#bib.bib31)\), GPT\-4o\([Hurst et al\. 2024](https://arxiv.org/html/2609.21492#bib.bib32)\), and GPT\-5\([Singh et al\. 2025](https://arxiv.org/html/2609.21492#bib.bib33)\)\) and four open\-weight models \(Llama\([AI 2024](https://arxiv.org/html/2609.21492#bib.bib36)\), Mistral\([Jiang et al\. 2023](https://arxiv.org/html/2609.21492#bib.bib38)\), Qwen2\.5\-7B, and Qwen2\.5\-14B\([Yang et al\. 2024](https://arxiv.org/html/2609.21492#bib.bib37)\)\)\. We use the vanilla CoT as our primary baseline \(BASE\)\. Additional baseline comparisons \(i\.e\. LogicReward\) can be found in Appendix C, and more detailed descriptions of the datasets and models are reported in Appendix B\.

#### Metrics\.

We evaluate models using four metrics that assess outcome\-level performance, process\-level performance, and their combination\.Outcome Accuracy \(OA\)is the fraction of LLM responses where the final answer is correct\.Verified Ratio \(VR\)measures the average proportion of reasoning steps that pass solver checks\.Unverified Ratio \(UR\)is the complementary fraction of unverified steps\.Verified Utility \(VU\)refers to answer accuracy restricted to all fully verified steps\.Verification\-Weighted Accuracy \(VWA\)combines both aspects by weighting each correct prediction by its per\-problem verification ratio\. More detailed metric descriptions are provided in Appendix B\.

### 3\.2Main Results: Higher Outcome Correctness and Step Verifiability

Figure[3](https://arxiv.org/html/2609.21492#S3.F3)compares the average OA and VU of the base models and LogicTrack across all seven models\. Overall, LogicTrack consistently improves both metrics on almost all settings\. The VU gains are especially pronounced: GPT\-4o\-mini rises from 21\.51% to 46\.61%, Llama3\.1\-8B from 9\.24% to 32\.75%, and Qwen2\.5\-7B from 16\.33% to 35\.54%\. Among the closed\-source models, GPT\-4o\-mini also achieves the strongest joint gain in OA, increasing from 70\.68% to 78\.49%\. The simultaneous improvement of OA and VWA suggests that verification does more than trigger backtracking; it can steer regeneration toward reasoning paths that are both more valid and more answer\-preserving\.

Table[1](https://arxiv.org/html/2609.21492#S3.T1)further confirms that this pattern holds at the benchmark level\. LogicTrack improves over the baseline in 133 out of 168 benchmark metric comparisons\. Specifically, LogicTrack preserves or improves OA on most model and dataset pairs, with especially large gains on tasks that require multi\-step deduction\. Qwen2\.5\-7B shows 0% VWA on QASC as it directly outputs answers with no reasoning steps, causing step\-level evaluation to fail\. This issue can be mitigated by our SFT model \(Table[5](https://arxiv.org/html/2609.21492#A3.T5)\)\. GPT\-4o\-mini on ProofWriter rises from 54\.27% to 79\.9%, Qwen2\.5\-7B on ProntoQA from 92% to 97%, and Mistral\-7B on ProofWriter from 27\.14% to 39\.2%\. Even when the base model is already strong, LogicTrack maintains OA while improving verifiability\. GPT\-5\-nano on ProntoQA, for example, stays at high OA while UR drops from 11\.17% to 10\.24%\. LogicTrack also reduces UR for most model and dataset pairs, confirming that backtracking replaces unverifiable steps with solver\-validated alternatives\. The largest reductions include Gemini\-2\.5 on FOLIO from 75\.63% to 27\.79%, Llama\-3\.1\-8B on SARA from 39\.1% to 9\.89%, and Llama\-3\.1\-8B on QASC from 44\.65% to 16\.3%\. These reductions are accompanied by large VWA gains\. GPT\-4o\-mini on ESNLI rises from 46\.38% to 87\.21%, and Gemini\-2\.5 on FOLIO from 21\.17% to 56\.37%\. Overall, these results show that LogicTrack improves both final answers and the verifiability of the reasoning process\.

![Refer to caption](https://arxiv.org/html/2609.21492v1/res_overall.png)Figure 3:Overall OA and VU for all models averaged across eight benchmarks under BASE and LogicTrack settings\. Here∙\\bulletindicates closed source models, and▲\\blacktriangleindicates locally deployed models\. Dashed arrows connect each model’s BASE and LogicTrack results\.
### 3\.3Ablation Study of LogicTrack

We perform an ablation study on SARA with both open\-source and proprietary LLMs to examine the effects of different reward designs and model backtracking strategies on the performance of LogicTrack\.

Effectiveness of SBR reward\.Table[2](https://arxiv.org/html/2609.21492#S3.T2)a ablates the contribution of each SBR component: fidelity reward onlyRfidelityR^\{\\mathrm\{fidelity\}\}, solver reward onlyRverifyR^\{\\mathrm\{verify\}\}, and the full SBR reward\. The fidelity rewardRfidelityR^\{\\mathrm\{fidelity\}\}yields stronger outcome\-based metric gains, with aΔ\\DeltaOA of 10\.7% on GPT\-4o\-mini and 11% on Llama\-8B\. Yet its effect on metrics that require step\-level verification is far more modest\. For instance, on the VWA metric, fidelity reward improves over the baseline by 5\.4% on GPT\-4o\-mini and a mere 0\.4% on Llama\-8B\. In contrast, the solver reward alone achieves VWA improvements exceeding 20% on both models\. This suggests that grounding each step in the given premises helps the model avoid certain flawed steps and therefore contributes positively to final answer correctness\. However, improving step\-level verifiability still requires other reward signals\. This gap supports the design choice of using solver feedback as a separate reward term\.

This is validated by the results showing that rewardRverifyR^\{\\mathrm\{verify\}\}greatly improved the VWA performance\. On GPT\-4o\-mini, the solver reward alone achieves 23\.4% VWA and 12\.9% OA gains over the baseline, while reducing the unverified ratio from 32\.55% to 15\.78%\. On Llama\-8B, it delivers an identicalΔ\\DeltaVWA of25\.4%25\.4\\%and brings the unverified step ratio down from 39\.10% to 7\.89%\. These results align with our expectation that the solver reward directly incentivizes the model to produce structurally valid, executable reasoning steps, which are precisely what VWA and UR measure\.

Combining both rewards \(SBR\) yields the best VWA for both models withΔ\\DeltaVWA of 25\.4% and 25\.9% over the baseline, as well as the lowest UR on GPT\-4o\-mini at 10\.81%\. On Llama\-8B, adding both rewards further lifts OA from 62\.50% to 63\.60%, confirming that these two signals are complementary\.RverifyR^\{\\mathrm\{verify\}\}incentivizes structural correctness whileRfidelityR^\{\\mathrm\{fidelity\}\}enforces factual grounding, and together they cover both dimensions of high\-quality structural logical reasoning\.

\(a\) SBR Reward Component Ablation

\(b\) Backtracking Search Strategy Variants

Table 2:Ablation Study of LogicTrack\. \(a\) SBR reward component ablation\. \(b\) Backtracking search strategy variants\. TheΔ\\Deltavalues report the absolute improvement \(%\) over the BASE model\.![Refer to caption](https://arxiv.org/html/2609.21492v1/misc/imgs_clean/ablation2.jpg)Figure 4:OA⇑\\Uparrowand VWA⇑\\Uparrowunder BASE, LogicTrack, and LogicTrack\-SFT averaged over all datasets\. LogicTrack\-SFT refers to the model fine\-tuned on LogicTrack\-generated train data\.Backtracking Search Strategy Variants\.Table[2](https://arxiv.org/html/2609.21492#S3.T2)b compares three search strategies, including default greedy backtracking, beam search, and Monte Carlo Tree Search\. The default strategy achieves the highest VWA and lowest UR across both models\. On GPT\-4o\-mini, it yields aΔ\\DeltaVWA of 25\.4% andΔ\\DeltaOA of 12\.9% over the baseline, with UR reduced to 10\.81%\. Beam search and MCTS improve VWA by only 14\.4% and 12\.6% respectively and retain higher unverified ratios of 23\.79% and 26\.84%\. On Llama\-8B, all three strategies converge in VWA improvement at 25\.9%, 24\.6%, and 24\.1%, yet the greedy strategy still achieves the lowest UR at 9\.89%, compared to 12\.88% and 13\.54%\.

This advantage can be attributed to the greedy strategy’s mechanism of immediate verification feedback: a failed step triggers the instant delivery of the solver’s audit log and regeneration from the exact failure position, whereas beam search and MCTS distribute their search budget across parallel candidates\. Notably, MCTS achieves a higherΔ\\DeltaOA than beam search on GPT\-4o\-mini, at 11\.8% compared with 8\.8%\. This suggests that broader exploration improves final\-answer correctness, albeit at the expense of step\-level verifiability\.

### 3\.4Extended Application of LogicTrack on SFT

LogicTrack operates at inference time to improve step\-level verification of model reasoning\. We further extend it to the construction of fine\-tuning datasets, exploring its potential for producing self\-backtracking SFT data\. We first report overall performance after SFT, then present case studies that compare reasoning steps before and after backtracking to show the effectiveness of the fine\-tuning\.

LogicTrack\-SFT surpasses inference\-time LogicTrack on answer correctness\.As shown in Figure[4](https://arxiv.org/html/2609.21492#S3.F4)a, models fine\-tuned on LogicTrack backtracking trajectories achieve the highest OA across all models\. Compared with inference\-time LogicTrack, SFT improves OA from 56\.81% to 68\.08% on Llama\-8B, from 52\.75% to 63\.11% on Mistral\-7B, and from 70\.60% to 71\.16% on Qwen\-7B\. This suggests that training on solver\-verified trajectories with explicit backtrack tokens enables the model to internalize reasoning patterns that generalize beyond what inference\-time search alone achieves\.

SFT partially transfers step\-level verification capability, though inference\-time LogicTrack retains the advantage\.Figure[4](https://arxiv.org/html/2609.21492#S3.F4)b shows that SFT also improves step\-level quality: VWA increases over the base model from 32\.12% to 39\.24% on Llama\-8B, from 31\.86% to 34\.62% on Mistral\-7B, and from 35\.07% to 38\.46% on Qwen\-7B, showing that LogicTrack trajectories can transfer partial verification capability into the model’s intrinsic reasoning\. However, inference\-time LogicTrack still achieves the highest VWA, reaching 47\.17%, 40\.25%, and 49\.42% on the three models respectively\. This gap shows that keeping the solver in the loop at inference time provides stronger step\-level guarantees\.

Better performance than other state\-of\-the\-art tuning methods\.Monitoring reasoning trajectories remains an under\-explored area, and the work most closely related to ours is LogicReward\([Xu et al\. 2025b](https://arxiv.org/html/2609.21492#bib.bib43)\)\. LogicReward designs a solver\-based reward to score multiple responses for each problem and then uses the top responses to construct training data for SFT and DPO\. Table[3](https://arxiv.org/html/2609.21492#S4.T3)compares LogicReward with two variants of LogicTrack in terms of average performance across datasets\. The results show that our methods achieve stronger overall performance: inference\-time LogicTrack improves OA from 0\.4338 to 0\.5765 and VWA from 0\.2656 to 0\.4782, while LogicTrack\-SFT further achieves the best OA of 0\.6808\. The full dataset\-level results in Table[3](https://arxiv.org/html/2609.21492#S4.T3)also show that LogicTrack reduces UR from 0\.4089 to 0\.1863\. Since both LogicReward and LogicTrack\-SFT rely on SFT, this improvement suggests that LogicTrack constructs higher\-quality SFT training data\.

To isolate the contribution of adding explicit backtracking supervision to training samples, we trained LogicTrack\-SFT\-NoBT, a control model trained on data without backtracking traces\. As shown in Figure[5](https://arxiv.org/html/2609.21492#S4.F5), models fine\-tuned with LogicTrack backtracking trajectory data consistently achieve higher VWA and lower UR than LogicTrack\-SFT\-NoBT across all benchmarks\. These results confirm that the observed gains are not only a generic effect of SFT on correct trajectories\. The better performance of LogicTrack\-SFT\-BT over LogicTrack\-SFT\-NoBT demonstrates that incorporating backtracking trajectories provides additional supervision and can effectively enhance fine\-tuned model performance\.

## 4Related Work

Table 3:Performance comparison among LogicReward and LogicTrack\. Full comparisons are in Table 6 of Appendix C\.![Refer to caption](https://arxiv.org/html/2609.21492v1/misc/tst-cmp-nobt.png)Figure 5:Effectiveness of backtracking supervision in LogicTrack\-SFT on Qwen2\.5\-7B\. The VWA↑\\uparrowand UR↓\\downarrowcomparison across inference\-time LogicTrack, LogicTrack\-SFT\-BT, and LogicTrack\-SFT\-NoBT\.### 4\.1LLM Reasoning Capability Enhancement

Many methods have been proposed to improve LLM reasoning patterns, and they can be broadly categorized into training\-based and training\-free approaches\. Training\-free approaches improve reasoning quality during inference without updating parameters, including prompting strategies\([Wang et al\. 2022](https://arxiv.org/html/2609.21492#bib.bib28);[Wei et al\. 2022](https://arxiv.org/html/2609.21492#bib.bib29)\), search\-based methods\([Yang et al\. 2025a](https://arxiv.org/html/2609.21492#bib.bib11);[Yao et al\. 2023b](https://arxiv.org/html/2609.21492#bib.bib27)\), and external knowledge augmentation\([Peng et al\. 2023](https://arxiv.org/html/2609.21492#bib.bib19)\)\. Training\-based methods design rewards to identify high\-quality reasoning data for fine\-tuning\([Gulcehre et al\. 2023](https://arxiv.org/html/2609.21492#bib.bib21);[Zelikman et al\. 2022](https://arxiv.org/html/2609.21492#bib.bib20)\), or to incorporate these rewards into the training objective\([Luong et al\. 2024](https://arxiv.org/html/2609.21492#bib.bib22)\)\. Reward designs include outcome\-based and process\-level critics that attend to intermediate steps\([Yue et al\. 2026](https://arxiv.org/html/2609.21492#bib.bib25);[Calanzone et al\. 2024](https://arxiv.org/html/2609.21492#bib.bib26);[Lightman et al\. 2023](https://arxiv.org/html/2609.21492#bib.bib23);[Wang et al\. 2024](https://arxiv.org/html/2609.21492#bib.bib30)\)\. However, the criteria used to assess reasoning quality generally lack formal grounding\. Outcome\-based critics evaluate only final\-answer correctness, while process\-level critics rely on human annotations or LLM\-generated judgments, limiting verifiability and allowing subtle logical errors to go undetected\. To address this, we define intermediate\-step reasoning quality based on whether each step is logically supported by deterministic step\-level feedback from solver verification\.

### 4\.2LLM Reasoning Chain Verification

Recent work increasingly combines LLMs with verification mechanisms to improve soundness of model\-generated reasoning\([Cheng et al\. 2025](https://arxiv.org/html/2609.21492#bib.bib15);[Liu et al\. 2025](https://arxiv.org/html/2609.21492#bib.bib16)\)\. Existing approaches generally fall into two broad paradigms: formalizing LLM\-generated responses and verifying them with external solvers\([Olausson et al\. 2023](https://arxiv.org/html/2609.21492#bib.bib13);[Pan et al\. 2023](https://arxiv.org/html/2609.21492#bib.bib14)\), or treating LLMs themselves as symbolic provers\([Xu et al\. 2025a](https://arxiv.org/html/2609.21492#bib.bib39);[Xu et al\. 2024](https://arxiv.org/html/2609.21492#bib.bib12)\)\. This work focuses on external solver\-based approaches, as they provide a more explicit and controllable verification signal than self\-verification\. Within this paradigm,\([Zhang et al\. 2025](https://arxiv.org/html/2609.21492#bib.bib41);[Ranaldi et al\. 2025](https://arxiv.org/html/2609.21492#bib.bib42)\)discuss efficient auto\-formalization;\([Xu et al\. 2026](https://arxiv.org/html/2609.21492#bib.bib40)\)study adaptive solver selection;\([Quan et al\. 2024](https://arxiv.org/html/2609.21492#bib.bib18);[Quan et al\. 2025](https://arxiv.org/html/2609.21492#bib.bib17)\)use solver feedback for iterative refinement\. These works mainly target reasoning tasks close to formal representations, or highly structured domains such as mathematics and programming\([Ren et al\. 2025](https://arxiv.org/html/2609.21492#bib.bib24)\), where complete responses can be directly passed to a solver for verification\. Step\-level verification for general natural language reasoning remains under\-explored, as it requires independently formalizing and checking each intermediate chain rather than one\-off final answer verification\. In contrast, LogicTrack verifies the symbolic formalization induced from each NL reasoning step and backtracks at the first failed step, preventing local errors from propagating through the full reasoning chain\.

## 5Conclusion

We presented LogicTrack, a neuro\-symbolic framework for generation\-time auditing of LLM reasoning trajectories\. LogicTrack decomposes each step into explicit context, explanations, and conclusions\. Following standard practice in solver\-based verification, LogicTrack uses autoformalization as a modular interface that maps NL reasoning steps to solver\-executable logical specifications\. Finally, LogicTrack uses the Solver\-based Backtracking Reward \(SBR\) to combine premise fidelity with solver feedback for online backtracking and regeneration\. Across eight reasoning benchmarks and seven LLMs, LogicTrack substantially improves step\-level verifiability and generally preserves or improves final\-answer accuracy, with ablations showing that solver verification drives most of the gains\. LogicTrack backtracking traces also serve as useful supervision for fine\-tuning open\-source models, improving both final answer accuracy and verification performance over the base models\. Future work on autoformalization optimazation, verification reward variants, backtracking strategies, and fine\-tuning approaches that enable LLMs to internalize verification capabilities will be valuable\.

## References

- AI \(2024\)M\. AIThe llama 3 herd of models\.CoRRabs/2407\.21783\.Cited by:[1st item](https://arxiv.org/html/2609.21492#A2.I3.i1.p1.1),[§3\.1](https://arxiv.org/html/2609.21492#S3.SS1.SSS0.Px1.p2.1)\.
- Anet al\.\(2023\)S\. An, Z\. Ma, Z\. Lin, N\. Zheng, J\. Lou, and W\. ChenLearning from mistakes makes llm better reasoner\.arXiv preprint arXiv:2310\.20689\.Cited by:[§2\.3](https://arxiv.org/html/2609.21492#S2.SS3.p2.1)\.
- Calanzoneet al\.\(2024\)D\. Calanzone, S\. Teso, and A\. VergariLogically consistent language models via neuro\-symbolic integration\.arXiv preprint arXiv:2409\.13724\.Cited by:[§4\.1](https://arxiv.org/html/2609.21492#S4.SS1.p1.1)\.
- Camburuet al\.\(2018\)O\. Camburu, T\. Rocktäschel, T\. Lukasiewicz, and P\. BlunsomE\-snli: natural language inference with natural language explanations\.Advances in Neural Information Processing Systems31\.Cited by:[1st item](https://arxiv.org/html/2609.21492#A2.I1.i1.p1.1),[§3\.1](https://arxiv.org/html/2609.21492#S3.SS1.SSS0.Px1.p1.1)\.
- Chenget al\.\(2025\)F\. Cheng, H\. Li, F\. Liu, R\. van Rooij, K\. Zhang, and Z\. LinEmpowering llms with logical reasoning: a comprehensive survey\.InProceedings of the International Joint Conference on Artificial Intelligence,pp\. 10400–10408\.Cited by:[§4\.2](https://arxiv.org/html/2609.21492#S4.SS2.p1.1)\.
- Comaniciet al\.\(2025\)G\. Comanici, E\. Bieber, M\. Schaekermann, I\. Pasupat, N\. Sachdeva, I\. Dhillon, M\. Blistein, O\. Ram, D\. Zhang, E\. Rosen,et al\.Gemini 2\.5: pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabilities\.arXiv preprint arXiv:2507\.06261\.Cited by:[3rd item](https://arxiv.org/html/2609.21492#A2.I2.i3.p1.1),[§3\.1](https://arxiv.org/html/2609.21492#S3.SS1.SSS0.Px1.p2.1)\.
- Fenget al\.\(2025\)Y\. Feng, N\. Weir, K\. Bostrom, S\. Bayless, D\. Cassel, S\. Chaudhary, B\. Kiesl\-Reiter, and H\. RangwalaVeriCoT: neuro\-symbolic chain\-of\-thought validation via logical consistency checks\.arXiv preprint arXiv:2511\.04662\.Cited by:[§B\.1](https://arxiv.org/html/2609.21492#A2.SS1.p1.1),[§1](https://arxiv.org/html/2609.21492#S1.p3.1)\.
- Gaoet al\.\(2023\)L\. Gao, A\. Madaan, S\. Zhou, U\. Alon, P\. Liu, Y\. Yang, J\. Callan, and G\. NeubigPal: program\-aided language models\.InInternational conference on machine learning,pp\. 10764–10799\.Cited by:[§1](https://arxiv.org/html/2609.21492#S1.p1.1)\.
- Gulcehreet al\.\(2023\)C\. Gulcehre, T\. L\. Paine, S\. Srinivasan, K\. Konyushkova, L\. Weerts, A\. Sharma, A\. Siddhant, A\. Ahern, M\. Wang, C\. Gu,et al\.Reinforced self\-training \(rest\) for language modeling\.arXiv preprint arXiv:2308\.08998\.Cited by:[§4\.1](https://arxiv.org/html/2609.21492#S4.SS1.p1.1)\.
- Guoet al\.\(2025\)D\. Guo, D\. Yang, H\. Zhang, J\. Song, P\. Wang, Q\. Zhu, R\. Xu, R\. Zhang, S\. Ma, X\. Bi,et al\.Deepseek\-r1: incentivizing reasoning capability in llms via reinforcement learning\.arXiv preprint arXiv:2501\.12948\.Cited by:[§1](https://arxiv.org/html/2609.21492#S1.p1.1)\.
- Hanet al\.\(2024\)S\. Han, H\. Schoelkopf, Y\. Zhao, Z\. Qi, M\. Riddell, W\. Zhou, J\. Coady, D\. Peng, Y\. Qiao, L\. Benson,et al\.Folio: natural language reasoning with first\-order logic\.InProceedings of the 2024 Conference on Empirical Methods in Natural Language Processing,pp\. 22017–22031\.Cited by:[2nd item](https://arxiv.org/html/2609.21492#A2.I1.i2.p1.1),[§3\.1](https://arxiv.org/html/2609.21492#S3.SS1.SSS0.Px1.p1.1)\.
- Holzenbergeret al\.\(2020\)N\. Holzenberger, A\. Blair\-Stanek, and B\. Van DurmeA dataset for statutory reasoning in tax law entailment and question answering\.arXiv preprint arXiv:2005\.05257\.Cited by:[7th item](https://arxiv.org/html/2609.21492#A2.I1.i7.p1.1),[§B\.1](https://arxiv.org/html/2609.21492#A2.SS1.p1.1),[§3\.1](https://arxiv.org/html/2609.21492#S3.SS1.SSS0.Px1.p1.1)\.
- Huang and Chang \(2023\)J\. Huang and K\. C\. ChangTowards reasoning in large language models: a survey\.InFindings of the association for computational linguistics: ACL 2023,pp\. 1049–1065\.Cited by:[§1](https://arxiv.org/html/2609.21492#S1.p1.1)\.
- Hurstet al\.\(2024\)A\. Hurst, A\. Lerer, A\. P\. Goucher, A\. Perelman, A\. Ramesh, A\. Clark, A\. Ostrow, A\. Welihinda, A\. Hayes, A\. Radford,et al\.Gpt\-4o system card\.arXiv preprint arXiv:2410\.21276\.Cited by:[1st item](https://arxiv.org/html/2609.21492#A2.I2.i1.p1.1),[§3\.1](https://arxiv.org/html/2609.21492#S3.SS1.SSS0.Px1.p2.1)\.
- Jaechet al\.\(2024\)A\. Jaech, A\. Kalai, A\. Lerer, A\. Richardson, A\. El\-Kishky, A\. Low, A\. Helyar, A\. Madry, A\. Beutel, A\. Carney,et al\.Openai o1 system card\.arXiv preprint arXiv:2412\.16720\.Cited by:[§1](https://arxiv.org/html/2609.21492#S1.p1.1)\.
- Jianget al\.\(2023\)A\. Q\. Jiang, A\. Sablayrolles, A\. Mensch, C\. Bamford, D\. S\. Chaplot, D\. de las Casas, F\. Bressand, G\. Lengyel, G\. Lample, L\. Saulnier, L\. R\. Lavaud, M\. Lachaux, P\. Stock, T\. L\. Scao, T\. Lavril, T\. Wang, T\. Lacroix, and W\. E\. SayedMistral 7b\.External Links:2310\.06825,[Link](https://arxiv.org/abs/2310.06825)Cited by:[2nd item](https://arxiv.org/html/2609.21492#A2.I3.i2.p1.1),[§3\.1](https://arxiv.org/html/2609.21492#S3.SS1.SSS0.Px1.p2.1)\.
- Khalifaet al\.\(2023\)M\. Khalifa, L\. Logeswaran, M\. Lee, H\. Lee, and L\. WangGrace: discriminator\-guided chain\-of\-thought reasoning\.InFindings of the Association for Computational Linguistics: EMNLP 2023,pp\. 15299–15328\.Cited by:[§1](https://arxiv.org/html/2609.21492#S1.p2.1)\.
- Khotet al\.\(2020\)T\. Khot, P\. Clark, M\. Guerquin, P\. Jansen, and A\. SabharwalQasc: a dataset for question answering via sentence composition\.InProceedings of the AAAI Conference on Artificial Intelligence,Vol\.34,pp\. 8082–8090\.Cited by:[6th item](https://arxiv.org/html/2609.21492#A2.I1.i6.p1.1),[§3\.1](https://arxiv.org/html/2609.21492#S3.SS1.SSS0.Px1.p1.1)\.
- Lightmanet al\.\(2023\)H\. Lightman, V\. Kosaraju, Y\. Burda, H\. Edwards, B\. Baker, T\. Lee, J\. Leike, J\. Schulman, I\. Sutskever, and K\. CobbeLet’s verify step by step\.InThe twelfth international conference on learning representations,Cited by:[§1](https://arxiv.org/html/2609.21492#S1.p2.1),[§4\.1](https://arxiv.org/html/2609.21492#S4.SS1.p1.1)\.
- Liuet al\.\(2025\)H\. Liu, Z\. Fu, M\. Ding, R\. Ning, C\. Zhang, X\. Liu, and Y\. ZhangLogical reasoning in large language models: a survey\.CoRRabs/2502\.09100\.Cited by:[§4\.2](https://arxiv.org/html/2609.21492#S4.SS2.p1.1)\.
- Liuet al\.\(2020\)J\. Liu, L\. Cui, H\. Liu, D\. Huang, Y\. Wang, and Y\. ZhangLogiqa: a challenge dataset for machine reading comprehension with logical reasoning\.arXiv preprint arXiv:2007\.08124\.Cited by:[3rd item](https://arxiv.org/html/2609.21492#A2.I1.i3.p1.1),[§3\.1](https://arxiv.org/html/2609.21492#S3.SS1.SSS0.Px1.p1.1)\.
- Luet al\.\(2022\)P\. Lu, S\. Mishra, T\. Xia, L\. Qiu, K\. Chang, S\. Zhu, O\. Tafjord, P\. Clark, and A\. KalyanLearn to explain: multimodal reasoning via thought chains for science question answering\.Advances in neural information processing systems35,pp\. 2507–2521\.Cited by:[§1](https://arxiv.org/html/2609.21492#S1.p1.1)\.
- Luonget al\.\(2024\)T\. Q\. Luong, X\. Zhang, Z\. Jie, P\. Sun, X\. Jin, and H\. LiReft: reasoning with reinforced fine\-tuning\.arXiv preprint arXiv:2401\.08967\.Cited by:[§4\.1](https://arxiv.org/html/2609.21492#S4.SS1.p1.1)\.
- Olaussonet al\.\(2023\)T\. Olausson, A\. Gu, B\. Lipkin, C\. Zhang, A\. Solar\-Lezama, J\. Tenenbaum, and R\. LevyLINC: a neurosymbolic approach for logical reasoning by combining language models with first\-order logic provers\.InProceedings of the 2023 Conference on Empirical Methods in Natural Language Processing,pp\. 5153–5176\.Cited by:[§1](https://arxiv.org/html/2609.21492#S1.p3.1),[§4\.2](https://arxiv.org/html/2609.21492#S4.SS2.p1.1)\.
- Panet al\.\(2023\)L\. Pan, A\. Albalak, X\. Wang, and W\. WangLogic\-LM: empowering large language models with symbolic solvers for faithful logical reasoning\.InFindings of the Association for Computational Linguistics: EMNLP 2023,pp\. 3806–3824\.Cited by:[§1](https://arxiv.org/html/2609.21492#S1.p3.1),[§4\.2](https://arxiv.org/html/2609.21492#S4.SS2.p1.1)\.
- Penget al\.\(2023\)B\. Peng, M\. Galley, P\. He, H\. Cheng, Y\. Xie, Y\. Hu, Q\. Huang, L\. Liden, Z\. Yu, W\. Chen,et al\.Check your facts and try again: improving large language models with external knowledge and automated feedback\.arXiv preprint arXiv:2302\.12813\.Cited by:[§4\.1](https://arxiv.org/html/2609.21492#S4.SS1.p1.1)\.
- Quanet al\.\(2024\)X\. Quan, M\. Valentino, L\. A\. Dennis, and A\. FreitasVerification and refinement of natural language explanations through LLM\-symbolic theorem proving\.InProceedings of the Conference on Empirical Methods in Natural Language Processing,pp\. 2933–2958\.Cited by:[§1](https://arxiv.org/html/2609.21492#S1.p3.1),[§4\.2](https://arxiv.org/html/2609.21492#S4.SS2.p1.1)\.
- Quanet al\.\(2025\)X\. Quan, M\. Valentino, L\. A\. Dennis, and A\. FreitasFaithful and robust LLM\-driven theorem proving for NLI explanations\.InProceedings of the Annual Meeting of the Association for Computational Linguistics,pp\. 17734–17755\.Cited by:[§4\.2](https://arxiv.org/html/2609.21492#S4.SS2.p1.1)\.
- Ranaldiet al\.\(2025\)L\. Ranaldi, M\. Valentino, and A\. FreitasImproving chain\-of\-thought reasoning via quasi\-symbolic abstractions\.InProceedings of the 63rd Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\),pp\. 17222–17240\.Cited by:[§4\.2](https://arxiv.org/html/2609.21492#S4.SS2.p1.1)\.
- Renet al\.\(2025\)Z\. Ren, Z\. Shao, J\. Song, H\. Xin, H\. Wang, W\. Zhao, L\. Zhang, Z\. Fu, Q\. Zhu, D\. Yang,et al\.Deepseek\-prover\-v2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition\.arXiv preprint arXiv:2504\.21801\.Cited by:[§4\.2](https://arxiv.org/html/2609.21492#S4.SS2.p1.1)\.
- Saparov and He \(2023\)A\. Saparov and H\. HeLanguage models are greedy reasoners: a systematic formal analysis of chain\-of\-thought\.InProceedings of the International Conference on Learning Representations,Cited by:[4th item](https://arxiv.org/html/2609.21492#A2.I1.i4.p1.1),[§3\.1](https://arxiv.org/html/2609.21492#S3.SS1.SSS0.Px1.p1.1)\.
- SemEval\-2026 Team \(2026\)SemEval\-2026 TeamSemEval\-2026 task 11: disentangling content and formal reasoning in large language models\.Note:https://sites\.google\.com/view/semeval\-2026\-task\-11Accessed: 2026\-03\-28Cited by:[8th item](https://arxiv.org/html/2609.21492#A2.I1.i8.p1.1),[§B\.1](https://arxiv.org/html/2609.21492#A2.SS1.p1.1),[§3\.1](https://arxiv.org/html/2609.21492#S3.SS1.SSS0.Px1.p1.1)\.
- Singhet al\.\(2025\)A\. Singh, A\. Fry, A\. Perelman, A\. Tart, A\. Ganesh, A\. El\-Kishky, A\. McLaughlin, A\. Low, A\. Ostrow, A\. Ananthram,et al\.Openai gpt\-5 system card\.arXiv preprint arXiv:2601\.03267\.Cited by:[2nd item](https://arxiv.org/html/2609.21492#A2.I2.i2.p1.1),[§3\.1](https://arxiv.org/html/2609.21492#S3.SS1.SSS0.Px1.p2.1)\.
- Singhet al\.\(2026\)V\. Singh, D\. Cassel, N\. Weir, N\. Feng, and S\. BaylessVERGE: formal refinement and guidance engine for verifiable llm reasoning\.arXiv preprint arXiv:2601\.20055\.Cited by:[§1](https://arxiv.org/html/2609.21492#S1.p3.1)\.
- Tafjordet al\.\(2021\)O\. Tafjord, B\. Dalvi, and P\. ClarkProofwriter: generating implications, proofs, and abductive statements over natural language\.InFindings of the Association for Computational Linguistics: ACL\-IJCNLP 2021,pp\. 3621–3634\.Cited by:[5th item](https://arxiv.org/html/2609.21492#A2.I1.i5.p1.1),[§3\.1](https://arxiv.org/html/2609.21492#S3.SS1.SSS0.Px1.p1.1)\.
- Turpinet al\.\(2023\)M\. Turpin, J\. Michael, E\. Perez, and S\. BowmanLanguage models don’t always say what they think: unfaithful explanations in chain\-of\-thought prompting\.Advances in Neural Information Processing Systems36,pp\. 74952–74965\.Cited by:[§1](https://arxiv.org/html/2609.21492#S1.p1.1)\.
- Wanget al\.\(2024\)P\. Wang, L\. Li, Z\. Shao, R\. Xu, D\. Dai, Y\. Li, D\. Chen, Y\. Wu, and Z\. SuiMath\-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:[§4\.1](https://arxiv.org/html/2609.21492#S4.SS1.p1.1)\.
- Wanget al\.\(2022\)X\. Wang, J\. Wei, D\. Schuurmans, Q\. Le, E\. Chi, S\. Narang, A\. Chowdhery, and D\. ZhouSelf\-consistency improves chain of thought reasoning in language models\.arXiv preprint arXiv:2203\.11171\.Cited by:[§4\.1](https://arxiv.org/html/2609.21492#S4.SS1.p1.1)\.
- Weiet al\.\(2022\)J\. Wei, X\. Wang, D\. Schuurmans, M\. Bosma, F\. Xia, E\. Chi, Q\. V\. Le, D\. Zhou,et al\.Chain\-of\-thought prompting elicits reasoning in large language models\.Advances in neural information processing systems35,pp\. 24824–24837\.Cited by:[§4\.1](https://arxiv.org/html/2609.21492#S4.SS1.p1.1)\.
- Xieet al\.\(2023\)Y\. Xie, K\. Kawaguchi, Y\. Zhao, J\. X\. Zhao, M\. Kan, J\. He, and M\. XieSelf\-evaluation guided beam search for reasoning\.Advances in Neural Information Processing Systems36,pp\. 41618–41650\.Cited by:[§1](https://arxiv.org/html/2609.21492#S1.p2.1)\.
- Xuet al\.\(2025a\)J\. Xu, H\. Fei, M\. Luo, Q\. Liu, L\. Pan, W\. Y\. Wang, P\. Nakov, M\. Lee, and W\. HsuAristotle: mastering logical reasoning with a logic\-complete decompose\-search\-resolve framework\.InProceedings of the 63rd Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\),pp\. 3052–3075\.Cited by:[§4\.2](https://arxiv.org/html/2609.21492#S4.SS2.p1.1)\.
- Xuet al\.\(2024\)J\. Xu, H\. Fei, L\. Pan, Q\. Liu, M\. Lee, and W\. HsuFaithful logical reasoning via symbolic chain\-of\-thought\.InProceedings of the Annual Meeting of the Association for Computational Linguistics,pp\. 13326–13365\.Cited by:[§1](https://arxiv.org/html/2609.21492#S1.p1.1),[§4\.2](https://arxiv.org/html/2609.21492#S4.SS2.p1.1)\.
- Xuet al\.\(2025b\)J\. Xu, H\. Fei, H\. Zhou, X\. Quan, Q\. Huang, S\. Wu, W\. Y\. Wang, M\. Lee, and W\. HsuLogicReward: incentivizing llm reasoning via step\-wise logical supervision\.arXiv preprint arXiv:2512\.18196\.Cited by:[3rd item](https://arxiv.org/html/2609.21492#A2.I1.i3.p1.1),[§B\.1](https://arxiv.org/html/2609.21492#A2.SS1.p1.1),[§B\.2](https://arxiv.org/html/2609.21492#A2.SS2.SSS0.Px3.p1.1),[§C\.1](https://arxiv.org/html/2609.21492#A3.SS1.p1.1),[§1](https://arxiv.org/html/2609.21492#S1.p3.1),[§3\.1](https://arxiv.org/html/2609.21492#S3.SS1.SSS0.Px1.p2.1),[§3\.4](https://arxiv.org/html/2609.21492#S3.SS4.p4.1),[Table 3](https://arxiv.org/html/2609.21492#S4.T3.1.1.2)\.
- Xuet al\.\(2026\)L\. Xu, P\. Beckmann, M\. Valentino, and A\. FreitasAdaptive llm\-symbolic reasoning via dynamic logical solver composition\.InProceedings of the 19th Conference of the European Chapter of the Association for Computational Linguistics \(Volume 1: Long Papers\),pp\. 1187–1208\.Cited by:[§4\.2](https://arxiv.org/html/2609.21492#S4.SS2.p1.1)\.
- Yanget al\.\(2024\)A\. Yang, B\. Zhang, B\. Hui, B\. Gao, B\. Yu, C\. Li, D\. Liu, J\. Tu, J\. Zhou, J\. Lin,et al\.Qwen2\. 5\-math technical report: toward mathematical expert model via self\-improvement\.arXiv preprint arXiv:2409\.12122\.Cited by:[3rd item](https://arxiv.org/html/2609.21492#A2.I3.i3.p1.1),[4th item](https://arxiv.org/html/2609.21492#A2.I3.i4.p1.1),[§3\.1](https://arxiv.org/html/2609.21492#S3.SS1.SSS0.Px1.p2.1)\.
- Yanget al\.\(2025a\)X\. Yang, X\. Zhu, W\. Wei, D\. Zhang, J\. Shao, Z\. Zhou, L\. Guo, and Y\. LiStep back to leap forward: self\-backtracking for boosting reasoning of language models\.arXiv preprint arXiv:2502\.04404\.Cited by:[§2\.3](https://arxiv.org/html/2609.21492#S2.SS3.p2.1),[§4\.1](https://arxiv.org/html/2609.21492#S4.SS1.p1.1)\.
- Yanget al\.\(2025b\)X\. Yang, X\. Zhu, W\. Wei, D\. Zhang, J\. Shao, Z\. Zhou, L\. Guo, and Y\. LiStep back to leap forward: self\-backtracking for boosting reasoning of language models\.arXiv preprint arXiv:2502\.04404\.Cited by:[§1](https://arxiv.org/html/2609.21492#S1.p6.1)\.
- Yaoet al\.\(2023a\)S\. Yao, D\. Yu, J\. Zhao, I\. Shafran, T\. Griffiths, Y\. Cao, and K\. NarasimhanTree of thoughts: deliberate problem solving with large language models\.Advances in neural information processing systems36,pp\. 11809–11822\.Cited by:[§1](https://arxiv.org/html/2609.21492#S1.p2.1)\.
- Yaoet al\.\(2023b\)S\. Yao, D\. Yu, J\. Zhao, I\. Shafran, T\. Griffiths, Y\. Cao, and K\. NarasimhanTree of thoughts: deliberate problem solving with large language models\.Advances in neural information processing systems36,pp\. 11809–11822\.Cited by:[§4\.1](https://arxiv.org/html/2609.21492#S4.SS1.p1.1)\.
- Yeet al\.\(2024\)T\. Ye, Z\. Xu, Y\. Li, and Z\. Allen\-ZhuPhysics of language models: part 2\.2, how to learn from mistakes on grade\-school math problems\.arXiv preprint arXiv:2408\.16293\.Cited by:[§2\.3](https://arxiv.org/html/2609.21492#S2.SS3.p2.1)\.
- Yueet al\.\(2026\)C\. Yue, C\. Dong, Y\. Gao, H\. He, J\. Chai, W\. Lin, and G\. YinPromoting efficient reasoning with verifiable stepwise reward\.InProceedings of the AAAI Conference on Artificial Intelligence,Vol\.40,pp\. 34530–34538\.Cited by:[§4\.1](https://arxiv.org/html/2609.21492#S4.SS1.p1.1)\.
- Zelikmanet al\.\(2022\)E\. Zelikman, Y\. Wu, J\. Mu, and N\. GoodmanStar: bootstrapping reasoning with reasoning\.Advances in Neural Information Processing Systems35,pp\. 15476–15488\.Cited by:[§4\.1](https://arxiv.org/html/2609.21492#S4.SS1.p1.1)\.
- Zhanget al\.\(2025\)L\. Zhang, M\. Valentino, and A\. FreitasMASA: llm\-driven multi\-agent systems for autoformalization\.InProceedings of the 2025 Conference on Empirical Methods in Natural Language Processing: System Demonstrations,pp\. 615–624\.Cited by:[§4\.2](https://arxiv.org/html/2609.21492#S4.SS2.p1.1)\.

## Appendix AAppendix A: Methods Implementation

### A\.1Backtracking Search Strategies

This section provides additional implementation details for the search\-strategy ablation in Table[2](https://arxiv.org/html/2609.21492#S3.T2)\(b\)\. We compare three variants: the default greedy backtracking search used in the main experiments, beam search, and Monte Carlo Tree Search \(MCTS\)\.

#### Default Search

The default search is the greedy backtracking strategy used throughout the main experiments and the implementation is described in Section[2\.2](https://arxiv.org/html/2609.21492#S2.SS2)\. Its step\-level acceptance threshold is set toθstep=0\.8\\theta\_\{\\mathrm\{step\}\}=0\.8, the running\-average threshold is set toθavg=0\.5\\theta\_\{\\mathrm\{avg\}\}=0\.5\. The maximum number of regeneration attempts per step position isk=2k=2\. If allkkattempts fail, the candidate with the highestSBR\\mathrm\{SBR\}is force\-forwarded to guarantee forward progress\.

#### Beam Search

Beam search maintains a frontier ofBBpartial reasoning paths and expands all of them in parallel at each layer\. At each layer, every frontier path contributes up tok=2k=2continuation branches: if the path carries a pending tail from a prior generation, its leading provisional step is consumed as one free branch; the remaining slots are filled by fresh LLM completions conditioned on the current verified prefix\. All verification tasks are dispatched concurrently\. After verification, nodes withSBR⁡\(st\)<0\.75\\mathrm\{SBR\}\(s\_\{t\}\)<0\.75are pruned; the top\-BBsurvivors ranked by path\-averageSBR\\mathrm\{SBR\}advance to the next layer\. If all candidates are pruned, the best low\-reward node is reactivated to guarantee forward progress\. The search terminates as soon as the top frontier node yields a complete reasoning chain; otherwise the best node found is returned\.

#### Monte Carlo Tree Search

We follow the standard MCTS framework, repeating four stages each iteration\. During selection, the algorithm traverses from the root by choosing at each node the child with the highest UCB score, which balances the mean backpropagatedSBR\\mathrm\{SBR\}against an exploration bonus, until it reaches a node with fewer thankkchildren\. During expansion, up tokkfresh LLM completions are generated from the selected node\. The first stepsts\_\{t\}of each completion is verified and attached as a new child\. A child is marked terminal ifSBR⁡\(st\)=0\\mathrm\{SBR\}\(s\_\{t\}\)=0, if the reasoning chain is complete, or if a depth limit is reached\. During rollout, each non\-terminal child whoseSBR⁡\(st\)≥θ\\mathrm\{SBR\}\(s\_\{t\}\)\\geq\\thetais extended by consuming the remaining provisional steps from the same generation, verifying each in turn without additional LLM calls, until the chain terminates or a step falls belowθ\\theta\. During backpropagation, the path\-averageSBR\\mathrm\{SBR\}of the reached leaf is propagated back to the root, updating each ancestor’s statistics\. After a fixed number of iterations the best complete leaf is returned, or, if none exists, the best leaf overall\.

### A\.2Backtracking SFT

We build the SFT data from backtracking traces produced by LogicTrack\. For each training example, we keep only cases whose final answer is correct and whose reasoning steps pass both syntactic and semantic verification\. From each trace, we extract the verified path𝐬\+=\(s1\+,…,sn\+\)\\mathbf\{s\}^\{\+\}=\(s\_\{1\}^\{\+\},\\ldots,s\_\{n\}^\{\+\}\)fromfinal\_pathand the rejected steps\{sk−\}\\\{s\_\{k\}^\{\-\}\\\}collected at backtracking points\. A rejected step at positionkkis kept only when its prefix up to stepk−1k\-1matches the verified path\. This keeps the error local and avoids trajectories that have already diverged earlier\.

We then construct three kinds of training trajectories:

- •Single backtracking correction\.One wrong step is followed by a dedicated backtracking token and then the verified continuation: s1\+⋯sk−1\+sk−<backtrack\>sk\+⋯sn\+y^\.s\_\{1\}^\{\+\}\\cdots s\_\{k\-1\}^\{\+\}\\;\\;s\_\{k\}^\{\-\}\\;\\;\\texttt\{<backtrack\>\}\\;\\;s\_\{k\}^\{\+\}\\cdots s\_\{n\}^\{\+\}\\;\\;\\boxed\{\\hat\{y\}\}\.
- •Multiple backtracking corrections\.These trajectories contain two or more corrections at different step positions\. We prefer cases whose wrong continuation ends with an incorrect final answer\.
- •Clean correct trajectories\.These trajectories contain all verified steps and provide positive examples\.

During fine\-tuning, we add<backtrack\>as the new vocabulary item\. The model learns to emit this token when a step is wrong and then continue with a corrected path, without relying on an external verifier at inference time\. The final training set contains∼~\\sim6,000 samples across the three trajectory types\. We fine\-tune three large language models on the constructed SFT dataset: Qwen2\.5\-7B\-Instruct, Mistral\-7B\-Instruct\-v0\.3, and Llama\-3\.1\-8B\-Instruct\. We use LoRA supervised fine\-tuning for 2 epochs with rank 32 and scaling factor 64\. Training uses bfloat16 and AdamW \(adamw\_torch\) with a learning rate of3×10−53\\times 10^\{\-5\}, a linear scheduler, warmup ratio 0\.05, and gradient clipping with maximum norm 0\.3\. The per\-device batch size is 2 and the effective batch size is 16\. We also enable gradient checkpointing and save checkpoints every 50 steps\.

## Appendix BAppendix B: Experimental Settings

### B\.1Datasets

We evaluate on eight reasoning benchmarks\. For e\-SNLI, FOLIO, LogiQA, ProntoQA, ProofWriter, and QASC, we adopt the processed releases used in LogicReward\([Xu et al\. 2025b](https://arxiv.org/html/2609.21492#bib.bib43)\)\. We then resplit their released ‘data\.jsonl‘ into training and test subsets with the ratio of 4 : 1\. All fine\-tuning experiments are based on the training dataset\. For SemEval\([SemEval\-2026 Team 2026](https://arxiv.org/html/2609.21492#bib.bib8)\), Task 2 is used for testing and the English portion of Task 4 is used for training\. For SARA\([Holzenberger et al\. 2020](https://arxiv.org/html/2609.21492#bib.bib6)\), we follow the instructions from\([Feng et al\. 2025](https://arxiv.org/html/2609.21492#bib.bib44)\)and use the instances from SARA Entailment in the testing stage only\. We briefly summarize the benchmarks below\.

- •e\-SNLI\([Camburu et al\. 2018](https://arxiv.org/html/2609.21492#bib.bib1)\)extends SNLI with human\-annotated natural language explanations for premise–hypothesis pairs\.
- •FOLIO\([Han et al\. 2024](https://arxiv.org/html/2609.21492#bib.bib2)\)is a human\-annotated benchmark for natural language reasoning with accompanying first\-order logic annotations that are automatically verified by an inference engine\.
- •LogiQA\([Liu et al\. 2020](https://arxiv.org/html/2609.21492#bib.bib3)\)is originally a multiple\-choice reading comprehension benchmark for logical reasoning over short passages\. We use the preprocessed version from\([Xu et al\. 2025b](https://arxiv.org/html/2609.21492#bib.bib43)\)\.
- •ProntoQA\([Saparov and He 2023](https://arxiv.org/html/2609.21492#bib.bib7)\)is a synthetic question answering benchmark in which each example is generated from a synthetic world model represented in first\-order logic, providing a controlled setting for analyzing multi\-step deduction\.
- •ProofWriter\([Tafjord et al\. 2021](https://arxiv.org/html/2609.21492#bib.bib4)\)is a synthetic benchmark over natural\-language theories of facts and rules, with associated questions and proofs at different reasoning depths\.
- •QASC\([Khot et al\. 2020](https://arxiv.org/html/2609.21492#bib.bib5)\)is an 8\-way multiple\-choice science question answering benchmark for question answering via sentence composition\.
- •SARA\([Holzenberger et al\. 2020](https://arxiv.org/html/2609.21492#bib.bib6)\)is a benchmark for statutory reasoning in tax law, with entailment and question answering tasks\.
- •SemEval\([SemEval\-2026 Team 2026](https://arxiv.org/html/2609.21492#bib.bib8)\)refers to SemEval\-2026 Task 11 on disentangling content from formal reasoning in multilingual syllogistic arguments\. We use Task 2 for testing and the English portion of Task 4 for training, and in both cases use the binary validity labels\.

### B\.2Models

Our experiments cover seven models with diverse architectures and scales\.

#### Proprietary models\.

- •GPT\-4o\-mini\([Hurst et al\. 2024](https://arxiv.org/html/2609.21492#bib.bib32)\)is a member of the GPT\-4o family that offers strong reasoning performance at low inference cost\.
- •GPT\-5\-nano\([Singh et al\. 2025](https://arxiv.org/html/2609.21492#bib.bib33)\)is the smallest model in the GPT\-5 family and is designed for fast and lightweight inference\.
- •Gemini\-2\.5\-Flash\-Lite\([Comanici et al\. 2025](https://arxiv.org/html/2609.21492#bib.bib31)\)is a lightweight model from the Gemini 2\.5 family that balances efficiency with strong reasoning ability\.

#### Open weight models\.

- •Llama\-3\.1\-8B\-Instruct\([AI 2024](https://arxiv.org/html/2609.21492#bib.bib36)\)is an instruction\-tuned model with 8B parameters from Meta’s Llama 3\.1 family\.
- •Mistral\-7B\-Instruct\-v0\.3\([Jiang et al\. 2023](https://arxiv.org/html/2609.21492#bib.bib38)\)is an instruction\-tuned model with 7B parameters from Mistral AI with strong performance relative to its size\.
- •Qwen2\.5\-7B\-Instruct\([Yang et al\. 2024](https://arxiv.org/html/2609.21492#bib.bib37)\)is an instruction\-tuned model with 7B parameters from the Qwen2\.5 family\.
- •Qwen2\.5\-14B\-Instruct\([Yang et al\. 2024](https://arxiv.org/html/2609.21492#bib.bib37)\)is an instruction\-tuned model with 14B parameters from the same Qwen2\.5 family with stronger reasoning capacity at higher computing cost\.

#### Implementations\.

For all models, the temperature is set to 0\.7 and the maximum generation length is set to 10240 tokens when answering questions\. For proprietary models, experiments are performed via corresponding OpenAI APIs111https://developers\.openai\.com/api/docsand Gemini APIs222https://ai\.google\.dev/gemini\-api/docs\. For open\-weight models, all testing and fine\-tuning experiments are conducted on NVIDIA A100 GPUs \(40 GB or 80 GB\) or equivalent GPUs, using PyTorch 2\.8 and Python 3\.12\. The BASE method in this paper is the zero\-shot strategy that uses the Reasoning Prompt described in Appendix D\. Our LogicTrack method uses the same reasoning prompt as the baseline and applies our monitoring mechanism during answer generation\. For formal verification, we use the ‘gpt\-4o\-min’ as the autoformalizer backend and Z3 SMT solver as the solver backend\. The automatic formalizer and fidelity judge in LogicTrack are both implemented with gpt\-4o\-mini\. Evaluating the intermediate reasoning processes of LLMs remains an underexplored area\. To the best of our knowledge, LogicReward\([Xu et al\. 2025b](https://arxiv.org/html/2609.21492#bib.bib43)\)is the only relevant prior work with open\-source code\. We select it as baseline and the performance comparison between LogicTrack and LogicReward is presented in Appendix C\.

### B\.3Metric Definitions

For each problemxx, letTxT\_\{x\}be the number of reasoning steps andKxK\_\{x\}the number of verified steps, giving the per\-problem verification ratioρx=Kx/Tx\\rho\_\{x\}=K\_\{x\}/T\_\{x\}\.

Outcome Accuracy \(OA\) is the fraction of examples with correct final answers\. Verified Ratio \(VR\) is the dataset\-average verification ratio1N​∑xρx\\tfrac\{1\}\{N\}\\sum\_\{x\}\\rho\_\{x\}, Unverified Ratio \(UR\) is the mean fraction of unverified steps1N​∑x\(1−ρx\)\\tfrac\{1\}\{N\}\\sum\_\{x\}\(1\-\\rho\_\{x\}\)\.

Verified Utility \(VU\) is the fraction of all examples for which the final answer is correct and the entire reasoning trajectory is verified:VU=1N∑x=1N𝟏\[y^x=yx\]⋅𝟏\[ρx=1\]\\mathrm\{VU\}=\\frac\{1\}\{N\}\\sum\_\{x=1\}^\{N\}\\mathbf\{1\}\[\\hat\{y\}\_\{x\}=y\_\{x\}\]\\cdot\\mathbf\{1\}\[\\rho\_\{x\}=1\]\.

Verification\-Weighted Accuracy \(VWA\) is defined as1N∑x=1Nρx⋅𝟏\[y^x=yx\]\\tfrac\{1\}\{N\}\\sum\_\{x=1\}^\{N\}\\rho\_\{x\}\\cdot\\mathbf\{1\}\[\\hat\{y\}\_\{x\}=y\_\{x\}\], it weights each correct prediction by its per\-problem verification ratio\.

## Appendix CAppendix C: Results

### C\.1More Results of LogicTrack Performance

Table[4](https://arxiv.org/html/2609.21492#A3.T4)reports the average OA and VU of the base models and LogicTrack across all seven models\. Table[5](https://arxiv.org/html/2609.21492#A3.T5)reports the performance of the three LogicTrack\-SFT models on each dataset\. We further compare LogicTrack with LogicReward\([Xu et al\. 2025b](https://arxiv.org/html/2609.21492#bib.bib43)\)on Llama\-8B\. LogicReward is based on their released model after SFT and DPO fine\-tuning333https://huggingface\.co/Aiden0526/LogicReward\-Llama3\.1\-8B\. Table[6](https://arxiv.org/html/2609.21492#A3.T6)compares LogicReward, LogicTrack, and LogicTrack\-SFT at the dataset level\.

Table 4:Overall performance for all models averaged across eight benchmarks under BASE and LogicTrack\. Here OA and VU correspond to the coordinates used in Figure[3](https://arxiv.org/html/2609.21492#S3.F3)Table 5:Performance of LogicTrack\-SFT across different models and datasets\. We report OA↑\\uparrow, VWA↑\\uparrow, and UR↓\\downarrow\.Table 6:Dataset\-level comparison among LogicReward, LogicTrack, and LogicTrack\-SFT on Llama\-3\.1\-8B\. We report OA↑\\uparrow, VWA↑\\uparrow, and UR↓\\downarrow\.
### C\.2Backtracking Case Study in LogicTrack\-SFT

Figure[6](https://arxiv.org/html/2609.21492#A3.F6)presents two representative examples of self\-backtracking from LogicTrack\-SFT \(Qwen2\.5\-7B\)\. In Example 1, the model makes a non\-sequitur by deriving an unrelated property instead of continuing the type chain\. After backtracking, it completes the correct deduction\. Example 2 shows an irrelevant derivation in which the model explores an off\-topic property\. The model triggers backtracking in these cases and, after backtracking, follows the targeted reasoning path\. These cases highlight LogicTrack\-SFT’s internalized backtracking ability and show how it recovers from non\-sequitur inferences and unproductive reasoning paths in a way that is consistent with the solver\-guided corrections in LogicTrack training trajectories\.

Example 1: Non\-sequitur inference\.Premises:Alex is a tumpus⇒\\Rightarrowjompus⇒\\Rightarrowdumpus⇒\\Rightarrowzumpus⇒\\Rightarrowyumpus; each yumpus is not cold\.Query:Alex is cold\. Answer label:False

Before<backtrack\>Step 4:\{C4,E4,q4\}\\\{C\_\{4\},E\_\{4\},q\_\{4\}\\\}, whereq4:q\_\{4\}:“Alex is not a wumpus \(since zumpuses are dull and cannot be cold\)\.” ————–×\\timesNon\-sequitur: “dull” is unrelated to “cold”; the chain must reach yumpus\.

After<backtrack\>Step 4:“Alex is a yumpus \(every zumpus is a yumpus\)\.” Step 5:“Each yumpus is not cold⇒\\RightarrowAlex is not cold\.” ————–✓\\checkmarkAnswer:False\.

Example 2: Irrelevant derivation\.Premises:Sally is a yumpus⇒\\Rightarrowzumpus⇒\\Rightarrownumpus; each numpus is not bitter\.Query:Sally is not bitter\. Answer labelTrue

Before<backtrack\>Step 1:\{C1,E1,q1\}\\\{C\_\{1\},E\_\{1\},q\_\{1\}\\\}, whereq1:q\_\{1\}:“Sally is a yumpus, which means she is not opaque\. But we need to determine if she is bitter or not\.” ————–×\\timesDerives irrelevant property \(“not opaque”\)\.

After<backtrack\>Step 1:“Sally is a yumpus⇒\\Rightarrowzumpus⇒\\Rightarrownumpus\.” Step 2:“Each numpus is not bitter⇒\\RightarrowSally is not bitter\.” ————–✓\\checkmarkAnswer:True\.

Figure 6:Self\-backtracking Examples of LogicTrack\-SFT\. Each pair contrasts the flawed step with the corrected continuation\.The examples above displayed the traces in the simplified way\. Below displays full settings of Example 2 in Figure[6](https://arxiv.org/html/2609.21492#A3.F6)\. It shows the original flawed step that triggers<backtrack\>and the regenerated continuation\.

#### Original Given premises\.

P=’ Every yumpus is not opaque; Yumpuses are zumpuses; Zumpuses are nervous; Every zumpus is a tumpus; Each tumpus is not large; Tumpuses are impuses; Impuses are temperate; Impuses are numpuses; Every wumpus is bitter; Each numpus is not bitter; Numpuses are vumpuses; Every vumpus is not kind; Vumpuses are rompuses; Rompuses are brown; Rompuses are jompuses; Every jompus is wooden; Every jompus is a dumpus; Sally is a yumpus\.’Query:Sally is not bitter\.Answer label:True

Model generated answer with backtracking is as follows\.

#### Initial flawed step and backtracking trigger\.

1Step1:

2\#\#Premises:\#\#Sallyisayumpus;Everyyumpusisnotopaque;Yumpusesarezumpuses;Zumpusesarenervous;Everyzumpusisatumpus;Eachtumpusisnotlarge;Tumpusesareimpuses;Impusesaretemperate;Impusesarenumpuses;Everywumpusisbitter;Eachnumpusisnotbitter;Numpusesarevumpuses;Everyvumpusisnotkind;Vumpusesarerompuses;Rompusesarebrown;Rompusesarejompuses;Everyjompusiswooden;Everyjompusisadumpus\.

3\#\#DerivedFact:\#\#Sallyisayumpus,whichmeanssheisnotopaque\.However,weneedtodetermineifsheisbitterornot\.

4<backtrack\>

5Step1:

6\#\#Premises:\#\#Sallyisayumpus;Everyyumpusisnotopaque;Yumpusesarezumpuses;Zumpusesarenervous;Everyzumpusisatumpus;Eachtumpusisnotlarge;Tumpusesareimpuses;Impusesaretemperate;Impusesarenumpuses;Everywumpusisbitter;Eachnumpusisnotbitter;Numpusesarevumpuses;Everyvumpusisnotkind;Vumpusesarerompuses;Rompusesarebrown;Rompusesarejompuses;Everyjompusiswooden;Everyjompusisadumpus\.

7\#\#DerivedFact:\#\#Sallyisayumpus\.Sinceyumpusesarezumpusesandzumpusesarenumpuses,wecanconcludethatSallyisalsoanumpus\.

8Step2:

9\#\#Premises:\#\#Sallyisanumpus;Eachnumpusisnotbitter\.

10\#\#DerivedFact:\#\#Sallyisnotbitter\.

11Step3:

12\#\#Premises:\#\#Thehypothesisstates:Sallyisnotbitter;WehaveestablishedthatSallyisnotbitter\.

13\#\#DerivedFact:\#\#Thehypothesismatchesthederivedfactabove\.Therefore,theclaimistrue\.Thefinalansweris\\boxed\{True\}\.

## Appendix DAppendix D: Prompt Templates

This section includes the prompt templates used in our experiments, including the reasoning prompt, the consistency check prompt, and the answer extraction procedure\.

#### Reasoning Prompt

Given a samplexx, the reasoning model receives a system message instructing it to reason step\-by\-step in the structured format described in §[2\.1](https://arxiv.org/html/2609.21492#S2.SS1.SSS0.Px1), followed by a user message containing the premisesPP, queryQQ, and a dataset\-specific answer instruction\. The system prompt includes an in\-context demonstration and enforces the three\-part step format \(Premises, Explanation, Derived Fact\)\.

System Prompt for Step\-by\-Step Reasoning[⬇](data:text/plain;base64,WW91IGFyZSBhIG1ldGljdWxvdXMgbG9naWNpYW4uIFJlYWQgdGhlIHVzZXIncyBnaXZlbiBwcmVtaXNlIGFuZCBoeXBvdGhlc2lzIGNhcmVmdWxseSwgdGhlbiByZWFzb24gc3RlcCBieSBzdGVwIGV4cGxpY2l0bHkgaW4gYSBOYXR1cmFsIExhbmd1YWdlIEluZmVyZW5jZSAoTkxJKSBzdHlsZSwgYW5kIGNvbmNsdWRlIHdpdGggXGJveGVke0xBQkVMfS4KRG8gbm90IHN0b3AgcmVhc29uaW5nIGp1c3QgYmVjYXVzZSB0aGUgY3VycmVudCBmYWN0cyBkbyBub3QgcHJvdmUgdGhlIGNsYWltLiBTdG9wIG9ubHkgd2hlbiB0aGUgY2xhaW0gaXMgc2V0dGxlZCwgb3Igd2hlbiBubyB1bnJlc29sdmVkIGluZmVyZW5jZSBwYXRoIGNhbiBzdGlsbCBzZXR0bGUgaXQuCgpFYWNoIHN0ZXAgaW4gdGhlIHJlc3BvbnNlIHN0YWdlIG11c3QgZm9sbG93IHRoZSBmb3JtYXQgYmVsb3csIHdoaWNoIGNvbnRhaW5zIHRocmVlIHNlY3Rpb25zOiBQcmVtaXNlcywgQXNzdW1wdGlvbnMsIGFuZCBEZXJpdmVkIEZhY3Q6CgoqKlJlc3BvbnNlIEZvcm1hdCoqClN0ZXAgWDoKIyNQcmVtaXNlczojIwotIFtGYWN0cyBmcm9tIHRoZSBpbnB1dCBwcmVtaXNlcyBvciBwcmlvciBkZXJpdmVkIGZhY3RzLl0KLSBbRG9uJ3QgaW5jbHVkZSBhbnkgdXNlciBxdWVyeSBvciBoeXBvdGhlc2lzIGhlcmUuXQojI0V4cGxhbmF0aW9uOiMjCi0gW0FkZCBsaW5ndWlzdGljIGJyaWRnZXMgb25seSAoZS5nLiwgc3lub255bXMsIGxleGljYWwgZXF1aXZhbGVuY2VzLCBkZWZpbml0aW9uYWwgbWFwcGluZ3MpXQotIFtOZXZlciB1c2UgQXNzdW1wdGlvbnMgdG8gZmlsbCBsb2dpY2FsIGdhcHMuIFdyaXRlIE5vbmUgaWYgbm8gYXNzdW1wdGlvbiBpcyBuZWVkZWRdCiMjRGVyaXZlZCBGYWN0OiMjCi0gW1RoZSBkZXJpdmVkIGZhY3QgbXVzdCBiZSBmdWxseSBzdXBwb3J0ZWQgYnkgdGhhdCBzdGVwJ3MgcHJlbWlzZXMgYW5kIGFzc3VtcHRpb25zLl0KLSBbRG8gbm90IHNwZWN1bGF0ZSBhYm91dCBvdGhlciBmYWN0cy5dCgpBZnRlciB5b3VyIGZpbmFsIHN0ZXAsIG91dHB1dCBleGFjdGx5IHlvdXIgYW5zd2VyIHdpdGggXGJveGVke0xBQkVMfS4KCg==)1Youareameticulouslogician\.Readtheuser’sgivenpremiseandhypothesiscarefully,thenreasonstepbystepexplicitlyinaNaturalLanguageInference\(NLI\)style,andconcludewith\\boxed\{LABEL\}\.2Donotstopreasoningjustbecausethecurrentfactsdonotprovetheclaim\.Stoponlywhentheclaimissettled,orwhennounresolvedinferencepathcanstillsettleit\.34Eachstepintheresponsestagemustfollowtheformatbelow,whichcontainsthreesections:Premises,Assumptions,andDerivedFact:56\*\*ResponseFormat\*\*7StepX:8\#\#Premises:\#\#9\-\[Factsfromtheinputpremisesorpriorderivedfacts\.\]10\-\[Don’tincludeanyuserqueryorhypothesishere\.\]11\#\#Explanation:\#\#12\-\[Addlinguisticbridgesonly\(e\.g\.,synonyms,lexicalequivalences,definitionalmappings\)\]13\-\[NeveruseAssumptionstofilllogicalgaps\.WriteNoneifnoassumptionisneeded\]14\#\#DerivedFact:\#\#15\-\[Thederivedfactmustbefullysupportedbythatstep’spremisesandassumptions\.\]16\-\[Donotspeculateaboutotherfacts\.\]1718Afteryourfinalstep,outputexactlyyouranswerwith\\boxed\{LABEL\}\.

#### Consistency Check Prompt

The consistency check described in §[2\.1](https://arxiv.org/html/2609.21492#S2.SS1)uses an LLM judge to determine whether the explanationsEiE\_\{i\}and contextCiC\_\{i\}conflict with the original given premisesPP\. The judge is instructed to be lenient, only flag direct and unambiguous conflicts\.

System Prompt for Consistency Check[⬇](data:text/plain;base64,WW91IGFyZSBhIGxvZ2ljYWwgY29uc2lzdGVuY3kgY2hlY2tlci4gRGV0ZXJtaW5lIHdoZXRoZXIgdGhlIGFzc3VtcHRpb24gaW4gdGhlIHJlYXNvbmluZyBzdGVwIGNvbmZsaWN0cyB3aXRoIHRoZSBvdmVyYWxsIGNvbnRleHQuCgoqRXhhbXBsZXMqCi0gQ29uc2lzdGVudDogZ2l2ZW4gY29udGV4dCBjb250YWlucyAndGhlIGluZmFudCBpcyBjcnlpbmcsIFRvbSBpcyByb3VuZCcsIGFuZCB0aGUgYXNzdW1wdGlvbiBzYXlzICdpbmZhbnRzIGFyZSBiYWJpZXM7IGdpdmVuIGNvbnRleHQgaW5jbHVkZXMgVG9tIGlzIHJvdW5kJy4KLSBJbmNvbnNpc3RlbnQ6IGdpdmVuIGNvbnRleHQgY29udGFpbnMgJ2RvZyBpcyByb3VuZCwgY2F0IGlzIGdyZWVuJywgYW5kIHRoZSBhc3N1bXB0aW9uIHNheXMgJ3dlIGRvbid0IGtub3cgaWYgY2F0IGlzIHJvdW5kJy4gQmVjYXVzZSBpdCBpbnRyb2R1Y2VzIGluZm9ybWF0aW9uIG5vdCBncm91bmRlZCBpbiB0aGUgY3VycmVudCBjb250ZXh0LgoKUmVzcG9uZCB3aXRoIGEgSlNPTiBvYmplY3QgaW4gdGhpcyBleGFjdCBmb3JtYXQ6CnsiY2hlY2tfcmVzdWx0IjogImNvbnNpc3RlbnQiLCAicmVhc29uIjogIi4uLiJ9Cm9yCnsiY2hlY2tfcmVzdWx0IjogImluY29uc2lzdGVudCIsICJyZWFzb24iOiAiLi4uIn0=)1Youarealogicalconsistencychecker\.Determinewhethertheassumptioninthereasoningstepconflictswiththeoverallcontext\.23\*Examples\*4\-Consistent:givencontextcontains’theinfantiscrying,Tomisround’,andtheassumptionsays’infantsarebabies;givencontextincludesTomisround’\.5\-Inconsistent:givencontextcontains’dogisround,catisgreen’,andtheassumptionsays’wedon’tknowifcatisround’\.Becauseitintroducesinformationnotgroundedinthecurrentcontext\.67RespondwithaJSONobjectinthisexactformat:8\{"check\_result":"consistent","reason":"\.\.\."\}9or10\{"check\_result":"inconsistent","reason":"\.\.\."\}

#### Answer Extraction

The predicted answery^\\hat\{y\}is extracted from the model’s response via a rule\-based procedure\. We first look for the`\\boxed\{\.\.\.\}`notation specified in the prompt, extracting the innermost content and stripping wrappers \(e\.g\.,`\\text\{\}`\)\. If no boxed answer is found, we also consider alternative patterns such as`<answer\>\.\.\.</answer\>`tags and common answer\-declaration phrases \(e\.g\., “the answer is \{LABEL\}”\) in the final sentences of the response\. If none of these patterns match, the prediction is marked as unanswered\.