← 返回 2026-08-11

SymDiag：基于神经符号验证的 LLM 推理可解释诊断框架 SymDiag: Explainable Diagnosis for LLM Reasoning via Neuro-Symbolic Verification

Wenyao Cui, Huaping Zhang, Yongyi Huang, Qiuchi Li, Jian Xu, Cheng-Lin Liu, Chunxiao Gao, Juan Wang, Baohua Zhang 📅 2026-08-09 👍 6 2026-08-16 18:30
CoT忠实度 LLM推理诊断 可解释AI 形式化验证 推理修复 神经符号方法
arXiv HuggingFace PDF

将 CoT 验证重构为符号化失败诊断：定位错误步骤、区分翻译噪声与推理缺陷，并用可验证证据指导修复

前置知识

CoT 忠实度（Faithfulness）

指思维链中每一步推理在逻辑上是否真的成立：中间论断能否从前文严格推出、有没有隐藏假设或非法变换。它与“答案正确”是两回事——存在“答案对但过程有缺陷”（不忠实）和“过程正确但答案算错”两类错法。忠实度评估因此必须逐条检查中间步骤，而非只看终点对不对。

SymDiag 的全部目标就是自动检测不忠实的 CoT 并定位缺陷；其评测集中 25% 的实例正是“答案正确但不忠实”，理解这一概念才能理解为何答案匹配基线会系统性漏检。

神经符号方法（Neuro-Symbolic）

把神经网络（擅长语义理解、处理灵活表述）与符号系统（擅长严格推理、结论可验证）结合的范式：神经网络负责把自然语言映射成形式表示，符号求解器负责推导、检验并给出机器可查的结论。代表工作有 Logic-LM、LINC、SymbCoT 等。

SymDiag 是典型的神经符号系统：LLM 把 CoT 翻译成 Prolog 程序，SWI-Prolog 做逐步验证；论文的核心创新 Self-Auditor 恰恰针对这类系统的固有痛点——翻译噪声污染验证信号。

Prolog 与 Horn 子句

Prolog 是逻辑编程语言，程序由 Horn 子句（形如“结论 :- 条件”的规则）构成，原生支持合一、回溯和归结推理，天然适合表达“前提+规则+约束”式的推导并被自动执行。相比 Lean、Coq 等重型证明助手，它轻量、可读、无需领域专用形式库。

论文选择 Prolog 作为符号后端：CoT 的每一步被编译成 Prolog 片段，求解器据此做可满足性与蕴含检查并产出反例等证据；理解其执行模型才能明白证据为何“机器可查”。

可满足性（SAT/UNSAT）与逻辑蕴含

可满足性检查询问一组公式是否存在使其同时为真的赋值；蕴含 $\Gamma \models \varphi$ 表示凡使 $\Gamma$ 为真的赋值必使 $\varphi$ 为真，标准判定法是否定目标后检验 $\mathrm{UNSAT}(\Gamma \wedge \neg\varphi)$——若仍可满足，反模型本身就是反例。

SymDiag 的两个核心检查都建立在此之上：$\mathrm{SAT}(P_i \wedge C_i)$ 查每步自洽性，$\mathrm{UNSAT}(P_{i-1} \wedge C_{i-1} \wedge \neg\varphi_i)$ 查步骤论断是否被前文支持；可满足时抽出的赋值就是论文所说的“反例证据”。

PRM 与 LLM-as-Judge

过程奖励模型（PRM）对推理的每个中间步骤打分，常用于 best-of-$n$ 选择或强化学习训练；LLM-as-Judge 则让另一个 LLM 阅读答案与过程后给出自然语言评价，可用多裁判投票增强。两者是当前过程级验证的主流，但输出分别是标量与不可验证的文本。

它们正是论文实验的两大基线（Reward Model 与 LLM-as-Judge）。理解其“打分/评判”本质，才能理解 SymDiag 提出的“诊断级”范式——定位+归因+可验证证据——到底多出了什么。

研究动机

LLM 的思维链存在“过程不忠实但答案正确”的系统性风险：中间步骤可能依赖隐藏假设、偷换概念或做非蕴含变换。更麻烦的是，现有验证信号都不是为诊断设计的：答案匹配只观察最终结果，输出 1 比特信息，无法在长推导中定位错误；LLM-as-Judge 的自然语言批评主观、前后不一致，且容易被流畅但逻辑有漏洞的推理说服；过程奖励模型（PRM）和标量奖励模型则把丰富的失败模式压缩成一个分数，既不能指出哪一步出错，也不能说明违反了哪条约束。在医疗、法律等高风险场景中，结果正确不等于过程可信，这一鸿沟是 LLM 推理器落地的主要障碍。论文自建数据也印证了问题规模：240 条人工审核实例中 104 条（43.3%）不忠实，其中 60 条（25.0%）属于“答案正确但过程有可定位缺陷”——纯结果评估对此完全失明。

本文的目标是本文把推理验证从“打分/评判”重构为“结构化失败诊断”，让系统对每条 CoT 输出四类可核查的信息：(i) 步骤级判定，对每个推理步 $s_i$ 给出 pass/fail；(ii) 失败定位，给出失败步骤索引集合 $F \subseteq \{1,\dots,T\}$；(iii) 错误归因，按预定义分类体系（前提缺失、无效推理、约束/边界忽略、规则误用、算术错误、类型不匹配、翻译错误）打标签；(iv) 机器可验证证据，如反例赋值、不一致见证（unsat core）和缺失前提指示器。在此之上，SymDiag 还要把诊断转成可执行反馈，驱动多轮修复（默认最多 4 轮），同时提升不忠实检测的准确率与修复后的任务准确率，并在数学、逻辑、科学、通识四类推理任务上验证同一框架的通用性。

与已有工作不同的是，神经符号验证并非全新思路：Logic-LM 用符号求解器替代推理、LogicReward/FoVer 用形式化检查构造训练信号、SymbCoT 在自然语言旁维护符号表达式。但它们要么只输出分数或修正后的轨迹，要么默认“符号检查失败就是推理错误”。SymDiag 的独特切入在于指出符号验证的一个根本混淆源：从自然语言到符号的翻译噪声同样会表现为“逻辑违例”，若不区分二者，验证器就会把解析/形式化错误误诊为推理缺陷，产生不可靠反馈。为此它引入 Self-Auditor，用双重符号编码的交叉一致性审计显式解耦 TranslationError 与 ReasoningError——把“诊断过程本身的可靠性”作为一等研究对象，这是已有验证工作普遍缺失的一环。

核心方法

直觉上，SymDiag 像一位出具检验报告的医生：不止说“有病”（不忠实），还要指出病灶在哪一步、病因属于哪类，并附上可复查的化验单。技术路线分两阶段。阶段 I（诊断）：把 CoT 表示为符号状态序列 $S_i = \{P_i, I_i, C_i\}$，分别编码累积前提、本步推理与约束；双分支神经符号生成器将其编译成两份独立的 Prolog 程序（形式翻译 + 批判性重述）；Self-Auditor 对双编码做一致性审计后，SWI-Prolog 对每步执行可满足性检查 $\mathrm{SAT}(P_i \wedge C_i)$ 与局部蕴含检查，失败时定位步骤并生成反例等证据。阶段 II（修复）：把诊断元组 verbalize 成结构化反馈，按 scope 让基础模型做局部补丁或从最早失败步全链重写，默认迭代最多 $N=4$ 轮。

核心创新有两点。第一是“诊断级”验证范式：不同于结果级（1 比特对错）与过程级（标量奖励或自然语言评价），SymDiag 输出一条可独立验证的符号证据链——每个失败结论都能在求解器中复现，例如通过构造让步骤论断 $\varphi_i$ 为假的具体赋值充当反例。第二是 Self-Auditor：用两个互补分支对同一步生成双编码——A 分支（形式翻译）按一致签名映射实体、谓词与关系，数学任务规范化量纲与等式，逻辑任务显式建模量词与辖域；B 分支（批判性重述）把步骤改写成更严格、显式辖域的论断以暴露隐藏假设。随后比较两分支的事实/约束重叠情况并运行轻量符号 sanity 测试：若表面“违例”在最小规范改写（变量重命名、与文本一致的约束放松）下消失，即归因为翻译噪声而非推理错误。只有通过审计的 Approved 状态才进入步骤验证器，从源头防止翻译噪声污染诊断。

方法步骤详情

完整流程七步。(1) 步骤状态表示：第 $i$ 步编译为 $S_i=\{P_i,I_i,C_i\}$ 的 Prolog 片段，$P_i$ 为累积前提与已推导事实，$I_i$ 为本步推理（规则应用、代数变形或蕴含声明），$C_i$ 为定义域/类型/边界约束。(2) 双分支生成：PrologA（形式翻译）与 PrologB（批判性重述）两份独立程序 Π(A)、Π(B)。(3) 确定性语法检查：签名一致性（元数/类型）、可接地性（检测应绑定而未绑定的自由变量）、约束规范化、求解器兼容性；失败即走 TranslationError 通路。(4) Self-Auditor 审计：翻译一致性检查（计算 Π(A) 与 Π(B) 事实集/约束集的重叠统计，分歧大即标记映射失败）+ 逻辑批判检查（即时矛盾、不可能类型赋值等 sanity 测试）。(5) 步骤级验证：一致性测试 $\mathrm{SAT}(P_i \wedge C_i)$；局部蕴含 $(P_{i-1} \wedge C_{i-1}) \models \varphi_i$，操作化为 $\mathrm{UNSAT}(P_{i-1} \wedge C_{i-1} \wedge \neg\varphi_i)$，若可满足则抽出反例赋值。(6) 全链判定：所有步骤在至少一个 Approved 分支通过才判 Faithful，两分支审计后均失败时保守判 Unfaithful。(7) 修复：诊断元组 $d_i=(\ell_i,E_i,\mathrm{scope}_i)$ 连同证据转成反馈，局部缺陷最小化编辑单步，传播性缺陷（如早期前提缺失）从最早失败步起重写。

技术新颖性

与 Logic-LM/LINC 等“用符号系统解题”的框架不同，SymDiag 不让符号系统替代推理，而是审计 LLM 自己的推理；与 LogicReward/FoVer 等“形式化检查只产出训练信号”的做法不同，它的输出是定位+归因+证据三元组，可直接人工或机器复核。双编码+交叉审计直面神经符号系统的公认痛点——翻译噪声污染验证信号——消融显示去掉 Self-Auditor 后总体 F1 从 70.7 跌到 61.4（−9.3 分），证明它是实打实的性能来源而非装饰。此外三点设计在同类工作中少见：保守的平局裁决（两分支均失败时宁可判不忠实）；把“答案正确但过程不忠实”作为一等检测目标；以及领域无关的六类错误分类法（附录 A）外加 TranslationError，使数学、逻辑、科学、通识四域共享同一诊断框架与输出格式。

SymDiag overview. Stage I (Diagnosis): a neuro-symbolic generator produces (i) a formal translation and (ii) a critical restatement of the original CoT as two independent Prolog programs; a Self-Auditor checks cross-encoding consistency... Stage II (Repair): SymDiag uses localized failures and evidence to prompt an LLM to generate a repaired reasoning trace that is solver-consistent.
Figure 2: SymDiag overview. Stage I (Diagnosis): a neuro-symbolic generator produces (i) a formal translation and (ii) a critical restatement of the original CoT as two independent Prolog programs; a Self-Auditor checks cross-encoding consistency... Stage II (Repair): SymDiag uses localized failures and evidence to prompt an LLM to generate a repaired reasoning trace that is solver-consistent.
Core experimental dataset composition. We manually audit 240 instances in total, sampling 30 examples from each dataset across four reasoning domains.
Figure 3: Core experimental dataset composition. We manually audit 240 instances in total, sampling 30 examples from each dataset across four reasoning domains.

实验结果

四组关键实验。① 忠实性检测：在 240 条人工审核实例上，SymDiag 总体 F1 达 70.7 全场最佳，超过同判官（GPTOSS-120B）的 LLM-as-Judge（66.2）、LogicReward（62.8），以及 Answer Matching（57.7）和 Reward Model（57.0）；优势在 AR-LSAT、LogiDed、MMLU 等逻辑/通识域最大，因为这些域“答案对但过程错”的比例高，基线系统性漏检。② 修复效果：默认 4 轮修复中，SymDiag 在全部 8 个数据集上增速与终值均为最佳（如 AR-LSAT 最高曲线约 89%→93%、MMLU-Pro 约 76%→79.5%）；LLM-as-Judge 早期小涨后迅速饱和，Answer Matching 几乎无提升，标量信号（RM/LogicReward）噪声大且不可定位。③ 消融：去步级符号验证掉分最多（70.7→60.2，−10.5），去 Self-Auditor −9.3，去批判性重述 −7.9，去形式翻译 −5.6，证明收益来自组件协同。④ 机理分析：错误分布随模型规模系统性迁移——Llama-3.2-1B 的 35% 是算术错误、30% 是前提缺失，而 GPTOSS-20B 的 32% 是规则误用、20% 是类型不匹配、算术错误仅 5%；Self-Auditor 三轮迭代把管线总错误率从 46.6% 降至 18.6%、通过率从 53.4% 升至 81.4%（翻译错误 20.1% 第三轮近零）；判官从 120B 缩到 20B 时 SymDiag 仍以 66.9 保持第一，结构化收益对模型缩水相对鲁棒。

Diagnosis-guided reasoning repair curves across datasets. Each subplot reports task accuracy after each repair round (Round 0 is the original answer). SymDiag yields faster and more sustained gains...
Figure 4: Diagnosis-guided reasoning repair curves across datasets. Each subplot reports task accuracy after each repair round (Round 0 is the original answer). SymDiag yields faster and more sustained gains...
Ablation results on overall faithfulness detection (F1).
Figure 5: Ablation results on overall faithfulness detection (F1).
Normalized distribution of reasoning error types identified by SymDiag. (Error Attribution Heatmap Across Models)
Figure 6: Normalized distribution of reasoning error types identified by SymDiag. (Error Attribution Heatmap Across Models)
Progressive reduction of error types in the SymDiag pipeline through iterative Self-Auditor feedback.
Figure 7: Progressive reduction of error types in the SymDiag pipeline through iterative Self-Auditor feedback.
Effect of base model scale on overall faithfulness detection F1. Solid bars compare GPTOSS-120B and GPTOSS-20B across three methods; dashed lines indicate Answer Matching and Reward Model baselines.
Figure 8: Effect of base model scale on overall faithfulness detection F1. Solid bars compare GPTOSS-120B and GPTOSS-20B across three methods; dashed lines indicate Answer Matching and Reward Model baselines.
查看结构化数据
任务指标本文基线提升
忠实性检测（240 条人工审核实例，AIME24/25、MATH、AR-LSAT、LogiDed、GPQA、MMLU、MMLU-Pro 八数据集合集） F1 70.7（SymDiag，判官 GPTOSS-120B） LLM-as-Judge 66.2 / LogicReward 62.8 / Answer Matching 57.7 / Reward Model 57.0 较最强基线 +4.5 分，较答案匹配 +13.0 分
诊断引导多轮修复（8 个基准，默认 4 轮） 任务准确率（逐轮学习曲线） 全部 8 个数据集上增速与终值均为最佳且持续增益（如 AR-LSAT 约 89%→93%，MMLU-Pro 约 76%→79.5%） LLM-as-Judge 早期饱和；Reward Model/LogicReward 信号噪声大、不可定位；Answer Matching 几乎无增益 修复样本效率与最终性能均为五方法第一（Figure 4）
组件消融（总体检测） F1 完整系统 70.7；去步级符号验证 60.2；去 Self-Auditor 61.4；去批判性重述 62.8；去形式翻译 65.1 完整 SymDiag 70.7 各组件贡献 5.6–10.5 分，步级符号验证（−10.5）与 Self-Auditor（−9.3）最关键
Self-Auditor 管线自净化（3 轮迭代审计） Passed 比例 / 管线总错误率 53.4%→81.4% / 46.6%→18.6%（翻译错误 20.1%→近零，执行失败约 5.5%→<1%） 无审计的初始管线状态 剩余错误以不可约的逻辑级批判失败为主，而非翻译噪声
判官模型规模敏感性（GPTOSS-120B → 20B） 总体检测 F1 SymDiag 70.7→66.9 LLM-as-Judge 66.2→61.2；Logic Reward 62.8→58.4；Answer Matching 57.7 与 Reward Model 57.0 不随规模变化 缩水后仍保持最大领先幅度，方法对判官规模相对鲁棒

局限与改进

作者承认的局限：选用 Prolog 而非 Lean/Coq，换来轻量通用但放弃了领域形式库，对高深数学的完整形式化能力有限；对欠规范自然语言仍敏感，需要更强或混合验证器；自动语料 437,792 条靠 LLM 多数投票构造，主实验只用了 240 条金标。我补充的观察：(1) 每个数据集仅 30 条金标，统计功效低，F1 数分的波动可能仍在噪声范围内；(2) 修复实验未报告多次运行的方差，LLM 采样随机性下 1–2 分差异说服力有限；(3) 诊断与反馈生成都依赖 GPTOSS-120B 强判官，系统成本是多次大模型调用加求解器时间，论文未报告延迟与费用，而答案匹配基线几乎免费，成本公平性存疑；(4) 平局保守判不忠实会推高假阳性，且 Faithful 占 56.7% 的类别构成下 F1 可能偏乐观；(5) 未与 Math-Shepherd 等自动化标注 PRM 的检测能力直接对比。

独立分析的弱点

独立分析三点弱点。其一，双编码一致性审计隐含假设“两分支一致⇒翻译正确”，但两个分支由同一个生成器 LLM 产生，会共享系统性误读——例如同错一个量词辖域时审计无法发现；改进方向是引入异构第三分支（不同底座模型或规则模板），或让求解器把符号程序反译回自然语言做双向对照。其二，步骤切分本身由 LLM 完成，若一步里塞进多个逻辑动作，蕴含检查粒度天然变粗，定位精度受限；可让 Self-Auditor 同时评估切分质量并自动细分过大的步骤。其三，诊断证据只服务于推理时修复、不改模型权重，同类错误会在下一条轨迹上重犯；论文已构造 437,792 条自动诊断语料，却未把它蒸馏回被诊断模型或用于训练奖励模型，监督信号被浪费。此外 Figure 7 显示剩余错误以“逻辑级批判失败”为主，说明批判检查自身也有不可约的错误率，需要人工抽检机制兜底。

未来方向

作者提出的方向：把符号后端扩展到更强或混合验证器；提升对欠规范、歧义自然语言的鲁棒性；利用诊断证据训练“诊断感知”的奖励模型与推理监督器，并结合高效微调与元学习范式。基于其成果可自然延伸：① 用 43.7 万条自动诊断语料做步骤级 RL 奖励或 PRM 蒸馏，让被诊断模型内化“避免规则幻觉与前提缺失”，形成诊断-训练闭环；② 按误差热图揭示的规模相关失败模式设计自适应监督——小模型重点补算术与前提追踪约束，大模型重点防过度泛化；③ 构建 Prolog 快速门控 + Lean/Coq 深度验证的分层架构，兼顾成本与严谨性；④ 把诊断范式迁移到 agent 长程任务（工具调用、代码生成）的轨迹审计；⑤ 设计人机协同实验，量化符号证据对人类审查者核查 CoT 效率的提升。

复现评估

复现难度中等偏高。有利条件：符号后端是开源 SWI-Prolog；所有底座与判官均为开放权重（Llama-3.2-1B、Qwen3-1.7B/8B、GPTOSS-20B/120B）；奖励基线（NVIDIA Qwen-3-Nemotron-32B-Reward）有公开 HF 权重；方法细节充分——状态表示、双分支编译、Self-Auditor 的两个检查、七类错误分类法都有明确算法描述，Figure 2 还给出可对照的完整运行示例。不利条件：论文未见代码或数据发布链接；金标与 43.7 万条自动语料的标签由特定判官 LLM 多数投票产生，完全对齐需重跑整条采样与投票管线；240 条金标虽小但需逐条人工审计（每个数据集约 30 条），人力不可省；每条实例要跑双编码翻译 + 语法检查 + 求解器验证 + 最多 4 轮修复，GPU 调用量可观。有经验的团队复现主结果表约需 1–2 周，完整复刻语料构造则需数周。

论文图表

Paradigms for evaluating chain-of-thought (CoT) reasoning. Outcome- and process-level approaches treat verification as scoring... SymDiag introduces a diagnosis-level paradigm, performing symbolic checks to localize reasoning failures and produce verifiable diagnostic evidence, enabling targeted repair.
Figure 1: Paradigms for evaluating chain-of-thought (CoT) reasoning. Outcome- and process-level approaches treat verification as scoring... SymDiag introduces a diagnosis-level paradigm, performing symbolic checks to localize reasoning failures and produce verifiable diagnostic evidence, enabling targeted repair.

对比三代 CoT 评估范式：结果级（答案匹配，仅 1 比特对错反馈）、过程级（LLM-as-Judge、奖励模型，给标量或自然语言反馈）与本文提出的诊断级——对推理轨迹做符号检查，定位失败步骤并输出可验证证据链，支持针对性修复。

一图看清本文的定位与差异化主张：不是“更好的验证器或奖励”，而是范式升级，是理解全文动机的入口。

Table 1: Faithfulness detection performance (F1) across datasets and overall. All results are evaluated on the manually audited diagnostic subset described in Section 3.4.

五种方法在 8 个数据集及总体的忠实性检测 F1（对应柱状图：数学/逻辑/科学/通识四域分组）：SymDiag 总体 70.7 最佳，超过 LLM-as-Judge 66.2、LogicReward 62.8、Answer Matching 57.7、Reward Model 57.0；在 AR-LSAT、LogiDed、MMLU 等逻辑与通识域领先幅度最大。

主结果表：量化支撑“符号化逐步诊断比结果匹配、主观评判与标量奖励更能识别不忠实推理”这一核心结论。