https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
终于再次出现遥遥领先的 AI,DeepMind 的 AI 在解决国际数学奥林匹克竞赛问题中达到银牌水平,是神经-符号混合型 AI;AGI 2.0 时代将会到来,终于能大大方方地说 LLM 只是统计游戏
家人们准备进入 AGI 2.0 时代,等这个一出,我也可以大大方方说 LLM 算什么 AGI,统计游戏罢了;很多公司特别是支那公司都在堆算力训练自己的 LLM,一点都没有遥遥领先的感觉
AI 在解决国际数学奥林匹克竞赛问题中达到银牌水平
突破性模型 AlphaProof 和 AlphaGeometry 2 解决了数学中的高级推理问题
具有高级数学推理能力的人工智能 (AGI) 有可能开启科学技术的新领域。
在构建人工智能系统方面,我们已经取得了很大进展,这些系统可以帮助数学家发现新见解、新算法以及开放问题的答案。但是,由于推理能力和训练数据的限制,当前的人工智能系统在解决一般数学问题方面仍然很吃力。
今天,我们推出了 AlphaProof,这是一个基于强化学习的新型形式化数学推理系统,以及 AlphaGeometry 2,这是我们几何求解系统的改进版本。这两个系统共同解决了今年国际数学奥林匹克竞赛 (IMO) 的六道题中的四道,首次达到了与该竞赛银牌获得者相同的水平。
解决复杂数学问题的突破性人工智能性能
国际数学奥林匹克竞赛 (IMO) 是历史最悠久、规模最大、最负盛名的青年数学家竞赛,自 1959 年以来每年举办一次。
每年,精英高中数学家都要进行训练,有时长达数千小时,以解决六道异常困难的代数、组合数学、几何和数论问题。许多菲尔兹奖(数学家的最高荣誉之一)的获得者都曾代表他们的国家参加过国际数学奥林匹克竞赛。
近年来,一年一度的国际数学奥林匹克竞赛也被广泛认为是机器学习领域的一项重大挑战,也是衡量人工智能系统高级数学推理能力的一个理想基准。
今年,我们将我们组合的人工智能系统应用于国际数学奥林匹克竞赛组委会提供的竞赛问题。我们的解决方案由著名的数学家Timothy Gowers 教授(国际数学奥林匹克竞赛金牌获得者和菲尔兹奖获得者)和Joseph Myers 博士(两届国际数学奥林匹克竞赛金牌获得者和 2024 年国际数学奥林匹克竞赛问题遴选委员会主席)根据国际数学奥林匹克竞赛的评分规则进行评分。
“
该程序能够想出这样一种非同寻常的构造,这真是令人印象深刻,远远超出了我认为的最先进水平。
Timothy Gowers 教授,
国际数学奥林匹克竞赛金牌获得者和菲尔兹奖获得者
首先,将问题手动翻译成我们的系统能够理解的形式化数学语言。在正式比赛中,学生在两场考试中提交答案,每场考试 4.5 小时。我们的系统在几分钟内解决了一个问题,而其他问题则花费了长达三天的时间。
AlphaProof 通过确定答案并证明其正确性,解决了两个代数问题和一个数论问题。这其中包括竞赛中最难的一道题,今年的国际数学奥林匹克竞赛中只有五名选手解出了这道题。AlphaGeometry 2 证明了几何问题,而两个组合数学问题仍然未解。
六道题每道题最高可获得 7 分,总分最高为 42 分。我们的系统最终获得了 28 分,每道解出的题都获得了满分,相当于银牌组的最高水平。今年,金牌门槛分值为 29 分,在正式比赛的609 名参赛者中,有 58 人达到了这一分数。
图表显示了我们的人工智能系统与 2024 年国际数学奥林匹克竞赛中人类选手的表现对比。我们在 42 分中获得了 28 分,达到了与该竞赛银牌获得者相同的水平。
AlphaProof:一种形式化的推理方法
AlphaProof 是一个训练自己在形式化语言 Lean 中证明数学陈述的系统。它将预先训练的语言模型与 AlphaZero 强化学习算法相结合,该算法之前教会了自己如何掌握国际象棋、日本将棋和围棋。
形式化语言提供了一个关键优势,即可以通过形式化验证来确保涉及数学推理的证明的正确性。然而,它们在机器学习中的应用以前一直受到可用的手写数据量非常有限的限制。
相比之下,基于自然语言的方法可能会产生似是而非但不正确的中间推理步骤和解决方案,尽管它们可以访问数量级更多的数据。我们通过微调 Gemini 模型来自动将自然语言问题陈述转换为形式化陈述,从而在这两个互补的领域之间架起了一座桥梁,创建了一个包含各种难度的形式化问题的大型库。
当 AlphaProof 收到一个问题时,它会生成候选解决方案,然后通过在 Lean 中搜索可能的证明步骤来证明或反驳这些解决方案。找到并验证的每个证明都被用来强化 AlphaProof 的语言模型,增强其解决后续更具挑战性问题的能力。
我们通过证明或反驳数百万个问题来训练 AlphaProof 参加国际数学奥林匹克竞赛,这些问题涵盖了广泛的难度和数学主题领域,在比赛前的几周内完成。在比赛期间也应用了训练循环,强化对竞赛问题的自生成变体的证明,直到找到完整的解决方案。
AlphaProof 强化学习训练循环的过程信息图:大约一百万个非正式数学问题由形式化网络转换为形式化数学语言。然后,求解器网络搜索问题的证明或反驳,并通过 AlphaZero 算法逐步训练自己,以解决更具挑战性的问题。
更具竞争力的 AlphaGeometry 2
AlphaGeometry 2 是 AlphaGeometry 的一个显著改进版本。它是一个神经符号混合系统,其语言模型基于 Gemini,并在比其前身多一个数量级的合成数据上从头开始训练。这有助于模型解决更具挑战性的几何问题,包括有关物体运动以及角度、比率或距离方程的问题。
AlphaGeometry 2 采用了一个符号引擎,其速度比其前身快两个数量级。当遇到新问题时,会使用一种新颖的知识共享机制来启用不同搜索树的高级组合,以解决更复杂的问题。
在今年的竞赛之前,AlphaGeometry 2 可以解决过去 25 年中所有历史国际数学奥林匹克竞赛几何问题的 83%,而其前身的解决率为 53%。在 2024 年国际数学奥林匹克竞赛中,AlphaGeometry 2 在收到问题 4 的形式化描述后,在 19 秒内就解决了这个问题。
问题 4 的图解,要求证明 ∠KIL 和 ∠XPY 的和等于 180°。AlphaGeometry 2 建议构造点 E,它是线 BI 上的一个点,使得 ∠AEB = 90°。点 E 有助于确定 AB 的中点 L 的用途,从而创建许多对相似三角形,例如 ABE ~ YBI 和 ALE ~ IPC,这些三角形是证明结论所需的。
数学推理的新领域
作为国际数学奥林匹克竞赛工作的一部分,我们还试验了一个自然语言推理系统,该系统建立在 Gemini 和我们最新的研究成果之上,以实现高级问题解决能力。该系统不需要将问题翻译成形式化语言,并且可以与其他人工智能系统相结合。我们还在今年的国际数学奥林匹克竞赛问题上测试了这种方法,结果显示出巨大的潜力。
我们的团队正在继续探索多种人工智能方法来推进数学推理,并计划很快发布有关 AlphaProof 的更多技术细节。
我们对数学家与人工智能工具协同工作的未来感到兴奋,这些工具可以探索假设,尝试大胆的新方法来解决长期存在的问题,并快速完成耗时的证明元素,而且像 Gemini 这样的人工智能系统在数学和更广泛的推理方面将变得更加强大。