江苏龙网

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

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


里尔还说 ， 她在自己的工作中越来越多地使用定理证明 。她说：“不一定要一直使用它 ， 也永远不能代替在纸上划划写写 ， 但是使用校对助手已经改变了我思考编写校样的方式 。”
AI人工智能|计算机距离数学推理自动化有多近？
文章图片

文章图片

定理证明者还提供了一种保持领域诚实的方法 。1999年 ， 俄裔美国数学家弗拉基米尔·沃沃斯基（Vladimir Voevodsky）在他的证明中发现了一个错误 。从那时起直到2017年去世 ， 他一直是使用计算机检查证明的拥护者 。海尔斯说 ， 他和弗格森在用计算机检查原始证明时发现了数百个错误 。即使是《欧几里得的元素》中的第一个命题也不是完美的 。如果机器可以帮助数学家避免此类错误 ， 那为什么不利用它呢？ （海尔斯提出的反对意见是有道理的还是没有道理的：如果数学家们不得不花时间将数学形式化以被计算机理解 ， 那么他们就不必花时间去做新的数学了 。）
AI人工智能|计算机距离数学推理自动化有多近？
文章图片

文章图片

但是 ， 剑桥大学的数学家和菲尔兹奖得主蒂莫西·高尔斯（Timothy Gowers）希望走得更远：他设想了一个定理证明将取代主要期刊上的人类裁判的未来 。他说：“我可以看到 ， 如果您希望您的论文被接受 ， 则必须通过自动检查器 ， 这已成为一种标准做法 。”与计算机交谈
但是在计算机可以普遍检查甚至设计证据之前 ， 研究人员首先必须扫除一个重要的障碍：人类语言与计算机的语言之间的沟通障碍 。
AI人工智能|计算机距离数学推理自动化有多近？
文章图片

文章图片

当今的定理证明并不是为了方便数学家而设计的 。第一种类型的ATP通常用于检验陈述是否正确（通常通过测试可能的情况） 。例如 ， 要求ATP验证一个人可以从迈阿密开车到西雅图 ， 并且它可能会搜索所有从迈阿密出发的道路所连接的城市 ， 并最终找到一条通往西雅图的道路 。
使用ATP ， 程序员可以编写所有规则或公理的代码 ， 然后询问是否有一个特定的猜想遵循这些规则 。然后 ， 计算机完成所有工作 。计算机科学家丹尼尔·黄（Daniel Huang）说：“您只要输入要证明的猜想 ， 就可以希望得到答案 。”他最近离开加州大学伯克利分校 ， 在一家创业公司工作 。
AI人工智能|计算机距离数学推理自动化有多近？
文章图片

文章图片

但是有一个难题：ATP不做的就是解释其工作 。所有这些计算都发生在机器内部 ， 在人眼看来 ， 它就像一串长长的0和1 。黄说 ， 因为看起来像一堆随机数据 ， 所以不可能扫描证明并遵循推理 。他说：“没有人会看那个证据 ， 并且会说'我明白了' 。”
ITP是第二类 ， 具有庞大的数据集 ， 其中包含多达数万个定理和证明 ， 他们可以对其进行扫描以验证证明是正确的 。与仅在黑匣子中工作并吐出答案的ATP不同 ， ITP在过程中需要人与人之间的互动甚至是指导 ， 因此它们并非难以获得 。黄说：“人们可以坐下来 ， 了解什么是证明级技术 。”
AI人工智能|计算机距离数学推理自动化有多近？
文章图片

文章图片

近年来 ， ITP变得越来越流行 。2017年 ， 布尔毕达哥拉斯三元组问题背后的三重奏使用了ITP Coq ， 来创建和验证其证明的正式版本；在2005年 ， 微软研究院（剑桥）的乔治·贡蒂埃（Georges Gonthier）使用Coq将四色定理形式化 。哈里斯在开普勒猜想的正式证明中还使用了称为HOL Light和Isabelle的ITP 。（“ HOL”代表“高阶逻辑” 。）


推荐阅读


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

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