发表于 2024年7月25日1年前 原文链接： https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/ 以下翻译来自谷歌 人工智能在解决国际数学奥林匹克问题上达到银牌标准 突破性模型 AlphaProof 和 AlphaGeometry 2 解决数学中的高级推理问题 具有高级数学推理能力的通用人工智能（ AGI ）有可能开辟科学技术的新领域。 我们在构建人工智能系统方面取得了巨大进步，该系统可以帮助数学家发现新见解、新算法和未解决问题。但由于推理能力和训练数据的限制，目前的人工智能系统仍然难以解决一般数学问题。 今天，我们推出了基于强化学习的新型形式数学推理系统 AlphaProof ，以及我们几何求解系统的改进版本 AlphaGeometry 2 。这两个系统共同解决了今年国际数学奥林匹克(IMO) 六道题目中的四道，首次在竞赛中取得与银牌得主同等的成绩。 突破性的人工智能性能解决复杂的数学问题 国际数学奥林匹克竞赛是历史最悠久、规模最大、最负盛名的青年数学竞赛，自 1959 年起每年举办。 每年，顶尖的大学前数学家们都要训练，有时要训练数千小时，以解决代数、组合学、几何学和数论领域的六道极其困难的难题。菲尔兹奖是数学家的最高荣誉之一，许多获奖者都曾代表他们的国家参加过国际数学奥林匹克比赛。 近年来，一年一度的国际数学奥林匹克竞赛也被广泛认为是机器学习领域的一大挑战，也是衡量人工智能系统高级数学推理能力的理想基准。 今年，我们将联合人工智能系统应用于 IMO 主办方提供的竞赛问题。我们的解决方案由著名数学家、IMO 金牌得主和菲尔兹奖得主蒂莫西·高尔斯爵士教授和两届 IMO 金牌得主、IMO 2024 问题选择委员会主席约瑟夫·迈尔斯博士根据 IMO 的评分规则进行评分。 该程序可以提出这种非显而易见的构造，这非常令人印象深刻，远远超出了我认为的最先进水平。 国际数学奥林匹克金牌得主、菲尔兹奖得主蒂莫西·高尔斯爵士教授 首先，问题被手动翻译成正式的数学语言，以便我们的系统理解。在正式比赛中，学生分两节提交答案，每节 4.5 小时。我们的系统在几分钟内解决了一个问题，而解决其他问题则需要三天时间。 AlphaProof 通过确定答案并证明其正确性，解决了两道代数题和一道数论题。其中包括比赛中最难的一道题，今年的 IMO 比赛中只有五名选手解决了这道题。AlphaGeometry 2 解决了几何问题，而两道组合问题仍未解决。 六道题目每道可得 7 分，总分最高为 42 分。我们的系统最终得分为 28 分，每道题目都获得满分 — 相当于银牌类别的最高分。今年，金牌门槛为 29 分，在正式比赛中，609 名参赛者中有 58 人达到了金牌门槛。 图表显示了我们的 AI 系统在 IMO 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 年所有 IMO 几何问题中的 83%，而其前身的解决率仅为 53%。在 IMO 2024 中，AlphaGeometry 2 在获得形式化后 19 秒内就解决了问题 4。 问题 4 的说明，要求证明 ∠KIL 与 ∠XPY 之和等于 180°。AlphaGeometry 2 建议构造 E ，即直线 BI 上的一个点，以便 ∠AEB = 90°。点 E 有助于确定 AB 的中点 L ，从而创建证明结论所需的多对相似三角形，例如 ABE ~ YBI 和 ALE ~ IPC 。 数学推理的新前沿 作为 IMO 工作的一部分，我们还试验了一种基于Gemini和我们最新研究的自然语言推理系统，以实现高级问题解决技能。该系统不需要将问题翻译成形式语言，并且可以与其他 AI 系统结合使用。我们还在今年的 IMO 问题上测试了这种方法，结果显示出巨大的潜力。 我们的团队正在继续探索多种用于推进数学推理的人工智能方法，并计划很快发布有关 AlphaProof 的更多技术细节。 我们很高兴看到未来数学家们能够利用人工智能工具探索假设，尝试大胆的新方法来解决长期存在的问题，并快速完成耗时的证明步骤——而像Gemini这样的人工智能系统在数学和更广泛的推理方面的能力将变得更强。
原文链接： https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
以下翻译来自谷歌
人工智能在解决国际数学奥林匹克问题上达到银牌标准
突破性模型 AlphaProof 和 AlphaGeometry 2 解决数学中的高级推理问题
具有高级数学推理能力的通用人工智能（ AGI ）有可能开辟科学技术的新领域。
我们在构建人工智能系统方面取得了巨大进步，该系统可以帮助数学家发现新见解、新算法和未解决问题。但由于推理能力和训练数据的限制，目前的人工智能系统仍然难以解决一般数学问题。
今天，我们推出了基于强化学习的新型形式数学推理系统 AlphaProof ，以及我们几何求解系统的改进版本 AlphaGeometry 2 。这两个系统共同解决了今年国际数学奥林匹克(IMO) 六道题目中的四道，首次在竞赛中取得与银牌得主同等的成绩。
突破性的人工智能性能解决复杂的数学问题
国际数学奥林匹克竞赛是历史最悠久、规模最大、最负盛名的青年数学竞赛，自 1959 年起每年举办。
每年，顶尖的大学前数学家们都要训练，有时要训练数千小时，以解决代数、组合学、几何学和数论领域的六道极其困难的难题。菲尔兹奖是数学家的最高荣誉之一，许多获奖者都曾代表他们的国家参加过国际数学奥林匹克比赛。
近年来，一年一度的国际数学奥林匹克竞赛也被广泛认为是机器学习领域的一大挑战，也是衡量人工智能系统高级数学推理能力的理想基准。
今年，我们将联合人工智能系统应用于 IMO 主办方提供的竞赛问题。我们的解决方案由著名数学家、IMO 金牌得主和菲尔兹奖得主蒂莫西·高尔斯爵士教授和两届 IMO 金牌得主、IMO 2024 问题选择委员会主席约瑟夫·迈尔斯博士根据 IMO 的评分规则进行评分。
国际数学奥林匹克金牌得主、菲尔兹奖得主蒂莫西·高尔斯爵士教授
首先，问题被手动翻译成正式的数学语言，以便我们的系统理解。在正式比赛中，学生分两节提交答案，每节 4.5 小时。我们的系统在几分钟内解决了一个问题，而解决其他问题则需要三天时间。
AlphaProof 通过确定答案并证明其正确性，解决了两道代数题和一道数论题。其中包括比赛中最难的一道题，今年的 IMO 比赛中只有五名选手解决了这道题。AlphaGeometry 2 解决了几何问题，而两道组合问题仍未解决。
六道题目每道可得 7 分，总分最高为 42 分。我们的系统最终得分为 28 分，每道题目都获得满分 — 相当于银牌类别的最高分。今年，金牌门槛为 29 分，在正式比赛中，609 名参赛者中有 58 人达到了金牌门槛。
图表显示了我们的 AI 系统在 IMO 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 年所有 IMO 几何问题中的 83%，而其前身的解决率仅为 53%。在 IMO 2024 中，AlphaGeometry 2 在获得形式化后 19 秒内就解决了问题 4。
问题 4 的说明，要求证明 ∠KIL 与 ∠XPY 之和等于 180°。AlphaGeometry 2 建议构造 E ，即直线 BI 上的一个点，以便 ∠AEB = 90°。点 E 有助于确定 AB 的中点 L ，从而创建证明结论所需的多对相似三角形，例如 ABE ~ YBI 和 ALE ~ IPC 。
数学推理的新前沿
作为 IMO 工作的一部分，我们还试验了一种基于Gemini和我们最新研究的自然语言推理系统，以实现高级问题解决技能。该系统不需要将问题翻译成形式语言，并且可以与其他 AI 系统结合使用。我们还在今年的 IMO 问题上测试了这种方法，结果显示出巨大的潜力。
我们的团队正在继续探索多种用于推进数学推理的人工智能方法，并计划很快发布有关 AlphaProof 的更多技术细节。
我们很高兴看到未来数学家们能够利用人工智能工具探索假设，尝试大胆的新方法来解决长期存在的问题，并快速完成耗时的证明步骤——而像Gemini这样的人工智能系统在数学和更广泛的推理方面的能力将变得更强。