K-文化的一切——从回归到 K-美妆，发送到您的邮箱订阅邮件

METAL MEDIA

SymDiag: Explainable Diagnosis for LLM Reasoning via Neuro-Symbolic Verification

arXiv:2608.087862026-08-08

一套用逻辑程序找出AI推理过程哪里出错、为何出错的诊断系统

SymDiag要解决的问题是:大语言模型给出的推理过程(思维链)即便最终答案正确,中间步骤也可能逻辑不成立。它把自然语言推理翻译成两套独立的Prolog逻辑程序,逐步检查每一步是否自相矛盾或结论没有依据,并用一个自我审计模块区分是真正的推理错误还是翻译过程带来的噪声。在覆盖数学、逻辑、科学和常识推理、经人工核验的240个样本上,该方法比现有方法更能检测出不可靠的推理,也更能有效引导多轮修正。

METAL MEDIA 解读图

SymDiag 两阶段诊断-修复流程

证据状态已报告实测结果

  1. 输入:大语言模型的推理过程接收问题、大语言模型生成的分步思维链以及最终答案。
  2. 双路逻辑翻译将自然语言推理分别编译成两套独立的Prolog程序:一套形式化翻译,一套更严格的批判性重述。
  3. 自我审计检查对比两套翻译程序,判断表面上的逻辑问题究竟是真正的推理缺陷还是翻译噪声,只让通过审计的状态进入下一步。
  4. 逐步符号验证用SWI-Prolog检查每一步是否自相矛盾(可满足性)以及其结论是否真能从前提推出(蕴含关系),给出通过/失败判定及反例、矛盾等证据。
  5. 依据证据修复根据失败步骤和证据,要求大语言模型只修补该步骤或从出错处开始重写后续推理,并可多轮反复进行。
这是 METAL MEDIA 制作的解读图，并非论文作者提供的原图。

他们做了什么

  1. 现有做法的问题在于:只比对最终答案、让LLM充当'裁判'给出主观点评、或者只给一个分数的奖励模型,都无法指出多步推导中具体是哪一步出了问题。
  2. SymDiag把自然语言思维链分别编译成两套独立生成的Prolog逻辑程序(一套是形式化翻译,另一套是更严格的'批判性重述'),再用SWI-Prolog求解器逐步检查每一步是否与之前信息自洽(可满足性)、其声称的结论是否真的能被推出(蕴含关系)。
  3. 系统专门设置了一个'自我审计'模块,对比两套翻译程序,判断检测到的逻辑问题究竟是真正的推理缺陷,还是把自然语言翻译成逻辑形式过程中产生的噪声。
  4. 一旦某一步验证失败,系统会给出反例、矛盾证据或缺失前提等具体证据,并据此要求模型只修补该步骤,或从出错处开始重写后续全部推理,如此反复进行诊断-修复循环。
  5. 评测使用了人工审核过的240个样本,涵盖数学(如AIME)、逻辑(AR-LSAT)、科学(GPQA)和常识推理(MMLU)四个领域的基准。
Figure 1. Paradigms for evaluating chain-of-thought (CoT) reasoning. Outcome- and process-level approaches treat verification as scoring, judging only final answers or subjective plausibility. 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, judging only final answers or subjective plausibility. SymDiag introduces a diagnosis-level paradigm, performing symbolic checks to localize reasoning failures and produce verifiable diagnostic evidence, enabling targeted repair.
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 to distinguish TranslationError from ReasoningError, and SWI-Prolog performs step-level satisfiability/consistency checks to output a faithful/unfaithful decision with verifiable evidence (e.g., counterexamples, inconsistency witnesses, missing-premise indicators). 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 to distinguish TranslationError from ReasoningError, and SWI-Prolog performs step-level satisfiability/consistency checks to output a faithful/unfaithful decision with verifiable evidence (e.g., counterexamples, inconsistency witnesses, missing-premise indicators). Stage II (Repair): SymDiag uses localized failures and evidence to prompt an LLM to generate a repaired reasoning trace that is solver-consistent.

研究结果

  • 在人工核验的240个样本上,SymDiag在所有数据集上取得了最高的整体F1分数(70.7),优于仅比对答案、LLM裁判和基于奖励模型的方法,在检测不可靠推理上表现更好。
  • 在AR-LSAT、LogiDed、MMLU等逻辑与常识推理基准上差距尤为明显,因为这些任务中最终答案正确、但中间推理无效的情况较多,而基线方法难以发现。
  • 在多轮修正实验中,SymDiag在各轮修正中都取得了比所有基线更快、更大的准确率提升;仅比对答案的方法几乎没有改进,奖励模型和LogicReward给出的信号带噪声且难以定位,LLM裁判早期略有提升但很快趋于饱和。
  • 消融实验显示,去掉逐步符号验证环节导致性能下降最大;去掉自我审计模块也会明显降低性能,因为翻译产生的偏差会被误判为推理错误。
  • 在自我审计的多轮反馈下,总体错误率从46.6%开始逐步下降,通过率从53.4%提升到81.4%;翻译错误从20.1%在三轮内降到接近零,执行失败从5.5%降到1%以下。
Figure 3. 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.
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, reflecting the benefit of localized, verifiable error evidence for targeted correction.
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, reflecting the benefit of localized, verifiable error evidence for targeted correction.

可应用场景

  • 检查大语言模型在数学、逻辑、科学或常识问题上给出的解答,找出那些答案正确但推理逻辑站不住脚的情况。
  • 构建自动化修复流程,在模型答案或推理过程存疑时,自动判断是只修补某一步还是重写整段推理。
  • 分析不同规模模型的错误类型差异(例如小模型多犯计算错误、大模型更容易凭空套用规则),据此设计针对模型规模的训练信号。
Figure 5. Ablation results on overall faithfulness detection (F1).
Figure 5. Ablation results on overall faithfulness detection (F1).
Figure 6. Normalized distribution of reasoning error types identified by SymDiag.
Figure 6. Normalized distribution of reasoning error types identified by SymDiag.

局限与待验证事项

  • 评测仅基于人工核验的240个样本,在完整的自动构建语料库(超过43.7万条)或更广泛的实际应用场景中的表现尚未单独报告。
  • 对于极其模糊或非结构化、难以转换成逻辑形式的自然语言推理,自我审计模块可能无法完全应对。
  • 诊断、错误分类和反馈生成依赖较强的判定模型(GPTOSS-120B);换成更小的判定模型(GPTOSS-20B)后,所有方法的整体F1都会下降,说明系统效果依赖判定模型的能力。
  • 论文提出的扩展到更强或混合的逻辑验证后端、提升对模糊语言的鲁棒性、利用诊断证据训练诊断感知型奖励模型等方向,均属于尚未开展的未来工作。
Figure 7. Progressive reduction of error types in the SymDiag pipeline through iterative Self-Auditor feedback. Translation Errors and Execution Failures are rapidly eliminated, leading to a steady increase in the overall pass rate.
Figure 7. Progressive reduction of error types in the SymDiag pipeline through iterative Self-Auditor feedback. Translation Errors and Execution Failures are rapidly eliminated, leading to a steady increase in the overall pass rate.
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. Larger base models consistently improve all methods, and SymDiag maintains the highest F1 under both model scales.
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. Larger base models consistently improve all methods, and SymDiag maintains the highest F1 under both model scales.

为什么重要

如果模型能'蒙对答案却推理错误'而无人察觉,这对在高风险场景中部署大语言模型是个严重隐患。这项研究表明,提供可核实、可定位的错误证据,比单纯打分或笼统点评更能有效推动推理过程的迭代修正。

本文术语

  • 思维链(Chain-of-Thought, CoT) · 大语言模型在给出最终答案前,逐步写出的推理过程
  • 神经符号方法(neuro-symbolic) · 把神经网络(大语言模型)和符号逻辑程序(如Prolog)结合起来,让推理过程变得可核验的方法
  • 可满足性/蕴含检查 · 用逻辑方法检验一组条件能否同时成立,以及某个结论是否真的能从前提推导出来
  • 自我审计(Self-Auditor) · 用来判断检测到的逻辑问题是真正的推理错误,还是把自然语言翻译成逻辑形式时产生的偏差的内部检查机制
  • 过程奖励模型(PRM) · 给推理的每个中间步骤打分的模型,只给出分数而不解释具体哪里、为何出错

论文原文摘要（英文）

Large language models (LLMs) increasingly serve as data-driven reasoners, yet their chains-of-thought (CoT) can be unfaithful even when final answers are correct. Most existing ``verification'' signals are not diagnostic: answer matching observes only the outcome, LLM-as-judge provides subjective and non-verifiable critiques, and scalar rewards (e.g., PRMs/RMs) offer little insight into where a multi-step derivation fails.We propose SymDiag, a neuro-symbolic framework that reframes reasoning verification as structured failure diagnosis. SymDiag translates natural-language CoT into symbolic constraints and performs step-level satisfiability/entailment checks to (i) localize failing steps and (ii) produce verifiable diagnostic evidence, including counterexamples, inconsistency witnesses, and missing-premise indicators. A central challenge is that apparent ``logic violations'' can be caused either by genuine reasoning defects or by neural-to-symbolic translation noise. SymDiag therefore incorporates a Self-Auditor that disentangles TranslationError from ReasoningError via dual symbolic encodings consistency checks, enabling robust diagnosis under partial observability. Across diverse mathematical, logical, scientific, and general reasoning benchmarks, SymDiag improves detection of unfaithful reasoning and provides substantially more effective feedback for multi-round reasoning repair than outcome-only verification and LLM-based judging, offering a principled foundation for trustworthy and scalable reasoning diagnosis.

作者 · Wenyao Cui

在 arXiv 阅读

最新论文

全部论文 →

METAL MEDIA 最新报道

图片来源： Wenyao Cui et al., arXiv:2608.08786, CC BY 4.0