Google AI가 IMO 수학 올림피아드 은메달을 획득하고 수학적 추론 모델 AlphaProof가 출시되었으며 강화 학습이 다시 시작되었습니다.

AI에게 수학 올림피아드는 더 이상 문제가 되지 않습니다.

목요일, Google DeepMind의 인공 지능은 AI를 사용하여 올해 국제 수학 올림피아드 IMO의 실제 문제를 해결하는 위업을 달성했으며 금메달 획득이 단 한 발 남았습니다.

지난주에 막 끝난 IMO 대회에서는 대수학, 조합론, 기하학, 수론 등 총 6개의 문제가 출제되었습니다. 구글이 제안한 하이브리드 AI 시스템은 4개 문제를 맞혀 28점을 얻어 은메달 수준에 이르렀다.

이달 초 UCLA 종신 교수인 테렌스 타오(Terence Tao)가 AI Math Olympiad(AIMO Progress Award)를 홍보하여 ​​백만 달러의 상금을 수여했습니다. 의외로 AI 문제 해결 수준이 7월 이전에 이 수준으로 향상되었습니다.

IMO에서 문제를 동시에 해결하고 가장 어려운 문제도 맞히세요

IMO는 1959년부터 매년 개최되는 젊은 수학자들을 위한 가장 오래되고 규모가 크며 권위 있는 대회입니다. 최근 IMO 대회는 머신러닝 분야에서도 거대한 도전으로 널리 인식돼 인공지능 시스템의 고급 수학적 추론 능력을 측정하는 이상적인 벤치마크가 되고 있다.

올해 IMO 대회에서 DeepMind 팀이 공동으로 개발한 AlphaProof와 AlphaGeometry 2가 획기적인 돌파구를 달성했습니다.

그 중 AlphaProof는 형식적인 수학적 추론을 위한 강화 학습 시스템인 반면, AlphaGeometry 2는 DeepMind의 기하학 해결 시스템인 AlphaGeometry를 개선한 버전입니다.

이 획기적인 발전은 과학과 기술의 새로운 영역을 여는 고급 수학적 추론 기능을 갖춘 일반 인공지능(AGI)의 잠재력을 보여줍니다.

그렇다면 DeepMind의 AI 시스템은 어떻게 IMO 대회에 참가하나요?

간단히 말하면, 먼저 이러한 수학적 문제를 AI 시스템이 이해할 수 있도록 공식적인 수학 언어로 수동으로 번역합니다. 공식 대회에서는 인간 참가자들이 2개의 세션(2일)에 걸쳐 답변을 제출하며, 세션당 시간 제한은 4.5시간입니다. 결합된 AlphaProof+AlphaGeometry 2 AI 시스템은 한 가지 문제를 몇 분 만에 해결했지만 다른 문제를 해결하는 데는 3일이 걸렸습니다. 규칙을 엄격히 따르면 DeepMind 시스템이 시간 초과되었습니다. 어떤 사람들은 이것이 많은 무차별 대입 크래킹을 포함할 수 있다고 추측합니다.

Google은 AlphaProof가 답을 결정하고 정확성을 입증함으로써 두 가지 대수학 문제와 한 정수론 문제를 해결했다고 말했습니다. 여기에는 올해 IMO에서 5명의 참가자만이 해결한 대회에서 가장 어려운 문제가 포함됩니다. 그리고 AlphaGeometry 2는 기하학 문제를 증명합니다.

AI가 제공하는 솔루션: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html

IMO 금메달 수상자이자 필즈상 수상자 Timothy Gowers 및 IMO 2회 금메달리스트이자 IMO 2024 문제 선택 위원회 의장인 Joseph Myers 박사는 IMO 채점 규칙에 따라 결합된 시스템이 제공하는 솔루션의 점수를 매겼습니다.

6개 질문은 각각 7점으로 최대 총점은 42점입니다. DeepMind의 시스템은 최종 점수 28점을 받았습니다. 이는 해결한 문제 4개 모두 만점을 받았음을 의미합니다. 이는 은메달 부문에서 가장 높은 점수에 해당합니다. 올해 금메달 기준점은 29점으로, 공식 대회에 참가한 609명의 참가자 중 58명이 금메달을 획득했습니다.

이 그래프는 IMO 2024에서 인간 경쟁자와 비교하여 Google DeepMind의 인공 지능 시스템의 성능을 보여줍니다. 이 시스템은 42점 만점에 28점을 얻어 대회의 은메달리스트와 동등한 점수를 받았습니다. 게다가 올해 금메달을 획득하려면 29점이면 충분하다.

AlphaProof: 형식적 추론 방법

Google에서 사용하는 하이브리드 AI 시스템에서 AlphaProof는 형식 언어 Lean을 사용하여 수학적 진술을 증명하는 자가 학습 시스템입니다. 사전 훈련된 언어 모델과 AlphaZero 강화 학습 알고리즘을 결합합니다.

그 중에서 형식 언어는 수학적 추론 증명의 정확성을 형식적으로 검증하는 데 중요한 이점을 제공합니다. 지금까지는 사람이 작성한 데이터의 양이 매우 제한적이었기 때문에 머신러닝에서는 이 기능이 제한적으로 사용되었습니다.

반대로 자연어 기반 방법은 더 많은 양의 데이터에 접근할 수 있지만 합리적이지만 부정확해 보이는 중간 추론 단계와 솔루션을 생성합니다.

Google DeepMind는 Gemini 모델을 미세 조정하여 자연어 문제 설명을 공식적인 설명으로 자동 번역함으로써 이 두 가지 상호보완적인 분야 사이에 다리를 놓아 다양한 난이도의 형식 문제로 구성된 대규모 라이브러리를 만듭니다.

수학적 문제가 주어지면 AlphaProof는 후보 솔루션을 생성한 다음 Lean에서 가능한 증명 단계를 검색하여 이를 증명합니다. 발견되고 검증된 각 증명 솔루션은 AlphaProof의 언어 모델을 강화하고 이후의 더욱 어려운 문제를 해결하는 능력을 향상시키는 데 사용됩니다.

为训练 AlphaProof，谷歌 DeepMind 在 IMO 比赛前几周内证明或反证明了涵盖广泛难度与主题的数百万个数学问题。比赛期间还应用了训练 loop，以强化自生成竞赛题变体的证明，直到找到完整的解决方案。

AlphaProof 强化学习训练 loop 过程信息图：约一百万个非形式化数学问题被形式化网络翻译成形式化数学语言。然后，求解器网络搜索问题的证明或反证，通过 AlphaZero 算法逐步训练自己解决更具挑战性的问题。

更具竞争力的 AlphaGeometry 2

AlphaGeometry 2 是今年登上《自然》杂志的数学 AI AlphaGeometry 的重大改进版本。它是一个神经 - 符号混合系统，其中的语言模型基于 Gemini，并在比其前身多一个数量级的合成数据上从头开始训练。这有助于该模型解决更具挑战性的几何问题，包括有关物体运动以及角度、比例或距离方程的问题。

AlphaGeometry 2 采用的符号引擎比上一代产品快两个数量级。当遇到新问题时，新颖的知识共享机制可实现不同搜索树的高级组合，以解决更复杂的问题。

在今年的比赛之前，AlphaGeometry 2 可以解决过去 25 年中所有 IMO 几何历史问题的 83%，而其前身的解决率仅为 53%。在 IMO 2024 中，AlphaGeometry 2 在收到问题 4 的形式化后 19 秒内就解决了它。

问题 4 的示例，要求证明∠KIL 与∠XPY 的和等于 180°。AlphaGeometry 2 提议在直线 BI 上构造点 E，使得∠AEB = 90°。点 E 有助于赋予线段 AB 中点 L 以意义，从而创建许多对相似三角形，如 ABE ~ YBI 和 ALE ~ IPC，以证明结论。

谷歌 DeepMind 还报告说，作为 IMO 工作的一部分，研究人员还试验了一种基于 Gemini 和一种最新的自然语言推理系统，希望实现高级的问题解决能力。该系统不需要将问题翻译成正式语言，并且可以与其他 AI 系统相结合。在今年的 IMO 赛题的测试中「显示出了巨大的潜力」。

谷歌正在继续探索推进数学推理的 AI 方法，并计划很快发布有关 AlphaProof 的更多技术细节。

我们对未来充满期待，数学家们将使用 AI 工具探索假设，尝试大胆的新方法来解决长期存在的问题，并快速完成耗时的证明元素——而像 Gemini 这样的 AI 系统将在数学和更广泛的推理方面变得更加强大。

研究团队

谷歌表示，新研究得到了国际数学奥林匹克组织的支持，此外：

AlphaProof 的开发由 Thomas Hubert、Rishi Mehta 和 Laurent Sartran 领导；主要贡献者包括 Hussain Masoom、Aja Huang、Miklós Z. Horváth、Tom Zahavy、Vivek Veeriah、Eric Wieser、Jessica Yung、Lei Yu、Yannick Schroecker、Julian Schrittwieser、Ottavia Bertolli、Borja Ibarz、Edward Lockhart、Edward Hughes、Mark Rowland 和 Grace Margand。

其中，Aja Huang、Julian Schrittwieser、Yannick Schroecker 等成员也是 8 年前（2016 年）AlphaGo 论文的核心成员。8 年前，他们基于强化学习打造的 AlphaGo 声名大噪。8 年后，强化学习在 AlphaProof 中再次大放异彩。有人在朋友圈感叹说：RL is so back！

AlphaGeometry 2 和自然语言推理工作由 Thang Luong 领导。AlphaGeometry 2 的开发由 Trieu Trinh 和 Yuri Chervonyi 领导，Mirek Olšák、Xiaomeng Yang、Hoang Nguyen、Junehyuk Jung、Dawsen Hwang 和 Marcelo Menegali 做出了重要贡献。

此外，David Silver、Quoc Le、哈萨比斯和 Pushmeet Kohli 负责协调和管理整个项目。

参考内容：

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

위 내용은 Google AI가 IMO 수학 올림피아드 은메달을 획득하고 수학적 추론 모델 AlphaProof가 출시되었으며 강화 학습이 다시 시작되었습니다.의 상세 내용입니다. 자세한 내용은 PHP 중국어 웹사이트의 기타 관련 기사를 참조하세요!