# LogicTrack: Auditing Reasoning Trajectories of Large Language Models with Formal Logic Solvers 论文总结与翻译
> 论文arXiv链接：https://arxiv.org/abs/2609.21492
## 一、论文主要内容
Chain‑of‑Thought（思维链CoT）能够提升大语言模型推理能力，但现有优化大多只依据最终输出结果做反馈，**不会校验中间推理步骤的逻辑有效性**，存在“中间推理逻辑错误，但碰巧得到正确答案”的问题。
本文提出**LogicTrack**，一套神经符号框架，在推理生成过程中审计模型推理路径：
1. 将模型每一步自然语言推理自动形式化为符号逻辑表示，调用自动定理证明器做逻辑校验；
2. 提出**基于求解器的回溯奖励SBR**，细粒度衡量每一步推理逻辑完备性，推理时驱动回溯树搜索；当某一步逻辑不达标，模型从该位置重新生成推理；
3. 利用框架产生的回溯轨迹构建监督微调（SFT）数据集，让模型把“分步逻辑审计”内化为自身能力，不再完全依赖外部求解器；
4. 在8个推理基准、7个大模型上开展大量实验。结果表明LogicTrack既提升推理链条的可验证性，也提高最终答案正确率，增强高风险场景下CoT推理的可信度。
整体分为三大模块：①推理步骤拆解+自动形式化与逻辑求解器验证；②SBR奖励引导的在线回溯搜索；③回溯轨迹监督微调LogicTrack‑SFT。
## 二、核心创新点
1. **生成时在线审计，而非事后校验**
过去相关工作是先生成完整推理链，再事后校验每一步。LogicTrack在推理生成过程中逐步骤校验，一旦发现逻辑错误
