发表机构
Beijing Institute of Technology; Zhongguancun Academy; Xinjiang Future Enterprise Incubator Co., Ltd.; Institute of Automation, Chinese Academy of Sciences（北京理工大学; 中关村学院; 新疆未来企业孵化器有限公司; 中国科学院自动化研究所）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
SymDiag是一种神经符号框架，将LLM推理验证重构为结构化故障诊断，可定位推理故障步骤、分离翻译与推理错误，在多类基准中提升了不可靠推理检测与推理修复反馈效果。
AI 中文摘要
大型语言模型（LLM）日益成为数据驱动的推理器，但其思维链（CoT）即便最终答案正确也可能不可靠。现有多数“验证”信号不具备诊断性：答案匹配仅观测结果，LLM作为评判者提供主观且不可验证的批评，标量奖励（如PRMs/RMs）几乎无法洞察多步骤推导的问题。本文提出SymDiag，这是一个神经符号框架，将推理验证重构为结构化故障诊断。SymDiag将自然语言CoT转换为符号约束，并执行步骤级的可满足性/蕴含检查，以（i）定位故障步骤，（ii）生成可验证的诊断证据，包括反例、不一致见证和缺失前提指标。一个核心挑战是，表面的“逻辑违规”可能由真正的推理缺陷或神经到符号的翻译噪声导致。因此SymDiag集成了一个自我审计器，通过双重符号编码一致性检查将翻译错误与推理错误分离，从而在部分可观测性下实现鲁棒诊断。在数学、逻辑、科学及通用推理等多样基准测试中，SymDiag提升了不可靠推理的检测能力，且与仅基于结果的验证和基于LLM的评判相比，为多轮推理修复提供了更有效的反馈，为可信且可扩展的推理诊断提供了原则性基础。
英文摘要
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 \textbf{SymDiag}, a neuro-symbolic framework that \textbf{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.
