人工智能知识库

自动定理证明

55分钟阅读

自动定理证明

文档概述

自动定理证明（Automated Theorem Proving, ATP）是人工智能与数理逻辑的交叉领域，旨在设计能在计算机上自动证明数学定理的程序。本文系统阐述归结原理、链接策略、霍恩子句及主流定理证明器，为构建智能推理系统提供方法论基础。

关键词速览

关键词英文术语核心含义
归结原理Resolution一阶逻辑的完备证明规则
合一Unification求取使两个公式相同的替换
子句Clause文字的析取式
霍恩子句Horn Clause至多一个正文字的子句
前向链接Forward Chaining从事实推导结论
后向链接Backward Chaining从目标回溯证明
SLD归结SLD-Resolution用于逻辑程序的归结
模型检测Model Checking有穷状态系统的自动化验证
证明助手Proof Assistant交互式定理证明工具

一、自动定理证明入门：让计算机证明数学定理

1.1 什么是自动定理证明

说起来自动定理证明，你可能会想：证明数学定理不是数学家的事情吗？计算机不就是跑跑程序、算算数字？让它去证明数学定理，这事儿听着就挺玄乎的。

其实这事儿的核心思路没你想的那么复杂。咱们可以把自动定理证明理解成：给计算机一套推理规则，然后让它按照这套规则去摆弄数学公式，直到把待证的命题证出来。

打个比方，就像你学几何的时候，老师给你公理和定理，然后让你用这些公理定理去证明新的命题。自动定理证明干的也是这个活儿，只不过把推理的过程完全交给计算机来做。

当然说起来简单，做起来可就复杂多了。这里头涉及到怎么把数学命题用计算机能理解的形式表示出来，怎么设计有效的推理规则，怎么让计算机在海量的推理可能性中快速找到正确的证明路径——这些问题困扰了研究者们好几十年。

1.2 从”逻辑机器”说起

1956年，Newell、Shaw和Simon这三个哥们儿整出来一个叫”逻辑理论家”的程序，这玩意儿被认为是自动定理证明的开山之作。它能在计算机上证明怀特黑德和罗素《数学原理》中的38条定理，这件事在当时引起了不小的轰动。

你想想看，那是1956年啊，计算机还是个占地面积跟房间差不多大小的庞然大物，内存可能还没你现在的手机大。在这样的机器上能让计算机做数学证明，确实是件挺了不起的事儿。

到了1965年，Robinson提出了归结原理，这玩意儿可以说是一阶逻辑定理证明领域的一次大革命。在归结原理出来之前，各种证明方法都是针对特定的逻辑系统或者特定类型的问题，通用性很差。Robinson的这篇论文直接给出了一个通用的、完备的证明方法，一下子把自动定理证明的研究推上了一个新台阶。

1.3 自动定理证明能干什么

好端端的为什么要让计算机去证明定理？吃饱了撑的吗？

还真不是。自动定理证明在现实中有着广泛的用途：

硬件设计验证——现代芯片设计复杂到人脑已经很难完全把握所有细节了。用定理证明器可以验证芯片设计是否满足规格说明，这在航空航天、医疗设备这些对可靠性要求极高的领域尤为重要。

软件正确性验证——谁也不想坐上一架软件可能有bug的飞机吧？定理证明可以用来验证关键软件系统的正确性，比如操作系统内核、编译器这些基础软件。

数学研究辅助——有些数学证明太长太复杂，人难免出错。形式化验证的证明可以彻底消除出错的可能。著名的例子就是四色定理和Kepler猜想的计算机证明。

人工智能推理——知识库问答、智能规划、专家系统，这些AI应用背后都用到了自动推理技术。

二、形式化数学：数学定理的机器可验证表示

2.1 为什么需要形式化

要跟计算机打交道，首先得把数学命题变成它能理解的格式。我们日常写数学证明用的是自然语言加数学符号，这玩意儿对计算机来说太模糊了。

比如说”所有偶数都能被2整除”，这句话里有”偶数”、“被整除”这些概念，还有”所有”这个量词。计算机要处理这个命题，首先得知道”偶数”是什么——是形如2n的整数？还是要用更形式化的方式定义？

形式化数学干的就是这事儿：把数学概念和命题用严格的逻辑语言表达出来，让计算机能够处理。

2.2 从命题逻辑到一阶逻辑

最简单的逻辑是命题逻辑，它只处理简单的陈述句，比如”P”、“Q”这样的原子命题，用”且”、“或”、“非”、“蕴含”这些连接词把它们连起来。

但命题逻辑的表达能力太弱了。很多数学命题都需要讨论”所有”和”存在”，比如”对所有的实数x，都存在一个整数n，使得n ≤ x < n+1”。这种命题命题逻辑就处理不了。

一阶逻辑解决了这个问题。它引入了变量、量词（∀表示”所有”，∃表示”存在”）、谓词（比如”是偶数(x)”、“大于(x,y)“）和函数符号。有了这些工具，一阶逻辑就能够表达绝大多数数学命题了。

2.3 公式的标准形式

要让计算机处理公式，首先得把公式变成标准格式。为什么要标准化？因为不同的证明方法要求不同的公式形式，而且标准化之后更容易设计算法。

前束范式：把所有量词都提到公式最前面，形成一个”量词前缀”加一个”无量词母式”的结构。这种形式便于理解，但不便于做归结。

斯科林范式：把存在量词用函数符号替代（存在函数），把全称量词都省略。这样处理之后，公式变得更简洁，便于归结。

子句形式：这是归结原理要求的格式。简单说就是把公式转化成一组子句，每个子句是若干文字的析取。

三、合一算法：谓词逻辑推理的核心工具

3.1 什么是合一

合一（unification）是自动定理证明中最基础、最重要的概念之一。你可以把合一理解成：找出一个替换，把两个公式中的变量具体化，使得它们变得完全相同。

举个例子。公式P(x, f(y))和公式P(g(z), f(b))，我们能不能找到一种替换，把x、y、z这些变量替换成具体的项，使得这两个公式变成一样的？

可以！把x替换成g(z)，然后把y替换成b，这样两个公式都变成了P(g(z), f(b))。替换{x/g(z), y/b}就是一个合一子。

但有些情况是合不起来的。比如P(x)和Q(x)，这两个公式的谓词都不一样，根本不可能变得相同，所以它们是不可合一的。

3.2 合一算法的工作原理

合一算法要做的事情就是：给定两个公式，找出它们的合一子——如果存在的话。

算法本质上是个递归过程，从两个公式的最外层开始，一项一项地对比，遇到变量就记录下要替换成什么，遇到常量或者函数就检查是否匹配。

举一个具体的例子：

要合一 P(x, f(y)) 和 P(g(a), f(b))

  1. 首先P匹配P，没问题
  2. 然后看第一个参数：x 和 g(a)
    • x是变量，g(a)是项，可以合一，记录替换 x → g(a)
  3. 然后看第二个参数：f(y) 和 f(b)
    • 函数符号f匹配f
    • 看参数：y 和 b
    • y是变量，b是常量，可以合一，记录替换 y → b

最终得到合一子 {x/g(a), y/b}。

3.3 合一的挑战：Occurs Check

合一算法有个很重要的问题要处理，就是occurs check（出现检查）。

考虑这种情况：合一 x 和 f(x)。从形式上看，x是变量，f(x)是函数，好像可以替换 x → f(x)。但这样替换之后，x就变成了f(x)，而f(x)里又包含x，变成f(f(x))，然后继续无穷无尽……

这显然是不行的。所以在合一算法中，必须检查：你要把变量x替换成某个项，这个项里能不能包含x本身？如果包含了，就不能做这个替换。

加入occurs check之后，合一 x 和 f(x) 会发现f(x)中确实包含x，拒绝这个合一，返回失败。

四、归结原理：Herbrand定理与反驳证明

4.1 归结的思想

归结原理是自动定理证明领域最重要的成果之一。Robinson在1965年提出的这个方法，第一次给出了一阶逻辑的完备证明方法——也就是说，只要命题是成立的，归结方法在有限步内一定能证出来。

归结原理的核心思想其实挺简单的，就是反证法。

要证明φ是真的，传统方法是直接证明。但归结换了个思路：假设φ是假的，看看能不能推出矛盾。如果能推出矛盾，那就说明φ必须是真的。

具体来说，证明Γ ⊨ φ的步骤是：

  1. 把¬φ（φ的否定）加入前提Γ
  2. 把所有公式都转换成子句形式
  3. 对子句集反复应用归结规则
  4. 如果能归结出空子句（表示矛盾），就说明Γ ∪ {¬φ}是不可满足的
  5. 因此φ必然成立

4.2 子句与归结规则

子句（clause）是归结原理的基本处理单元。一个子句就是若干文字的析取，可以理解成”或者”连接的一组条件。

正文字比如P(x)表示P(x)成立，负文字比如¬P(x)表示P(x)不成立。一个子句L1 ∨ L2就是”L1成立或者L2成立”的意思。

归结规则是说：如果有两个子句C1 = L ∨ C1’和C2 = ¬L’ ∨ C2’，而且L和L’可以合一（存在合一子θ），那么就可以推出归结式(C1’θ) ∨ (C2’θ)。

直观理解就是：如果L成立，那么C1’θ一定成立；如果L不成立（即¬L成立），而L’可以合一说明L’和L等价，所以¬L’θ成立，那么C2’θ必须成立。无论哪种情况，(C1’θ) ∨ (C2’θ)都必须成立。

4.3 Herbrand定理

说到归结原理的完备性证明，就不得不提Herbrand定理。Herbrand是法国逻辑学家，1930年因为滑雪事故去世了，年仅23岁，但他留下的思想影响了整个数理逻辑领域。

Herbrand定理的核心是说：一个公式集S是不可满足的，当且仅当存在S的某个基例（把变量都替换成具体项后的实例）是不可满足的。

这个定理看起来好像是在说废话，但实际上它给出了证明不可满足性的一个思路：如果S不可满足，那么一定存在某个有限的基例是不可满足的。这个”有限的基例”就是归结过程要去找的东西。

不过这里有个问题：基例的数目可能是无穷多的。所以Herbrand定理只是保证了存在性，并没有给出具体的搜索方法。归结原理实际上就是在Herbrand定理的框架下，给出了一种系统化搜索基例的方法。

4.4 一个归结证明的例子

说理论太枯燥，来看看具体的例子。假设我们有这些前提：

  1. 所有喜欢运动的人都是健康的
  2. 存在不喜欢运动的人

要证明：存在不健康的人

首先把前提和待证命题的否定都转成子句形式：

  1. ¬LikesSports(x) ∨ Healthy(x) （所有喜欢运动的人都是健康的）
  2. ∃x ¬LikesSports(x) （存在不喜欢运动的人）
    • 斯科林化后：¬LikesSports(a) （a是某个具体的人）
  3. ¬∃x ¬Healthy(x) 即 ∀x Healthy(x)（假设不存在不健康的人）
    • 转成子句：Healthy(x)（所有x都是健康的）

现在对这三个子句做归结：

  • 子句1和子句3归结：¬LikesSports(x) ∨ Healthy(x) 和 Healthy(y)，无法归结（Healthy不匹配）
  • 实际上我们需要一个包含¬Healthy的子句来和Healthy(x)归结

哦等等，我重新组织一下。要证”存在不健康的人”，假设其否定”所有人都是健康的”，然后用子句Healthy(x)来表示。

然后把前提转成子句：

  1. ¬LikesSports(x) ∨ Healthy(x)
  2. ¬LikesSports(c) （c是某个常量）
  3. Healthy(x)

子句1和子句3归结得到：¬LikesSports(x)

然后子句¬LikesSports(x)和子句¬LikesSports(c)归结，x和c可合一，得到空子句！

所以矛盾出现了，假设不成立，原命题成立：确实存在不健康的人。

五、合一与替换：逻辑推理的基本操作

5.1 替换的概念

在逻辑推理中，替换（substitution）是最基本的操作之一。简单说，替换就是用项去替换变量。

比如替换θ = {x/a, y/f(z)}表示把变量x替换成常量a，把变量y替换成项f(z)。

把替换应用到公式上，就是同时对公式中所有的变量做这个替换操作。比如对公式P(x, y)应用替换θ = {x/a, y/f(z)}，得到P(a, f(z))。

5.2 替换的复合

替换可以复合。θ1 ∘ θ2表示先做θ2，再做θ1。

比如θ1 = {x/y}，θ2 = {y/a}。对x应用θ1 ∘ θ2：

  • 先应用θ2：x变成y
  • 再应用θ1：y变成y（因为θ1不改变y）

所以最终x变成了y，也就是θ1 ∘ θ2 = {x/y}。你发现没有，替换的复合不是简单的叠加，需要按顺序应用。

5.3 最一般合一

给定两个公式，可能有很多种合一方式，但其中最”简单”的那个叫最一般合一（MGU，Most General Unifier）。

比如合一 x 和 y，有无数种方法：

  • {x/a, y/a}
  • {x/b, y/b}
  • {x/y} ——这就是最一般合一
  • {y/x}

{x/y}是最一般的，因为它只是说x和y是一样的，没有把任何具体的值绑定给它们。其他合一都可以看成是在{x/y}的基础上再做替换得到的。

六、自然演绎系统：像人一样做证明

6.1 自然演绎的思路

自然演绎（Natural Deduction）是Gentzen在1935年提出的一种证明系统。它的设计目标是模拟人类做数学证明时的思维过程，所以叫”自然”。

在自然演绎中，证明不是像归结那样把公式变成子句然后机械地归结，而是通过一系列推理规则，一步一步把结论推导出来。

基本的推理规则包括：

  • 合取引入：要证明A ∧ B，先分别证明A和B
  • 合取消去：已知A ∧ B，可推出A（或B）
  • 析取引入：要证明A ∨ B，证明A或证明B都行
  • 蕴含引入：要证明A → B，假设A成立，然后证明B
  • 否定引入：要证明¬A，假设A成立，然后推出矛盾
  • 否定消去：已知¬¬A，可推出A

这些规则都很符合直觉。比如说合取引入，如果我想证明”小明既会弹钢琴又会拉小提琴”，我当然得分别证明小明会弹钢琴和小明会拉小提琴。

6.2 证明树与证明脚本

自然演绎的证明可以用证明树来表示。树的根是待证的命题，叶子是已知的公理和假设，中间是应用推理规则得到的中间结论。

在证明助手中，自然演绎的证明通常以”证明脚本”的形式给出。证明脚本记录了每一步使用的推理规则和参数。比如在Lean中：

theorem example (h1 : P → Q) (h2 : Q → R) : P → R :=
  fun hp : P =>
    have hq : Q := h1 hp,
    show R from h2 hq

这段脚本说：假设P能推出Q，Q能推出R，要证P能推出R。证明方法是：假设P成立（fun hp），由h1得到Q（have hq），再由h2得到R（show R）。

七、证明策略：正向链接与反向链接

7.1 正向链接（Forward Chaining）

正向链接是从已知的事实出发，应用规则产生新的事实，一直推到目标出现为止。

想象一个医疗诊断系统。已知事实：

  • 病人发烧
  • 病人咳嗽

规则：

  • 发烧 ∧ 咳嗽 → 可能感冒
  • 可能感冒 → 需要休息

用正向链接，系统会从已知事实出发，首先用第一条规则得到”可能感冒”，然后用第二条规则得到”需要休息”。

正向链接的特点是数据驱动——从已知数据出发，朝着目标方向推导。

7.2 反向链接（Backward Chaining）

反向链接正好相反，是从目标出发，递归地证明子目标。

还是上面的例子。要证明”需要休息”，反向链接会问：怎么才能需要休息？答案是”可能感冒”的时候。那怎么证明”可能感冒”？需要”发烧”和”咳嗽”。这两个条件在已知事实里，所以证明完成。

反向链接是目标驱动的——从要证明的东西出发，往回找需要的条件。

7.3 两种策略的比较

正向链接和反向链接各有优劣。

正向链接：

  • 适合从大量已知事实中导出所有可能的结论
  • 不容易漏掉任何可能的推导
  • 可能产生很多与目标无关的中间结论

反向链接：

  • 适合只关心某个特定目标的证明
  • 搜索空间相对集中
  • 但可能重复探索相同的子目标

Prolog用的就是反向链接。写Prolog程序的时候，你在定义规则和事实，然后在查询窗口问Prolog一个问题，Prolog就用反向链接去证明这个问题能不能从已知规则和事实推导出来。

八、霍恩子句与Prolog

8.1 霍恩子句的特殊之处

霍恩子句（Hom Clause）是至多含有一个正文字的子句。这个看起来不起眼的限制，实际上带来了巨大的计算优势。

为什么这么说？因为霍恩子句对应的是一种特殊的逻辑程序：要么是事实（只有一个正文字，没有负文字），要么是规则（一个正文字加若干负文字），要么是查询（没有正文字，只有负文字）。

这种格式正好对应Prolog程序：事实就是Prolog里直接写的原子语句，规则就是带body的clause，查询就是?-开头的问句。

8.2 SLD归结

对霍恩子句做归结，可以使用一种更高效的专门方法：SLD归结（SLD-Resolution）。

SLD的意思是”用于确定子句的线性归结，附带有选择函数”。线性是说每次归结，其中一个亲本子句是上一步归结的结果；选择函数是说每次从查询中选择哪个子目标来分解。

SLD归结配合深度优先搜索和回溯，就构成了Prolog的执行引擎。这套系统虽然不完备（可能会漏掉一些解），但对于绝大多数实际应用来说足够用了，而且效率很高。

8.3 Prolog的局限

说了这么多Prolog的好处，也得说说它的局限。

首先是深度优先搜索带来的问题。Prolog默认使用深度优先搜索，这可能会导致无限递归。比如定义：

p :- p.

Prolog会陷入无限递归，找不到解。更糟糕的是，有些正确的程序也会因为规则顺序的原因陷入无限递归，比如：

ancestor(X, Y) :- ancestor(X, Z), parent(Z, Y).
ancestor(X, Y) :- parent(X, Y).

如果第一条规则在前，Prolog可能会陷入无限递归。

其次是封闭世界假设。Prolog默认认为：如果一个命题推导不出来，那就是假的。这个假设有时候不符合现实。比如你告诉Prolog”麻雀会飞”和”企鹅是鸟”，但不告诉它”企鹅不会飞”，那么问Prolog”企鹅会飞吗”，它会说”不会”——因为推导不出来。但这可能不是你想表达的意思。

九、交互式定理证明：Lean、Coq、Isabelle

9.1 为什么需要交互式证明

自动定理证明器很强，但有个根本的局限：一阶逻辑的自动证明是不可判定的。也就是说，没有任何算法能保证在有限时间内证明或否定任意一阶逻辑命题。

这在实际应用中是个大麻烦。比如你想证明某个复杂的数学定理，自动证明器可能算到天荒地老也出不来结果——你根本不知道它是真没解出来，还是需要再等等。

交互式定理证明器（也叫证明助手）解决了这个问题。它们不是全自动的，而是要求人类和机器协作：人类提供证明思路，机器检查每一步是否正确。

这种方式的好处是：只要人类给出一个正确的证明，机器就能验证它——这比纯机器证明或者纯人工证明都要可靠。

9.2 Coq

Coq是法国INRIA开发的证明助手，基于直觉类型论。Coq最牛的地方在于它的理论基础——Curry-Howard同构揭示了证明和程序之间的深层联系。

简单说，Curry-Howard同构告诉我们：证明就是程序。一个证明对应一个程序，证明的步骤对应程序的计算。比如要证明”对所有自然数n，n+0=n”，对应的程序是一个对n做递归的函数。

Coq的证明语言是函数式编程语言Gallina，证明过程用的是策略语言Ltac。

用Coq写证明大概长这样：

Theorem add_zero : forall n : nat, n + 0 = n.
Proof.
  induction n.
  - reflexivity.  (* 0+0=0显然成立 *)
  - simpl.       (* 假设n+0=n，证明Sn+0=Sn *)
    rewrite IHn. (* 用归纳假设 *)
    reflexivity. (* 证毕 *)
Qed.

9.3 Lean

Lean是微软研究院开发的证明助手，由Tayor和de Moura开发。相比Coq，Lean的语法更现代一些，学习曲线也稍微平缓一点。

Lean 4还加入了完整的编程语言功能，可以用来写高性能的正式验证程序。

Lean的代码大概长这样：

theorem add_zero (n : Nat) : n + 0 = n := by
  induction n with
  | zero => rfl
  | succ n ih => simp [Nat.add_succ, ih]

9.4 Isabelle

Isabelle是剑桥大学Paulson教授开发的证明助手，特点是支持多种逻辑系统——HOL（高阶逻辑）、ZF（集合论）、NAT（自然数理论）等等。

Isabelle/HOL是用的最多的版本，它的逻辑基础是简单类型的高阶逻辑，比一阶逻辑表达能力强得多。

Isabelle有个很有特色的证明语言叫Isar，写的证明读起来很像人类写的数学证明：

lemma "A ⟶ A ∨ B"
proof (rule impI)
  assume A
  show "A ∨ B" by (rule disjI1)
qed

这段代码说的是：要证A蕴含A或B，先假设A成立（assume A），然后证明A或B（A ∨ B），用到的规则是disjI1（或者-introduction，意思是如果A成立，那么A或任何东西都成立）。

十、自动证明器：E、Z3、Vampire

10.1 纯自动定理证明器

与交互式证明助手不同，纯自动定理证明器（ATP）追求的是完全自动化——你把问题扔进去，它要么给你一个证明，要么说它证不出来（或者超时）。

这类系统在工业界用得很多，特别是硬件验证、程序验证这些场景。数学研究中也有人用它们来探索新的定理。

10.2 Vampire

Vampire是维也纳理工大学开发的自动定理证明器，从1994年开始就在各种竞赛中获奖，被称为”定理证明器中的常胜将军”。

Vampire支持丰富的一阶理论，包括数组、位向量、整数运算等。这让它特别适合验证程序和硬件——这些领域经常需要处理数组访问、位运算等问题。

10.3 E定理证明器

E是Stephan Schulz开发的开源自动定理证明器，基于重写和归结的混合方法。

E的特点是可配置性强，你可以选择不同的证明策略、搜索方法、启发式规则等。对于不同的定理类型，调整参数可能会带来巨大的性能差异。

10.4 Z3

Z3是微软研究院开发的SMT（Satisfiability Modulo Theories，可满足性模理论）求解器。虽然严格来说不算纯ATP，但Z3在自动推理领域的影响力可能比任何纯ATP系统都大。

SMT求解器可以看成是SAT求解器的升级版。SAT处理命题逻辑的可满足性，SMT则在此基础上加入了对各种理论的支持——整数、实数、数组、位向量、非线性运算等等。

Z3在程序验证领域的地位几乎无可替代。微软的很多产品都用Z3来做验证，Linux内核的某些部分也用Z3进行验证。CBMC、Crab等程序分析工具的后端都是Z3。

十一、四色定理与形式化验证的巨大挑战

11.1 四色定理的计算机证明

四色定理大概是世界上最著名的”计算机证明”了。1976年，Appel和Haken宣布证明了四色定理：任何地图都可以用四种颜色染色，使得相邻的区域颜色不同。

这个证明之所以轰动，是因为它是历史上第一个借助计算机证明的大定理。证明的一部分需要检查大量的特殊情况，这些情况的正确性只能由计算机来验证——人脑根本处理不了那么多case。

11.2 为什么这个证明有争议

四色定理的证明出来之后，数学界有一些争议。主要的批评是：

  1. 不可审核性：证明中包含大量计算机计算，没有人能手动检查每一步是否正确
  2. 程序可能有bug：万一程序写错了呢？

这些担忧不是没有道理的。历史上确实有很多被广泛接受的”证明”后来被发现有问题——只不过那些是纯数学家的证明，有问题也是逻辑错误，不是程序bug。

11.3 形式化验证的价值

正因为对证明可靠性的担忧，数学家们后来用形式化证明助手重新证明了四色定理。2017年，Wenzel等人用Isabelle/HOL给出了四色定理的形式化证明。

形式化证明的好处是：机器会检查证明的每一步，不存在”程序bug”的问题（当然证明助手的实现本身也需要验证）。如果形式化证明通过了，那这个证明在逻辑上是绝对可靠的。

十二、AI for Math：神经定理证明器

12.1 传统ATP的局限

传统ATP系统虽然强大，但有个根本问题：它们缺乏”数学直觉”。

给一个数学问题，传统ATP会机械地应用推理规则，在巨大的搜索空间中漫游。这对于某些问题很有效，但如果问题需要一点”创造力”——比如需要想到某个关键引理，或者需要把问题转化成一个更容易处理的形式——传统ATP就抓瞎了。

12.2 AlphaProof

2024年，Google DeepMind发布了AlphaProof，这是一个结合了形式化证明和神经网络的系统。

AlphaProof的思路大概是：用一个神经网络（基于AlphaZero的训练方法）来指导证明搜索，搜索过程在Lean 4的形式化证明环境中进行。这样既有了神经网络的”直觉”，又有了形式化证明的严格性。

在2024年的国际数学奥林匹克（IMO）中，AlphaProof解决了若干道金牌级别的题目。

12.3 大模型与形式化证明

除了AlphaProof，还有很多团队在探索把大语言模型和形式化证明结合。

思路一般是：让LLM生成证明步骤（可能是自然语言，也可能是形式化语言），然后用形式化证明器来验证。如果验证失败，把错误信息反馈给LLM，让它修正。

这种方式确实取得了一些进展，但也面临挑战：LLM的推理能力还不够稳定，有时候会生成看起来很对但实际上有问题的证明。

十三、自动定理证明在程序验证中的应用

13.1 为什么程序需要验证

程序员写代码，总会出错。普通的bug最多导致程序崩溃或者产生错误结果，但对于航空航天、医疗设备、核电站控制这些关键系统来说，bug可能会造成灾难性后果。

传统的方法是测试——跑各种输入，看看程序输出对不对。但测试有个根本问题：你不可能测试所有输入。对于稍微复杂一点的程序，输入空间几乎是无限的，你怎么测都可能有漏网之鱼。

形式化验证提供了另一种思路：用数学方法证明程序的正确性。如果你能数学地证明”对于所有可能的输入，程序都会产生正确的输出”，那就不需要担心遗漏了。

13.2 Hoare逻辑

Hoare逻辑是程序验证的基础，由Tony Hoare在1969年提出。

Hoare逻辑的核心是Hoare三元组：{P} C {Q}

意思是：如果程序C执行前P成立，那么执行后Q一定成立。P叫前置条件，Q叫后置条件。

比如对于程序x := x + 1，有Hoare三元组：

{a = 5} x := x + 1 {a = 6}

意思是：如果执行前x=5，执行后x=6。

Hoare逻辑给出了证明程序正确性的推理规则。比如合成规则：如果{P} C1 {Q}且{Q} C2 {R}，则{P} C1;C2 {R}。

13.3 验证编译器：CompCert

CompCert是一个用Coq证明正确的C编译器。它能保证：如果你用CompCert编译出来的程序，在语义上和你写的源代码是等价的。

这有什么意义呢？一般来说，编译器也可能有bug，导致编译出来的程序和源代码行为不一致。CompCert用形式化方法证明了编译器不会引入这种bug。

CompCert在航空电子设备等安全关键领域有应用。Airbus的一些项目就用了CompCert来保证关键软件的正确性。

13.4 验证操作系统：seL4

seL4是一个用Isabelle/HOL验证过的微内核。它是世界上第一个在数学上证明无运行时错误的操作系统内核。

seL4的证明非常全面，包括：

  • 证明内核的实现满足规格说明
  • 证明内核调度器满足实时约束
  • 证明内存隔离的正确性

这些证明加起来有几十万行，耗费了团队好几年的时间。但结果是：seL4的可靠性是任何传统方式开发的系统无法企及的。

十四、归结策略与优化

14.1 朴素归结的问题

理论上，只要你不停地做归结，最终一定能证出所有成立的命题（或者确定它不成立）。但”最终”可能是多久？可能是永远。

一阶逻辑的归结搜索空间是巨大的。子句的组合数、合一的可能性、归结的选择……这些都能指数级增长。如果不加任何策略，朴素归结很快就会陷入搜索爆炸。

所以实用的归结系统都需要各种优化策略来缩小搜索空间。

14.2 支撑集策略

支撑集策略要求每次归结，至少有一个亲本子句来自原假设集。直观上，这避免了归结产生的新子句之间的”自我归结”——那些归结虽然可能产生有趣的结果，但通常不是通向证明的捷径。

支撑集策略是完备的（只要命题成立，支撑集策略一定能找到证明），但可能会错过一些更短的证明路径。

14.3 单元归结优先

单元归结（unit resolution）是指归结时至少有一个亲本是单元子句——只有一个文字的子句。

单元归结可以大大加快证明速度，因为单元子句通常代表了一些重要的公理或事实，优先使用它们可以让归结过程更”聚焦”。

但单元归结不完备——用单元归结可能会错过某些证明。

14.4 语义归结

语义归结的思想是：给子句集赋予一个语义解释（比如把某些子句标记为”真”，某些标记为”假”），然后只对语义值不同的子句进行归结。

这个策略可以显著减少归结的候选对数，但需要额外的机制来维护和更新语义信息。

十五、模型检测

15.1 有限状态系统的自动验证

模型检测（Model Checking）是一种自动验证有限状态系统是否满足规格说明的技术，由Clarke和Emerson在1981年提出。

想象你要验证一个硬件电路或者通信协议。你可以用状态机建模这个系统，用时序逻辑（比如CTL）写出你要验证的性质（比如”任何请求最终都会被响应”），然后让模型检测器自动检查这个性质是否成立。

模型检测的优势是自动化程度高：不需要人工指导，算法会自动穷举系统的所有状态。不过这也限制了它的应用范围——状态数太多的系统会遭遇”状态爆炸”问题。

15.2 CTL模型检测

CTL（Computation Tree Logic，计算树逻辑）是一种用来描述系统性质的时序逻辑。

CTL公式描述的是系统的执行路径上的性质。比如：

  • AG p：所有全局路径上所有状态都满足p
  • AF p：所有全局路径上最终都会达到满足p的状态
  • EG p：存在一条全局路径上所有状态都满足p

一个经典的例子是：AG (req → AF ack)，意思是”如果请求发生，那么最终一定会有响应”。这是任何公平系统都应该满足的基本要求。

15.3 BDD与符号模型检测

传统的模型检测直接穷举系统状态。对于有n个布尔变量的系统，可能有2^n个状态——这个数字增长极快。

符号模型检测用BDD（二叉决策图）来表示状态集合和状态转移关系。BDD是一种紧凑的布尔函数表示方法，可以有效地压缩状态空间。

符号方法让模型检测能够处理的状态数大大增加。模型检测能够实用，很大程度上要归功于BDD技术。

十六、动手实验：用Z3 Python API求解逻辑谜题

16.1 Z3的安装

Z3有Python绑定，安装很简单：

pip install z3-solver

16.2 一个数独求解器

Z3可以用来解数独。思路很直接：81个变量，每个代表一个格子里的数字，加上每行、每列、每宫的唯一性约束。

from z3 import *
 
def solve_sudoku(grid):
    s = Solver()
    
    # 创建81个变量
    X = [[Int(f"x_{i}_{j}") for j in range(9)] for i in range(9)]
    
    # 每个变量在1-9之间
    for i in range(9):
        for j in range(9):
            s.add(X[i][j] >= 1, X[i][j] <= 9)
    
    # 每行不同
    for i in range(9):
        s.add(Distinct([X[i][j] for j in range(9)]))
    
    # 每列不同
    for j in range(9):
        s.add(Distinct([X[i][j] for i in range(9)]))
    
    # 每宫不同
    for bi in range(3):
        for bj in range(3):
            s.add(Distinct([X[bi*3 + i][bj*3 + j] 
                          for i in range(3) for j in range(3)]))
    
    # 加入已知的数
    for i in range(9):
        for j in range(9):
            if grid[i][j] != 0:
                s.add(X[i][j] == grid[i][j])
    
    if s.check() == sat:
        model = s.model()
        result = [[model.evaluate(X[i][j]).as_long() 
                   for j in range(9)] for i in range(9)]
        return result
    else:
        return None
 
# 测试
grid = [
    [5,3,0,0,7,0,0,0,0],
    [6,0,0,1,9,5,0,0,0],
    [0,9,8,0,0,0,0,6,0],
    [8,0,0,0,6,0,0,0,3],
    [4,0,0,8,0,3,0,0,1],
    [7,0,0,0,2,0,0,0,6],
    [0,6,0,0,0,0,2,8,0],
    [0,0,0,4,1,9,0,0,5],
    [0,0,0,0,8,0,0,7,9]
]
 
result = solve_sudoku(grid)
if result:
    for row in result:
        print(row)

16.3 逻辑谜题：狼羊菜渡河

经典的逻辑谜题：一个人要把狼、羊、白菜渡过河，但船一次只能载一个人和一样东西。如果人不在，狼会吃羊，羊会吃白菜。问怎么渡？

用Z3建模：

from z3 import *
 
# 状态：(人, 狼, 羊, 菜) 在哪边，0=左岸，1=右岸
# 初始状态：(0,0,0,0)，目标状态：(1,1,1,1)
 
def solve_river_crossing():
    s = Solver()
    
    # 变量：每一步的状态
    steps = 7  # 我们预期最多7步
    man = [Int(f"man_{i}") for i in range(steps)]
    wolf = [Int(f"wolf_{i}") for i in range(steps)]
    goat = [Int(f"goat_{i}") for i in range(steps)]
    cabbage = [Int(f"cabbage_{i}") for i in range(steps)]
    
    # 约束：每步只能带一样东西
    for i in range(steps - 1):
        # man移动，cargo = 0表示不带东西，1=狼，2=羊，3=白菜
        cargo = Int(f"cargo_{i}")
        s.add(Or(cargo == 0, cargo == 1, cargo == 2, cargo == 3))
        
        # man的位置必须改变
        s.add(man[i+1] == 1 - man[i])
        
        # 被带的东西和man一起移动
        s.add(If(cargo == 1, wolf[i+1] == 1 - wolf[i], wolf[i+1] == wolf[i]))
        s.add(If(cargo == 2, goat[i+1] == 1 - goat[i], goat[i+1] == goat[i]))
        s.add(If(cargo == 3, cabbage[i+1] == 1 - cabbage[i], cabbage[i+1] == cabbage[i]))
        
        # 不带的东西位置不变（简化表示）
    
    # 约束：不能有东西被吃掉
    for i in range(steps):
        # 如果狼和羊在一边而人不在另一边，非法
        s.add(Not(And(wolf[i] == goat[i], wolf[i] != man[i])))
        # 如果羊和白菜在一边而人不在另一边，非法
        s.add(Not(And(goat[i] == cabbage[i], goat[i] != man[i])))
    
    # 初始状态
    s.add(man[0] == 0, wolf[0] == 0, goat[0] == 0, cabbage[0] == 0)
    
    # 目标状态
    s.add(man[steps-1] == 1, wolf[steps-1] == 1, goat[steps-1] == 1, cabbage[steps-1] == 1)
    
    if s.check() == sat:
        model = s.model()
        print("找到解！")
        for i in range(steps):
            m = model.evaluate(man[i]).as_long()
            w = model.evaluate(wolf[i]).as_long()
            g = model.evaluate(goat[i]).as_long()
            c = model.evaluate(cabbage[i]).as_long()
            print(f"Step {i}: 人={'右' if m else '左'}, 狼={'右' if w else '左'}, "
                  f"羊={'右' if g else '左'}, 菜={'右' if c else '左'}")
    else:
        print("无解")
 
solve_river_crossing()

十七、应用领域

17.1 硬件验证

现代芯片设计极其复杂，少则几十亿晶体管，多则上千亿晶体管。这么复杂的系统，用传统方法验证几乎不可能。

自动定理证明和模型检测在硬件验证中扮演了关键角色。Intel、AMD、NVIDIA等芯片公司都用这些技术来验证其芯片设计的正确性。

硬件协议验证也是个重要应用。比如AXI总线协议、DDR内存协议等，这些协议的正确性直接影响芯片能否正常工作。用形式化方法可以发现协议规范中的歧义和漏洞。

17.2 软件验证

软件验证是形式化方法应用最广泛的领域之一。

编译器验证（如CompCert）、操作系统内核验证（如seL4、F力Max）、程序分析工具（如Crab、IKOS）……这些系统都需要形式化验证来保证正确性。

智能合约验证是近年来的热点。以太坊上的智能合约涉及真金白银，一旦有漏洞就可能导致财产损失。用定理证明器验证智能合约的正确性，已经成为区块链安全的重要手段。

17.3 数学研究

虽然大多数数学研究还是靠传统方法，但形式化验证正在慢慢改变数学的面貌。

四色定理、Kepler猜想、Feit-Thompson定理……这些著名的大定理都已经有了形式化证明。这不仅提高了证明的可靠性，也方便了数学家之间交流和验证彼此的工作。

数学定理库（如Mathlib、Mizar）积累了几十万条已证明的定理，这些定理库可以供自动定理证明器使用，也可以供人类数学家检索。

17.4 AI推理

在人工智能领域，自动推理技术有着广泛的应用。

知识图谱推理：判断知识图谱中实体之间是否存在某种关系，可以用归结方法来做。

专家系统：医疗诊断、法律咨询、财务分析等领域的专家系统，背后都用到了一阶逻辑推理。

自动规划：机器人的行动规划、智能体的任务规划，都可以用归结原理或模型检测来处理。

十八、历史沿革

18.1 时间线回顾

时期里程碑事件代表系统
1950s逻辑机器Newell-Shaw-Simon (1956)
1960s归结原理Robinson (1965)
1970s霍恩子句与PrologColmerauer (1972)
1980s有限模型检测模型检测工具诞生
1990s证明助手成熟Coq, Isabelle
2000s+深度学习+ATPAlphaProof等

18.2 问题分类

可判定的证明问题：

  • 命题逻辑的可满足性（SAT）— NP完全，但有高效的SAT求解器
  • 某些一阶理论的可判定片段 — 比如只含等式的理论

不可判定的证明问题：

  • 一般一阶逻辑 — 图灵可识别但不可判定
  • Peano算术 — 半可判定（完备证明系统存在，但不能判定命题是否成立）

哥德尔不完备性的影响

任何足够强的递归可枚举理论都是不完备的，意味着存在真但不可证明的命题。这限制了自动定理证明的能力边界。

参考文献

  1. Robinson, J. A. (1965). A Machine-Oriented Logic Based on the Resolution Principle. JACM, 12(1), 23-41.
  2. Lloyd, J. W. (1987). Foundations of Logic Programming (2nd ed.). Springer.
  3. Fitting, M. (2012). Types, Tableaus, and Gödel’s God. Springer.
  4. Nipkow, T., Paulson, L. C., & Wenzel, M. (2002). Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer.
  5. Baader, F., & Nipkow, T. (1998). Term Rewriting and All That. Cambridge University Press.
  6. Clarke, E. M., Grumberg, O., & Peled, D. A. (1999). Model Checking. MIT Press.
  7. de Moura, L., & Bjørner, N. (2008). Z3: An Efficient SMT Solver. TACAS.
  8. Hales, T. C., et al. (2017). A Formal Proof of the Kepler Conjecture. Forum of Mathematics, Pi, 5, e2.

相关文档

关系图谱

反向链接