代码说

code is poetry

代码说    
碎碎念:天外有天,用自己抵挡剑尖;天满烽烟,大地汹涌出我的天。 -- 大唐双龙传  换一换

56、机器数学家

作者:coderzheng 发布于:2016-8-23 20:13 Tuesday 分类:大话星程  阅读模式

达特默斯会议后,美国开始形成几个人工智能研究群体。会议参加者艾伦·纽厄尔(A.Newell)和赫伯特·西蒙(H.Simon)等人首先取得突破性进展。 
毕业于普林斯顿大学的纽厄尔博士,1961年从兰德公司转到卡内基—梅隆大学,创办了并领导了计算机科学系,使该大学跻身于世界级大学行列;他出版过10部著作,发表过250篇学术论文。赫伯特·西蒙则是芝加哥大学博士出身,在经济学、哲学、心理学、认知科学、决策科学和电脑科学等领域都作出了卓越的贡献,并以其"有限理性说"获得1978年诺贝尔经济学奖;他素有"世界著名博学家"之称,驰骋在自然科学和社会科学两大领域的前沿。 
1956年,纽厄尔、西蒙率先编制出《逻辑理论机》(TheLogicTheoryMachine),即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种不同问题的"通用问题求解程序"(GeneralProblemSolving),简称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年的光阴。

你可以发表评论、引用到你的网站或博客,或通过RSS 2.0订阅这个博客的所有文章。
上一篇: 55、AI的旗帜  |  下一篇:57、电脑大灾难