自动推理
自动推理（Automated Reasoning）是人工智能中研究如何让计算机自动地进行逻辑推导的领域。它涵盖了从布尔可满足性（SAT）求解到形式化定理证明的广泛技术，是软件验证、硬件设计、数学证明和 AI 安全的基础工具。
近年来，随着深度学习与形式化方法的融合（如 AlphaProof、神经定理证明），自动推理正在经历一场深刻的变革。本笔记涵盖 SAT/SMT 求解、定理证明、形式化验证以及与深度学习融合的前沿方向。
1. 推理系统的分类
| 分类维度 | 类型 | 说明 |
|---|---|---|
| 按逻辑层次 | 命题逻辑推理 | 变量只有真/假两种取值 |
| 一阶逻辑推理 | 支持量词（\(\forall, \exists\)）和谓词 | |
| 高阶逻辑推理 | 变量可以是函数或谓词本身 | |
| 按自动化程度 | 全自动 | SAT/SMT 求解器 |
| 半自动（交互式） | Lean, Coq, Isabelle | |
| 按推理方向 | 前向推理 | 从公理和已知定理出发推导 |
| 后向推理 | 从待证目标出发分解为子目标 |
2. SAT 问题与求解器
2.1 布尔可满足性问题
SAT 问题：给定一个布尔公式 \(\varphi\)（通常为 CNF 形式），判断是否存在一个变量赋值使 \(\varphi\) 为真。
- SAT 是第一个被证明为 NP-完全的问题（Cook-Levin 定理，1971）
- 尽管最坏情况下是指数时间，现代 SAT 求解器在实际问题上表现极好
2.2 DPLL 算法
DPLL（Davis-Putnam-Logemann-Loveland, 1962）是最早的系统化 SAT 求解算法：
DPLL(φ):
1. 单元传播（Unit Propagation）：
如果某个子句只剩一个文字，则必须赋值为真
2. 纯文字消除（Pure Literal Elimination）：
如果某个变量只以正或负形式出现，则赋相应值
3. 分支（Branching）：
选择一个变量，尝试赋值为真/假，递归求解
4. 回溯（Backtracking）：
如果当前赋值导致冲突，回退到上一个决策点
2.3 CDCL 算法
CDCL（Conflict-Driven Clause Learning）是现代 SAT 求解器的核心算法，在 DPLL 基础上增加了：
| 增强机制 | 说明 |
|---|---|
| 冲突分析 | 冲突发生时，分析原因并学习一个冲突子句 |
| 非时序回溯 | 直接回溯到冲突的根源（而非上一个决策点） |
| 子句学习 | 将冲突子句加入公式，避免重复搜索 |
| 变量选择启发式 | VSIDS（Variable State Independent Decaying Sum）等策略 |
| 重启策略 | 周期性重启搜索，保留已学习的子句 |
代表求解器：MiniSat, CaDiCaL, Kissat, Z3（SAT 部分）
SAT 竞赛
每年举办的 SAT Competition 推动了求解器技术的快速发展。现代求解器可以处理数百万变量的实例。
2.4 WalkSAT
WalkSAT 是一种随机局部搜索算法：
- 随机生成初始赋值
- 选择一个不满足的子句
- 以概率 \(p\) 随机翻转该子句中的一个变量；以概率 \(1-p\) 翻转使不满足子句数最少的变量
- 重复直到找到满足赋值或达到上限
适合求解可满足性判定（找到一个解），但不能证明不可满足。
3. SMT 求解器
3.1 可满足性模理论
SMT（Satisfiability Modulo Theories） 将 SAT 推广到更丰富的逻辑理论：
| 背景理论 | 缩写 | 示例 |
|---|---|---|
| 线性整数/实数算术 | LIA/LRA | \(x + 2y \leq 5\) |
| 位向量 | BV | 32 位整数溢出检测 |
| 数组 | AR | \(\text{read}(\text{write}(a, i, v), i) = v\) |
| 未解释函数 | UF | \(f(x) = f(y) \Rightarrow x = y\)（若 \(f\) 单射） |
| 字符串 | S | 正则表达式匹配 |
3.2 DPLL(T) 框架
现代 SMT 求解器采用 DPLL(T) 框架：SAT 求解器处理布尔骨架，理论求解器检查理论一致性。
SAT 求解器 ←→ 理论求解器(T)
布尔赋值 → T-一致性检查
冲突子句 ← T-冲突解释
3.3 Z3 简介
Z3（Microsoft Research）是最广泛使用的 SMT 求解器：
from z3 import *
x, y = Ints('x y')
s = Solver()
s.add(x + y == 10)
s.add(x > 0, y > 0)
s.add(x > y)
if s.check() == sat:
print(s.model()) # [x = 6, y = 4]
应用领域：程序验证、符号执行、约束求解、测试生成。
4. 定理证明
4.1 自动定理证明
归结法（Resolution） 是自动定理证明的基础：
- 将待证命题的否定转化为 CNF
- 反复应用归结规则：从 \((A \lor C)\) 和 \((\neg A \lor D)\) 推出 \((C \lor D)\)
- 如果推出空子句 \(\Box\)，则原命题成立（反证法）
| 自动定理证明器 | 特点 |
|---|---|
| E Prover | 一阶逻辑，等式推理 |
| Vampire | 一阶逻辑，SAT 竞赛冠军 |
| SPASS | 一阶逻辑，模排序策略 |
4.2 交互式定理证明
交互式定理证明器（ITP）需要人类提供证明策略，由计算机验证每一步的正确性。
| 证明助手 | 逻辑基础 | 语言 | 代表项目 |
|---|---|---|---|
| Lean | 依赖类型论（CIC 变体） | Lean 4 | Mathlib（100万+ 定理） |
| Coq | 归纳构造演算（CIC） | Gallina | CompCert（验证的 C 编译器） |
| Isabelle | 高阶逻辑（HOL） | Isar | seL4（验证的微内核） |
| Agda | 依赖类型论 | Agda | 类型论研究 |
Lean 4 示例（证明 \(n + 0 = n\)）：
theorem add_zero (n : Nat) : n + 0 = n := by
induction n with
| zero => rfl
| succ n ih => simp [Nat.add_succ, ih]
Mathlib 项目
Mathlib 是 Lean 4 上最大的数学形式化库，涵盖代数、分析、拓扑、数论等领域，目前包含超过 100 万条形式化定理和定义。
5. 形式化验证
5.1 模型检验
模型检验（Model Checking）自动验证有限状态系统是否满足给定的时序逻辑性质。
输入：系统模型 \(M\)（有限状态机）+ 性质 \(\phi\)（如 CTL/LTL 公式）
输出：\(M \models \phi\)（满足）或反例路径
| 工具 | 应用领域 |
|---|---|
| SPIN | 并发协议验证 |
| NuSMV | 硬件设计验证 |
| CBMC | C/C++ 程序有界模型检验 |
| TLA+ | 分布式系统设计（Amazon 大规模使用） |
5.2 程序验证
| 方法 | 说明 | 工具 |
|---|---|---|
| 霍尔逻辑 | 使用前置条件/后置条件推导程序正确性 | Dafny, Frama-C |
| 符号执行 | 用符号值代替具体值执行程序 | KLEE, angr |
| 抽象解释 | 在抽象域上分析程序行为 | Astrée |
| 有界模型检验 | 展开有限步循环后转化为 SAT/SMT | CBMC |
6. AI 中的形式化方法
6.1 神经网络验证
验证神经网络的鲁棒性：对于输入 \(x\) 的 \(\epsilon\)-邻域内的所有扰动 \(x'\)，网络输出是否保持一致。
| 验证工具 | 方法 |
|---|---|
| \(\alpha,\beta\)-CROWN | 分支定界 + 线性松弛 |
| Marabou | SMT-based 验证 |
| ERAN | 抽象解释 |
| VNN-COMP | 年度神经网络验证竞赛 |
6.2 LLM 输出验证
- 代码验证：用形式化方法验证 LLM 生成的代码是否满足规约
- 推理链验证：验证 Chain-of-Thought 推理过程中每一步的逻辑正确性
- 事实核查：将 LLM 输出中的事实声明转化为可验证的逻辑命题
7. 与深度学习的融合
7.1 AlphaProof
AlphaProof（DeepMind, 2024）是将 AlphaZero 风格的强化学习应用于数学定理证明的系统：
- 在 Lean 4 形式化环境中证明 IMO（国际数学奥林匹克）竞赛题
- 将证明搜索建模为类似下棋的搜索问题
- 使用 LLM 生成证明候选，用形式化系统验证
7.2 神经定理证明
| 系统 | 方法 | 目标 |
|---|---|---|
| GPT-f | Transformer 生成证明步骤 | Lean/Metamath 证明 |
| HTPS | 超树搜索 + 神经网络 | Lean 证明搜索 |
| LeanDojo | LLM + Lean 交互环境 | 开放研究平台 |
| Llemma | 数学专用 LLM | 数学推理与证明 |
| DeepSeek-Prover | 强化学习 + 形式化验证 | Lean 定理证明 |
核心思路：
- 语言模型生成证明策略（tactic）
- 形式化系统验证每一步的正确性
- 搜索算法（如 MCTS）探索证明空间
- 强化学习从成功的证明中学习
7.3 前景与挑战
| 维度 | 现状 | 挑战 |
|---|---|---|
| 证明能力 | 可解决本科水平数学题 | 距离前沿数学研究仍有差距 |
| 形式化覆盖 | Mathlib 覆盖了大量基础数学 | 许多高级领域尚未形式化 |
| 搜索效率 | 依赖 LLM 引导减少搜索空间 | 复杂证明的搜索空间仍然巨大 |
| 泛化能力 | 在训练分布内表现良好 | 对全新类型的问题泛化有限 |
形式化不等于理解
当前的神经定理证明系统能够找到正确的证明，但这不意味着系统"理解"了数学概念。证明的正确性由形式化系统保证，而非由神经网络保证。
参考资料
- Biere et al., Handbook of Satisfiability
- Harrison, Handbook of Practical Logic and Automated Reasoning
- Baier & Katoen, Principles of Model Checking
- Trinh et al., "Solving olympiad geometry without human demonstrations" (Nature, 2024)
- Lean 4 Documentation
- Z3 Theorem Prover