第一个逻辑推理AI ：逻辑理论家程序

创作时间:

作者:

@小白创作中心

第一个逻辑推理AI ：逻辑理论家程序

引用

来源

https://www.bilibili.com/read/cv37830537/

1956年夏天，一群计算机科学的先驱们在达特茅斯学院集会，讨论一个新概念：人工智能。会议提案中的愿景是，“人类学习能力或逻辑推理的能力（智力）的各个方面原则上都可以被精确地描述，以至于可以制造一台机器来模拟它。”最终，他们展示了一个操作程序，该程序存储在计算机打孔卡上，它就是逻辑理论家程序（Logic Theorist）。

许多人称逻辑理论家为第一个人工智能程序，尽管这一描述在当时——甚至在今天——都存在争议。逻辑理论家旨在模仿人类的技能，但人们对于这项发明是否真正反映了人类思维，以及机器是否真的能复制我们智能的洞察力，仍存在分歧。然而，科学史学家们认为，逻辑理论家是第一个模拟人类如何使用逻辑推理解决复杂问题的程序，也是最早为电脑制作的程序之一（这个区别于乘法表、素数表、算盘口诀这样的古老程序）。

该程序是用一种新的信息处理语言创建的（这里的新是相对于类似算盘口诀的旧语言），编码过程需要在纸张上策略性地打孔（这样的语言就是第一代编程语言：机器语言），然后将其送入计算机。在短短几个小时内，逻辑理论家程序就证明了《数学原理》中的52个定理中的38个，这是一本数学推理的基础教科书。

怀特黑德和罗素, 《数学原理》

逻辑理论家的设计反映了其创造者之一赫伯特·西蒙（Herbert Simon）的思想。西蒙不是数学家，而是一名政治科学家。普渡大学科技史学家叶卡捷琳娜·巴宾采娃（Ekaterina Babintseva）解释说，西蒙对组织如何增强理性决策感兴趣。他认为，人工智能可以帮助人们做出更明智的选择。

“逻辑理论家程序是一种特定类型的人工智能，类似政府组织类型的智能，”巴宾采娃说，“也就说，逻辑理论家程序具有的是一个官僚的智力。”

西蒙弗雷泽大学的历史学家兼助理教授斯蒂芬妮·迪克（Stephanie Dick）说，西蒙将人类思维和人工智能程序都视为信息处理系统，因此二者之间存在着根本的相似性。西蒙在非营利研究机构兰德公司（RAND Corporation）任职顾问期间，遇到了计算机科学家和心理学家艾伦·纽厄尔（Allen Newell），后者成为了他最亲密的合作者。受数学家乔治·波利亚（George Pólya）的启发, 他们发明了一种智能的机器来复制人类的逻辑推理(我翻译的不好, 原话是Inspired by the heuristic teachings of mathematician George Pólya, who taught problem-solving, they aimed to replicate Pólya’s approach to logical, discovery-oriented decision-making with more intelligent machines).

这种对人类推理的尝试被写成了一个程序，该程序用于兰德公司早期建造的一台计算机JOHNNIAC。逻辑理论家程序通过其创作者所说的启发式演绎方法来证明《数学原理》中的数学定理：它反向工作，对可能的答案进行微小替换，直到得出与已经证明的结论等价的结论。在此之前，计算机程序主要通过遵循线性的、按步骤的指令来解决问题。

巴宾采娃说，逻辑理论家程序是一个突破，因为它是符号人工智能中的第一个程序，该程序使用符号或概念而非单纯的数值数据来训练计算机像人一样思考。她解释说，直到20世纪90年代，它一直是人工智能的主要方法。最近，研究人员复兴了20世纪50年代达特茅斯会议上考虑的另一种方法：通过机器学习算法和神经网络模仿我们的大脑，而不是模拟我们的推理方式。一些科学家和工程师认为，将这两种方法结合起来是人工智能发展的下一阶段。

一些人评论人工智能，说它实际上并没有引导启发式思维，而是展示了精确的试错问题解决方式（当然，在尝试的时候可能优先选择了概率更大的方向）。换句话说，它可以模拟人类思维的运作方式，但不能模拟其思维的自发性（ the spontaneity of its thoughts，这一点实际上小概率方向也会偶尔尝试的，这和思维的自发性也有点类似）。关于这种程序是否能与我们的智力相匹配的争论仍在继续。巴宾采娃说:“人工智能真的是一个移动的目标，许多计算机科学家会告诉你，人工智能并不存在。”

逻辑理论家（Logic Theorist）程序的基本原理包括：

思维被视为对短期和长期记忆中的符号进行处理（即转换）。逻辑理论家程序中所使用的符号是抽象和非模态的，它们并不直接与感官信息（如视觉、听觉等）相连。换句话说，这些符号不是基于具体的感知体验或感官输入的，而是更加抽象和概念化的。“非模态”则意味着这些符号并不依赖于特定的感知模态（如视觉、听觉等）。它们不是基于某种特定的感官输入或输出，而是更加通用和灵活的。这使得逻辑理论家程序能够处理各种不同类型的问题，而不仅仅局限于与特定感官相关的任务。
符号被视为携带信息，可以通过代表世界中的事物和事件来指导生物体的行为，也可以通过引发其他信息的变化来指导生物体的行为。用纽厄尔（Newell）和西蒙（Simon）的话来说，“symbols function as information entirely by virtue of their making the information processes act differentially”。

首先，符号被视为携带信息的实体。这些符号不仅仅是简单的标记或标签，它们承载着关于世界的知识和信息。这些符号可以代表具体的事物、事件，也可以代表更抽象的概念和关系。

其次，符号在认知过程中发挥着双重作用。一方面，符号具有代表作用，它们可以代表世界中的事物和事件，这是一种直接的、描述性的作用。通过符号，我们可以将复杂的事物或事件简化为易于处理和理解的形式。另一方面，符号更重要的是通过影响其他信息过程来指导生物体的行为。这意味着符号不仅仅是对现实的描述，它们还具有一种动态的功能，能够引发、修改或控制其他的信息处理过程。

纽厄尔和西蒙进一步强调了符号作为信息的核心特征。他们认为，符号之所以被视为信息，是因为它们能够使信息过程产生差异性行为。换句话说，符号的存在和变化会导致信息处理的方式和结果发生变化。这种差异性行为是符号作为信息的本质属性。符号不是静态的，而是动态的、有影响力的，它们能够改变认知系统的状态和行为。

最后，符号与行为之间存在着密切的关系。符号不仅仅是对现实的反映或描述，它们更是指导行为的关键。生物体（包括人类和其他智能体）通过处理和操作符号来理解和改变世界。符号处理是认知活动的核心，它决定了生物体如何感知、思考、决策和行动。因此，符号在认知科学中具有举足轻重的地位，它们是智能行为的基石。

符号以层次化的方式表示知识。例如，在逻辑理论家中，逻辑表达式的表示是层次化的，包含元素和子元素。同样，逻辑理论家所使用的过程也是层次化的，因为这些过程会设定子目标，从而引发新的过程。
复杂问题是通过使用启发式方法来解决的，这些方法相当高效，但不能保证找到解决方案。
逻辑理论家通过启发式方法从待证明的定理出发，进行逆向推理，直到得出有效的推论并达到公理。

这里的观点并不是说纽厄尔和西蒙开创了这些原理，而是说他们将这些原理进行整合并应用于开发一个能够解决复杂问题的实际工作系统。

专家系统是一种基于知识的系统，它利用专业知识和经验来解决问题和做出决策。这些系统通常包含大量的规则、事实和启发式信息，用于模拟人类专家在特定领域内的决策过程。Logic Theorist作为早期逻辑推理的典范，为专家系统的发展奠定了基础。专家系统通过逻辑推理和知识表示，能够在特定领域内提供与人类专家相当或更优的决策和解决方案。

这一观点至今仍被许多认知建模系统所遵循，其中几个典型的系统包括GOMS、ACT-R、SOAR和EPIC。

GOMS（Goals, Operators, Methods, and Selection rules）是由Card等人于1983年提出的一个认知建模框架。它侧重于描述和预测人类在执行特定任务时的认知过程和行为。GOMS模型通过定义目标、操作符、方法和选择规则等组件，来模拟人类在处理任务时的认知活动，从而帮助我们更好地理解人类认知的工作原理。

ACT-R（Adaptive Control of Thought-Rational）则是由Anderson和Lebiere于1998年提出的一个综合性的认知架构。它旨在模拟人类认知的多个方面，包括记忆、学习、问题解决和决策制定等。ACT-R模型通过定义一系列的认知模块和它们之间的交互作用，来揭示人类认知的复杂性和动态性。这一模型在认知心理学和人工智能领域都产生了广泛的影响。

SOAR（State, Operator, and Result）是由Newell于1990年提出的一种基于心理学理论的智能架构。它侧重于模拟人类问题解决、学习和决策制定的认知过程。SOAR通过定义状态、操作符和结果等基本概念，以及它们之间的相互作用关系，来构建一个能够模拟人类认知行为的智能系统。这一架构在认知科学、人工智能和机器人领域都有着广泛的应用。

最后，EPIC（Executive-Process/Interactive Control）是由Meyer和Kieras于1997年提出的一个认知建模框架。它旨在揭示人类在执行复杂任务时的认知控制过程。EPIC模型通过定义一系列的执行过程和交互控制机制，来模拟人类在处理任务时的认知活动和决策过程。这一模型对于我们理解人类认知的灵活性和适应性具有重要的意义。

GOMS、ACT-R、SOAR和EPIC都是基于传统表征观点的认知建模系统，它们在认知心理学和人工智能领域都发挥着重要的作用。这些模型通过模拟人类的认知过程和行为，为我们提供了更深入的理解人类认知的工具和方法。

值得注意的是，这种基于逻辑推理的AI与后来发展起来的数学定理的机械化证明也有着密切的联系。例如，吴方法、Coq和Lean等系统都是在这一领域内的杰出代表。它们通过逻辑推理和机械化证明，能够验证数学定理的正确性，为数学研究提供了有力的工具。特别是Lean，由陶哲轩等大力推广，展示了逻辑推理AI在数学领域的蓬勃发展和应用潜力。

尽管大语言模型等基于数据的AI技术在当前备受瞩目，但逻辑推理AI仍然在蓬勃发展，并且与基于数据的AI技术相结合，为解决问题提供了更全面的方法。感性和理性相结合做出决策，猜测机器AI和逻辑推理AI相结合也是未来发展的方向。这种结合有望为人工智能领域带来更大的突破和创新，推动我们在更多领域取得进展。

p.s. 下面时我搜集的一些资料，与大家分享：

SAINT：詹姆斯·斯拉格尔（James Slagle）开发了SAINT（Symbolic Automatic INTegrator），一个早期的符号自动积分器。这个系统体现了人工智能中的符号处理和自动推理能力，因此可以认为是人工智能的一部分。
Lisp：Lisp是一种编程语言，特别适合于符号处理和人工智能应用。它允许开发者编写能够处理复杂逻辑和符号计算的程序，因此是人工智能领域的重要工具。
符号计算：符号计算是人工智能中的一个重要领域，涉及使用符号而非数值进行计算和推理。这种计算方法在定理证明、自动推理等领域有广泛应用，因此属于人工智能的范畴。
Lean：如果指的是数学定理证明工具 Lean，那么它绝对属于人工智能领域，因为它涉及自动化推理和证明，是人工智能在逻辑推理方面的典型应用。
计算机自动化：这是一个宽泛的概念，涉及使用计算机技术来自动化各种任务。虽然不是所有计算机自动化都涉及人工智能，但如果这种自动化包括了自我学习、推理或问题解决等智能行为，则可以视为人工智能的一部分。
coq, sympy, sagemath：这些都是数学和符号计算的工具或库。Coq是一个定理证明助手，涉及逻辑推理和自动化证明，属于人工智能。Sympy和SageMath则是用于符号计算的Python库，它们在执行复杂的数学运算和推理时展示了人工智能的某些特征。