AlphaGeometry:DeepMind 大算力再造奇迹,但「算力代替智力」或许并非最优解

本文主要是介绍AlphaGeometry:DeepMind 大算力再造奇迹,但「算力代替智力」或许并非最优解,希望对大家解决编程问题提供一定的参考价值,需要的开发者们随着小编来一起学习吧!

作者:李宝珠

编辑:三羊

封面图来源:Google DeepMind

DeepMind 用算力堆出奇迹?被夸上天的 AlphaGeometry 含金量有多高

近日,谷歌 DeepMind 的 Alpha 系列再添新成员——AlphaGeometry,依旧声势浩大,「里程碑」、「史诗级」、「逼近人类」等赞美之词溢出屏幕。那么,这个号称奥数能力金牌级的 AI 系统到底有多少含金量呢?

AlphaGeometry 由谷歌 DeepMind 团队和纽约大学的研究人员共同研发,将神经语言模型 (neural language model) 与符号引擎 (symbolic deduction engine) 相结合,能够解决复杂的几何问题,并且水平接近人类。

在对 30 道国际奥林匹克数学竞赛 (IMO) 几何题的基准测试中,在给定时间内 AlphaGeometry 解决了其中的 25 道题,之前 SOTA 的「吴方法」解决了 10 道,而人类 IMO 金牌得主平均可以解决 25.9 个问题。

在这里插入图片描述

诚然,自 AlphaGo 面世以来,伴随着多次面向不同学科的革新性突破,「DeepMind 出品,必属精品」的定位逐渐在人们心中扎根。但同时,业内也不乏理性、辩证的声音——算力替代智力固然可喜,但实际应用价值更加重要。所以,借着 AlphaGeometry 的发布,我们想浅谈一下,这到底是算力优势下的狂欢,还是 AI for Science 的探路。

值得一提的是,我们采访到了北京大学智能学院教授林宙辰,针对相关学术问题进行了探讨与学习。林宙辰教授曾先后在南开大学、北京大学、香港理工大学攻读数学和应用数学专业,而后又回到了北京大学数学学院攻读博士学位,开始进入人工智能领域。(点击查看林宙辰教授专访)

表达与计算量:AI for Math 的两大挑战

林宙辰教授表示:“过去,数学定理的「表达」与大规模的计算量是 AI 进行数学定理证明的两大挑战。”

“首先,作为十分抽象化、且高度依赖逻辑推理的学科,数学拥抱 AI 的第一步就是要解决「表达」问题,将数学定理表达为计算机可以计算的方式是后续 AI 应用的基础。”

“AlphaGeometry 所针对的几何问题,「表达」的难度属于数学中较低的一种,解析几何、代数几何的出现,其实已经实现了通过数值来表示几何形状和几何对象间的关系,加之吴文俊院士在 20 世纪 70 年代所提出的「数学机械化」,也在一定程度上为平面几何定理与机器语言之间构建了连接桥梁。”

“其次,吴文俊院士提出的「吴方法」以及传统的Gröbner基等方法,已经从理论上解决了平面几何定理证明的问题,但是却囿于算力,换言之,由于存储量、计算量大,尤其是在面对比较难的平面几何问题时,操作空间会呈指数级增长,所以过往的很多方法都难以处理高难度问题。”

“计算量大的问题对于「财大气粗」的 DeepMind 而言显然不是主要障碍,主要困难在于如何避免操作空间指数级增长,此时机器学习方法可以帮上忙。”

具体而言,AlphaGeometry 基于 1 亿个合成数据进行训练,无需人类演示即可自主应对复杂的几何学挑战,并生成人类可阅读的证明。

如下图所示,以我国中小学生最熟悉的「等腰定理」为例,想要证明 ∠ABC=∠BCA,需要先手动将问题转化为计算机语言,进而将其输入到 AlphaGeometry。
在这里插入图片描述

AlphaGeometry 通过运行符号推演引擎启动证明搜索,该引擎从定理前提中「穷尽」地推演出新的陈述,直到定理得到证明或新的陈述被用尽。如果符号推演引擎未能找到证明,语言模型就会构建一个辅助点,增加可证明的条件,进而重新开始通过符号引擎搜索证明。如此循环,直到找到解决方案。

解决方案将会被自动解析为人类可阅读的语言,所以还能够进行验证、评估。

值得一提的是,AlphaGeometry 使用了合成数据进行模型训练,解决了相关数据库匮乏的问题。

研究人员通过在各种随机定理前提上使用现有的符号引擎,利用 10 万个 CPU 运行了 72 小时后,获得了大约 5 亿个合成的定理证明示例,进行形式规范化及去重后,最终得到了 1 亿个定理证明示例,其中有 900 万个示例涉及至少一个辅助构造,许多证明步骤超过 200 步,是国际奥林匹克数学竞赛几何题平均证明长度的 4 倍。
在这里插入图片描述

合成数据生成过程

为了对比测试 AlphaGeometry 解决实际问题的能力,研究人员尝试将自 2000 年以来的 IMO 竞赛中的几何问题转化为符号引擎可读的机器语言,并发现其中只有 75% 可以成功表达,进而形成了一个由 30 道经典几何问题组成的测试集 IMO-AG-30。

每个问题都有不同的运行时间,这是因为其推导闭包大小各不相同。研究人员发现,运行时间与问题的难度并不相关。例如,IMO 2019 P6 比 IMO 2008 P1a 难得多,但要在 IMO 时限内求解,所需的并行化时间却要少得多。

由于语言模型解码过程会返回 k 个不同的序列,描述 k 个可供选择的辅助结构,研究人员在 k 个选项上进行集束搜索 (beam search),使用每个集束的得分作为其值函数。这种方法具有很强的并行性,在有并行计算资源的情况下,可以大幅提高搜索速度。

研究人员发现,在 GPU V100 加速语言模型有四个并行副本的情况下,解决所有 25 个问题并保持在规定时间内的最少并行 CPU 数量如下图所示:
在这里插入图片描述

10 个不同的模型/方法,在 IMO-AG-30 测试集中的表现如下图所示。有意思的是,GPT-4 在测试中竟一道题都没有做对。

在这里插入图片描述

算力替代智力的背后,应用价值才是重点

最近两天,网络上铺天盖地的各类报道已经将 AlphaGeometry 的成果剖白得淋漓尽致,其影响力无需赘述,所以我们更希望能够探究,喧闹过后,AlphaGeometry 能为科研、为 AI 应用发展带来哪些实际价值?

对此,林宙辰教授表示:“目前来看,AlphaGeometry 能够像 AlphaGo 一样成为「老师」,在教学方面起到更大的辅助作用。此外,AlphaGeometry 在模型性能方面的突破不可否认,其更是进一步展示了「大力出奇迹」——强大的算力优势造就了强悍的模型性能,这也在某种程度上进一步为「崇尚」算力的研究人员、企业增添了信心。”

不过,正如林宙辰教授所言,在 AI 领域,尽管我们已经无数次见证了「算力替代智力」的有效性,但最终迈向行业专家的最后1% 的突破还是很难靠 AI 来实现的

所以,就目前而言,无论是 AlphaGeometry,亦或 GPT 模型等其他 AI 工具,在人们的日常生活以及科研工作中,仍是「亦师亦友」的存在,灵活使用 AI 工具已是大势所趋,如何将算力造就的「奇迹」应用于实际问题才是人类难以被取代的价值所在。

借古鉴今,AI 工具的快速崛起与计算机的普及有着很多相似之处,例如革命性的工作方式转变,正势如破竹地替代传统方法,逐渐成为职场能力的考核标准……但对比之下,AI 工具的局限性也更加凸显,那就是特异性。

林宙辰教授认为:“目前的 AI 工具缺乏统一性,即使只针对数学学科,面向数论和面向几何学所开发的 AI 工具就已经存在很大差别,更不用提跨学科的AI工具了。AI 工具还没有像当今的计算机一样,成为基础底座,可以方便取用。目前的计算机语言有 C 语言、Java、Python等,完全可以基于其中一种语言解决数学、物理、化学等多学科的问题,这体现了其通用性,但是 AI 工具则不然,光看 Alpha 系列便可知一二。”

所以,林宙辰教授认为:“未来,当 AI 工具可以抽象出来可以重用时,AI for Science 才能够「大行其道」。”

这也是 HyperAI超神经在持续追踪 AI for Science 发展进程时所观察到的现象,部分课题组或研究团队会在本学科成员之外,专门招聘一位主攻 AI 的成员,负责开发研究中需要的 AI工具,而Science 部分则还是交由传统的科研人员来完成。

毫无疑问,AI 对科研进程的帮助与提升已经日益明显,正在成为新趋势,但这种 AI+Science 的团队模式又是否是长久之计呢?

林宙辰教授认为:“未来,一方面需要将 AI 工具的使用门槛降低,达到一定的统一性,使得 Science 人员也能够针对不同的问题自行组合使用 AI 工具的组件,就像计算机编程一样;另一方面,Science 人员也需要逐步提升使用 AI工具的能力,才能充分发挥AI的威力。”

道阻且长,行之将至。AI for Science 由DeepMind 等大厂引发,加之国家政策推进,已经开始了漫漫征程,其中的荆棘需要科研与产业界共同肃清,才能够真正在落地中为人类发展创造价值。

最后,感谢北京大学智能学院林宙辰教授对笔者撰文提供的帮助与支持。目前林宙辰教授的课题组正在招聘博士研究生,欢迎符合要求的学生将简历发送至:zlin@pku.edu.cn

我信奉的信条是物理学家路德维希·波兹曼的名言:没有什么比一个好的理论更实用的了。我现在想招数学能力强(但这并不意味着你必须来自数学系)、对理论分析非常感兴趣的博士研究生,以便与我一起享受如何优雅地使用数学解决实际问题。欢迎发送简历给我。

——林宙辰

这篇关于AlphaGeometry:DeepMind 大算力再造奇迹,但「算力代替智力」或许并非最优解的文章就介绍到这儿,希望我们推荐的文章对编程师们有所帮助!



http://www.chinasem.cn/article/626033

相关文章

如何用GPU算力卡P100玩黑神话悟空?

精力有限,只记录关键信息,希望未来能够有助于其他人。 文章目录 综述背景评估游戏性能需求显卡需求CPU和内存系统需求主机需求显式需求 实操硬件安装安装操作系统Win11安装驱动修改注册表选择程序使用什么GPU 安装黑神话悟空其他 综述 用P100 + PCIe Gen3.0 + Dell720服务器(32C64G),运行黑神话悟空画质中等流畅运行。 背景 假设有一张P100-

17 通过ref代替DOM用来获取元素和组件的引用

重点 ref :官网给出的解释是: ref: 用于注册对元素或子组件的引用。引用将在父组件的$refs 对象下注册。如果在普通DOM元素上使用,则引用将是该元素;如果在子组件上使用,则引用将是组件实例: <!-- vm.$refs.p will be the DOM node --><p ref="p">hello</p><!-- vm.$refs.child will be the c

一些数学经验总结——关于将原一元二次函数增加一些限制条件后最优结果的对比(主要针对公平关切相关的建模)

1.没有分段的情况 原函数为一元二次凹函数(开口向下),如下: 因为要使得其存在正解,必须满足,那么。 上述函数的最优结果为:,。 对应的mathematica代码如下: Clear["Global`*"]f0[x_, a_, b_, c_, d_] := (a*x - b)*(d - c*x);(*(b c+a d)/(2 a c)*)Maximize[{f0[x, a, b,

4-4.Andorid Camera 之简化编码模板(获取摄像头 ID、选择最优预览尺寸)

一、Camera 简化思路 在 Camera 的开发中,其实我们通常只关注打开相机、图像预览和关闭相机,其他的步骤我们不应该花费太多的精力 为此,应该提供一个工具类,它有处理相机的一些基本工具方法,包括获取摄像头 ID、选择最优预览尺寸以及打印相机参数信息 二、Camera 工具类 CameraIdResult.java public class CameraIdResult {

servlet用反射代替if..else

String methodName = request.getParameter("method"); Method method = this.getClass().getDeclaredMethod(methodName,HttpServletRequest.class, HttpServletResponse.class); method.invoke(this, request, re

Banana Pi BPI-F3 进迭时空RISC-V架构下,AI融合算力及其软件栈实践

RISC-V架构下,AI融合算力及其软件栈实践 面对未来大模型(LLM)、AIGC等智能化浪潮的挑战,进迭时空在RISC-V方向全面布局,通过精心设计的RISC-V DSA架构以及软硬一体的优化策略,将全力为未来打造高效且易用的AI算力解决方案。目前,进迭时空已经取得了显著的进展,成功推出了第一个版本的智算核(带AI融合算力的智算CPU)以及配套的AI软件栈。 软件栈简介 AI算法部署旨

重生奇迹MU老大哥剑士职业宝刀未老

重生奇迹MU中,老大哥剑士职业一直以来备受玩家们的喜爱。这个职业不仅拥有强大的攻击力、防御力和战斗技巧,而且还能够通过使用各种宝刀来增强自身的战斗能力。即便经过了多年的沉淀,老大哥剑士依然是一名宝刀未老的男人,仍然能够在战场上力挽狂澜。如果你是一名重生奇迹MU玩家,不妨选择老大哥剑士职业,体验一下宝刀未老的快感! 人们常常怀念过去,那是因为过去有深刻的记忆。在重生奇迹MU里,最令人难忘的职业便是

去 IOE 的本质不是 PR 砸场,而是云端再造

「青云一直有一个目标,就是要建立一朵更好的云,全模云的推出也标志着我们在实现这个目标上往前走了一大步。」 本文由青云QingCloud CTO 甘泉的演讲内容整理而来,共 2628 字,8 图,阅读大概需要 7 分钟。 青云QingCloud 如何解决「敏态」问题 先谈谈传统业务的 IT 部署模式,基本上都是刀片机+存储柜的模式,它们都是真实的物理机,上图密密麻麻的是刀片机,右边是存

没通过算法备案 或许是这几点你没做好

没通过算法备案 或许是这几点你没做好 当企业提交算法备案遭遇“不予通过”时,往往是因为一些看似微小却至关重要的细节未能达到标准。以下是一些常见的原因,希望能为准备备案的企业提供一些预警和指导: ICP备案缺失:互联网信息服务业务需先通过ICP(互联网信息服务)备案,这是基础门槛。如果上线平台未完成这一步骤,就如一座大厦未打地基,后续的备案自然难以通过。确保你的平台已经完成了必要的网络身份

AI技术颠覆游戏开发:谷歌DeepMind GameNGen实时生成《DOOM》探秘

引言 近年来,生成式人工智能(AIGC)在图像和视频生成领域取得了巨大突破。然而,谁能想到,这项技术正逐渐渗透进游戏开发领域,且潜力巨大。2023年8月29日,谷歌DeepMind发布了名为《扩散模型是实时游戏引擎》(Diffusion Models Are Real-Time Game Engines)的论文,提出了全新的AI游戏生成引擎GameNGen。令人惊讶的是,GameNGen无需传统