江苏龙网

  1. 首页 > 资讯 > 科技 > >

AI人工智能|计算机距离数学推理自动化有多近？( 四 )


今天 ， 在该领域最前沿的努力旨在将学习与推理相结合 。他们经常将ATP与ITP结合在一起 ， 并且还集成了机器学习工具来提高两者的效率 。他们设想可以使用演绎推理（甚至可以传达数学思想）的ATP / ITP程序 ， 其方式与人们的做法相同 ， 或者至少以类似的方式 。理性的极限
AI人工智能|计算机距离数学推理自动化有多近？
文章图片

文章图片

约瑟夫·厄本（Josef Urban）认为 ， 证明所需的演绎推理和归纳推理的结合可以通过这种组合方法来实现 。他的小组建立了以机器学习工具为指导的定理证明者 ， 使计算机可以通过经验自己学习 。在过去的几年中 ， 他们探索了神经网络的使用——神经计算的各个层 ， 它们通过大致模拟我们大脑的神经元活动来帮助机器处理信息 。7月 ， 他的小组报告了由经过定理证明数据训练的神经网络产生的新猜想 。
厄本受到安德烈·卡尔帕西（Andrej Karpathy）的部分启发 ， 安德烈·卡帕西（Andrej Karpathy）几年前训练了一个神经网络 ， 以生成看起来像数学的谬论 ， 这对非专家而言是合法的 。不过 ， 厄本不想要废话 ， 而是他和他的团队设计了自己的工具 ， 在经过数百万个定理的训练后 ， 可以找到新的证明 。然后他们使用网络生成新的猜想 ， 并使用称为E的ATP检查了这些猜想的有效性 。
AI人工智能|计算机距离数学推理自动化有多近？
文章图片

文章图片

该网络提出了50,000多个新公式 ， 尽管有数千个重复 。乌尔班说：“看来我们还没有能力证明更有趣的猜想 。”
谷歌研究公司的塞格迪将计算机证明中的自动推理视为更大领域的一个子集：自然语言处理 ， 这涉及在单词和句子的使用中进行模式识别 。（模式识别也是计算机视觉背后的驱动思想 ， 这是塞格迪之前在谷歌的项目的目标 。）与其他小组一样 ， 他的团队也希望定理证明者能够找到并解释有用的证明 。
受诸如AlphaZero（可以在国际象棋 ， 围棋和将棋上击败人类的DeepMind程序）之类的AI工具迅速发展的启发 ， 塞格迪的小组希望利用语言识别的最新进展来编写证明 。他说 ， 语言模型可以证明令人惊讶的扎实的数学推理 。
AI人工智能|计算机距离数学推理自动化有多近？
文章图片

文章图片

他在谷歌研究公司的小组最近描述了一种使用语言模型（通常使用神经网络）生成新证据的方法 。训练模型以识别已知定理中的某种树状结构后 ， 他们进行了一种自由形式的实验 ， 只需要求网络生成并证明一个定理 ， 而无需任何进一步的指导 。在成千上万的猜想中 ， 约有13％都是可证明的和新的（这意味着它们没有重复数据库中的其他定理） 。他说 ， 该实验表明 ， 神经网络可以自学一种对证明看起来像什么的理解 。
塞格迪说：“神经网络能够发展出一种人工的直觉风格 。”
AI人工智能|计算机距离数学推理自动化有多近？
文章图片

文章图片

当然 ， 目前还不清楚这些努力是否能满足40年前科恩的预言 。高尔斯曾表示 ， 他认为到2099年 ， 计算机将能够超越数学家但我认为这将持续很短的时间 。”
毕竟 ， 如果机器继续改进 ， 并且可以访问大量数据 ， 那么它们也应该变得非常擅长于完成有趣的部分 。高尔斯说：“他们将学习如何做自己的提示 。”
哈里斯不同意 。他认为计算机专家不是必需的 ， 否则他们将不可避免地“使人类数学家过时” 。他说 ， 如果计算机科学家能够对一种合成的直觉进行编程 ， 那么它仍然无法与人类相提并论 。“即使计算机能够理解 ， 它们也无法以人类的方式理解 。”


推荐阅读


上一篇：小米手机|单日大涨11%，小米高端布局见成效，获得多机构强力看好

下一篇：股权激励|做股权激励有6大误区，千万要避免