为 AI 智能体加上神经符号护栏：让答案可以被验证

Nearform – Latest from our Insights & Digital Community 2026-11-04T09:40:22.974840

2023 年 10 月，纽约市推出了 MyCity，一个聊天机器人，用来根据数千页官方指南回答企业主的问题。五个月后，The Markup 的记者问它，餐馆是否可以停止接受现金。它回答说：“是的，你可以让你的餐馆不收现金。纽约市没有任何法规要求企业必须接受现金作为支付方式。”而自 2020 年起，当地法律恰恰要求餐馆必须接受现金。

这样的回答可能具有法律效力。2024 年，加拿大一家法庭裁定，加拿大航空须为其网站聊天机器人承诺的退款负责，尽管这一承诺与该航空公司自身的政策相悖。

在 Nearform，我们基于当下的大语言模型（LLM）、检索和评估技术栈来构建智能体。对大多数问题来说，一个经过充分测试的智能体已经够用了。但当答案必须遵循成文规则时，还有一种更严谨的选择，而且它比用来检查它的那些模型还要古老。符号 AI 是这个领域中以显式逻辑为基础的分支，几十年来一直在用规则核验陈述。2010 年代深度学习吸引了大量关注，而与此同时，基于逻辑的工具正在验证芯片设计和飞行软件。

LLM 来自另一个分支，也就是从示例中学习的那一支。我们能否把这种逻辑与 LLM 配对，让它的答案按照本应遵循的规则接受检查？把成文政策转译成形式逻辑后，就可以用数学方法检查每一条 LLM 答案和智能体动作；一旦违反规则，检查程序会指出是哪条规则、由哪些值导致。

符号 AI 的来路

“人工智能”这个词，最早出现在一份 1956 年达特茅斯暑期研讨会的提案里。此后发展出的两条路线，与本文关系密切。

一条是符号 AI：把知识写成针对符号的明确规则，每个结论都能追溯到人可以逐条检查的规则和变量。另一条是神经网络：从样例中学习，这条路可以上溯到 1958 年 Frank Rosenblatt 的感知机。神经网络在很长一段时间里默默无闻，直到 2012 年，Geoffrey Hinton 在多伦多大学的团队用一个深度网络，以明显优势拿下 ImageNet 图像识别竞赛。今天的大语言模型（LLM）正是沿着这条路线发展起来的。

与此同时，基于逻辑的方法也一直在发展，只是常常不在“人工智能”的名下，而是藏在定理证明器、模型检测器和求解器里。本文示例用的是求解器：给它一组逻辑命题，它判断这些命题能否同时为真，要么返回让每条命题都成立的取值，要么给出证明，说明这样的取值不存在。写这种逻辑需要专家，所以形式化验证只在“一旦出错，代价远超验证成本”的场合使用。1994 年，Intel 因奔腾处理器的除法缺陷计提 4.75 亿美元，此后业界对浮点硬件大量引入形式化验证。2003 年，静态分析工具 Astrée 证明，空客 A340 的飞控软件不会产生任何运行时错误。

要比较“检查过”和“没检查过”的代码有何差别，最清楚的例子来自航天器。1997 年，NASA 团队对 Remote Agent 的一部分做了模型检测，找出五个错误。Remote Agent 是自主控制软件，后来在一次飞行实验中操控了“深空一号”探测器。1999 年，Remote Agent 正在操控探测器时，一个没有经过检测的兄弟子系统发生死锁，任务随之中断。团队事后报告称，这正是两年前已经发现过的那种缺陷模式。

神经符号 AI 是什么

神经符号 AI（Neurosymbolic AI）指的是把神经网络和符号推理结合起来的系统。研究人员研究这个思路已经超过二十年，2020 年的一篇论文把它称为人工智能的第三次浪潮。同一年，Henry Kautz 在国际人工智能促进协会（AAAI）年会上的一次演讲中，把这些方法归为六类。本文采用他的第三类（写作 Neuro | Symbolic），即神经网络和符号系统各自负责互补的任务，并通过彼此的输入输出交互。大语言模型（LLM）负责写出答案，由求解器判断这个答案是否成立。

LLM 改变了「谁来写逻辑」这件事——过去这活儿得由专家来做。现在，LLM 可以从策略文档里起草规则，策略负责人逐条审核，之后每一次回答都由求解器对照这些规则来检查。Amazon Bedrock Guardrails 从 2025 年起就提供了这套流程的托管版本，叫做自动推理检查（Automated Reasoning checks）。

检查是怎么做的

整个检查分三个阶段（如下图），只有第一个阶段需要人来参与。

神经检查示意图：每个策略版本只需起草并审核一次规则，之后每个回答或智能体的每个动作都要对照这些规则检查。

如果事实本身与规则矛盾，就没有可判断的对象，检查会将它们报告为不一致。

“可满足”是是非判断器无法表达的判定，在实践中却很常见，因为真实问题往往会遗漏事实。把它报成允许或拒绝都只是猜测，正确的做法是追问缺失的事实。

如今更常见的答案检查方式是 LLM-as-a-judge（让另一个模型充当裁判）：由第二个模型阅读答案和政策，判断答案是否合规。2023 年的一项研究让裁判模型给聊天机器人回答打分，发现 GPT-4 与人类偏好的吻合率超过 80%，大致相当于人与人之间的一致程度。研究还测量了偏差，比如偏好两个答案中的第一个或更长的那个。裁判模型能处理“合理”这类模糊措辞，逻辑做不到这一点，但它的判定仍是另一个模型的输出，可能以与被检查答案相同的方式出错。求解器的判定则来自政策负责人已审核的规则，相同逻辑下每次结果一致，并会指出背后的规则，尽管它只覆盖被翻译成逻辑的那部分内容。

下面我们一步步构建这个检查，看看实际效果。

把政策变成逻辑

我们用一个简单的差旅政策作为贯穿全文的示例。它由四句话组成：

这些示例使用 SMT（可满足性模理论），它在布尔逻辑的基础上加入了整数运算、时长等理论，因此规则里面可以谈金额和时长。SMT 的标准语言叫 SMT-LIB，语法借自 Lisp：每个表达式都是括号括起来的列表，运算符放在最前面。所以 (> costEur 1000) 表示 costEur 大于 1000，(and a b) 表示 a 和 b，(=> a b) 表示 a 蕴含 b：只要 a 成立，b 就必须成立。

同样的规则也可以换别的方式表达。答案集编程（ASP）配合 clingo 求解器，用类似 Prolog 的语法来写规则，适合建立在默认规则和例外之上的政策，也适合规划、产品配置这类搜索问题：求解器负责找出满足全部规则的组合。SMT 更适合做输出护栏（output guardrail），也就是在用户看到答案之前先对答案做一道检查。护栏需要判断：某条说法是能从规则推导出来的，还是与规则冲突，还是规则没有覆盖；SMT 求解器跑两次就能给出结论。

我们用的求解器是 Z3。微软研究院在 2008 年的一次验证领域会议上公开发表了它，从 2015 年起以 MIT 许可证开源。我们用 uv 来安装：执行 uv tool install z3-solver，就会把 z3 命令加到 PATH 里；后面那些 Python 脚本会把 Z3 声明为依赖，uv 在首次运行时自动拉取。先跑一次看看，用费用那句话，加上一个问题：

$ z3 -in <<'EOF'
(declare-const costEur Int)
(declare-const managerApproved Bool)
(declare-const tripApproved Bool)
(assert (=> (and (> costEur 1000) (not managerApproved)) (not tripApproved)))
(assert (= costEur 2500))
(assert (not managerApproved))
(assert tripApproved)
(check-sat)
EOF
unsat

declare-const 会创建一个带类型的变量，assert 声明一条必须成立的条件，check-sat 则问：这些条件能不能同时成立。输出 unsat（unsatisfiable 的缩写，意为不可满足）表示不能：一笔 2500 欧元、未经审批的差旅，不可能被批准。

用 Python 的 if 语句也能表达这条规则，一条规则配一个问题，足够了。但两者思路不同。Python 是指令式的：它按你写的顺序、拿你传入的值一步步执行。SMT-LIB 是声明式的：你只说明什么必须成立，求解器自己去判断存不存在一组取值能让全部条件同时满足——它会覆盖规则允许的所有情况，而不只是你碰巧测过的那几种。规则一多，这个差别就明显了。几十条相互影响的规则叠在一起，嵌套的 if 很快就难写对，更难维护；而声明式的策略始终是一份扁平的规则清单，每条都能单独增删改。

整套策略可以放进一个文件，policy.smt2：

(set-option :produce-unsat-cores true)   ; report which named rules conflict

; The facts a question can supply, and the outcomes the policy decides.
(declare-const costEur Int)
(declare-const international Bool)
(declare-const managerApproved Bool)
(declare-const tenureMonths Int)
(declare-const tripApproved Bool)
(declare-const bookingAllowed Bool)

; The situations the policy forbids, each defined once so the rules can reuse it.
(define-fun expensiveUnapproved () Bool (and (> costEur 1000) (not managerApproved)))
(define-fun abroadUnapproved () Bool (and international (not managerApproved)))
(define-fun abroadTooSoon () Bool (and international (< tenureMonths 6)))

; The rules. (! ... :named x) gives each one a name the solver can report.
(assert (! (=> expensiveUnapproved (not tripApproved)) :named cost-rule))
(assert (! (=> abroadUnapproved (not tripApproved)) :named international-rule))
(assert (! (=> abroadTooSoon (not tripApproved)) :named six-months-rule))
(assert (! (= bookingAllowed tripApproved) :named booking-rule))

; Not in the document: a trip that no rule forbids is approved.
(assert (! (=> (not (or expensiveUnapproved abroadUnapproved abroadTooSoon)) tripApproved)
           :named closed-world))

define-fun 给某个条件起个名字，规则里就能重复使用。每条规则都是一个单独的具名断言，这样当某次出差申请被驳回时，求解器能报告是哪条规则拦下的。最后一条规则并不在文档里。策略只列出了会驳回的情形，所以缺了这条规则，任何申请都无法获批。凡是没有任何规则禁止的申请都予以批准——这是封闭世界假设（closed-world assumption）的典型用法，必须由策略负责人确认。

在让任何结论依赖这份翻译之前，先核对翻译对不对。该策略的负责人说，服务满六个月就符合条件。如果翻译写成 tenureMonths > 6（严格大于六，六个月本身不合格），那条规则就写错了。求解器照它推理依然正确，所以它给出的每个结论都是关于这条错误规则的、逻辑上有效的证明。让求解器找出两份翻译在哪里分歧，就能把问题揪出来：

$ z3 -in <<'EOF'
(declare-const tenureMonths Int)
(assert (>= tenureMonths 0))
(assert (distinct (>= tenureMonths 6) (> tenureMonths 6)))
(check-sat)
(get-value (tenureMonths))
EOF
sat
((tenureMonths 6))

返回 sat 且值为 6，说明两份翻译恰好在六个月这个点上分歧，于是负责人的说法把规则钉在了 >=。对每条规则都拿文档核对一遍，再去相信任何依赖它的结论。

六是两种读法唯一分歧的取值（distinct），也正是那句话留下歧义的边界。当存在多种翻译时，一致的部分可以当作投票，每个分歧点都变成要问负责人的问题。测试用例也能独立发现同一个错误：把负责人对具体取值的答复（六个月符合、五个月不符合、十二个月符合）逐条对照各份翻译，> 6 的版本只在第一项上失败。求解器没法判断规则是否与文档一致，这个判断只能交给人。可以让 LLM 当裁判（LLM-as-a-judge）帮上忙，标出那些看起来与原文句子对不上的规则，但最终签字确认的仍然是负责人。

校验回答

汉堡的一名员工来问：他想预订一趟去柏林、花费 2500 欧元的行程，但还没获批，这样行不行？

我们让大语言模型（LLM）给出给员工的答复，同时在同一次回答里把这份答复写成逻辑形式，事实和结论分开写：

Answer the employee in plain English. Then, between <smt> and </smt>,
restate your answer in SMT-LIB using only these variables:

costEur         Int   total trip cost in euros
  international   Bool  the trip crosses a national border
  managerApproved Bool  a line manager has approved the trip
  tenureMonths    Int   months of continuous service
  tripApproved    Bool  the trip is approved under this policy

Write each

查看原文