江苏龙网

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

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

据报道 ， 在1970年代 ， 已故的数学家保罗·科恩（Paul Cohen）是唯一获得过数学逻辑领域勋章的人 ， 据此做出了一个广泛的预测 ， 这一预测继续激起和激发了数学家——“在未来的某个不确定的时期 ， 计算机将取代数学家 。”因在集合论中大胆的方法而闻名的科恩（Cohen）预测 ， 所有数学都是可以自动化的 ， 包括编写证明 。
AI人工智能|计算机距离数学推理自动化有多近？
文章图片

文章图片

证明是一步一步的逻辑论证 ， 它验证猜想或数学命题的真实性 。（一旦证明 ， 猜想就成为一个定理 。）它既可以建立陈述的有效性 ， 又可以解释其成立的原因 。但是 ， 证明很奇怪 。它是抽象的 ， 不受物质体验的束缚 。卡内基梅隆大学的认知科学家西蒙·德迪奥（Simon DeDeo）说：“这是假想的非物质世界与生物进化的生物之间的疯狂接触 。”他通过分析证明的结构来研究数学确定性 。“我们并没有这样做 。”
计算机对于大型计算很有用 ， 但证明要求有所不同 。归纳推理是一种关于一个有趣问题的直觉 ， 它来自于归纳推理 ， 而证明通常遵循推论 ， 逐步的逻辑 。它们通常需要复杂的创造性思维以及需要付出更多努力才能填补空白 ， 而机器无法实现这种结合 。
AI人工智能|计算机距离数学推理自动化有多近？
文章图片

文章图片

计算机定理证明者可以分为两类 。自动化定理证明者（ATP）通常使用蛮力方法进行大量计算 。交互式定理证明者（ITP）充当证明助手 ， 可以验证参数的准确性并检查现有证明是否有错误 。但是 ， 即使结合使用这两种策略（如较新的定理证明就是这种情况） ， 它们也不会合计为自动推理 。
另外 ， 这些工具还没有被推广或被广泛认可 ， 大多数数学家也不使用或欢迎它们 。“对于数学家来说 ， 这是非常有争议的 。”德迪奥说 ， “大多数人不喜欢这个主意 。”
这个领域的一个艰巨的开放挑战会问 ， 实际上有多少校样可以自动化：一个系统能产生一个有趣的猜想 ， 并用人们理解的方式来证明它吗？来自世界各地实验室的一系列最新进展表明 ， 人工智能工具可以回答这个问题 。布拉格捷克信息学、机器人学和网络学研究所的约瑟夫·厄本（Josef Urban） ， 正在探索各种使用机器学习来提高现有证明者效率和性能的方法 。7月 ， 他的小组报告了一组由机器生成和验证的原始推测和证据 。今年6月 ， 由克里斯蒂安·塞格迪（Christian Szegedy）领导的谷歌（Google）研究公司小组发布了最新成果 ， 这些成果是利用自然语言处理的优势 ， 使计算机证明在结构和解释上更加人性化的结果 。
AI人工智能|计算机距离数学推理自动化有多近？
文章图片

文章图片

一些数学家认为定理证明是潜在的改变游戏规则的工具 ， 可以训练大学生进行证明写作 。其他人则说 ， 让计算机编写证明对于推进数学是不必要的 ， 而且可能是不可能的 。但是 ， 一个可以预测有用猜想并证明新定理的系统将会实现一些新的东西——某种机器版本的理解 ， 塞格迪说 ， 这就暗示了自动实现推理本身的可能性 。有用的机器
长期以来 ， 数学家、逻辑学家和哲学家一直在争论证明的哪一部分是人为因素 ， 如今有关机械化数学的争论仍在继续 ， 尤其是在连接计算机科学和纯数学的深谷中 。
AI人工智能|计算机距离数学推理自动化有多近？
文章图片

文章图片

对于计算机科学家来说 ， 定理证明没有争议 。它们提供了一种严格的方法来验证程序是否有效 ， 关于直觉和创造力的争论不如找到解决问题的有效方法重要 。例如 ， 在麻省理工学院 ， 计算机科学家亚当·克莱帕拉（Adam Chlipala）设计了定理证明工具 ， 该工具生成传统上由人类编写的加密算法 ， 以保护互联网交易 。他小组的代码已经用于Google Chrome浏览器上的大多数通信 。


推荐阅读


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

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