论文
LogicTrack：用形式逻辑求解器审计大语言模型的推理轨迹
LogicTrack: Auditing Reasoning Trajectories of Large Language Models with Formal Logic Solvers
摘要
思维链（CoT）推理已被证明能提升大语言模型（LLM）的性能，但现有优化方法主要依赖基于结果的反馈，中间推理步骤的逻辑有效性在很大程度上未经核验。针对LLM通过逻辑有缺陷的中间推理链得到正确最终答案这一缺口，我们提出LogicTrack——一个神经符号框架，将每个推理步骤自动形式化为符号表示并用自动定理证明器核验，从而审计推理轨迹。LogicTrack引入基于求解器的回溯奖励（SBR），一种逐步评分机制，量化逻辑稳健性并在推理时引导回溯树搜索。我们进一步扩展LogicTrack，从其轨迹中构建带回溯痕迹的监督微调（SFT）数据，使微调模型将逐步审计内化为自身能力。在8个推理基准与7个LLM上的大量实验表明，LogicTrack有效提升推理链的可验证性与最终答案通过率，从而增强高风险领域的整体CoT质量与可信度。
