SymDiag：基于神经符号验证的LLM推理可解释诊断

Hugging Face Daily Papers 论文
llm-reasoning neuro-symbolic verification chain-of-thought diagnosis satisfiability

摘要

SymDiag 是一种神经符号框架，将思维链推理转化为符号约束，并执行步骤级可满足性检查，以定位 LLM 推理中的失败，从而区分翻译错误与推理错误。

大型语言模型（LLM）日益成为数据驱动的推理者，但它们的思维链（CoT）即使最终答案正确，也可能不忠实。大多数现有的“验证”信号并不是诊断性的：答案匹配仅观察结果，LLM 作为评判者提供主观且不可验证的批评，而标量奖励（如 PRM/RM）对多步推导在哪一步失败提供的洞察很少。我们提出 SymDiag，一个神经符号框架，将推理验证重构为结构化失败诊断。SymDiag 将自然语言 CoT 翻译成符号约束，并执行步骤级可满足性/蕴含检查，以（i）定位失败步骤，（ii）生成可验证的诊断证据，包括反例、不一致性见证和缺失前提指示。一个核心挑战是，表面上的“逻辑违规”可能由真正的推理缺陷或神经到符号的翻译噪声引起。因此，SymDiag 融入了自审计器（Self-Auditor），通过双重符号编码一致性检查来区分 TranslationError 和 ReasoningError，从而在部分可观测性下实现鲁棒诊断。在多种数学、逻辑、科学和通用推理基准上，SymDiag 比仅看结果的验证和基于 LLM 的评判更能提高对不忠实推理的检测，并为多轮推理修复提供更有效的反馈，为可信且可扩展的推理诊断提供了原则性基础。
查看原文
查看缓存全文

缓存时间: 2026/08/12 08:23

论文页面 - SymDiag：通过神经符号验证对LLM推理进行可解释诊断

来源：https://huggingface.co/papers/2608.08786

摘要

SymDiag 将推理验证重新定义为结构化故障诊断：通过将思维链转化为符号约束，执行逐步可满足性检查，并将翻译错误与推理错误区分开来，从而提供可验证的诊断证据。大型语言模型（LLMs）越来越多地充当数据驱动的推理器，但它们的思维链 (https://huggingface.co/papers?q=chains-of-thought)（CoT）即使最终答案正确也可能不忠实。大多数现有的“验证”信号不具备诊断性：答案匹配只观察结果，LLM 作为评判者提供主观且不可验证的批评，而标量奖励（例如 PRMs/RMs）对多步推导在哪一步失败几乎没有洞察。我们提出 SymDiag，一个神经符号框架 (https://huggingface.co/papers?q=neuro-symbolic%20framework)，将推理验证重新构建为结构化故障诊断。SymDiag 将自然语言 CoT 转化为符号约束 (https://huggingface.co/papers?q=symbolic%20constraints)，并执行逐步可满足性 (https://huggingface.co/papers?q=satisfiability)/蕴含 (https://huggingface.co/papers?q=entailment) 检查，以（i）定位失败的步骤，（ii）产生可验证的诊断证据，包括反例 (https://huggingface.co/papers?q=counterexamples)、不一致见证 (https://huggingface.co/papers?q=inconsistency%20witnesses) 和缺失前提指标 (https://huggingface.co/papers?q=missing-premise%20indicators)。一个核心挑战是，表面上的“逻辑违规”可能由真正的推理缺陷或神经到符号的翻译噪声引起。因此，SymDiag 纳入了一个 Self-Auditor (https://huggingface.co/papers?q=Self-Auditor)，通过双符号编码 (https://huggingface.co/papers?q=dual%20symbolic%20encodings) 一致性检查将 TranslationError (https://huggingface.co/papers?q=TranslationError

相似文章

面向数据敏感领域的LLM输出的神经符号验证（扩展预印本）

arXiv cs.AI

本文提出了一种针对高风险领域LLM输出的神经符号验证架构，结合形式化符号方法与神经语义分析。在一个医疗器械损伤评估系统上进行的评估显示，该架构对结构化实体的幻觉检测率超过83%，语义虚构的检测率达72%，报告创建时间缩短30%。

模拟、推理、决策：基于LLM的科学推理驱动仿真决策

arXiv cs.AI

密歇根大学的研究人员推出了MechSim——一个基于机制的神经符号推理框架，使LLM智能体能够对科学模拟器的内部假设、依赖关系和执行行为进行推理，而非将其视为黑盒。该框架在医疗、金融和公共政策等高风险领域提升了解释质量与决策可靠性。

逻辑正则化验证器激发大语言模型的推理能力

arXiv cs.CL

介绍了 LoVer，一种使用逻辑规则（否定一致性、组内一致性和组间一致性）来在无标签数据下提升大语言模型推理能力的无监督验证器，在推理基准测试中达到了接近监督验证器的性能。