用户名:  密码:   
网站首页即时通讯活动公告最新消息科技前沿学人动向两岸三地人在海外历届活动关于我们联系我们申请加入
栏目导航 — 美国华裔教授专家网最新消息社区报道
关键字  范围   
 
史上首次,AI超越人类奥赛金牌得主!吴方法加持,30题做出27道破纪录
2024/4/11 12:46:17 | 浏览:218 | 评论:0

就在刚刚,首位超越人类数学奥赛金牌得主的AI诞生了!剑桥大学等机构的研究者发现,结合「吴方法」的DeepMind数学模型AlphaGeometry,在解决奥数题时直接秒杀了人类IMO金牌得主,30道几何题中做对了27道。

首位超越国际奥林匹克竞赛金牌得主的AI,刚刚诞生了!

印度理工学院海得拉巴分校、图宾根AI中心、剑桥大学的研究者发现——

通过「吴方法」,可以让AI变成和人类数学奥赛银牌得主同样的水平,而「AI数学大师」AlphaGeometry,则直接超越了IMO金牌得主。

史上首次,AI超越人类奥赛金牌得主!吴方法加持,30题做出27道破纪录

吴方法,是吴文俊在1970年代提出的开创性算法。

经过改进后,它变得非常强大,可以解决国际数学奥林匹克竞赛30个问题中的27个!直接秒杀人类。

相比之下,之前的AlphaGeometry,仅能解决25个。

史上首次,AI超越人类奥赛金牌得主!吴方法加持,30题做出27道破纪录
论文地址:https://arxiv.org/abs/2404.06405
项目地址:https://huggingface.co/datasets/bethgelab/simplegeometry

之前曾有人估计,到2026年代,AI才能达到IMO人类金牌得主的水平。而如今,这个时间表再次被打破了。

史上首次,AI超越人类奥赛金牌得主!吴方法加持,30题做出27道破纪录

AI做IMO奥数题,有新SOTA了


证明几何定理是视觉推理的重要表现,它融合了直觉和逻辑思维。

因此,自动化证明奥林匹克级别的几何题目,代表着人类级自动推理的一个重要里程碑。

此前推出的AlphaGeometry,是一个通过1亿个合成样本训练的神经符号模型,代表了一个重大的突破。

史上首次,AI超越人类奥赛金牌得主!吴方法加持,30题做出27道破纪录
论文地址:https://www.nature.com/articles/s41586-023-06747-5

它成功解决了国际数学奥林匹克(IMO)30个问题中的25个,而传统的基于吴方法的系统,仅能解决10个。

但这一次,研究者们重新评估了AlphaGeometry引入的IMO-AG-30挑战,有了新的发现——

吴方法异常强大!

仅靠吴方法,就能解决15个问题,其中一些问题是靠其他方法根本无法解决的。

史上首次,AI超越人类奥赛金牌得主!吴方法加持,30题做出27道破纪录

而这就带来了两个关键发现:

1. 通过将「吴方法」和经典的演绎数据库(DD)以及角度、比率和距离追踪(AR)的合成方法相结合,仅使用一台配备CPU的笔记本,在每个问题的5分钟限时内,就能解决30个问题中的21个。

这种经典组合方法(Wu&DD+AR)仅比AlphaGeometry少解决了4个问题,并建立了第一个完全基于符号的基准,其性能足以与国际数学奥林匹克(IMO)银牌得主媲美。

2. 吴方法还解决了AlphaGeometry未能解决的5个问题中的2个。

因此,现在IMO-AG-30有新的SOTA了!

通过将AlphaGeometry与吴方法结合产生的新AI,直接解决了30个问题中的27个,一举超越IMO金牌得主,成为世上首个达此成就的AI。

欧氏几何,AI推理能力的试金石


如何测试AI的推理能力强不强?欧几里得几何就是一个很好的标准。

因为,欧几里得几何已经被有限地公理化了,而且这么多年来,有许多非常适合自动定理证明的欧几里得几何证明系统被提了出来。

史上首次,AI超越人类奥赛金牌得主!吴方法加持,30题做出27道破纪录

此外证明的搜索可以通过图形表示、概率验证,或是使用人类设计的启发式方法,来对角度、面积和距离进行大量推理引导。

国际数学奥林匹克中,这些方法被参赛者戏称为「三角破解」和「重心破解」。

还有一件有趣的事,就是这个领域的缺陷——它需要定义特定的证明系统来指定问题,缺乏训练数据,问题时常涉及复杂的退化情况。

这些困难非常棘手,由此坊间有这样一句戏言——「几何问题永远不会解决退化问题。」

史上首次,AI超越人类奥赛金牌得主!吴方法加持,30题做出27道破纪录

在几何自动推理领域,可以将方法分为代数方法和合成方法。

演绎数据库(DD)这个合成方法就颇受关注。

它会模仿人类的证明技巧,通过将定理证明视为依据一组几何公理进行的逐步搜索问题,从而生成易于理解的证明。

比如,DD会采用一组固定的、由专家策划的几何规则,这些规则会不断地应用到初始的几何配置上,直至系统达到一个状态,即用现有规则无法推导出新的事实为止。

史上首次,AI超越人类奥赛金牌得主!吴方法加持,30题做出27道破纪录

而神经符号证明器AlphaGeometry在这一领域取得了突破性的进展。

在DD的基础上,它增加了新的规则,用于进行角度、比率和距离的追踪(AR),并通过大模型(DD+AR+LLM-构造)提出的构建方法,进一步增强了由此生成的符号引擎。该模型是基于1亿个合成证明训练的。

而吴方法和Gröbner基方法之类的代数方法,能够将几何假设,转换成多项式系统,来验证结论。

这些方法已被证实,能够有效处理广泛的几何问题。

其中,对于所有假设和结论都能用代数方程表示的问题,吴方法都能处理,并且还能自动产生非退化条件。

而这就表明,吴方法不仅适用于平面几何问题,也适用于固体和更高维的几何问题。

5秒解决14个问题


今年1月,谷歌DeepMind团队同时推出了新的基准测试IMO-AG-30。

这是团队从2000年至2022年间竞赛题中,筛选出30道经典几何问题组成的测试集,目的是为了展示AlphaGeometry的性能。

基准中,问题的解决数量与IMO选手的平均解题数量相对应。

如下图,灰色水平线所示,铜牌、银牌和金牌得主平均分别解决了19.3个、22.9个和25.9个问题。

所有参赛者平均解题数为15.2。

IMO-AG-30收集的具体问题集在图1(B)的左列中有所列出。

史上首次,AI超越人类奥赛金牌得主!吴方法加持,30题做出27道破纪录
(A)在IMO-AG-30问题集上,符号系统和增强型大模型(LLM-Augmented)的表现,以及与人类表现的对比
(B)展示了不同方法在解决IMO-AG-30问题集时的情况

实验

研究人员根据Trinh等人提供的基线和数据集,使用IMO-AG-30基准进行性能评估。

他们通过JGEX软件手动将IMO-AG-30问题转换成兼容格式,并重新实现了吴方法。

同时,研究者也从AlphaGeometry代码库中成功重现了必要的DD+AR基线。

经过手动验证了自己翻译的几个问题,团队确认JGEX生成的假设和结论方程是正确的。

吴方法解决了AlphaGeometry未能解决的两个问题,方案插图如下所示。

2008-P1B(JGEX):

史上首次,AI超越人类奥赛金牌得主!吴方法加持,30题做出27道破纪录

生成的答案:

史上首次,AI超越人类奥赛金牌得主!吴方法加持,30题做出27道破纪录

史上首次,AI超越人类奥赛金牌得主!吴方法加持,30题做出27道破纪录

2021-P3(JGEX):

史上首次,AI超越人类奥赛金牌得主!吴方法加持,30题做出27道破纪录

生成的答案:

史上首次,AI超越人类奥赛金牌得主!吴方法加持,30题做出27道破纪录

结果

研究结果与的先前结果,已经在图1中进行了展示。

图1(A)比较了解决问题的数量,图1(B)展示了各种方法解决的具体问题,以此可视化不同方法之间的重叠或互补性。

具体来说,研究人员将吴方法与DD+AR结合,创建了一个新的符号性能基准(Wu&DD+AR),该基准比所有传统方法多解决了6个问题。

这种组合解决了IMO-AG-30问题中的21个,与图2中未经微调(仅FT-9M)的AlphaGeometry的表现相匹配。

史上首次,AI超越人类奥赛金牌得主!吴方法加持,30题做出27道破纪录
(A)展示了在IMO-AG-30问题集上,符号方法和LLM增强(LLM-Augmented)方法的表现,以及与人类表现的对比
(B)展示了不同方法在IMO-AG-30问题上的表现

吴方法在非常低的计算需求下实现了这一表现。

在一台装有AMD Ryzen 7 5800H处理器和16 GB RAM的笔记本上,研究人员在5秒内解决了15个问题中的14个,其中一个问题(2015 P4)需要耗时3分钟。

在实验中,吴方法要么几乎立即解决问题,要么在5分钟内使笔记本内存耗尽。

值得一提的是,研究者通过吴方法解决的15个问题中的2个(2021 P3, 2008 P1B),原本是AlphaGeometry难以解决的5个问题之中的2个。

因此,通过简单地将Wu的方法与AlphaGeometry结合,实现了在IMO-AG-30基准上解决了27个问题,这一成就在图1的绿色/橙色条形(Wu&AG)中有所展示。

代数方法攻克IMO


代数方法,在自动化几何推理中解决IMO几何问题中,蕴藏着巨大的潜力。

这项研究恰恰印证了这一点,吴方法也从过往能够解决10个问题,增加到了15个问题。

而这些问题中,有几个对于目前流行的合成方法,以及增强LLM的方法,也具有非常高的挑战性。

研究者表示,其设立的符号基线,是首个在性能上超越一般IMO参赛者,并接近银牌水平。

此外,AlphaGeomtery和吴方法结合的系统,也是首个在IMO几何问题上超越人类金牌得主的AI系统。

这一成就证明了,代数方法与合成方法在这一领域的互补性。特别是,2008 P1B和2021 P3这两个问题目前仅有吴方法能解决,显示了代数方法的独特价值。

史上首次,AI超越人类奥赛金牌得主!吴方法加持,30题做出27道破纪录

尽管代数方法以其理论保证而著称,但之前因速度慢和难以为人理解而受到质疑。

而最新的研究观察显示,吴方法在多个问题上的效率远超预期,作者认为不应仅因其无法生成人类可读的证明而忽视它。

目前,研究还在进行中,受限于现有实现的不足,包括结构的限制和性能不佳。

研究者相信,传统方法有可能超越AlphaGeometry的证明能力,并希望这份研究能促进这一领域经典计算方法软件的改进。

另一方面,最新方法取得的显著成功表明,尽管IMO几何问题对人类具有挑战性,但可能并未充分挑战现代计算求解器的极限。

解题的成功更多依赖于,重复使用人定义的启发式方法和有限的构造,而不是深入探索复杂的组合可能性。

这与国际象棋残局的情况类似,其相对较早就被暴力求解器掌握了。

而研究人员希望这份研究,能激励开发几何领域自动定理证明器的新基准。

参考资料:
https://arxiv.org/abs/2404.06405

相关栏目:『社区报道
20幅讽刺现代人的插画,真实又残忍,看完第一幅就被刺痛了 2024-05-17 [4]
美国藤校生,毕业季爆改“起义季” 2024-05-16 [60]
美国驻华总领事们都有谁?(上) 2024-05-09 [140]
丘成桐讲座:中国数学的现状和将来 2024-05-08 [163]
19名杰出个人获得今年总统自由勋章 2024-05-08 [115]
AI教母李飞飞首次创业!成立“空间智能”公司,已完成种子轮 2024-05-05 [201]
祝贺!鲍哲南教授多位华人学者当选美国国家科学院院士 2024-05-05 [231]
数学大师丘成桐:为何说中国的科技肯定要倒退20年? 2024-04-26 [545]
丛京生教授等13位华人学者当选美国艺术与科学院院士 2024-04-26 [477]
清华学霸杀妻案再度开庭 2024-04-24 [287]
相关栏目更多文章
最新图文:
:美国加大审查范围 北大多名美国留学生遭联邦调查局质询 :天安门广场喜迎“十一”花团锦簇的美丽景象 马亮:做院长就能够发更多论文?论文发表是不是一场“权力的游戏”? :印裔人才在美碾压华裔:我们可以从印度教育中学到什么? :北京452万人将从北京迁至雄安(附部分央企名单) :《2019全球肿瘤趋势报告》 :阿尔茨海默病预防与干预核心讯息图解 :引力波天文台或有助搜寻暗物质粒子
更多最新图文
更多《即时通讯》>>
 
打印本文章
 
您的名字:
电子邮件:
留言内容:
注意: 留言内容不要超过4000字,否则会被截断。
未 审 核:  是
  
关于我们联系我们申请加入后台管理设为主页加入收藏
美国华裔教授专家网版权所有,谢绝拷贝。如欲选登或发表,请与美国华裔教授专家网联系。
Copyright © 2024 ScholarsUpdate.com. All Rights Reserved.