LogicTrack: Auditing Reasoning Trajectories of Large Language Models with Formal Logic Solvers

📄 arXiv: 2609.21492v1 📥 PDF

作者: Jingyu Hu, Shu Yang, Weiru Liu, Di Wang

分类: cs.AI, cs.LO, cs.SC

发布日期: 2026-09-18

💡 一句话要点

提出LogicTrack以解决大语言模型推理链的逻辑有效性问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 逻辑推理 大语言模型 神经符号框架 自动定理证明 推理链审计 回溯奖励机制 模型优化

📋 核心要点

  1. 现有方法在优化大语言模型推理时，主要依赖结果反馈，导致中间推理步骤的逻辑有效性缺乏验证。
  2. 本文提出LogicTrack，通过将推理步骤形式化为符号表示并使用定理证明器进行验证，来审计推理轨迹。
  3. 实验结果显示，LogicTrack在多个基准测试中显著提高了推理链的可验证性和最终答案的通过率。

📝 摘要（中文）

链式思维（CoT）推理已被证明能提升大语言模型（LLMs）的性能，但现有优化方法主要依赖结果反馈，导致中间推理步骤的逻辑有效性未得到验证。为了解决这一问题，本文提出了LogicTrack，一个神经符号框架，通过将每个推理步骤自动形式化为符号表示并使用自动定理证明器进行验证，从而审计推理轨迹。LogicTrack引入了基于求解器的回溯奖励（SBR），量化逻辑合理性并指导推理时的回溯树搜索。通过在8个推理基准和7个LLMs上的广泛实验，证明LogicTrack有效提升了推理链的可验证性和最终答案的通过率，从而增强了高风险领域的CoT质量和可信度。

🔬 方法详解

问题定义：本文旨在解决大语言模型在推理过程中存在的逻辑有效性问题，现有方法未能验证中间推理步骤的合理性，可能导致错误的最终答案。

核心思路：LogicTrack通过将每个推理步骤自动形式化为符号表示，并利用自动定理证明器进行验证，从而实现对推理轨迹的审计，确保推理过程的逻辑合理性。

技术框架：LogicTrack的整体架构包括推理步骤的自动形式化、符号表示的逻辑验证和基于求解器的回溯奖励机制。推理过程中的每一步都被量化并反馈到模型中，以指导后续推理。

关键创新：最重要的创新在于引入了基于求解器的回溯奖励（SBR），这一机制不仅量化了推理步骤的逻辑合理性，还为推理过程提供了动态反馈，显著提高了推理链的可信度。

关键设计：在设计中，SBR机制通过评估每个推理步骤的逻辑有效性来调整模型的推理策略，确保模型在推理时能够内化审计能力，进而提升最终答案的准确性。实验中使用了多种损失函数和网络结构，以优化推理性能。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

在8个推理基准和7个大语言模型的实验中，LogicTrack显著提高了推理链的可验证性和最终答案的通过率，提升幅度达到了XX%（具体数据需根据实验结果补充），证明了其在高风险领域的有效性和可靠性。

🎯 应用场景

该研究的潜在应用领域包括高风险决策支持系统、法律推理、医疗诊断等场景，能够有效提升大语言模型在复杂推理任务中的可信度和可靠性。未来，LogicTrack有望在更多领域推广应用，推动智能系统的逻辑推理能力。

📄 摘要（原文）

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.