Eidoku: A Neuro-Symbolic Verification Gate for LLM Reasoning via Structural Constraint Satisfaction

📄 arXiv: 2512.20664v1 📥 PDF

作者: Shinobu Miya

分类: cs.AI, cs.LO

发布日期: 2025-12-19

💡 一句话要点

Eidoku：通过结构约束满足实现LLM推理的神经符号验证门

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 推理验证 约束满足问题 神经符号 幻觉检测

📋 核心要点

  1. 现有基于概率的LLM验证方法难以检测高概率但结构不一致的幻觉。
  2. 提出Eidoku，将LLM推理验证建模为约束满足问题，基于结构违反成本进行可行性检查。
  3. 实验表明，Eidoku能有效拒绝“平滑的谎言”，为生成推理提供神经符号健全性检查。

📝 摘要（中文）

大型语言模型(LLMs)经常产生幻觉，即模型本身赋予这些陈述很高的可能性，这暴露了基于概率的验证的一个根本局限性。这表明幻觉通常不是一个低置信度的现象，而是结构一致性的失败。本文将LLM推理的验证重新定义为一个约束满足问题(CSP)，该问题独立于生成可能性运行。验证不是优化统计上的合理性，而是被建模为基于结构违反成本的可行性检查——将候选推理步骤嵌入到上下文图结构中所需的计算成本。我们定义了一个由三个代理组成的总体成本函数：(i)图连通性(结构)，(ii)特征空间一致性(几何)，和(iii)逻辑蕴含(符号)。至关重要的是，验证是通过一个轻量级的System-2门Eidoku执行的，它拒绝超过上下文校准成本阈值的候选者。该阈值不是学习得到的，而是从上下文的内在统计数据中导出的，避免了特别的启发式方法。我们证明了这种方法成功地拒绝了“平滑的谎言”——那些高度可能但结构上断开的陈述——而基于概率的验证器原则上无法检测到这些陈述。我们在一个受控的诊断数据集上的实验表明，显式地强制执行结构约束可以确定性地拒绝这种特定类型的幻觉，从而为生成推理提供神经符号健全性检查。

🔬 方法详解

问题定义：大型语言模型在推理过程中会产生幻觉，即生成看似合理但与上下文或事实不符的内容。现有的基于概率的验证方法，即使模型对这些错误陈述赋予高置信度，也难以有效识别这些“平滑的谎言”，因为它们缺乏对结构一致性的考量。

核心思路：论文的核心思路是将LLM推理的验证过程转化为一个约束满足问题（CSP）。通过评估将候选推理步骤嵌入到上下文图结构中的“结构违反成本”，来判断其合理性。这种方法不依赖于LLM自身的概率输出，而是关注推理步骤与上下文的结构关系，从而能够检测出那些高概率但结构上不一致的幻觉。

技术框架：Eidoku作为一个轻量级的System-2门，其验证流程主要包含以下几个阶段：1. 构建上下文图结构，表示已知的知识和信息。2. 将候选推理步骤嵌入到该图中。3. 计算结构违反成本，该成本由三个代理组成：图连通性（结构）、特征空间一致性（几何）和逻辑蕴含（符号）。4. 将计算得到的总成本与一个上下文校准的阈值进行比较。如果成本超过阈值，则拒绝该候选推理步骤。

关键创新：该论文最重要的创新在于将LLM推理验证问题转化为一个结构约束满足问题，并提出了基于结构违反成本的验证方法。与传统的基于概率的验证方法不同，Eidoku关注推理步骤与上下文的结构关系，能够有效检测高概率但结构不一致的幻觉。此外，Eidoku的阈值不是通过学习得到的，而是从上下文的内在统计数据中导出的，避免了引入额外的启发式规则。

关键设计：结构违反成本是Eidoku的关键设计。它由三个部分组成：1. 图连通性：衡量候选推理步骤与上下文图的连接程度。2. 特征空间一致性：衡量候选推理步骤在特征空间中与上下文的相似度。3. 逻辑蕴含：衡量候选推理步骤是否符合逻辑规则。这三个部分共同构成了一个综合的评估指标，用于判断候选推理步骤的合理性。阈值校准是另一个关键设计，它基于上下文的内在统计数据，避免了人工设定阈值的主观性。

📊 实验亮点

实验结果表明，Eidoku能够成功拒绝那些高概率但结构上断开的“平滑的谎言”，而传统的基于概率的验证器无法检测到这些错误。在受控的诊断数据集上，Eidoku通过显式地强制执行结构约束，实现了对特定类型幻觉的确定性拒绝，为生成推理提供了一种有效的神经符号健全性检查。

🎯 应用场景

该研究成果可应用于各种需要LLM进行推理的场景，例如问答系统、对话系统、知识图谱构建等。通过Eidoku的验证，可以有效减少LLM产生的幻觉，提高系统的可靠性和准确性。未来，该方法可以进一步扩展到更复杂的推理任务中，并与其他验证技术相结合，构建更强大的LLM验证体系。

📄 摘要（原文）

Large Language Models (LLMs) frequently produce hallucinated statements that are assigned high likelihood by the model itself, exposing a fundamental limitation of probability-based verification. This suggests that hallucination is often not a low-confidence phenomenon, but a failure of structural consistency. In this work, we reformulate the verification of LLM reasoning as a Constraint Satisfaction Problem (CSP) operating independently of the generation likelihood. Rather than optimizing for statistical plausibility, we model verification as a feasibility check based on structural violation cost -- the computational cost required to embed a candidate reasoning step into the contextual graph structure. We define a total cost function composed of three proxies: (i) graph connectivity (structural), (ii) feature space consistency (geometric), and (iii) logical entailment (symbolic). Crucially, verification is performed via a lightweight System-2 gate, Eidoku, which rejects candidates exceeding a context-calibrated cost threshold. The threshold is not learned but is derived from the intrinsic statistics of the context, avoiding ad hoc heuristics. We demonstrate that this approach successfully rejects ``smooth falsehoods'' -- statements that are highly probable yet structurally disconnected -- that probability-based verifiers are principally incapable of detecting. Our experiments on a controlled diagnostic dataset show that explicitly enforcing structural constraints allows for the deterministic rejection of this specific class of hallucinations, serving as a neuro-symbolic sanity check for generative reasoning.