自动定理证明 — 符号派的理论底座
这一章讲三件事: 让机器证明定理这个念头从哪来(希尔伯特的梦,以及哥德尔怎么 判了它死刑);归结原理怎么让"一条规则证明一切"看起来可行,又怎么被组合爆炸拖垮; 以及这个"失败"的领域给后来的一切留下了什么——专家系统的术语、NP 完全性、 吴文俊的几何定理证明,和今天大模型时代的证明器复兴。 这一章的术语密度是全书最高的一章,但每个词后面三章都会再用到,值得慢读。
1. 这一章讲什么
符号派 AI 的思想源头是定理证明:原书原话,"人工智能中符号派的思想源头和理论基础就是 定理证明,不懂定理证明就没法深入了解符号派"1。
它的大背景是一场数学危机。20 世纪初的数学哲学有三大派:逻辑主义(罗素,主张把数学 归约到逻辑)、形式主义(希尔伯特,主张数学就是把一串符号按规则变成另一串符号)、 直觉主义。希尔伯特的梦想是找到一个统一的算法,让所有数学问题都能被机械地解答2。
哥德尔 1931 年的不完全性定理判了这个梦想死刑:任何足够强的数学系统中, 都有真命题无法被证明。机器定理证明研究继承的是梦想的残余部分—— "用机器来证明和判定那些可以证明和判定的问题"2。
本章的主线一句话:一个"道理上通、工程上堵"的领域——归结原理在数学上完美, 在算力上爆炸;它倒下之后,它的概念被邻居们打包带走,而它自己在三十年后等来了 深度学习和大模型给它接的氧气。
2. 顶层全景
1931 哥德尔:完备的机械数学不存在(梦想收缩为"做可判定的部分")
↓
1954 戴维斯:第一个定理证明程序(只能算"只有加法的算术",跑出
"两个偶数之和还是偶数"就已经激动不已)
↓
1956 逻辑理论家(达特茅斯,命题逻辑) ──被逻辑学家鄙视──→
1958 王浩:9 分钟碾压一阶逻辑 ──其学生库克──→ 1971 NP完全性
↓
1965 罗宾逊:归结原理(一条规则统吃)→ 阿贡小组工程化(Otter)
↓ ↓
70-80年代 组合爆炸 + 路线斗争 1996 EQP 证罗宾斯猜想
(定理证明 vs 问题解决;中心移向欧洲) (486 跑 13 天)
↓ ↓
2006 阿贡小组被裁(同年辛顿发表深度学习) ──术语被专家系统打包──→
2013→ Lean 证明器 → 大模型时代 AlphaProof、o1/R1:起死回生
图说:上半场是"证明一切的野心",下半场是"野心碎掉之后的遗产"。
每一格后面都有可走查的具体例子,主走查在第 3.3 节。
3. 核心原理
3.1 先分清两个"逻辑":命题逻辑和一阶逻辑
这一章(以及全书)反复用到这两个词,先就地讲清。
命题逻辑处理的是整句之间的连接:用"并且、或者、非"把已经当作整体的命题拼起来。 它简单,但表达力弱——"所有人都会死"这句话,命题逻辑只能当成一个不可拆的原子。
一阶逻辑(也叫谓词逻辑)把句子拆到个体和性质:"对所有 x,如果 x 是人, 那么 x 会死"可以写成一条带变量(变量,就是可以代入不同名字的占位符,比如 x)的规则。代价是推理变难了——后面所有技术性情节 (合一、归结、不可判定)都发生在这一层3。
3.2 第一个程序:从"可判定"的边角下刀
定理证明的第一步不是证明难的定理,而是找机器能判定的问题。 "判定"的意思是:存在一个算法,对任何输入都能在有限步内给出"是"或"否"。
数学家戴维斯 1954 年写出了第一个定理证明程序,跑在以冯诺伊曼昵称命名的电子管计算机 JOHNNIAC 上。他选的战场叫普利斯博格算术——只含加法、不含乘法的自然数算术。 这个选择背后的分界线是:完整的算术(皮亚诺算术)不可判定,哥德尔证的; 但去掉乘法之后的加法算术是可判定的4。
代价依然惊人:普利斯博格算术的判定算法,要花比按指数(一秒翻倍、再翻倍地滚雪球)速率增长还要多的时间。 所以这台电子管机器上跑出的第一个成果朴素得可爱:"两个偶数之和还是偶数"4。 参照物(补充:不在书里,来自通用知识):今天一部手机的算力大约是这台机器的千万倍以上——第一个定理证明程序的 全部产出,在今天连一次屏幕刷新都撑不满。
戴维斯后来与哲学家普特南合作出戴维斯-普特南(DP)过程,再演化为 DPLL—— 这个名字今天还活着:它是一切 SAT 求解器(判断一堆逻辑条件能否同时满足的程序) 的祖先5。
3.3 主走查:归结原理,一条规则统吃
1965 年,阿兰·罗宾逊发表了归结(resolution)原理。它回答的问题是: 以前的定理证明要用很多条推理规则,能不能把所有证明归约成一条规则?
归结原理说能。主走查就从这里开始,拿逻辑学最著名的例子走一遍: 证明"苏格拉底必死"。已知两条知识6:
大前提: 对所有 x:Man(x) → Mortal(x) (人都会死)
小前提: Man(Socrates) (苏格拉底是人)
第 0 步,反证法准备。 定理证明器用反证法工作:把"苏格拉底必死"的否定加进知识库, 如果能推出矛盾,原命题就得证。三条"子句"(子句就是只含"或"连接的最简逻辑式, 这是归结原理要求的格式):
C1: ¬Man(x) 或 Mortal(x) ← 大前提改写成子句
C2: Man(Socrates) ← 小前提
C3: ¬Mortal(Socrates) ← 结论的否定
第 1 步,合一。 归结只能在"一个子句里有 Mortal(·)、另一个里有 ¬Mortal(·)" 这种正反配对时使用。C1 里的变量 x 和 C3 里的 Socrates 不直接匹配, 合一(unification)就是找一组变量替换,让两边的式子长得一样:取 x := Socrates, C1 变成 ¬Man(Socrates) 或 Mortal(Socrates),和 C3 的 ¬Mortal(Socrates) 正好碰上。
第 2 步,归结出矛盾。 把 C1(替换后)和 C3 归结:Mortal(Socrates) 与 ¬Mortal(Socrates) 一正一负互相抵消,剩下 ¬Man(Socrates)。
第 3 步,再来一次。 剩下的 ¬Man(Socrates) 与 C2 的 Man(Socrates) 归结, 抵消后什么都不剩——得到空子句。空子句就是矛盾:知识库里既有 Man(Socrates) 又推出 ¬Man(Socrates),说明"结论的否定"站不住,原命题得证。
C1: ¬Man(x) ∨ Mortal(x) C3: ¬Mortal(Socrates)
│ 合一 x:=Socrates,归结 │
└────────────→ ¬Man(Socrates) ←────┘
│ 与 C2: Man(Socrates) 归结
▼
空子句 □ = 得证
图说:每一步都是"一正一负相消"。归结证明 = 反复合一 + 相消,直到撞出空子句。
为什么这件事曾经让人狂热? 因为它把"证明"这件事完全机械化了:不需要聪明, 不需要直觉,只需要不知疲倦地做"合一、相消"这一对动作。一招鲜,吃遍天—— 整个逻辑主义定理证明的理想就在这四个字里7。
为什么它后来停摆? 副作用:归结每一步都可能生成大量新子句,而绝大多数新子句没用。 原书打的比方:像图书馆清理旧书——已知"所有人必死"时,生成的中间结论 "苏格拉底必死"不必保存,因为一般命题已经包含(subsumption)了它8。 但判断"谁包含谁"本身就是开销:有的证明器要花超过 95% 的时间做包含测试9。 规则只有一条,搜索空间却是指数的——归结没有消灭复杂性,只是把它从"规则的多样性" 搬进了"子句的爆炸"。 这个"组合爆炸"就是符号派此后一切挫败的技术根源。
3.4 会答问题的证明器:ANS 谓词
归结证明只能回答"是/否"。1969 年格林想出一个便宜的办法让证明器顺带报出答案: 在待证子句上挂一个系统谓词 ANS,把变量绑在它身上。
走一遍(接上面的格式):想知道"玛丽的丈夫是谁",不问 "玛丽有丈夫吗",而是问否定式 ¬Husband(x, Mary) 或 ANS(x)。知识库里有一条 Husband(John, Mary)。两子句归结,x 被 John 替换,得到 ANS(John)—— 矛盾达成了,而答案就在 ANS 里:玛丽的丈夫是约翰10。
这个技巧至今活在定理证明器里(Otter 系统里所有系统谓词以 $ 开头,$ANS 跟踪变量取值)10。 它也是"问答系统"最早的技术雏形——第 07 章的问答系统与沃森, 问的都是同一个问题:证明之外,把答案带出来。
3.5 王浩:9 分钟、一条岔路和一个学科
1958 年,王浩在一台 IBM 704 上只花 9 分钟就证明了《数学原理》一阶逻辑全部 150 条 定理中的 120 条;1959 年的改进版证明了全部一阶逻辑定理11。对照物: 逻辑理论家只有一个暑假的命题逻辑——王浩的速度优势在百倍以上(补充:不在书里,来自通用知识——按同期同类计算机的任务量折算)。
比速度更重要的是他注意到的一件小事:《数学原理》里的公式都是"全称量词在前、 存在量词在后"的特定形状(AE 形)。沿着这个形状往下挖,他的学生库克在 1971 年 发表了《定理证明的复杂性》,提出 NP 完全性——今天计算机科学最重要的问题 P 与 NP 是否相等,直接从定理证明里长了出来。库克自己说:"图灵和王浩研究谓词逻辑, 我研究命题逻辑。"12 原书判语:"王浩的定理证明研究孕育了整个理论计算机科学。"12
这条线在第 09 章展开。这里只需要带走一件事:符号派最值钱的遗产不是证明出来的定理, 而是从证明里长出来的复杂性理论。
3.6 阿贡小组:把理想熬成工程
归结原理的工程化主场在芝加哥的阿贡国家实验室。小组的灵魂人物沃思是位盲人数学家, 另一个关键人物马库恩用 C 语言写了定理证明器 Otter——顺带说一句,美国 AI 的主流语言 是 LISP,马库恩开玩笑说自己不会写 LISP 只会写 C13。
1996 年 10 月 10 日,马库恩的 EQP 证明了罗宾斯猜想——一个 1933 年提出、 悬置 63 年的布尔代数猜想:一台 486 个人电脑跑了 13 天给出证明, 再用一台工作站验证了 7 天14。对照:逻辑理论家证明一条三段论要小时级机时, EQP 的输出是一份人类专家确认无误的 63 年悬案证明。《纽约时报》当即报道 。
但这是高峰也是尾声。定理证明界的内部撕裂(引入过程知识的"不纯派"与认为那算作弊的 "纯派"、逻辑与心理之争)、费根鲍姆对罗宾逊的攻击、经费转向,让美国的定理证明 在 70 年代后凋零,重心移向欧洲——在那里,逻辑程序应运而生,成为日本五代机的 理论基础(第 03 章接这一棒)15。2006 年,阿贡小组被裁撤;同一年, 辛顿的深度学习论文发表在《科学》上。原书把这两件事并置为时代的换幕16。
3.7 吴文俊:另一条路——先找对子领域
归结想"一招鲜吃遍天",吴文俊走了相反的路。他在研究中国数学史时受到启发, 1977 年(大年初一取得突破)给出了针对初等几何这一大类问题的高效机器证明方法17。
这个分野原书讲得很清楚:逻辑学家把机器定理证明当目标,数学家把它当工具; 逻辑学家看是否纯粹,数学家看是否有用18。王浩早就总结过:"最有效的方法是先找对 一个相对可控的子领域,然后针对这个子领域的特性,找到有效的算法。"19 吴文俊的方法后来经学生周咸青在得州奥斯汀发扬光大,他本人 1997 年获定理证明领域的 最高奖埃尔布朗奖20。"领域特定"对"通用一招鲜"的胜利,是本章最重要的方法论结论, 第 05 章强化学习的"苦涩的教训"会再次回到它——但方向相反。
3.8 复兴:Lean 与大模型把氧气送了回来
定理证明的现代化身叫证明辅助器——不完全自动,而是机器逐步验证人写的证明。 2008 年,Coq 被用来验证四色定理的机器证明;2013 年,微软的莫拉把 Lean 开源(公开源代码,人人可用)。 大语言模型出现后,Lean 的地位被强化:Meta、Google(AlphaProof)、DeepSeek 都支持它, 数论家巴扎德正用 Lean 重写费马大定理的证明,陶哲轩呼吁数学家把已证定理用 Lean 重新捋一遍21。
绕回来的原因正是本章开头那条线:2022 年起的大语言模型数学推理能力弱于 语言生成能力 (下一节细说),于是有人把强化学习接进来练推理——OpenAI 的 o1(2024 年夏)、 DeepSeek 的 R1(2025 年 1 月 20 日发布)是代表22。定理证明这个最"死"的领域, 成了检验"机器会不会思考"最硬的试金石。
4. 作者的判断与证据
史实层:本章全部关键事件(戴维斯 1954、王浩 1958-59、罗宾逊 1965、EQP 1996、 阿贡 2006 被裁)有论文与机构记录支撑,原书引用了戴维斯的口述与历史综述。 作者自己就是这段历史的近距离观察者——他当面问过戴维斯对五代机的看法, 老头儿狡猾地答"我对工业不太懂"23。
作者观点层(需与史实分开):
- "有些领域一开始就把百分之八十的容易问题解决了,而后就一直很难"——AI 如此, 定理证明尤其如此24;
- "数学家没觉得这玩意儿有用,人工智能的两派人马都不待见"——定理证明两头受气的处境, 是作者反复强调的解释框架25;
- 对"机器证明算不算证明"的哲学讨论,作者的立场偏向实用主义:数学共同体的实践标准 正在从"数学家互相核实"变成"数学家信任的程序互相核实"26。
原书自己注明的不确定处:吴文俊自称方法受中国古代数学(算法传统)启发, "这一点尚未得到数学史家的共识"27——原书照实声明了,拆解也照实转。
5. 边界与局限
- 自动定理证明没有兑现"证明一切"的承诺。 组合爆炸至今没有理论解;一阶逻辑尚且 举步维艰,高阶逻辑更难24。
- AlphaZero 式的自学在证明领域没有复刻成功。 对弈有胜负信号,证明的"进展信号" 很难定义——这是它比下棋难的本质原因(原书:"定理证明比下棋可难多了")28。
- 本章未覆盖大模型时代证明进展的细节(AlphaProof 的具体成绩原书只提了一句), 2024 年后 IMO 级别的突破请 以最新资料为准。
- 原文里"罗宾斯猜想的第三公理可能是印刷错误"是马库恩的玩笑,不是学术判断, 引用时要小心14。
6. 可带走的
- 符号派的底座是定理证明,而定理证明的底座是"找可判定的子问题"—— 完整算术不可判定,只加法的算术可判定:先圈一块能算的阵地;
- 归结原理 = 合一 + 相消,直到空子句:一条规则机械地完成一切证明, 这是符号派理想的极简形态;
- 它的失败原因是组合爆炸:规则少了,中间产物(子句)指数膨胀, 95% 的时间耗在"删掉没用的中间结论"上;
- 王浩 9 分钟对一阶逻辑的碾压说明:同一个目标,专用算法可以百倍于通用框架;
- 库克的 NP 完全性从定理证明里长出来——P 对 NP 的问题就是"验证容易求解难" 的形式化,这句直觉的严格版在第 09 章;
- "领域特定"胜过"通用一招鲜"(王浩、吴文俊),但 2019 年的《苦涩的教训》 会给出大数据算力条件下的反向结论——两个结论各自的适用边界是全书的一条暗线;
- 今天 AI 圈的一半术语来自这里:知识库=公理集合、规则库=支持集、 知识图谱的描述逻辑=被约束的一阶逻辑子集29;
- Lean + 大模型是定理证明的复兴,它的深层意义:数学证明正在变成 可被机器验证、可被模型学习的数据。
7. 原文地图
| 主题 | 原书章 | 原文位置 |
|---|---|---|
| 定理证明是符号派源头、希尔伯特纲领 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:46(搜「思想源头」) · text/06-ch02.txt:19(搜「三大派」) |
| 哥德尔判死、继承残余 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:25(搜「证明这一切是不可能」) · text/06-ch02.txt:26(搜「证明和判定」) |
| 戴维斯第一个程序、普利斯博格算术 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:51(搜「JOHNNIAC」) · text/06-ch02.txt:67(搜「普利斯博格」) |
| 两个偶数之和、超指数 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:70(搜「超指数」) · text/06-ch02.txt:72(搜「偶数之和」) |
| DP→DPLL | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:84(搜「DPLL」) |
| 苏格拉底三段论的形式化 | 第3章 从专家系统到知识图谱 | text/07-ch03.txt:157(搜「苏格拉底」) |
| 逻辑理论家被克里尼退稿、王浩的批评 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:104(搜「克里尼」) · text/06-ch02.txt:114(搜「杀鸡焉用宰牛刀」) |
| 王浩 9 分钟、AE 形式、库克 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:138(搜「9分钟」) · text/06-ch02.txt:159(搜「AE形式」) · text/06-ch02.txt:161(搜「NP完全性」) |
| 王浩孕育理论计算机科学 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:163(搜「孕育了整个理论计算机科学」) |
| 普拉维茨、合一概念 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:120(搜「自然演绎」) · text/06-ch02.txt:125(搜「合一」) |
| 罗宾逊归结原理、包含 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:219(搜「归结」) · text/06-ch02.txt:231(搜「包含」) · text/06-ch02.txt:233(搜「图书馆」) |
| 组合爆炸 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:361(搜「组合爆炸」) |
| ANS 谓词走查 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:306(搜「玛丽的丈夫」) · text/06-ch02.txt:318(搜「ANS」) |
| 阿贡小组、沃思、马库恩 Otter | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:260(搜「阿贡小组」) · text/06-ch02.txt:279(搜「Otter」) |
| EQP 证罗宾斯猜想(486/13天) | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:293(搜「罗宾斯猜想」) · text/06-ch02.txt:294(搜「486」) |
| 路线斗争、逻辑与心理、移向欧洲 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:329(搜「路线斗争」) · text/06-ch02.txt:364( 搜「重心逐渐从美国转向欧洲」) |
| 项重写、Knuth-Bendix、superposition | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:241(搜「项重写」) · text/06-ch02.txt:253(搜「1970年开启」) |
| 吴文俊 1977 突破、数学机械化 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:399(搜「大年初一」) · text/06-ch02.txt:446(搜「数学机械化」) |
| 王浩论领域特定 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:441(搜「一招鲜」) · text/06-ch02.txt:444(搜「子领域」) |
| 周咸青、埃尔布朗奖 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:403(搜「周咸青」) · text/06-ch02.txt:768(搜「埃尔布朗奖」) |
| 弗雷德金奖、芒福德"一百年都够呛" | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:497(搜「莱布尼茨奖」) · text/06-ch02.txt:502(搜「一百年都够呛」) |
| 四色定理、200TB 证明、有限单群 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:515(搜「四色定理」) · text/06-ch02.txt:537(搜「200TB」) · text/06-ch02.txt:546(搜「1万页」) |
| 术语重新包装(知识库=公理集合) | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:624(搜「重新包装」) · text/06-ch02.txt:627(搜「被约束的一阶逻辑的子集」) |
| 阿贡 2006 被裁、辛顿同年 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:609(搜「2006年被裁」) |
| 八十容易问题、领域判断 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:619(搜「百分之八十」) |
| o1/R1、Lean 复兴、陶哲轩 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:662(搜「o1」) · text/06-ch02.txt:673(搜「Lean」) · text/06-ch02.txt:523(搜「费马大定理」) |
| 吕埃勒"后人类数学"、比下棋难 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:761(搜「后人类数学」) · text/06-ch02.txt:764(搜「可难多了」) |
| 戴维斯"我对工业不太懂" | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:97(搜「对工业不太懂」) |
| 数学共同体的标准在变 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:556(搜「实践标准在变」) |
| 吴文俊思路尚无共识 | 第2章 自动定理证明兴衰纪 | text/06-ch02.txt:592(搜「尚未得到数学史家的」) |