机器数学家

　　达特默斯会议后，美国开始形成几个人工智能研究群体。会议参加者艾伦·纽厄尔（A.Newell）和赫伯特·西蒙（H.Simon）等人首先取得突破性进展。

　　毕业于普林斯顿大学的纽厄尔博士，1961年从兰德公司转到卡内基—梅隆大学，创办了并领导了计算机科学系，使该大学跻身于世界级大学行列；他出版过10部著作，发表过250篇学术论文。赫伯特·西蒙则是芝加哥大学博士出身，在经济学、哲学、心理学、认知科学、决策科学和电脑科学等领域都作出了卓越的贡献，并以其“有限理性说”获得1978年诺贝尔经济学奖；他素有“世界著名博学家”之称，驰骋在自然科学和社会科学两大领域的前沿。

　　1956年，纽厄尔、西蒙率先编制出《逻辑理论机》（The Logic Theory Machine），即LT数学定理证明程序，被人们公认是第一个AI程序。在卡内基—梅隆大学计算机实验室，纽厄尔和赫伯特·西蒙从分析人类解答数学题的技巧入手，让一些人对各种数学题作周密的思考，要求他们不仅写出求解的答案，而且说出自己推理的方法和步骤。通过大量的观察实例，纽厄尔和西蒙广泛收集了人类求解一般性数学问题的各种方案。例如，他们给出一个用字母表达的算术式，式中相同的字母代表相同的数字：
　　A　A　　　　　　　　　2　2
　　＋B　B　　　　　　　　＋9　9
　　--------　　　→　　　-------
　　C　A　C　　　　　　　　1　2　1

　　然后，请受试者判断哪些数字能够使这种算术式成立。纽厄尔和西蒙发现，人们解答这类问题通常是用试凑方法进行，试凑时不一定列出了所有的可能性，常常从某些极端的数（如0或9）或者平均数（如5）开始，经过逻辑推理，迅速缩小搜索的范围。经过反复实验，他们进一步认识到，人类证明数学定理也有类似的思维规律，经过“分解”和“代入”等方法，用已知的定理、公理或解题规则进行试探性推理，直到所有的子问题最终都变成已知的定理或公理，从而解决整个问题。

　　在实验结果启发下，纽厄尔和西蒙用LT程序向数学定理发起了激动人心的第一次冲击。电脑果然不负众望，一举证明了数学大师罗素的名著《数学原理》第二章中的38个定理。1963年，经过改进的LT程序在一部更大的电脑上，最终完成了全部52条数学定理的证明。在成功的基础上，纽厄尔和西蒙把LT程序扩充到人类求解一般问题的过程，设想用机器模拟具有普遍意义的人类思维活动。他们编制了能解答10种不同问题的“通用问题求解程序”（General Problem Solving），简称GPS，被IBM公司引进作为研究AI的工具。因为开拓了人工智能“问题求解”的重大领域，纽厄尔与西蒙共享了1975年“图林奖”。

　　在纽厄尔和西蒙之后，美籍华人学者、洛克菲勒大学教授王浩在“自动定理证明”上获得更大的成功。1959年，王浩用他首创的“王氏算法”，用一台速度不高的IBM704电脑再次向《数学原理》发起挑战。不到9分钟，机器把这本数学史上视为里程碑的著作中全部（350条以上）定理，统统证明了一遍。该书作者、数学大师罗素得知此事后感慨万端，他在一封信里写到：“我真希望，在怀海特和我浪费了10年的时间用手算来证明这些定理之前，就知道有这种可能。”

　　人工智能定理证明最有说服力的例子，是机器证明了困扰数学界长达100余年之久的难题——“四色定理”。据说，“四色问题”最早是1852年一位21岁的大学生提出的数学难题：任何地图都可以用最多四种颜色着色，就能区分任何两相邻的国家或区域。这个看似简单的问题，就象“哥德巴赫猜想”一样，不知难倒了多少著名数学家和献身数学的业余爱好者，属于世界上最著名的数学难题之一。

　　1976年6月，美国伊利诺斯大学的两位数学家沃尔夫冈·哈肯（W.Haken）和肯尼斯·阿佩尔（K.Apple）自豪地宣布，他们用电脑证明了这一定理。当“四色定理”被证明的消息传出后，许多大学的教师都纷纷中断讲课，打开香槟酒以示庆贺。在该定理被证明的所在地——伊利诺斯州乌班纳，连邮政局员工都欣喜若狂，他们在寄出的所有信件上都加盖了“四色是足够的”字样邮戳。

　　哈肯和阿佩尔攻克这一难题使用的方法仍然是前人提出的“穷举归纳法”，只是别人用的是手工计算，无论如何也不能“穷举”所有的可能性。哈肯和阿佩尔编制出一种很复杂的程序，让3台IBM360大型电脑去自动高速寻找各种可能的情况，并逐一判断它们是否可以被“归纳”。十几天后，共耗费了1200个机时，做完了200亿个逻辑判断，电脑终于证明了“四色定理”。虽然至今有些从事纯数学研究的学者仍对此半信半疑，那冗长乏味的证明是否就是“四色难题”的最后结论？但他们毫无办法来验证电脑是否真正给出了答案，200亿个逻辑判断是人不可能逐一检验的天文数字。如果你有兴趣深入探讨，可以自己去研究《伊利诺斯数学杂志》第21卷刊载的检验表，那张表足有460页厚，可能会消磨掉你10年的光阴。

转载本站内容时，请务必注明来自W3xue，违者必究。