谷歌AI拿下IMO奥数银牌,数学推理模型AlphaProof面世,强化学习 is so back

AI最新资讯2个月前发布 tree
26 0 0

今日应用


今日话题


谷歌AI拿下IMO奥数银牌,数学推理模型AlphaProof面世,强化学习 is so back
谷歌AI拿下IMO奥数银牌,数学推理模型AlphaProof面世,强化学习 is so back
 

重点标签 AlphaProofAlphaGeometry 2DeepMindAI数学奥林匹克形式化数学

文章摘要


AlphaProofAlphaGeometry 2 在 IMO 中的表现

在 2024 年的国际数学奥林匹克竞赛(IMO)中,谷歌 DeepMind 研发的人工智能系统完成了六道赛题中的四道,获得了 28 分,达到了银牌水平。AlphaProof 是一种形式化数学推理的强化学习系统,而 AlphaGeometry 2DeepMind 几何求解系统的改进版本。这两个系统在几分钟内解决了一个问题,但花了三天时间来解决其他问题,尽管这超出了正式比赛的时间限制。

AlphaProof 的形式化推理方法

AlphaProof 是一个自训练系统,使用形式语言 Lean 来证明数学陈述。它结合了预训练语言模型与 AlphaZero 强化学习算法,通过微调 Gemini 模型自动将自然语言问题陈述翻译为形式陈述。AlphaProof 生成候选解题方案,并通过搜索 Lean 中可能的证明步骤来证明它们。每个验证的证明方案都用来强化其语言模型,以解决更具挑战性的问题。

AlphaGeometry 2 的神经 – 符号混合系统

AlphaGeometry 2 是基于 Gemini 语言模型的神经 – 符号混合系统,它在合成数据上从头开始训练,能够解决更具挑战性的几何问题。与前身相比,AlphaGeometry 2 的符号引擎速度更快,且在遇到新问题时,能够实现不同搜索树的高级组合,以解决更复杂的问题。

AI 在数学领域的应用前景

DeepMind 的 AI 系统在 IMO 中的表现证明了通用人工智能在高级数学推理方面的能力。未来,数学家们有望使用 AI 工具探索假设,尝试新方法解决长期存在的问题,并快速完成耗时的证明元素。随着 AI 系统在数学和更广泛推理方面变得更加强大,它们将在科学技术新领域的开启中发挥重要作用。

研究团队的贡献

谷歌 DeepMind 的新研究得到了国际数学奥林匹克组织的支持。AlphaProof 的开发由 Thomas Hubert、Rishi Mehta 和 Laurent Sartran 领导,主要贡献者包括 Aja Huang、Julian Schrittwieser、Yannick Schroecker 等,他们也是 8 年前 AlphaGo 论文的核心成员。AlphaGeometry 2 的开发由 Trieu Trinh 和 Yuri Chervonyi 领导,Mirek Olšák、Xiaomeng Yang、Hoang Nguyen 等做出了重要贡献。整个项目由 David Silver、Quoc Le、哈萨比斯和 Pushmeet Kohli 协调和管理。

文章来源


原文地址: 点我阅读全文
原文作者: 机器之心

© 版权声明

相关文章

暂无评论

暂无评论...