often produce correct final answers through logically flawed intermediate steps, raising trust concerns in high-stakes domains. Existing methods rely on outcome-based feedback or LLM-based judges, which are inconsistent. LogicTrack addresses this by auto-formalizing each reasoning step into symbolic representations and verifying them with automated theorem provers during generation.
LogicTrack introduces Solver-Based Backtracking Reward (SBR), a step-wise score that quantifies logical soundness and triggers backtracking when a step falls below a threshold. Beyond inference-time auditing, it constructs supervised fine-tuning data from backtracking trajectories, enabling models to internalize step-wise .
Experiments across 8 reasoning benchmarks and 7 LLMs show that LogicTrack improves both the verifiability of reasoning chains and final answer pass rate, enhancing chain-of-thought quality and trustworthiness.