Chain-of-Thought (CoT) improves the reasoning performance of large language models (LLMs), yet most existing optimizations rely on outcome‑based feedback and leave the logical soundness of intermediate steps unchecked. To close the gap where LLMs reach correct answers through flawed reasoning chains, we introduce LogicTrack, a neuro‑symbolic framework that auto‑formalizes each reasoning step into a symbolic form and verifies it with automated theorem provers.
LogicTrack features a Solver‑Based Backtracking Reward (SBR) that assigns a logical soundness score to every step and steers a backtracking tree search during inference, allowing the model to correct logical deviations on the fly.
We also harvest backtracking traces as supervised fine‑tuning (SFT) data, enabling fine‑tuned models to internalize step‑wise auditing as an intrinsic capability.
Extensive experiments on eight reasoning benchmarks across seven LLMs show that LogicTrack markedly improves both the verifiability of reasoning chains and the final answer pass rate, thereby enhancing CoT quality and trustworthiness in high‑stakes domains.
Review