<div id="readability-page-1">高级数学推理是现代人工智能的关键能力。今天，Google 宣布了一项长期重大挑战中的一个重要里程碑：Google 混合人工智能系统在今年的国际数学奥林匹克竞赛（IMO）中获得了相当于银牌的成绩 具体来说 google 展示了第一个以银牌级别解决国际数学奥林匹克问题的人工智能 它结合了 AlphaProof（一种新的突破性形式推理模型）和 AlphaGeometry 2（之前系统的改进版本） 国际数学奥林匹克竞赛是全球最悠久、规模最大、最具声望的青年数学家比赛，自 1959 年起每年举办一次。参赛者需要解决六道涉及代数、组合学、几何和数论的极其困难的问题。许多菲尔兹奖得主曾在青年时期代表国家参加过 IMO。近年来，IMO 也成为了机器学习领域的一个重要挑战，被视为衡量人工智能系统高级数学推理能力的标杆 在今年的比赛中，DeepMind 的 AI 系统获得了 28 分（满分 42 分），相当于银牌获得者的水平。这一成绩仅差 1 分就能达到金牌标准，而在今年的 609 名参赛者中，只有 58 人获得了金牌 <img src="https://imageproxy.pbkrs.com/https://wpimg-wscn.awtmt.com/544750ab-e0e1-4481-a546-47a442ae625a.png/query-aW1hZ2VWaWV3Mi8yL3cvNjQw?x-oss-process=image/auto-orient,1/interlace,1/resize,w_1440,h_1440/quality,q_95/format,jpg" width="640" height="640" original-src="https://imageproxy.pbkrs.com/https://wpimg-wscn.awtmt.com/544750ab-e0e1-4481-a546-47a442ae625a.png/query-aW1hZ2VWaWV3Mi8yL3cvNjQw"/> <h2>AlphaProof：形式化数学推理的突破</h2> AlphaProof 系统采用强化学习方法，将预训练的语言模型与 AlphaZero 算法相结合。这种方法的优势在于可以正式验证涉及数学推理的证明的正确性。为了克服形式化语言训练数据不足的问题，研究团队通过微调 Gemini 模型，创建了一个包含各种难度的形式化问题库 AlphaProof 是一个自学习系统，专门用于在形式化数学语言 Lean 中证明数学陈述。它的核心创新在于结合了预训练语言模型和 AlphaZero 强化学习算法 工作流程如下： <img src="https://imageproxy.pbkrs.com/https://wpimg-wscn.awtmt.com/2041e0fd-1562-4867-b465-d5c43a1fd165.png/query-aW1hZ2VWaWV3Mi8yL3cvNjQw?x-oss-process=image/auto-orient,1/interlace,1/resize,w_1440,h_1440/quality,q_95/format,jpg" width="640" height="640" original-src="https://imageproxy.pbkrs.com/https://wpimg-wscn.awtmt.com/2041e0fd-1562-4867-b465-d5c43a1fd165.png/query-aW1hZ2VWaWV3Mi8yL3cvNjQw"/> 1.问题转化：首先，使用经过微调的 Gemini 模型将自然语言的数学问题自动转换为 Lean 的形式化语言。这一步骤创建了一个大型的形式化问题库，涵盖不同难度级别 <img src="https://imageproxy.pbkrs.com/https://wpimg-wscn.awtmt.com/d17b6ac9-1238-4a42-8b81-90326c49db97.png/query-aW1hZ2VWaWV3Mi8yL3cvNjQw?x-oss-process=image/auto-orient,1/interlace,1/resize,w_1440,h_1440/quality,q_95/format,jpg" width="640" height="640" original-src="https://imageproxy.pbkrs.com/https://wpimg-wscn.awtmt.com/d17b6ac9-1238-4a42-8b81-90326c49db97.png/query-aW1hZ2VWaWV3Mi8yL3cvNjQw"/> 2.解决方案生成：面对一个新问题时，AlphaProof 会生成可能的解决方案 3.证明搜索：系统在 Lean 中搜索可能的证明步骤，试图证明或反驳这些解决方案 4.强化学习：每找到并验证一个证明，就用它来强化 AlphaProof 的语言模型，提高系统解决后续更具挑战性问题的能力 5.持续训练：在准备 IMO 比赛期间，AlphaProof 在数周内证明或反驳了数百万个问题，覆盖各种难度和数学主题。在比赛过程中，它还继续应用这个训练循环，通过证明自己生成的比赛问题变体来增强能力，直到找到完整解决方案 <h2>AlphaGeometry 2</h2> AlphaGeometry 2 是 AlphaGeometry 的改进版本，它的语言模型基于 Gemini，并在比前代多一个数量级的合成数据上进行了训练 <img src="https://imageproxy.pbkrs.com/https://wpimg-wscn.awtmt.com/bf039204-358c-469b-9ef2-ff7ed613e75f.png/query-aW1hZ2VWaWV3Mi8yL3cvNjQw?x-oss-process=image/auto-orient,1/interlace,1/resize,w_1440,h_1440/quality,q_95/format,jpg" width="640" height="640" original-src="https://imageproxy.pbkrs.com/https://wpimg-wscn.awtmt.com/bf039204-358c-469b-9ef2-ff7ed613e75f.png/query-aW1hZ2VWaWV3Mi8yL3cvNjQw"/> AlphaGeometry 2 是一个神经符号混合系统。主要改进包括： 1.增强的语言模型：基于 Gemini，从头开始训练，使用了比前代多一个数量级的合成数据。这大大提高了模型处理复杂几何问题的能力，包括物体运动、角度方程、比例或距离等问题 2.更快的符号引擎：新版本的符号处理引擎速度提高了两个数量级，大大加快了问题解决速度 3.知识共享机制：引入了新的知识共享机制，能够高级组合不同的搜索树，以解决更复杂的问题 4.性能提升：在接受今年 IMO 比赛前，AlphaGeometry 2 能够解决过去 25 年 IMO 几何问题的 83%，远超前代系统 53% 的解决率 5.实时表现：在今年的 IMO 中，AlphaGeometry 2 在接收到形式化的第 4 题后，仅用 19 秒就解决了这个问题 6.DeepMind 的研究团队还在探索基于自然语言推理的系统，这种系统不需要将问题转换为形式化语言，可能与其他 AI 系统结合使用。这种方法在今年的 IMO 问题上也显示出了巨大的潜力 本文作者：AI 寒武纪，来源：AI 寒武纪，原文标题：《数学界的 AlphaGo 时刻：谷歌 DeepMind AI 19 秒解 IMO 几何题，仅差 1 分即可摘金牌》 </div>

谷歌-A

谷歌-C

谷歌的人工智能系统在国际数学奥林匹克竞赛中获得了相当于银牌的成绩，展示了其在解决数学问题方面的突破性能力。该系统结合了 AlphaProof 和 AlphaGeometry 2，以较高水平解答了国际数学奥林匹克问题。这是一项重要的里程碑，显示了人工智能在数学领域的潜力。

- Google 混合人工智能系统在国际数学奥林匹克竞赛获得相当于银牌的成绩，展示了高级数学推理能力。
- AlphaProof 结合了预训练语言模型和 AlphaZero 算法，用于形式化数学推理，通过强化学习方法验证数学证明的正确性。
- AlphaGeometry 2 是神经符号混合系统，速度更快，能解决过去 25 年 IMO 几何问题的 83%，在今年的比赛中仅用 19 秒解决一个问题。