人工智能伦理

图1.146 自然之美的背后必定有一个成因，多半能够解释为某类数学

合情推理

图1.147 波利亚

美籍匈牙利裔数学家、教育家乔治·波利亚（GeorgePólya, 1887—1985）在其著作《数学与合情推理》中提出了一种基于“不完全归纳”的启发式推理——合情推理（plausiblereasoning）^[39]。例如，哥德巴赫猜想至今未被证明或证伪，无论计算机提供多少正例都不算证明，但要证伪它，一个反例就足够了。目前找到的正例越来越多，所以人们在心理上更倾向于认为该猜想是对的。

例1.31 1742年，德国数学家克里斯蒂安·哥德巴赫（Christian Goldbach, 1690—1764）提出一个猜想：任意不小于6的偶数都可分解为两个奇素数之和，简称为“1+1”。例如，12=5+7,100=53+47=59+41=···=97+3。

图1.148 1966年，中国数学家陈景润（1933—1996）取得了迄今为止哥德巴赫猜想最好的结果，所用方法被誉为“筛法理论光辉的顶点”

陈景润证明了，“任何充分大的偶数都可表示为一个素数及一个不超过两个素数的乘积之和”，简称为“1+2”。例如，$1 2 { = } 3 { + } 3 { \times } 3 { = } 2 { + } 2 { \times } 5$ 。下面用Maxima给出了100的哥德巴赫分解，并验证了6至 $2 \times 1 0 ^ { 3 }$ 的偶数都满足哥德巴赫猜想。为简单起见，算法未经优化。

目前，利用计算机已经验证了 $\eta \equiv 1 0 ^ { 1 8 }$ 的偶数都满足哥德巴赫猜想。但面对无限个可能的情形，有限的验证不等于证明，哥德巴赫猜想依然是未解决的数学难题。但大多数的数学家相信该猜想是正确的，证得它只是早晚的问题。

数学推理

数学是一切自然科学的工具，强人工智能在理性思维上要达到甚至超越人类的水平，首先必须在数学的机械化上有所突破。更直白地说，强人工智能先得成为一位数学家，具备自动推理（ automated reasoning ） 的 能 力 ， 例 如 ， 自 动 定 理 证 明（automated theorem proving,ATP）^[40]，才有可能创造理性思维的新高度。

SLOVENSKO

MEDZINÁRODNÁ 1.25 MATEMATICKÁ OLYMPIÁDA

图1.149 自动推理是数理逻辑、计算机科学、统计推断的交叉学科，它的目标是让机器具备和人类一样的推理能力

口 两位图灵奖得主（1975）艾伦·纽厄尔和赫伯特·西蒙，以及AI科学家克里夫·肖（Clifford Shaw,1922—1991），分别于1956年和1959年研制出自动逻辑推理工具“逻辑学家”（logic theorist）和“通用问题求解器”（general problem solver,GPS）。“逻辑学家”证明了《数学原理》⁽²²⁾第二章中的三十多条定理。

口 1959年，美籍华人数理逻辑学家、计算机科学家、哲学家王浩（Hao Wang, 1921—1995）在IBM 704计算机上用时几分钟证明了《数学原理》中数百条定理，该工作于1983年荣获人工智能国际联合会议的第一个自动定理证明里程碑奖。

那时的AI先驱们对未来充满信心，“逻辑学家”的创造者们认为，“现在世界上有能思考、学习和创造的机器。并且，它们做这些事情的能力将迅速提升，（在可预见的未来）它们所能处理问题的范围将与人类思维所及的范围相一致”。

这个目标太宏伟了，至今仍未实现，估计短期之内没啥希望，除非机器学习和人工智能在自动推理上有突破性的进展。尽管像四色定理、哥德尔不完全性定理、微积分基本定理、代数基本定理、若尔当曲线定理、布劳威尔不动点定理、柯西留数定理、素数定理、奇阶定理等一些著名的数学结果都已有机器证明，我们依然缺乏系统的方法，广泛地实现数学的机械化。

■ 法国国家信息与自动化研究所（INRIA）、巴黎综合理工学院、巴黎第十一大学、巴黎第七大学、法国国家科学研究中心等单位联合开发的Coq（法文“雄鸡”）系统，是开源的交互式定理证明辅助工具。数学家和计算机科学家已经利用Coq证明了几个需要长篇论证的结果，如四色定理、奇阶定理（即奇阶的有限群都是可解的）等。