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

今日应用

135编辑器官网

135编辑器是一款提供微信公众号文章排版和内容编辑的在线工具，样式丰富，支持秒刷、收藏样式和颜色、图片素材编辑、图片水印、一键排版等功能，轻松编辑微信公众号图文。

今日话题

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

 

重点标签 AlphaProof、AlphaGeometry 2、DeepMind、AI数学奥林匹克、形式化数学

文章摘要

AlphaProof 和 AlphaGeometry 2 在 IMO 中的表现

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

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 协调和管理。

文章来源

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