发表机构
University of Bristol; King Abdullah University of Science and Technology（布里斯托大学; 阿卜杜拉国王科技大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
LogicTrack通过自动形式化推理步骤并用定理证明器验证，引入逐步回溯奖励，提升LLM推理链的逻辑可验证性与最终答案通过率。
AI 中文摘要
思维链（Chain-of-Thought, CoT）推理已被证明能提升大型语言模型（LLMs）的性能，然而现有的优化方法主要依赖于基于结果的反馈，导致中间推理步骤的逻辑有效性在很大程度上未经验证。为了解决LLMs通过逻辑有缺陷的中间推理链得出正确最终答案这一差距，我们提出了LogicTrack，一个神经符号框架，通过将每个推理步骤自动形式化为符号表示，并使用自动定理证明器进行验证，从而审计推理轨迹。LogicTrack引入了基于求解器的回溯奖励（Solver-Based Backtracking Reward, SBR），这是一种逐步评分机制，用于量化逻辑健全性，并在推理时指导回溯树搜索。我们进一步扩展LogicTrack，利用其轨迹中的回溯痕迹构建监督微调（SFT）数据，使微调后的模型能够将逐步审计内化为一种固有能力。在8个推理基准和7个LLM上的广泛实验表明，LogicTrack有效提高了推理链的可验证性和最终答案的通过率，从而在高风险领域中增强了整体CoT质量和可信度。
英文摘要
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.
