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

# 面向数据敏感领域的 LLM 输出的神经符号验证（扩展预印本）
来源：https://arxiv.org/html/2605.26942
11机构：班贝格大学，德国班贝格 22机构：柏林自由大学，德国柏林
电子邮件：[email protected], [email protected]

###### 摘要

在高风险领域部署的 LLM 面临根本性的可靠性挑战：幻觉、不一致性和隐私漏洞会引入不可接受的风险，尤其是在错误会带来法律、财务或安全后果的场景。本文提出了一种混合验证架构，将形式化符号方法与神经语义分析相结合，为 LLM 生成的内容提供互补性保障。

该架构采用逻辑推理进行输入验证，利用完备性属性为结构化需求提供可判定的保证。在输出验证方面，基于嵌入的语义相似度检测可在形式化方法缺乏表达能力的地方检测上下文幻觉。这种分离通过一个并行的、基于参与者的流水线实现，解决了基于提示的自我验证方法（该方法继承了产生幻觉的分布偏差）的局限性。

所提出的架构和类型感知验证方法通过 HAIMEDA 进行验证，HAIMEDA 是一个通过行动设计研究开发的实际医疗设备损伤评估报告生成系统。评估结果表明，对于结构化实体的幻觉检测率超过 83%，对于语义编造内容的检测率达到 72%，同时报告创建时间减少 30%，这表明神经符号架构可以为数据敏感领域的 LLM 部署提供原则性的安全保障。

## 1 引言

大语言模型（LLM）在各种任务中展现出了强大的能力，然而其在高风险领域的应用仍然充满挑战。在信息准确性至上的专业环境中，例如医疗诊断、法律审查和监管事务，纯神经方法存在显著风险。即使是当前最先进的模型，幻觉（即生成可信但虚假的信息）的发生率仍高达 3% 到 10%[20 (https://arxiv.org/html/2605.26942#bib.bib1),22 (https://arxiv.org/html/2605.26942#bib.bib2)]。对于错误会带来法律、财务或安全后果的领域，这些缺陷是不可接受的。

除了准确性担忧，许多数据敏感工作流需要本地处理，以满足监管、机构或客户对数据传输的限制要求[13 (https://arxiv.org/html/2605.26942#bib.bib3),23 (https://arxiv.org/html/2605.26942#bib.bib4)]。这些问题指向了通用 LLM 的一个局限性——无论其规模大小，它们都缺乏为专业化场景保留信息完整性的能力。像检索增强生成（RAG）或思维链提示设计等方法所能提供的有效性，无法为高风险应用等专业化场景提供必要的保证。一种更具原则性的方法需要整合不同人工智能范式的互补优势。

混合人工智能系统通过结合亚符号方法（即擅长模式识别、自然语言处理和应对新输入的神经网络）与符号方法（提供显式推理、规则执行和可验证保证）来解决这一差距[15 (https://arxiv.org/html/2605.26942#bib.bib5),27 (https://arxiv.org/html/2605.26942#bib.bib6)]。这种整合使得架构能够系统性地验证 LLM 生成的内容是否符合领域约束、事实数据库和逻辑一致性要求，然后才将其呈现给最终用户。

尽管人们对混合人工智能潜力的认识日益增强，但实践者仍面临架构集成方面的差距。现有研究已经产生了许多有价值的单项技术，包括神经符号推理系统、验证框架和特定领域架构，但针对数据敏感领域、经过验证的端到端验证架构仍然稀缺。关于如何在系统层面结合符号和亚符号组件以保持信息完整性的问题，仍然缺乏系统性的答案[4 (https://arxiv.org/html/2605.26942#bib.bib7),33 (https://arxiv.org/html/2605.26942#bib.bib8)]。

本文针对数据敏感领域可验证的 LLM 部署做出了两个技术贡献。首先，我们提出了一种用于数据敏感领域 LLM 辅助生成的验证架构，该架构结合了基于 Tableaux 的输入验证、基于参与者的故障隔离，以及一种类型感知的后生成验证方法（对结构化声明进行确定性符号检查，对自由文本声明进行语义相似度评分）。其次，我们通过 HAIMEDA（一个本地部署的医疗设备评估报告生成系统）验证了该架构，该系统展示了对无根据内容的强大检测能力，并显著改进了工作流程。

## 2 相关工作

涉及 LLM 生成内容混合验证的研究涉及三个领域：神经符号架构、幻觉检测方法和输出验证系统。此外，对人工智能系统的实施导向研究有助于理解此类架构在实践中是如何构建的。

##### 神经符号人工智能架构。

神经符号集成将神经学习与符号推理相结合[15 (https://arxiv.org/html/2605.26942#bib.bib5)]。关键框架包括 Logic Tensor Networks[3 (https://arxiv.org/html/2605.26942#bib.bib9)]、DeepProbLog[26 (https://arxiv.org/html/2605.26942#bib.bib10)] 和 Scallop[25 (https://arxiv.org/html/2605.26942#bib.bib11)]。尽管这些模型在算法集成领域很有用，但它们本质上意味着架构修改或训练，这限制了它们对预训练 LLM 的适应性。

##### LLM 幻觉检测。

检测 LLM 输出中的事实错误仍然具有挑战性。自一致性方法[37 (https://arxiv.org/html/2605.26942#bib.bib12)] 会采样多个回复并衡量一致性，而检索增强验证[14 (https://arxiv.org/html/2605.26942#bib.bib13)] 则会将输出与外部知识库进行交叉引用。然而，这些方法继承了被验证模型的分布偏差[20 (https://arxiv.org/html/2605.26942#bib.bib1),22 (https://arxiv.org/html/2605.26942#bib.bib2)]，从而限制了在高风险领域的可靠性。知识编辑技术[19 (https://arxiv.org/html/2605.26942#bib.bib14)] 试图进行训练后纠正，但难以处理复杂或依赖上下文的幻觉。

##### 输出验证与防护栏。

运行时验证工具提供了实用的安全保障：Guardrails AI[10 (https://arxiv.org/html/2605.26942#bib.bib15)] 和 NeMo Guardrails[31 (https://arxiv.org/html/2605.26942#bib.bib16)] 实现了可编程验证，而约束解码[38 (https://arxiv.org/html/2605.26942#bib.bib17)] 则强制结构合规。这些方法解决了格式和策略检查问题，但针对源内容的语义验证能力有限。特定领域系统如 TrustKG[8 (https://arxiv.org/html/2605.26942#bib.bib18)] 和 Teriyaki[5 (https://arxiv.org/html/2605.26942#bib.bib19)] 在专业上下文中展示了验证能力，但仍属点解决方案，缺乏可推广的架构模式。

总体而言，当前的技术水平已建立了高效的神经符号推理、幻觉缓解和运行时保护方法。然而，一个综合性的架构方法——结合形式化验证和语义验证以用于数据敏感领域的 LLM 部署——仍然缺失。

## 3 验证架构与设计原理

在数据敏感领域部署 LLM 会引发验证挑战，这些挑战指导了所提架构的设计。输入验证在投入昂贵的推理之前，受益于可判定的保证。输出验证需要符号和神经分析两种机制，最好具有故障隔离以防止级联故障。在受监管领域，隐私考虑通常需要本地部署而非基于云端的 API。我们的架构通过结合基于 Tableaux 的输入约束验证、用于故障隔离并行处理的参与者模型并发，以及用于输出验证的神经符号集成来应对这些挑战。

该架构遵循四个设计原则：本地优先处理以实现数据主权[23 (https://arxiv.org/html/2605.26942#bib.bib4)]、符号组件与神经组件的模块化分离[30 (https://arxiv.org/html/2605.26942#bib.bib20)]、基于参与者的故障隔离结合函数不可变性以实现鲁棒性[2 (https://arxiv.org/html/2605.26942#bib.bib21),17 (https://arxiv.org/html/2605.26942#bib.bib22),21 (https://arxiv.org/html/2605.26942#bib.bib23)]，以及类型感知的声明验证（即对结构化声明进行确定性符号检查，对自由文本声明进行神经语义检查）[15 (https://arxiv.org/html/2605.26942#bib.bib5),33 (https://arxiv.org/html/2605.26942#bib.bib8)]。

### 3.1 用于输入验证的 Tableaux 逻辑

数据敏感工作流中的输入验证是一个关于交互约束的一致性检查问题。在后续 HAIMEDA 中实例化的医疗设备评估工作流中，报告是逐节组装的，这些章节在验证需求上存在显著差异：有些主要是叙述性的，有些遵循技术模式，有些包含具有法律后果的评估，还有些主要用于记录支持性证据。因此，在任何 LLM 调用之前，必须检查强制性的元数据和矛盾状态，但具体的要求配置文件因目标章节而异。

这种可变性需要一个验证机制，该机制能够在一个单一的声明性方案中既表达累积性义务，也表达替代性满足路径。Tableaux 方法非常适合这一角色，因为它们将公式分解为必须同时成立的合取（α）义务，以及代表可接受替代方案的析取（β）分支。对于命题和可判定片段，这会产生可靠且完备的过程[9 (https://arxiv.org/html/2605.26942#bib.bib24),36 (https://arxiv.org/html/2605.26942#bib.bib25)]。

该架构将验证编码为声明性条件的可配置层级，因此高阶条件可以对低阶条件的结果进行推理。设 Call 表示当前章节配置文件中所有条件标识符的集合。*核心条件* C ⊆ Call 以编程方式评估原子谓词（例如，元数据存在性或最小标题质量）。*元条件* 和 *聚合条件* 形成高阶集合 H = Call \ C：元条件表达条件组之间的集合论关系，而聚合条件计算条件属性上的统计信息。

设 Csat ⊆ Call 表示观察到成立的条件，Creq ⊆ C 表示所需的核心条件，Cshould_sat 表示根据规则集预期成立的条件。*正集合* Cpos 包含观察和预期满足状态一致的条件，而 Cneg = Call \ Cpos 捕获极性不匹配；BuildPositiveSet 根据 Csat 和规则集的期望声明计算这种对齐。最后，Ceval 跟踪哪些条件已被处理，从而实现按先决条件排序的评估：仅当高阶条件 h ∈ H 所依赖的所有条件都已出现在 Ceval 中时，才对其进行评估。

然后，一个强制一致性门控检查条件 (Creq ∩ Ceval) ⊆ Cpos，这意味着所有已评估的所需条件必须正向对齐，同时一个聚合规则通过 |Cneg| ≤ τ 约束总的极性不匹配。这些规则超越了平面的 if-else 验证，因为其结果取决于动态构建的条件集合之间的关系。

因此，该领域本质上是集合论的：验证状态表示为一个命名条件 ID 集合的论域 U（C, Csat, Creq, Ceval, Cpos, Call）。Tableaux 分解直接映射到集合运算：α-展开表现为交集，β-展开表现为并集，否定表现为在 Call 上的补集[36 (https://arxiv.org/html/2605.26942#bib.bib25)]。这在生成之前产生了确定性、可审计的门控，同时保留了声明性的领域配置。算法 1 (https://arxiv.org/html/2605.26942#alg1) 总结了该引擎。上述的强制一致性门控充当硬停止（如果未满足则阻止生成），而聚合极性不匹配规则可以产生警告反馈而不阻塞，说明了在同一引擎内分级响应的机制。

算法 1 基于 Tableaux 的输入验证
1: 输入数据 I，规则集 R，包含核心条件 C 和高阶条件 H
2: // 阶段 1：核心条件的程序化评估
3: Csat ← {c ∈ C | Eval(c, I) = ⊤}
4: Creq ← {c ∈ C | c.required = ⊤}
5: Ceval ← InitializeEvaluatedSet(R, C)
6: // 阶段 2：条件关系上的 Tableaux 推理
7: Cpos ← BuildPositiveSet(Csat, R)
8: U ← {C, Csat, Creq, Ceval, Cpos} ⊳ 论域集合
9: for h ∈ H do
10:   if Prerequisites(h) ⊈ Ceval then continue
11:   φh ← BuildFormula(h, U) ⊳ 例如，Creq ⊆ Cpos
12:   ⟦φh⟧ ← TableauxSolve(φh, U) ⊳ α/β-分解
13:   if ⟦φh⟧ ≠ ∅ then
14:     Csat ← Csat ∪ {h}
15:   end if
16:   Ceval ← Ceval ∪ {h} ⊳ 记录已处理规则
17: end for
18: // 阶段 3：根据满足状态触发动作
19: for action a with trigger condition τa and event e ∈ {sat, unsat} do
20:   if (τa ∈ Csat) = (e = sat) then ⊳ 仅当实际满足状态