维基百科

逻辑理论家

（重定向自Logic Theorist）

逻辑理论家（英语：Logic Theorist）是由艾伦·纽厄尔、司马贺和约翰·克里夫·肖（英语：John Clifford Shaw）于1955年和1956年间编写的计算机程序，是首个可以自动进行推理的程序，被称为“史上首个人工智能程序”。[a]它最后证明了在怀特黑德和罗素合作撰写的数学原理中首52个定理中的38个，在当中更是找到既新颖又优雅的证明。[2]

历史

编辑

1955年，当纽厄尔和西蒙开始研发逻辑理论家时，人工智能领域尚未存在，就连术语“人工智能”也在第二年的夏天才开始使用。[b]

西蒙本身是一位政治科学家，当时他已经在研究官僚如何运作以及持续拓展他的有限理性理论（为此他后来得到诺贝尔奖）。研究商业组织时需要人工智能拥有像人类一样决策和解决问题的洞察力。西蒙记得在20世纪50年代初向兰德咨询时看到一台打印机在印地图，使用普通字母和标点符号作为符号。他意识到可以整理和排列符号的机器也可以模拟决策过程，甚至可以模拟人类的思考过程。[4][5]

打印地图的程序是由研究物流和组织理论的兰德公司科学家纽厄尔编写的。对于纽厄尔来说，决定性的时刻是在1954年奥利弗·塞尔弗里奇（Oliver Selfridge）到兰德来描述他在模式匹配方面的工作。观看演示时，纽厄尔忽然明白简单的可编程单元的交互如何实现复杂的行为，包括人类的智能行为。他后来说：“这一切都发生在一个下午。”[6]这是科学界人物顿悟的罕见时刻。

“我的感觉很清晰，这是一条新的道路，我将会走下去；我并不是每次也有这种感觉。”[7]

纽厄尔和西蒙开始讨论教机器思考的可能性。他们的首个程序是要能够证明数学定理的，于伯特兰·罗素和阿尔弗雷德·诺思·怀特黑德撰写的数学原理中可找到。他们还有来自兰德的计算机程序员约翰·克里夫·肖（英语：John Clifford Shaw）帮忙开发该程序。（纽厄尔说“克里夫是三人中真正的计算机科学家”[8]）。首个版本是手工模拟的：他们将程序编写到3x5卡片上，正如西蒙回忆的那样：

在1956年1月，我让我的妻子与三个孩子们跟一批研究生聚集在一起。我们给了小组的每个成员一张卡片，使每一张卡片将对应于计算机程序的一个组成部分……这就是大自然模仿艺术模仿自然。[9]

他们成功地证明了该程序可以像一位才华横溢的数学家般成功地证明定理。然后，克里夫能够在兰德的圣莫尼卡工厂里面的计算机上运行该程序。1956年夏天，约翰·麦卡锡、马文·闵斯基、克劳德·香农和纳撒尼尔·罗切斯特组织了一次会议，是关于“人工智能”（麦卡锡为了该会议而创造的术语）的。纽威尔和西蒙自豪地向小组介绍了逻辑理论家，但当听众反应冷淡时，他们感到有些惊讶。帕梅拉·麦科杜克写道：“可以肯定当时除了纽维尔和西蒙之外，没有人能够感受到他们所做的事情具有长远意义。”[10]西蒙承认“我们对这一切可能相当傲慢”[11]并补充道：

他们不想听我们的介绍，我们也肯定不想听到他们的回应：我们有东西要向他们展示！……在某种程度上，这是有点儿讽刺的，因为我们已经满足了他们的期望；其次，他们没有太在意它。[12]

逻辑理论家很快就证明了数学原理第2章中的前52个定理中的首38个，当中定理2.85的证明实际上比罗素和怀特黑德手抄的证明更优雅。西蒙能够向拉塞尔本人展示新的证明，他“高兴地回答”。[2]他们试图将新的证明发表到《符号逻辑学报》中，但它被拒绝的理由是一个基本数学定理的新证明并不值得注意，显然忽略了其中一个作者是计算机程序的事实。[13][2]

纽厄尔和西蒙建立了长久的合作伙伴关系，创建了其中一个最早的人工智能实验室卡内基科技（英语：Carnegie Tech），并开发和发展了一系列富有影响力的人工智能程序和理念，包括通用解难器、Soar及认知统一理论。

逻辑理论家对人工智能的影响

编辑

逻辑理论家引入了几个对人工智能研究至关重要的概念：

推理为搜索
逻辑理论家用到了搜索树：搜索树的根是最初的假设，每条分支都是推论，于是树中的某个地方将会是该程序旨在证明的命题，每条分岔路都是一个形式证明（英语：Formal proof）——使用逻辑规则推导出的一系列陈述，这些陈述从假设到要证明的命题。
启发式
纽厄尔和西蒙意识到搜索树会指数增长，他们需要使用“经验法则”来确定哪些路径不太可能导出解决方案，然后再“修剪”一些分支。他们称这规则“启发式”，出自乔治·波利亚在其关于数学证明的经典著作《怎样解题》（纽维尔曾在斯坦福大学攻读过波利亚的课程）。[14]启发式算法将成为人工智能研究的一个重要领域，并且仍然是克服指数增长搜索招致组合爆炸（英语：Combinatorial explosion）的重要方法。
列表处理
为了在计算机上实现逻辑理论，这三位研究人员开发了一种编程语言，名为资讯处理语言。

哲学意涵

编辑

帕梅拉·麦科杜克写道，逻辑理论家“积极地展示了机器具有创意和智能”。[2]因此，它代表了人工智能发展和我们对智能的理解的里程碑。

1956年1月，西蒙着名地告诉给其中一班研究生，“圣诞节期间，艾伦·纽厄尔与我发明了一台会思考的机器”[15][16]，

并写道：

我们发明了一种能够以非数字方式思考的计算机程序，从而解决了古老的心物问题，解释了由物质组成的系统如何具有心灵的属性。[17]

“机器可以像人一样有思想”的这种说法后来被哲学家约翰塞尔命名为“强人工智能”。到目前为止，它仍然是一个严肃的辩论主题。

逻辑理论家令帕梅拉·麦科杜克都受到启发，一种新的心理理论——资讯处理模型（有时称为心灵计算理论）因而首次亮相。她写道，“这种观点将成为他们后期工作的核心，并且在他们看来，这是二十世纪理解思想的核心，因为达尔文的自然选择原则是在十九世纪理解生物学。”[18]纽厄尔和西蒙后来将这个提议正式化为物理符号系统假设。


笔记

编辑
  1. ^ 逻辑理论家通常被认为是第一个真正的人工智能计划，尽管约翰·克里夫·肖（英语：John Clifford Shaw）的跳棋程序更早。克里斯托弗斯特拉奇（英语：Christopher Strachey）也在1951年写了一个跳棋程序。[1]
  2. ^ “人工智能”一词是由约翰·麦卡锡在1956年达特矛斯会议的提案中创造的。据丹尼尔·克雷维尔（英语：Daniel Crevier）所言，是次会议“被普遍认为是新科学的官方诞生日期。”[3]

引文

编辑
  1. ^ Crevier 1993，第44页.
  2. ^ 2.0 2.1 2.2 2.3 McCorduck 2004，第167页.
  3. ^ Crevier 1993，第49–50页.
  4. ^ Crevier 1993，第41–44页.
  5. ^ McCorduck 2004，第148页.
  6. ^ McCorduck 2004，第157–158页.
  7. ^ McCorduck 2004，第158–159页.
  8. ^ McCorduck 2004，第169页.
  9. ^ Crevier 1993，第45页.
  10. ^ McCorduck 2004，第124页.
  11. ^ Crevier 1993，第48页.
  12. ^ Crevier 1993，第49页.
  13. ^ Crevier 1993，第146页.
  14. ^ Crevier 1993，第43页.
  15. ^ McCorduck 2004，第138页.
  16. ^ CMU Libraries: Problem Solving Research. [2019-05-03]. （原始内容存档于2020-02-18）. 
  17. ^ Crevier 1993，第46页.
  18. ^ McCorduck 2004，第127页.

参考

编辑
  • Crevier, Daniel (1993), AI: The Tumultuous Search for Artificial Intelligence, New York, NY: BasicBooks, ISBN 0-465-02997-3, pp. 44–46.
  • McCorduck, Pamela (2004), Machines Who Think (2nd ed.), Natick, MA: A. K. Peters, Ltd., ISBN 1-56881-205-1, pp. 161–170.
  • Russell, Stuart J.; Norvig, Peter (2003), Artificial Intelligence: A Modern Approach (2nd ed.), Upper Saddle River, New Jersey: Prentice Hall, ISBN 0-13-790395-2, p. 17.

外部链接

编辑
检索自“https://zh.wikipedia.org/w/index.php?title=逻辑理论家&oldid=72891740”