谷歌数学AI在Nature上展示超越1978年吴文俊法的IMO金牌几何证明能力
来源:51CTO.COM
时间:2024-01-24 21:15:05 296浏览 收藏
知识点掌握了,还需要不断练习才能熟练运用。下面golang学习网给大家带来一个科技周边开发实战,手把手教大家学习《谷歌数学AI在Nature上展示超越1978年吴文俊法的IMO金牌几何证明能力》,在实现功能的过程中也带大家重新温习相关知识点,温故而知新,回头看看说不定又有不一样的感悟!
谷歌DeepMind再发Nature,Alpha系列AI重磅回归,数学水平突飞猛进。
AlphaGeometry,无需人类演示达到IMO金牌选手的几何水平。
有当年AlphaZero无需人类知识学围棋《Mastering the game of Go without human knowledge》的感觉了。
AlphaGeometry在30道IMO难度的几何定理证明题中做对了25道,而人类金牌选手平均做对了25.9道。此外,之前SOTA方法(1978年的吴文俊法)仅能做对10道。
IMO金牌得主陈谊廷(Evan Chen)负责评估AI生成的答案,他评价到:
AlphaGeometry的输出令人印象深刻,既可靠又干净。过去的人工智能解决方案存在偶然性,导致输出有时需要人工检查。
AlphaGeometry的解决方案具有可验证的结构,既可以由机器验证,也可以由人类理解。它使用经典几何规则,如角度和相似三角形,就像学生一样。
除成绩亮眼之外,这项研究中还有三个重点引起业界关注:
- 无需人类演示,也就是只用了AI合成数据训练,延续了AlphaZero自学围棋的方式。
- 大模型结合其他AI方法,与AlphaGo和OpenAI Q*传闻相似。
- 与许多先前方法不同,AlphaGeometry可以生成人类可读的证明过程,且模型和代码都开源。
团队认为,AlphaGeometry提供了一个实现高级推理能力、发现新知识的潜在框架。
这可能有助于推动人工智能的定理证明——被视为构建AGI的关键一步。
另外,量子位在与作者团队交流过程中,打听到了是否真的会让AlphaGeometry去参加一届IMO竞赛,就像当年AlphaGo挑战人类围棋冠军一样。
他们表示正在努力提高系统的能力,还需要让AI能解决几何之外更广泛的数学问题。
AI证明几何也画辅助线
此前AI系统不能很好解决几何问题,卡就卡在缺乏优质训练数据。
人类学习几何可以借助纸和笔,在图像上使用现有知识来发现新的、更复杂的几何属性和关系。
谷歌团队为此用生成了10亿个随机几何对象图,以及其中点和线间的所有关系,最终筛选出1亿不同难度的独特定理和证明,AlphaGeometry在这些数据上完全从头训练。
系统由两个模块组成,相互配合寻找复杂的几何证明。
- 语言模型,预测可用来解决问题的几何结构(也就是添加辅助线)。
- 符号推理引擎,使用逻辑规则推导出结论。
一作Trieu Trinh介绍,AlphaGeometry的运作过程类似人脑分为快与慢两种类型。
也就是诺贝尔经济学奖得主丹尼尔·卡尼曼的畅销书《思考快与慢》中普及的“系统1、系统2”概念。
系统1提供快速、直观的想法,系统2提供更加深思熟虑、理性的决策。
一方面,语言模型擅长识别数据中的模式和关系,可以快速预测潜在有用的辅助结构,但通常缺乏严格推理或解释其决策的能力。
另一方面,符号推理引擎基于形式逻辑并使用明确的规则来得出结论。它们是理性且可解释的,但它们缓慢且不灵活,尤其是在独自处理大型、复杂的问题时。
例如在解决一道IMO 2015年的竞赛题时,蓝色部分为AlphaGeometry的语言模型添加的辅助结构,绿色部分是最终证明的精简版,共有109个步骤。
在做题过程中,AlphaGeometry还发现了2004年IMO竞赛题中一个未使用的前提条件,并因此发现了更广义的定理版本。
不需要O是BC的中点这个条件,就能证明P、B、C共线。
另外研究还发现,对于人类得分最低的3个问题,AlphaGeometry也需要非常长的证明过程和添加非常多的辅助结构才能解决。
但在相对简单的问题上,人类平均得分和AI生成的证明长度之间没有显著相关性 (p = −0.06)。
One More Thing
对于AlphaGeometry与AlphaGo的联系和区别,在与团队交流过程中,谷歌科学家Quoc Le介绍到:
他们都是在一个非常复杂的决策空间中搜索,但AlphaGo的方法更传统(注:神经网络负责模式识别),AlphaGeometry中的神经网络负责建议下一步要采取的行动,指导搜索算法在决策空间中向正确的方向移动。
虽然这次成果随Alpha系列命名,第一单位也是Google DeepMind,但其实作者主要是前谷歌大脑成员。
Quoc Le大神不用过多介绍,一作Trieu Trinh与通讯作者Thang Luong都在谷歌工作了六七年,Thang Luong自己高中时也是IMO选手。
两位华人作者中,何河是纽约大学助理教授。吴宇怀此前参与了谷歌数学大模型Minerva研究,现在已经离开谷歌加入马斯克团队,成为xAI的联合创始人之一。
论文地址:https://www.nature.com/articles/s41586-023-06747-5。
参考链接:
[1]https://www.nature.com/articles/d4186-024-00141-5。
[2]https://deepmind.google/discover/blog/alphageometry-an-olympiad-level-ai-system-for-geometry。
今天带大家了解了的相关知识,希望对你有所帮助;关于科技周边的技术知识我们会一点点深入介绍,欢迎大家关注golang学习网公众号,一起学习编程~
-
501 收藏
-
501 收藏
-
501 收藏
-
501 收藏
-
501 收藏
-
250 收藏
-
475 收藏
-
440 收藏
-
142 收藏
-
165 收藏
-
285 收藏
-
369 收藏
-
240 收藏
-
192 收藏
-
284 收藏
-
438 收藏
-
299 收藏
-
- 前端进阶之JavaScript设计模式
- 设计模式是开发人员在软件开发过程中面临一般问题时的解决方案,代表了最佳的实践。本课程的主打内容包括JS常见设计模式以及具体应用场景,打造一站式知识长龙服务,适合有JS基础的同学学习。
- 立即学习 542次学习
-
- GO语言核心编程课程
- 本课程采用真实案例,全面具体可落地,从理论到实践,一步一步将GO核心编程技术、编程思想、底层实现融会贯通,使学习者贴近时代脉搏,做IT互联网时代的弄潮儿。
- 立即学习 508次学习
-
- 简单聊聊mysql8与网络通信
- 如有问题加微信:Le-studyg;在课程中,我们将首先介绍MySQL8的新特性,包括性能优化、安全增强、新数据类型等,帮助学生快速熟悉MySQL8的最新功能。接着,我们将深入解析MySQL的网络通信机制,包括协议、连接管理、数据传输等,让
- 立即学习 497次学习
-
- JavaScript正则表达式基础与实战
- 在任何一门编程语言中,正则表达式,都是一项重要的知识,它提供了高效的字符串匹配与捕获机制,可以极大的简化程序设计。
- 立即学习 487次学习
-
- 从零制作响应式网站—Grid布局
- 本系列教程将展示从零制作一个假想的网络科技公司官网,分为导航,轮播,关于我们,成功案例,服务流程,团队介绍,数据部分,公司动态,底部信息等内容区块。网站整体采用CSSGrid布局,支持响应式,有流畅过渡和展现动画。
- 立即学习 484次学习