# **课程 Project：基于约束求解的规则与结论验证**

## **项目背景**

约束求解研究如何判断一组条件能否同时成立。很多实际问题都可以表示成变量以及变量之间的约束关系，例如“年龄必须大于等于 18 岁”“一本已经被其他人预约的图书不能续借”“经济舱旅客只能携带一件不超过规定重量和尺寸的随身行李”等。将这些规则形式化以后，约束求解器可以判断某个具体情况是否满足全部规则，也可以判断一个新的结论是否会与已有规则产生矛盾。

从这个角度看，约束求解不仅可以用于排课、调度和资源分配，也可以用于对知识和结论进行验证。假设一份材料给出了背景规则 R，现在需要判断一个结论 C 是否符合这份材料。首先可以检查背景规则本身是否可满足；在此基础上，如果 R∧C 不可满足，说明结论 C 与材料中的约束发生冲突；如果 R∧¬C 不可满足，则说明在这些规则下 C 必须成立；如果两种情况都存在可满足的解，则现有材料不足以唯一判断这一结论。这样，一个自然语言中的“这个说法符合材料吗”的问题，就可以转化成若干约束可满足性问题。

这类问题在知识抽取和基于材料的问答中十分常见。系统可能从知识库、规章制度、说明文档或其他材料中提取信息，再根据这些信息给出新的结论，但最终结论可能遗漏某个条件、忽略一个例外、违反数值上下限，或者在组合多条规则时出现错误。近年来，大语言模型越来越多地被用于根据给定材料回答问题，同样可能出现这样的情况：回答在语言上十分自然，也正确引用了部分材料，但最终结论并不满足材料中的全部约束。因此，可以尝试在生成或抽取系统之外增加一个基于约束求解的验证过程，用形式化规则检查一个结果是否真正与原始材料相符。

本项目围绕这一问题展开：选择一份包含明确自然语言规则的材料，将其中适合形式化的部分转换为约束，并利用约束求解方法判断若干给定结论是否符合材料。项目关注的核心不是自然语言处理本身，而是从实际规则中识别变量和约束、建立形式模型，以及利用可满足性判断对结果进行验证。

## **Toy Example**
设有如下简化规则文档：

规则 1：“每位读者最多同时借阅 10 本图书。”
规则 2：“如果读者存在逾期未归还的图书，则不能继续借书。”
规则 3：“如果读者没有逾期图书，且借阅新书后总借阅数量不超过 10 本，则允许继续借书。”

定义变量：borrowed_books 表示当前已借图书数量，new_books 表示本次希望借阅的图书数量，has_overdue 表示是否存在逾期图书，can_borrow 表示本次借阅是否被允许。将每条自然语言规则分别形式化，得到规则集合：

R1: can_borrow = true -> borrowed_books + new_books <= 10

R2: has_overdue = true -> can_borrow = false

R3: (has_overdue = false AND borrowed_books + new_books <= 10)
    -> can_borrow = true

于是文档对应的形式化规则集合为：

R = {R1, R2, R3}

现在给出一个问答对。问题为：“Alice 当前已经借了 9 本书，没有逾期图书，现在还想再借 2 本，她可以借吗？”回答为：“可以。”

问题中的事实可以建模为：

F1: borrowed_books = 9

F2: new_books = 2

F3: has_overdue = false

回答“可以”对应待验证结论：

C: can_borrow = true

首先，背景规则和问题事实本身是可满足的。随后，将待验证结论 C 加入约束系统，检查：R ∪ {F1, F2, F3, C} 是否可满足。由于 C 指定 can_borrow = true，根据规则 R1 必须满足：borrowed_books + new_books <= 10 而由 F1 和 F2 可得： 9 + 2 <= 10 该条件不成立，因此加入结论后整个约束集合不可满足，求解器返回 UNSAT。这说明回答中的结论“可以借这 2 本书”与给定规则发生冲突，因此应判定为错误。

这只是一个最小的参考实例且并不是最好的实现方法（其中一些细节被有意隐去），你不需要完全参照这个 Example 实现你的项目。

## **项目内容**

你的项目应当从一份自然语言规则材料开始（你应该自行寻找相关的材料，我们提供了一些参考以供选择）。材料可以来自现实生活中的规章、服务规则、使用说明、学校规定、票务规定、交通规则等，只要其中包含足够明确的条件、数量限制、范围、例外或规则之间的关联即可。材料不需要很长，十几条到几十条具有实际含义的规则已经足以形成一个完整项目。例如，图书馆借阅规则中可能同时规定借书数量、借阅期限、续借次数和不能续借的条件。交通和行李规定也是很直观的例子。国航的随身行李规则根据舱位规定了件数、单件重量以及长宽高限制，例如头等舱和公务舱与经济舱适用不同的件数和重量上限，这类材料只需要整数、布尔变量、比较关系和简单条件分支即可形式化，但已经包含了多个规则共同作用的情况。你需要对这个文档进行完全的建模，将它形式化为若干约束，从而保证后续你可以基于这些规则对任意的基于材料作出的结论做基本的检查。

完成形式化后，项目中的主要程序应当能够接收一组（已经形式化的）背景条件和一个（已经形式化的）待验证结论，并通过约束求解给出结果。最基本的结果可以分为三类：结论与背景规则一致并且可由规则确定；结论与背景规则冲突；根据现有规则无法确定。是否还存在其他需要区分的情况，请结合你的建模自行分析。
除了最终分类，还可以给出相应的可满足解或冲突原因，使验证结果能够被理解和检查。理论上，这一部分需要一个约束求解器来完成，你可以使用现有的约束求解器（如Z3 或 CVC5等）来完成你的任务，也可以自己实现需要支持的功能的约束求解器。

项目中应当包含一定（adequate）数量的测试场景，来证明你的建模一定程度上较为完备。简单场景用于确认单条规则是否被正确表达，边界场景用于检查诸如 < 和 <=、最大数量、年龄临界点等问题，组合场景则需要同时利用多条规则才能得到结论。一个形式化模型能够正常运行，并不意味着它一定正确表达了原始自然语言。例如把“未满 14 周岁”错误形式化成 age <= 14，求解器仍然可以正常工作，但年龄正好为 14 岁时就会产生错误结论。形式化规则与原始材料之间是否一致，因此也是整个项目需要研究的问题之一。

## **开放扩展**

基本项目占总成绩的 90%。另外 10% 为开放扩展部分，扩展方向不作限定。可以增加更丰富的规则类型、更复杂的组合推理、优化目标、冲突解释、反例生成、不同约束编码方式的比较，或者对模型进行更加系统的测试和性能分析。

我们提供一个可供参考的开放扩展方向：使用大模型技术端到端地自动化你的约束求解工作流。例如，可以尝试使用 LLM 从自然语言材料中提取变量和规则、生成候选约束，或者根据材料和问题产生待验证的答案，再利用约束求解器进行检查。通过自动化从文档当中抽取结论和自动从自然语言Q/A当中提取形式化结论，再进入约束求解器形成有理论保证的结果。你可能需要比较自动生成的形式模型与人工理解之间是否存在差异，以及约束求解能否发现这些差异所造成的错误结论。

不使用大语言模型也可以获得完整的开放扩展分。例如，在约束建模、测试方法、冲突分析、自动反例生成或求解效率等方面进行更深入的工作，同样属于有效扩展。

## **项目成果要求与生成式人工智能使用政策**

项目的基本要求需要你至少完成：

- 对一个较复杂的自然语言材料的形式化。
- 若干自然语言测试用例（其中包含正确的和错误的结论），对它们基于自然语言材料的形式化建模，以及你对它们的验证结果。
- 实现一个自动检查结论和自然语言材料匹配程度的求解程序/工作流，并描述你是如何实现的。
- 回答一些关于项目的问题（见下）。

你需要交付的内容包括：

- 一个报告（必须使用 LaTeX 编译生成，否则会扣减一定比例的成绩），描述所有关于你是如何完成项目的必要阐述。你可以使用中文或者英文撰写你的报告。如果你没有对格式的偏好，可以使用 **Springer LNCS format**。报告长度建议控制在15-25页（LNCS 格式），明显过长或过短的报告正文会导致你的分数受到负面影响，请保证你的报告的信息密度和适当表达。
- 你的程序实现（Artifact），至少包括调用约束求解器实现自动验证约束的那部分的程序实现。
- （如有）附加材料。

在你的报告中，必须包含一个独立章节（如果不包含这一章节你可能不会得到60%以上的分数），回答如下几个问题：

**1.如果你现在正在某个研究生岗位/工作岗位的面试阶段，当面试者问起你的这个项目时，尝试用一段话介绍你的项目。**

**2.从你完成项目的过程来看，你认为约束求解器在各种场景下能够证明什么，不能证明什么？**

**3.为什么约束求解可以（或者不完全可以）用于验证一个结论是否符合背景知识？**

**4.将自然语言规则建模为形式约束时，可能会出现哪些问题？**

**5.披露你的项目在哪些环节（如报告撰写，程序编写，工作流当中等）使用了生成式人工智能，说明你是如何使用的。**

这些问题的回答并非越长越好。如果你认为一句话就足够描述你的Insight，几个字或者一句话的回答也是好的；如果长篇大论地阐述你的思想，请确保言之有物。

本项目允许生成式人工智能的使用。你可以使用你认为必要的AI工具完成项目，但你必须完全披露你的使用方式。合理地使用人工智能是你能够适当调用前沿工具的能力体现，但不加选择地滥用则并不能让你学到东西，同时AI的各种问题可能会让你的项目空洞无物、缺少必要的规范。但是，**严禁在上面的“独立章节”（即回答5个问题）的章节使用生成式人工智能，你必须通过亲自敲击键盘输入文字的方式完成那个章节。助教从2023年以来长期从事人工智能相关工作，使用各种模型提供商和AI工具的经验非常丰富，总Token使用量在1000亿以上，并有鉴别人工智能生成内容的工作经历，如果你尝试通过各种手法仍然使用人工智能生成了你未披露的内容或用于回答上述的5个问题，你的分数将受到对应程度的扣减。**

评分会基于你的报告质量、项目完成度和程序实现来完成，并不一定完成了基本要求就一定能得到全部的90%分数。另外的10%会根据项目的创新性给出，你也可以通过各种方式报告你在哪里作出了别出心裁的设计。

## **可参考的自然语言规则材料**

选题材料不限定为以下文档，下面几份材料只用于展示适合本项目的规则的大致形态。

北京大学图书馆的“图书借还与续借”“外借册数和期限”等规则篇幅短、语言直接，同时包含数量限制、时间限制、续借条件和例外，是最简单的入门材料之一。[北京大学图书馆：图书借还与续借](https://www.lib.pku.edu.cn/portal/cn/jy/jybl/jiehuanxujie?utm_source=chatgpt.com) [北京大学图书馆：外借册数和期限](https://www.lib.pku.edu.cn/portal/cn/fw/rgzn/guizhangzhidu/notice3?utm_source=chatgpt.com)

中国铁路 12306 的“铁路旅客购票须知”包含年龄区间、儿童优惠票、免费儿童数量、是否占用席位以及同行成年人等条件，是典型的多条件规则材料，而且几乎不需要额外领域知识。[中国铁路12306：铁路旅客购票须知](https://www.12306.cn/mormhweb/zxdt/202311/t20231114_40286.html?utm_source=chatgpt.com)

国航的“旅客、行李运输总条件”以及随身行李说明包含舱位、件数、重量、尺寸和特殊物品例外，非常适合使用整数约束和条件表达式进行建模。[国航：旅客、行李运输总条件](https://webresource.airchina.com.cn/zh-CN/content/c/2025-04-25/24891.shtml?utm_source=chatgpt.com)

## **参考阅读**

以下资料仅供参考，不要求全部阅读，也不限定项目必须使用其中的工具或方法。

1. **Amazon Bedrock Automated Reasoning Checks**  
   这是和本项目思路最接近的工业案例之一。Amazon Bedrock 提供 Automated Reasoning Checks，用自然语言文档中的规则建立 formal policy，再利用形式逻辑检查大模型回答是否符合这些规则。官方文档中将 policy 定义为由规则、变量和类型组成的形式化模型，并明确说明可以从 HR 手册、合规文档、产品规范等自然语言材料中提取规则。  
   特别推荐阅读其 Concepts 和 Testing 两部分。Testing 文档中区分了“规则本身是否正确”和“自然语言问答是否被正确翻译成逻辑”两个测试问题，与本项目中的模型验证非常接近。  
   [Automated Reasoning Checks Overview](https://docs.aws.amazon.com/bedrock/latest/userguide/guardrails-automated-reasoning-checks.html?utm_source=chatgpt.com)  
   [Automated Reasoning Checks Concepts](https://docs.aws.amazon.com/bedrock/latest/userguide/automated-reasoning-checks-concepts.html?utm_source=chatgpt.com)  
   [Testing an Automated Reasoning Policy](https://docs.aws.amazon.com/bedrock/latest/userguide/test-automated-reasoning-policy.html?utm_source=chatgpt.com)

2. **Z3 / Z3Py**  
   Z3 是本项目中最直接可用的 SMT 求解器之一。Z3Py 提供 Python 接口，可以使用 Int、Real、Bool、And、Or、Implies 等对象表示变量和约束，再使用 Solver.add() 和 Solver.check() 判断约束集合是否为 sat 或 unsat。官方教程包含大量可以直接运行和修改的例子。  
   [Z3 Online Guide](https://microsoft.github.io/z3guide/?utm_source=chatgpt.com)  
   [Z3Py Introduction](https://microsoft.github.io/z3guide/programming/Z3%20Python/Introduction/?utm_source=chatgpt.com)

3. **SMT-LIB**  
   SMT-LIB 是 SMT 求解器通用的逻辑语言和标准。如果希望进一步理解 Z3 中变量、逻辑公式、check-sat和 model 背后的概念，可以参考 SMT-LIB。对于本项目不需要完整阅读标准，只需要理解变量声明、逻辑表达式、可满足性判断和模型即可。当前 SMT-LIB 官方标准为 Version 2.7。  
   [SMT-LIB 官方网站](https://smt-lib.org/?utm_source=chatgpt.com)

4. **MiniZinc**  
   MiniZinc 是另一种适合约束建模的工具。与直接编写 Z3 表达式相比，MiniZinc 更强调“描述问题中的变量和约束”，然后将模型交给不同求解器执行，适合排课、资源分配、组合优化等问题。官方 Handbook 提供从基础语法到完整建模的教程。  
   [MiniZinc Tutorial](https://docs.minizinc.org/en/stable/part_2_tutorial.html?utm_source=chatgpt.com)

5. **AWS 关于大模型幻觉与形式验证的介绍**  
   如果希望了解为什么约束求解可以用于验证大模型回答，可以阅读 AWS 对 Automated Reasoning 的介绍。其基本流程是将规则文档转换为形式化 policy，再把问题和模型回答转换成逻辑表示，通过自动推理判断回答是否符合 policy。AWS 将返回结果区分为类似 Valid、Invalid 和缺少足够信息的情况。  
   [Minimize generative AI hallucinations with Amazon Bedrock Automated Reasoning checks](https://aws.amazon.com/blogs/machine-learning/minimize-generative-ai-hallucinations-with-amazon-bedrock-automated-reasoning-checks/?utm_source=chatgpt.com)

6. **Logic-LM：自然语言与符号求解器结合**  
   这篇工作展示了一个典型的“自然语言 → 符号表示 → 求解器”的流程：首先把自然语言问题转换成形式化表示，然后由确定性的 symbolic solver 进行推理，并利用求解器错误信息修正形式化结果。适合作为使用 LLM 进行自动形式化时的扩展阅读。  
   [Logic-LM 论文](https://aclanthology.org/2023.findings-emnlp.248/?utm_source=chatgpt.com)

7. **Don't Trust: Verify — Autoformalization 与验证**  
   该工作研究如何将非形式化的问题和解答自动转换为形式表示，再利用形式化工具检查结果的一致性。其重点并不是让形式工具重新完成整个任务，而是使用形式化验证识别生成结果中的逻辑或计算错误。可作为开放扩展部分的进一步参考。  
   [Don't Trust: Verify](https://proceedings.iclr.cc/paper_files/paper/2024/hash/0a79ecda13603817de4cdfc68b417e89-Abstract-Conference.html?utm_source=chatgpt.com)

对于第一次接触约束求解的同学，建议优先参考 **Z3Py Introduction**；希望理解项目整体应用场景时，可以优先阅读 **Amazon Bedrock Automated Reasoning Checks**。SMT-LIB、MiniZinc 和后两篇论文属于进一步阅读材料。

本项目是第一年正式用于课程，可能有诸多不完善之处，如有疑问或建议请通过邮箱联系助教：[zhangyihao@stu.pku.edu.cn](mailto\:zhangyihao@stu.pku.edu.cn) 。本Project 文档的撰写部分使用了 Chat GPT生成，但已经过人工的修改和校对。