切换深色模式
约束求解：让决策具有可检查的依据
对应 CS224V · 2026-11-09 · Accountable AI: SMT。日期为校方课表日期，可能调整。核对官方课表。
资料状态
核对日期：2026-09-19。对应课程尚未开课；本文是基于公开课纲与文中原始资料的原创预习技术解读，不是课堂实录、讲义翻译或官方作业答案。本文于 2026-09-20 深度修订。示例为原创教学设计；离线实验与真实模型实验的边界分别说明，不以推演冒充模型实测。
课程 C3 要求完成先修 B，用户没有提供 B 的记录。求解器找到一个令“用户完成 B”为真的赋值，于是返回可满足。系统能否据此告诉用户“你符合要求”？不能：存在一种满足条件的情况，与已知事实证明用户符合要求，是两件不同的事。
本讲围绕这个差别建立可检查决策，并解释形式化方法把错误转移到了哪些边界。
将业务条件翻译成逻辑
使用一个简化课程规则：满足 A 或 B、没有时间冲突、加入后不超过学分上限。记资格结论为 E：
text
E = (A ∨ B) ∧ ¬conflict ∧ (current + requested <= limit)Z3 官方指南介绍 SMT 如何处理布尔与数值等约束。本文用有限布尔赋值解释原理，不把手工枚举当成完整 SMT 求解器实现。
首先检查自然语言翻译：原文“完成 A 或 B”不能变成“两者都完成”；“至多 10 学分”包含等于 10。求解器只能对输入公式负责，不知道翻译是否忠实。
可满足、被事实蕴含、被事实否定
令 F 表示已知事实与规则。先检查 F 自身是否一致。若 F 矛盾，需要修复数据，不能利用矛盾前提推导任意结论。
若 F 一致，分别检查 F ∧ E 与 F ∧ ¬E：
| 结果 | 意义 |
|---|---|
| E 可满足，非 E 不可满足 | 已知事实推出符合 |
| E 不可满足，非 E 可满足 | 已知事实推出不符合 |
| 两者都可满足 | 信息不足，资格未知 |
这是三种知识状态。求解器因资源限制返回的 unknown 是另一回事，不能与“事实不足”混用。
用两个可能世界看清未知
假设 A 明确为假，B 未知，时间无冲突，学分满足。在世界一，B 为真，E 成立；世界二，B 为假，E 不成立。两者都与已知事实兼容，因此资格未知。
若后来用户提供可信的 B 完成记录，世界二被排除，才可以确认符合。若只看到数据库没有记录，在数据不完整的前提下，不能擅自添加 B=false。
这正是前面结构化查询中未知状态的形式化解释。
用有限枚举做一个可检查的最小原型
对只有 A、B、conflict 三个布尔变量的小例子，可以枚举 8 个世界；固定数值后，用事实 F 筛选世界，再观察资格 E 的真假。它适合验证概念，不适合代替处理大量变量与算术约束的 SMT 引擎。
text
worlds = 所有满足 F 的赋值
若 worlds 为空：返回 inconsistent
若每个 world 都满足 E：返回 entailed
若每个 world 都不满足 E：返回 refuted
否则：返回 undetermined第一个分支不可省略。在程序语言中，空集合上的 all(...) 通常为真；如果直接检查“所有世界都符合”，矛盾事实会被错误标成已证实符合。先检查一致性既是逻辑要求，也是可以实际触发的代码缺陷。
还应保存每条输入事实的来源。若系统加入 A 为假，是用户明确声明、权威完整记录推导，还是模型从“没查到”猜测？这三种依据不能无差别写进 F。将未经证实的假设与已知事实分开，可以生成条件式回答：“如果你已完成 B，则满足先修；目前仍需核实 B。”这比展示一个可满足模型后宣布通过更加忠实。
不可满足核心不是自动生成的业务真相
当规则冲突，求解器可能帮助定位一组导致不可满足的约束。例如已选学分 8、课程需 3、上限 10。解释可以指出学分限制。
但核心不一定唯一或最小，也不一定是对用户最有帮助的说明。系统应把公式映射回原始规则与数据来源，并避免展示一串用户无法理解的符号。
如果一个核心依赖错误抽取的“课程需 30 学分”，形式推理依然正确，业务结论却错误。数值和规则都需要来源校验。
形式化决策的三道质量门
第一道检查输入事实：来源、版本和未知值。第二道检查语义翻译：逻辑连接词、单位、比较符和例外条件。第三道检查求解与解释：一致性、状态分类及理由是否对应实际规则。
可以采用一组变形测试：把上限从 10 改为 11，学分结论按预期变化；把 A 或 B 改为 A 且 B，未知场景不应被误通过；同时加入 B 真和 B 假，应报告数据矛盾，而不是选择方便的一条。
资料边界与应用范围
公开课表提及 SatIR、VERDICT。本次仍未取得足以详解其实现的原始资料，所以本篇不编写这两个系统的内部架构或性能数字。
本例只讨论虚构选课规则。形式化方法能够保证在某套输入与逻辑下的推导，却不能自动保证世界事实完整、规则无遗漏或政策含义被正确翻译。越是重要的决策，越需要分别验证这些边界。
下一讲回到软件系统，用同样的“可观察、可执行、可验证”原则设计编程 Agent 的运行环境。继续阅读Harness。