VeriCoT: 通过逻辑一致性检查进行神经符号链式思维验证
论文原始标题：VeriCoT: Neuro-symbolic Chain-of-Thought Validation via Logical Consistency Checks
论文作者：Authors: Yu Feng, Nathaniel Weir, Kaj Bostrom, Sam Bayless, Darion Cassel, Sapana Chaudhary, Benjamin Kiesl-Reiter, Huzefa Rangwala
原始摘要：LLMs can perform multi-step reasoning through Chain-of-Thought (CoT), but they cannot reliably verify their own logic. Even when they reach correct answers, the underlying reasoning may be flawed, undermining trust in high-stakes scenarios. To mitigate this issue, we introduce VeriCoT, a neuro-symbolic method that extracts and verifies formal logical arguments from CoT reasoning. VeriCoT formalizes each CoT reasoning step into first-order logic and identifies premises that ground the argument in source context, commonsense knowledge, or prior reasoning steps. The symbolic representation enables automated solvers to verify logical validity while the NL premises allow humans and systems to identify ungrounded or fallacious reasoning steps. Experiments on the ProofWriter, LegalBench, and BioASQ datasets show VeriCoT effectively identifies flawed reasoning, and serves as a strong predictor of final answer correctness. We also leverage VeriCoT's verification signal for (1) inference-time self-reflection, (2) supervised fine-tuning (SFT) on VeriCoT-distilled datasets and (3) preference fine-tuning (PFT) with direct preference optimization (DPO) using verification-based pairwise rewards, further improving reasoning validity and accuracy.
翻译标题：VeriCoT: 通过逻辑一致性检查进行神经符号链式思维验证
翻译摘要：大型语言模型（LLM）可以通过链式思维（CoT）进行多步推理，但它们无法可靠地验证自身的逻辑。即使最终答案正确，其背后的推理可能仍存在缺陷，这在高风险场景中会削弱信任。为缓解这一问题，我们引入了 VeriCoT，这是一种神经符号方法，能够从 CoT 推理中提取并验证形式化逻辑论证。VeriCoT 将每一步 CoT 推理形式化为一阶逻辑，并识别支撑论证的前提，这些前提可以来自源上下文、常识知识或先前推理步骤。符号表示使自动化求解器能够验证逻辑有效性，而自然语言前提则让人类和系统能够识别缺乏依据或存在逻辑谬误的推理步骤。在 ProofWriter、LegalBench 和 BioASQ 数据集上的实验表明，VeriCoT 能有效识别错误推理，并作为最终答案正确性的强预测指标。我们还利用 VeriCoT 的验证信号进行 (1) 推理时的自我反思，(2) 在 VeriCoT 精炼数据集上进行监督微调 (SFT)，以及 (3) 使用基于验证的成对奖励进行偏好微调 (PFT) 与直接偏好优化 (DPO)，进一步提升推理有效性和准确性。
论文导览：
智能问答：
Q1: 这篇论文试图解决什么问题？
论文旨在解决大语言模型（LLM）在 Chain-of-Thought（CoT）多步推理中“逻辑不可靠”的核心问题：
即便最终答案正确，中间推理步骤仍可能包含虚假、矛盾或缺乏依据的陈述，导致在高风险领域（法律、医学等）难以信任。
为此，作者提出 VERICOT——一种神经-符号验证框架，能够将自然语言 CoT 每一步自动形式化为一阶逻辑公式，并通过 SMT 求解器检查其是否被显式前提（源自上下文、常识或前序步骤）逻辑蕴含。若无法通过验证，则给出具体错误类型（无依据、矛盾、不可形式化），并据此提供可解释的反馈信号，用于推理时自修正、监督微调与偏好优化，从而提升 CoT 的逻辑一致性与任务准确率。
Q2: 有哪些相关研究？
Explanation-Refiner（Quan et al., 2024b）
迭代地将自然语言解释自动形式化，再用定理证明器验证与精化，但仅针对 NLI 任务，且不逐步 grounding 到上下文。
Logic-LM（Pan et al., 2023）
将问题一次性翻译成逻辑后调用求解器，缺少逐步验证与上下文前提溯源。
SATLM（Ye et al., 2023）
用 LLM 生成 SAT 约束再调用求解器，同样无逐步逻辑一致性检查。
Deductive Verification of CoT（Ling et al., 2023）
仅用 LLM 自身判断每步是否矛盾，无外部符号求解器，验证客观性不足。
LINC / Certified DR（Olausson et al., 2023；Poesia et al., 2024）
结合 LLM 与一阶逻辑证明器，但侧重代码或数学领域，依赖固定形式库，未面向开放领域 NL-CoT。
Entailment Tree 系列（Dalvi et al., 2021；Tafjord et al., 2022；Weir et al., 2024）
用自然语言蕴含关系构建多步推理树，缺乏形式逻辑与自动求解器保障。
Theorem Prover-as-a-Judge（Leang et al., 2025）
用定理证明反馈做强化学习，仅限 Lean/mathlib 数学环境；VERICOT 将证明器用于任意 NL 上下文。
Q3: 论文如何解决这个问题？
论文把“LLM 无法自证 CoT 逻辑有效性”这一难题拆成三步，并给出对应机制：
自动形式化
用 LLM 将每步自然语言推理翻译成 SMT-LIB 一阶逻辑公式，若翻译失败则标记为 untranslatable。
前提溯源与 entailment 检查
若公式 F_i 已被前序知识 F_i−1 逻辑蕴含（F_i−1 ⊨ F_i），直接通过。
若 F_i−1 ⊨ ¬F_i，标记 contradiction。
否则调用 LLM 从上下文、源文档、常识三处抽取候选前提，经一致性筛选后得到新增前提集合 P_i，再判 F_i−1 ∧ P_i ⊨ F_i；仍不成立则标记 ungrounded。
利用验证信号反哺模型
推理时自反思：把上述错误类型与形式化结果作为 prompt，让 LLM 当场重写 CoT，平均验证通过率相对提升 46%。
监督微调（SFT）：只保留“验证通过且 LLM-as-Judge 认为前提可接受”的 CoT 构建训练集，7 B 模型任务准确率提升 3%。
偏好微调（DPO）：以“通过验证 vs 未通过”构建 pairwise 奖励，进一步把验证通过率再提高 18%。
通过“神经生成-符号验证-反馈再训练”的闭环，VERICOT 在 ProofWriter、LegalBench-SARA、BioASQ 上同时提高了 CoT 的逻辑一致性（验证通过率）与最终答案正确率。
Q4: 论文做了哪些实验？
实验围绕 “VERICOT 能否可靠验证 CoT” 与 “验证信号能否提升模型” 两条主线展开，覆盖 3 个数据集、4 大指标、3 种应用方式。
维度 设置 关键结果
数据集 ProofWriter（逻辑规则推理）、LegalBench-SARA（税法条文）、BioASQ（生物医学 QA）
基线 Explanation-Refiner、Direct-SMT、VERICOT-NoPrem（无主动前提生成）
主指标 验证通过率 ↑、验证器精度 ↑、Verified-Correct-Answer-Rate(VCAR) ↑、最终任务精度
直接验证性能 表 1 VERICOT 在三数据集均取得最高通过率和 VCAR，精度始终高于原始任务准确率，证明“被验证”是更强的正确信号
错误分析 图 2 + 附录表 3-5 未验证样本中 60-70 % 为 ungrounded；自反思后 valid 比例平均提升 46 %
前提质量 表 2 LLM-as-Judge 评估：上下文前提可接受率 87-96 %，常识前提 83-93 %
推理时自反思 表 3 相对基线，VCAR 平均再提升 41 %，最终任务准确率同步增长
监督微调 表 4 Qwen2.5-7 B 在 BioASQ/ProofWriter 上任务精度 +3 %，验证通过率 +1-2 %
偏好微调（DPO） 表 4 在 SFT 基础上再用“验证通过 vs 失败”做 DPO，验证通过率相对再提升 18 %，VCAR 再提升 17 %
综上，实验既验证了 VERICOT 作为符号验证器的可靠性，也证明了其信号在推理-训练全链路中持续有效。
Q5: 有什么可以进一步探索的点？
以下方向可继续推进，分为“验证器本身”与“验证信号利用”两大层面：
逻辑片段扩展
目前仅用 SMT-LIB 的线性算术、未解释函数与量词。可引入模态逻辑、时序逻辑、概率逻辑以覆盖“可能”、“将来”、“大概率”等自然语言表述，降低 untranslatable 比例。
前提可信度量化
现用 LLM-as-Judge 做二值判断。可改为连续置信度或多源证据重叠度，并引入不确定性推理（如 Markov Logic Network），让“弱前提”也能参与 entailment 计算并给出置信区间。
跨语言与多模态
将 autoformalization 扩展到多语言 CoT与图文混合上下文（医疗影像 + 文本），验证视觉前提与文本结论之间的一致性。
在线前提补全
对 ungrounded 步骤，主动调用检索器或知识图谱获取缺失公理，再判 entailment，实现“验证-检索”闭环。
更细粒度错误定位
当前仅定位到单步。可借助最小不可满足子句（MUS）技术，精确定位“哪一条前提 + 哪一段文本”导致矛盾，生成更短、可解释的修正建议。
验证信号用于强化学习
把 VERICOT 的 0/1 验证信号作为稀疏奖励，结合 Monte-Carlo Tree Search 或 PPO，在更大规模通用任务上直接优化“可验证性”而非表面答案正确率。
与形式化证明库对接
对数学/代码子域，尝试将 VERICOT 抽出的前提自动映射到 Lean、Coq 的已有引理，实现自动补全形式证明而非仅做一致性检查。
人机协同验证界面
开发可视化界面，让领域专家实时编辑前提或规则，VERICOT 即时反馈 entailment 变化，用于法规审查、临床指南制定等高风险场景。
Q6: 总结一下论文的主要内容
VERICOT：神经-符号 CoT 验证与修复框架
问题
LLM 的 Chain-of-Thought 常含“中间步骤虚假/无依据”现象，即使答案正确也难以信任。
方法
逐句自动形式化为一阶逻辑（SMT-LIB）。
用 Z3 检查是否被上下文、常识或前序步骤逻辑蕴含；无法通过则标记 ungrounded / contradiction / untranslatable。
验证信号反哺：
– 推理时自反思 → 46 % 相对提升验证通过率；
– 监督微调 → 任务准确率 +3 %；
– 偏好优化（DPO）→ 验证通过率再 +18 %。
实验
ProofWriter、LegalBench-SARA、BioASQ 三数据集上，VERICOT 的验证通过率、VCAR、精度均显著高于现有基线，且被验证的 CoT 精度持续高于原始任务准确率。
贡献
首个面向非数学/代码领域的逐步 CoT 符号验证器；
提出“可验证性”作为可量化的训练与推理目标；
验证信号可直接用于自反思、SFT、PFO，全链路提升逻辑一致性与最终答案正确率。
阅读全文 →
来源：Arxiv2025-11-06 18:50:08 UTC
