谷歌数学AI登Nature:IMO金牌几何水平,定理证明超越1978年吴文俊法

1,477次阅读
没有评论

梦晨 发自 凹非寺
量子位 | 公众号 QbitAI

谷歌DeepMind再发Nature,Alpha系列AI重磅回归,数学水平突飞猛进。

AlphaGeometry,无需人类演示达到IMO金牌选手的几何水平。

谷歌数学AI登Nature:IMO金牌几何水平,定理证明超越1978年吴文俊法

有当年AlphaZero无需人类知识学围棋《Mastering the game of Go without human knowledge》的感觉了。

具体来说,30道IMO难度的几何定理证明题,AlphaGeometry做对25道,人类金牌选手平均25.9道,之前SOTA方法(1978年的吴文俊法)做对10道。

谷歌数学AI登Nature:IMO金牌几何水平,定理证明超越1978年吴文俊法

IMO金牌得主陈谊廷(Evan Chen)负责评估AI生成的答案,他评价到:

AlphaGeometry的输出令人印象深刻,既可验证又干净。过去的人工智能解决方案偶然性很大,输出有时是正确的,需要人工检查。

AlphaGeometry没有这个弱点,它的解决方案具有机器可验证的结构,并且是人类可读的……它像学生一样使用带有角度和相似三角形的经典几何规则。

除成绩亮眼之外,这项研究中还有三个重点引起业界关注:

  • 无需人类演示,也就是只用了AI合成数据训练,延续了AlphaZero自学围棋的方式。

  • 大模型结合其他AI方法,与AlphaGo和OpenAI Q*传闻相似。

  • 与许多先前方法不同,AlphaGeometry可以生成人类可读的证明过程,且模型和代码都开源

谷歌数学AI登Nature:IMO金牌几何水平,定理证明超越1978年吴文俊法

团队认为,AlphaGeometry提供了一个实现高级推理能力、发现新知识的潜在框架。

这可能有助于推动人工智能的定理证明——被视为构建AGI的关键一步。

谷歌数学AI登Nature:IMO金牌几何水平,定理证明超越1978年吴文俊法

另外,量子位在与作者团队交流过程中,打听到了是否真的会让AlphaGeometry去参加一届IMO竞赛,就像当年AlphaGo挑战人类围棋冠军一样。

他们表示正在努力提高系统的能力,还需要让AI能解决几何之外更广泛的数学问题。

AI证明几何也画辅助线

此前AI系统不能很好解决几何问题,卡就卡在缺乏优质训练数据。

人类学习几何可以借助纸和笔,在图像上使用现有知识来发现新的、更复杂的几何属性和关系。

谷歌团队为此用生成了10亿个随机几何对象图,以及其中点和线间的所有关系,最终筛选出1亿不同难度的独特定理和证明,AlphaGeometry在这些数据上完全从头训练

谷歌数学AI登Nature:IMO金牌几何水平,定理证明超越1978年吴文俊法

系统由两个模块组成,相互配合寻找复杂的几何证明。

  • 语言模型,预测可用来解决问题的几何结构(也就是添加辅助线)

  • 符号推理引擎,使用逻辑规则推导出结论。

谷歌数学AI登Nature:IMO金牌几何水平,定理证明超越1978年吴文俊法

一作Trieu Trinh介绍,AlphaGeometry的运作过程类似人脑分为快与慢两种类型。

也就是诺贝尔经济学奖得主丹尼尔·卡尼曼的畅销书《思考快与慢》中普及的“系统1、系统2”概念。

系统1提供快速、直观的想法,系统2提供更加深思熟虑、理性的决策。

一方面,语言模型擅长识别数据中的模式和关系,可以快速预测潜在有用的辅助结构,但通常缺乏严格推理或解释其决策的能力。

另一方面,符号推理引擎基于形式逻辑并使用明确的规则来得出结论。它们是理性且可解释的,但它们缓慢且不灵活,尤其是在独自处理大型、复杂的问题时。

例如在解决一道IMO 2015年的竞赛题时,蓝色部分为AlphaGeometry的语言模型添加的辅助结构,绿色部分是最终证明的精简版,共有109个步骤。

谷歌数学AI登Nature:IMO金牌几何水平,定理证明超越1978年吴文俊法

在做题过程中,AlphaGeometry还发现了2004年IMO竞赛题中一个未使用的前提条件,并因此发现了更广义的定理版本。

不需要O是BC的中点这个条件,就能证明P、B、C共线。

谷歌数学AI登Nature:IMO金牌几何水平,定理证明超越1978年吴文俊法

另外研究还发现,对于人类得分最低的3个问题,AlphaGeometry也需要非常长的证明过程和添加非常多的辅助结构才能解决。

但在相对简单的问题上,人类平均得分和AI生成的证明长度之间没有显著相关性 (p = −0.06)

谷歌数学AI登Nature:IMO金牌几何水平,定理证明超越1978年吴文俊法

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

—  —

点这里👇关注我,记得标星哦~

一键三连「分享」、「点赞」和「在看」

科技前沿进展日日相见 ~ 

谷歌数学AI登Nature:IMO金牌几何水平,定理证明超越1978年吴文俊法

 

Read More 

正文完
可以使用微信扫码关注公众号(ID:xzluomor)
post-qrcode
 0
评论(没有评论)

文心AIGC

2024 年 1 月
1234567
891011121314
15161718192021
22232425262728
293031  
文心AIGC
文心AIGC
人工智能ChatGPT,AIGC指利用人工智能技术来生成内容,其中包括文字、语音、代码、图像、视频、机器人动作等等。被认为是继PGC、UGC之后的新型内容创作方式。AIGC作为元宇宙的新方向,近几年迭代速度呈现指数级爆发,谷歌、Meta、百度等平台型巨头持续布局
文章搜索
热门文章
潞晨尤洋:日常办公没必要上私有模型,这三类企业才需要 | MEET2026

潞晨尤洋:日常办公没必要上私有模型,这三类企业才需要 | MEET2026

潞晨尤洋:日常办公没必要上私有模型,这三类企业才需要 | MEET2026 Jay 2025-12-22 09...
共推空天领域智能化升级!趋境科技与金航数码强强联手

共推空天领域智能化升级!趋境科技与金航数码强强联手

共推空天领域智能化升级!趋境科技与金航数码强强联手 十三 2025-12-09 18:18:41 来源:量子位...
起底“豆包手机”:核心技术探索早已开源,GUI Agent布局近两年,“全球首款真正的AI手机”

起底“豆包手机”:核心技术探索早已开源,GUI Agent布局近两年,“全球首款真正的AI手机”

起底“豆包手机”:核心技术探索早已开源,GUI Agent布局近两年,“全球首款真正的AI手机” 西风 202...
面向「空天具身智能」,北航团队提出星座规划新基准丨NeurIPS’25

面向「空天具身智能」,北航团队提出星座规划新基准丨NeurIPS’25

面向「空天具身智能」,北航团队提出星座规划新基准丨NeurIPS’25 鹭羽 2025-12-13 22:37...
5天连更5次,可灵AI年末“狂飙式”升级

5天连更5次,可灵AI年末“狂飙式”升级

5天连更5次,可灵AI年末“狂飙式”升级 思邈 2025-12-10 14:28:37 来源:量子位 让更大规...
最新评论
ufabet ufabet มีเกมให้เลือกเล่นมากมาย: เกมเดิมพันหลากหลาย ครบทุกค่ายดัง
tornado crypto mixer tornado crypto mixer Discover the power of privacy with TornadoCash! Learn how this decentralized mixer ensures your transactions remain confidential.
ดูบอลสด ดูบอลสด Very well presented. Every quote was awesome and thanks for sharing the content. Keep sharing and keep motivating others.
ดูบอลสด ดูบอลสด Pretty! This has been a really wonderful post. Many thanks for providing these details.
ดูบอลสด ดูบอลสด Pretty! This has been a really wonderful post. Many thanks for providing these details.
ดูบอลสด ดูบอลสด Hi there to all, for the reason that I am genuinely keen of reading this website’s post to be updated on a regular basis. It carries pleasant stuff.
Obrazy Sztuka Nowoczesna Obrazy Sztuka Nowoczesna Thank you for this wonderful contribution to the topic. Your ability to explain complex ideas simply is admirable.
ufabet ufabet Hi there to all, for the reason that I am genuinely keen of reading this website’s post to be updated on a regular basis. It carries pleasant stuff.
ufabet ufabet You’re so awesome! I don’t believe I have read a single thing like that before. So great to find someone with some original thoughts on this topic. Really.. thank you for starting this up. This website is something that is needed on the internet, someone with a little originality!
ufabet ufabet Very well presented. Every quote was awesome and thanks for sharing the content. Keep sharing and keep motivating others.
热评文章
小冰之父李笛智能体创业,公司取名Nextie!陆奇是股东

小冰之父李笛智能体创业,公司取名Nextie!陆奇是股东

小冰之父李笛智能体创业,公司取名Nextie!陆奇是股东 Jay 2025-12-09 08:26:01 来源...
梁文锋,Nature全球年度十大科学人物!

梁文锋,Nature全球年度十大科学人物!

梁文锋,Nature全球年度十大科学人物! 一水 2025-12-09 09:46:23 来源:量子位 来自安...
起底“豆包手机”:核心技术探索早已开源,GUI Agent布局近两年,“全球首款真正的AI手机”

起底“豆包手机”:核心技术探索早已开源,GUI Agent布局近两年,“全球首款真正的AI手机”

起底“豆包手机”:核心技术探索早已开源,GUI Agent布局近两年,“全球首款真正的AI手机” 西风 202...
摩尔线程新一代GPU架构10天后发布

摩尔线程新一代GPU架构10天后发布

摩尔线程新一代GPU架构10天后发布 思邈 2025-12-09 15:46:09 来源:量子位 国内首个聚焦...
极客公园创新大会 2026在京落幕,罗永浩、张楠、何小鹏、刘靖康等共议 AI 时代「进程由我」

极客公园创新大会 2026在京落幕,罗永浩、张楠、何小鹏、刘靖康等共议 AI 时代「进程由我」

极客公园创新大会 2026在京落幕,罗永浩、张楠、何小鹏、刘靖康等共议 AI 时代「进程由我」 henry 2...