读天才与算法:人脑与AI的数学思维笔记13_Coq证明助手

这篇具有很好参考价值的文章主要介绍了读天才与算法:人脑与AI的数学思维笔记13_Coq证明助手。希望对大家有所帮助。如果存在错误或未考虑完全的地方,请大家不吝赐教,您也可以点击"举报违法"按钮提交疑问。

读天才与算法:人脑与AI的数学思维笔记13_Coq证明助手

1.       计算机

1.1.         对于计算机来说,它就很擅长处理这种重复而机械且计算量庞大的任务

1.1.1.           在速度与准确性等方面,计算机是远超过手工计算的

1.2.         计算机只能执行指令,并无自主创造力

1.2.1.           想要证实程序中是否存在错误是很困难的

1.2.2.           我们能在多大程度上相信计算机,这个问题一直困扰着人工智能领域的学者

1.2.3.           当我们进入由算法主导的未来时,确保代码中没有未被检测出的错误,将成为一项艰巨的挑战

1.3.         哲学家大卫·休谟(David Hume)指出的,大多数科学研究都建立在归纳法之上——通过观察特定的例子来推断出一个普遍的规律或原则

1.3.1.           基于归纳法,曾产生了许多著名的科学理论,这反过来证实了归纳法确实是一种科学研究的好方法

1.4.         人类大脑的物理局限性,审核人必须得充分相信计算机的能力,就好比我们第一次乘坐飞机一样,心中难免惴惴不安

1.4.1.           许多问题的证明往往都存在不足或错误,人类犯错的可能性通常比计算机更大

1.4.2.           错误可以被修正,但遗憾的是,在证明的验证和审核阶段它们并没有被找出来

1.4.2.1.            证明的验证和审核非常重要,它是发现缺陷和漏洞的重要环节

1.4.3.           以安德鲁·怀尔斯证明“费马大定理”为例,在其证明方法付梓之前,审验人员发现了一个小缺陷

1.4.3.1.            怀尔斯和理查德·泰勒(Richard Taylor,曾是怀尔斯的学生)奇迹般地修正了这一缺陷

1.5.         许多新的证明极其复杂,以至于数学家们很担心一些潜在的错误难以被发现

1.5.1.           “魔群”是最大的“散在单群”

1.5.1.1.            需要196 883维线性空间才能表达的“魔群”

1.5.1.2.            “魔群”具有的元素个数超过了构成地球的原子个数

1.5.2.           “魔群定理”的证明散落在100多篇论文中,合计超过10 000页,涉及数百名数学家

1.5.3.           真理的产生取决于你的证明方法

1.6.         20世纪70年代,计算机对“四色定理”的证明轰动了全世界

1.6.1.           四色定理指的是“任何一张地图只用四种颜色就能使具有共同边界的国家着上不同的颜色。”

1.6.1.1.            在不引起混淆的情况下,一张地图至少需要四种颜色来标记

1.6.2.           1976年,数学家凯尼斯·阿佩尔(Kenneth Appel)和沃尔夫冈·哈肯(Wolfgang Haken)在前人的基础上用计算机证明了四色定理

1.6.2.1.            阿佩尔与哈肯把地图的无限种可能情况简化为1936种构型,但是要靠人工逐一验证如此之多的构型是不现实的,所以才需要借助计算机进行验证

1.6.2.2.            整个证明过程的耗时超过了1000小时

1.7.         1992年,牛津物理学家利用弦理论中的启发法对高维几何空间中可识别的代数结构数量进行了预测

1.7.1.           事实证明,否定这个预测的错误证据正是由一个有缺陷的计算机程序生成的

1.7.2.           错的是数学家,而不是物理学家

1.7.2.1.            程序的错误把他们引入了歧途

1.8.         2006年匹兹堡大学的托马斯·黑尔斯(Thomas Hales)教授在《数学年鉴》上发表了关于借助计算机证明著名的数学问题——“开普勒猜想”的论文

1.8.1.           开普勒猜想就是对在空间中如何最密集地堆积圆球的解答

1.8.2.           用了8年时间,数学家们证明了黑尔斯是正确的,但其确定性是99%

1.8.2.1.            对于数学纯化论者来说,这1%也是不可容忍的

1.8.2.2.            因为无法确定计算机程序是否存在潜在缺陷

2.       Coq证明助手

2.1.         数学是最伟大的浪漫主义学科之一,即便是天才,也得掌握所有知识才能激发灵感,理解一切。

2.1.1.           贡蒂尔

2.2.         在过去,数学问题的证明和验证过程全凭人工完成

2.2.1.           人类的大脑存在物理上的局限性

2.3.         越来越多的证明开始借力于计算机,但因为验证的过程既烦冗又复杂,并且工作量巨大,人类大脑的局限性决定了无法采用人工验证的方式判断其对错

2.3.1.           通过构建新的程序来验证计算机证明的正确性

2.3.2.           所做的一切能够叩开人类与机器彼此信任、持续合作的新时代“大门”

2.4.         人类手工证明与计算机证明不同,手工证明过程中会跳过一些烦琐或众人皆知的步骤,而计算机却依赖于明确、细化的步骤才能正确执行指令

2.4.1.           类似于写小说和写保姆指导手册的区别

2.4.2.           前者不需要对主人公的每一个动作都解释得一清二楚

2.4.3.           后者则需要尽可能地明确和详尽,包括一天中婴儿的食谱,以及吃饭、睡觉、上厕所的每一个细节

2.5.         20世纪80年代末,法国数学家皮埃尔·于埃(Pierre Huet)和蒂埃里·科昆德(Thierry Coquand)开始从事结构微积分(calculus of

constructions)项目文章来源地址https://www.toymoban.com/news/detail-861768.html

2.5.1.           该项目简称CoC,但很快又被称为Coq(法语里意为“公鸡”)

2.5.2.           在法国一直有以动物命名开发工具的习惯

2.5.3.           Coq是其开发者之一科昆德姓氏的前三个字母

2.5.4.           Coq为验证数学证明而生,很快也成了验证计算机证明的重要程序

2.6.         2000年,微软研究院首席研究员乔治·贡蒂尔(Georges Gonthier)及其同事使用Coq对阿佩尔与哈肯的四色定理的计算机证明进行了验证,因为这是史上第一个需要计算机才能完成的证明(假定Coq不存在任何缺陷)

2.6.1.           计算机用了5年的时间进一步自动识别并验证人类证明的过程

2.6.2.           这期间,人们惊讶地发现了在第一次证明中被忽略的数学知识

2.7.         越来越多的计算机证明被Coq所验证,使我们更加确信Coq是可靠的

2.7.1.           用一个计算机程序来验证多个计算机证明,比编制一个特定的证明程序或者进行人工证明更值得我们信任

2.8.         为了充分理解数学理论的构建过程并使之与Coq充分融合

3.       奇阶定理

3.1.         odd order theorem

3.2.         奇阶定理是对称性研究最重要的指导定理之一,通常被认为是有限单群分类的基石

3.3.         有限单群是构成数学有限群论“元素周期表”中的基本元素,所有的对象都由有限单群构成

3.4.         具有素数边的正多边形(如正三角形、正五边形)是该周期表中的元素

3.5.         该定理指出,任何奇阶对称结构的基本组成单元都是素数多边形,此外再无其他结构

3.6.         如果把对称物体分为奇阶和偶阶两种,那么该定理就等于涵盖了其中的一半,意义重大

3.7.         奇阶定理的原始论文有255页,占据了《太平洋数学期刊》的全部篇幅

3.7.1.           在它出版之前,大多数证明最多只有几页,一天内即可掌握

3.7.2.           这个冗长复杂的证明,对每一位数学家来说都是一个挑战

3.7.3.           其中是否存在细微的缺陷或错误,始终无法考证

到了这里,关于读天才与算法:人脑与AI的数学思维笔记13_Coq证明助手的文章就介绍完了。如果您还想了解更多内容,请在右上角搜索TOY模板网以前的文章或继续浏览下面的相关文章,希望大家以后多多支持TOY模板网!

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处: 如若内容造成侵权/违法违规/事实不符,请点击违法举报进行投诉反馈,一经查实,立即删除!

领支付宝红包 赞助服务器费用

相关文章

  • 读天才与算法:人脑与AI的数学思维笔记05_算法的幻觉

    1.3.4.1. 我们可通过编程为感知器分配初始的权值和阈值,通过真实的输入数据对其进行训练,每一次错误的预测都将会作为反馈,用以促进权值的调整和修正 1.6.3.1. 严格意义上说,也不是完全免费,因为我们也在它们提供的服务中获得了数据的“交换 1.6.3.2. 很多人意识不

    2024年04月22日
    浏览(46)
  • 读天才与算法:人脑与AI的数学思维笔记11_算法如何思考

    1.3.2.1. 在创造艺术行为伊始,有了最初的想法之后不久,就出现了最初的反向运动,即接受性的最初运动 1.3.2.1.1. 德国艺术家保罗·克利

    2024年04月27日
    浏览(38)
  • 读天才与算法:人脑与AI的数学思维笔记06_算法的进化

    1.5.2.1. 深度学习算法提取出了人类无法用语言描述和表达的特征信息 1.5.2.2. 就好比在没有建立颜色的概念,也没有红色或蓝色这种表示颜色的词汇的情况下,仅仅通过我们对所见事物表现出的好恶,计算机就能帮我们实现蓝色和红色的分类 2.1.1.1. 现实中数据之间的逻辑关

    2024年04月22日
    浏览(42)
  • 读天才与算法:人脑与AI的数学思维笔记03_AlphaGo

    2.6.2.1. 原本平静的丛林之中激起的一丝混乱,极有可能预示着另一种动物的潜入 2.6.2.2. 这类敏感信息备受动物们的关注,因为它关系到自己会成为猎物还是猎食者,这就是大自然的生存法则 2.6.2.3. 人类的大脑非常擅长识别模式并预测它们的发展方向,同时做出适当的反应

    2024年04月22日
    浏览(38)
  • 读天才与算法:人脑与AI的数学思维笔记07_数字绘画

    2.3.2.1.            一个物种开始做标记,其目的可能不仅仅是为了实用——印记的出现预示着人类种群迈入了全新的进化阶段 2.7.2.1.            制作出这些“艺术品”需要耗费非常大量的劳动力以及劳动时间 2.7.3.1.            这些都反映了人类将艺术创作的

    2024年04月23日
    浏览(51)
  • 读天才与算法:人脑与AI的数学思维笔记02_激发创造力

    2.2.1.1.            一位独具慧眼的科学家 2.2.1.2.            研究涉及哲学、心理学、医学、人工智能、认知科学等领域,并能将其很好地融会贯通 2.2.2.1.            探索型创造力 2.2.2.2.            组合型创造力 2.2.2.3.            变革型创造力 3.

    2024年04月17日
    浏览(42)
  • 读天才与算法:人脑与AI的数学思维笔记01_洛夫莱斯测试

    1.8.2.1.            机器会发挥作用,提出一些新的想法和建议,以启发我们突破思维定式,防止我们陷入简单的重复 1.8.2.2.            最终,机器可能会帮助我们,而作为人类,我们应该表现得不那么像机器 Minsky)和唐纳德·米基(Donald Michie)等一系列先驱,并引

    2024年04月16日
    浏览(29)
  • 读天才与算法:人脑与AI的数学思维笔记08_生物的创造力

    1.5.2.1.            如果人工智能创作出的艺术品遇到了上述的诉讼纠纷,那么艺术品的知识产权归属又应是怎样的? 1.5.2.2.            知识产权法存在的原因是知识产权具有排他性,也称独占性或专有性,指知识产权所有人对其知识或智力成果享有独占或排他的权

    2024年04月24日
    浏览(41)
  • 多智能体共识算法的粗略数学证明

    这篇文章是对论文《Consensus and Cooperation in Networked Multi-Agent Systems》中定理一的粗略数学证明。 论文中的定理一 : 对一个由 n 个智能体以拓扑结构 G 组成的网络,使用以下共识算法: x ˙ i ( t ) = Σ j ∈ N i a i j ( x j ( t ) − x i ( t ) ) ,   x ( 0 ) = z dot{x}_i(t)=Sigma_{jin N_i}a_{ij}(x_

    2024年02月12日
    浏览(30)
  • python机器学习经典算法代码示例及思维导图(数学建模必备)

    最近几天学习了机器学习经典算法,通过此次学习入门了机器学习,并将经典算法的代码实现并记录下来,方便后续查找与使用。 这次记录主要分为两部分:第一部分是机器学习思维导图,以框架的形式描述机器学习开发流程,并附有相关的具体python库,做索引使用;第二部

    2024年02月12日
    浏览(39)

觉得文章有用就打赏一下文章作者

支付宝扫一扫打赏

博客赞助

微信扫一扫打赏

请作者喝杯咖啡吧~博客赞助

支付宝扫一扫领取红包,优惠每天领

二维码1

领取红包

二维码2

领红包