继在围棋和战略棋盘游戏中战胜人类顶尖高手后，谷歌“深度思维”公司的人工智能 (AI) 系统在 2024 年英国巴斯举办的国际数学奥林匹克竞赛 (IMO) 中，仅以一分之差错失金牌，获得了银牌。这是 AI 选手首次登上 IMO 领奖台。
英国《自然》杂志网站在 7 月 27 日的报道中指出，“深度思维”正在与其他公司竞争解决数学领域的难题。近年来，IMO 被广泛认为是对机器学习的挑战，也是衡量 AI 系统高级数学推理能力的理想基准。AI 系统在今年 IMO 中的表现出色，标志着它即将取得另一项突破：在解决数学难题方面击败世界上最优秀的学生。
首次登上领奖台
“深度思维”公司训练了一个专门用于解答数学奥赛试题的 AI 系统，成功解答了 6 道竞赛题中的 4 道，获得了 28 分（满分 42 分），达到了本次比赛银牌获得者的水平。
该系统包括解答数学推理问题的模型 AlphaProof 和解答几何问题的模型 AlphaGeometry 的升级版 AlphaGeometry 2。其中，AlphaGeometry 2 解决了一个几何问题，而 AlphaProof 则解答了两个代数问题和一个数论问题。
今年 1 月份，AlphaGeometry 在解决欧几里得几何问题上，已经展现出奖牌级选手的水平。在今年的 IMO 比赛前，AlphaGeometry 2 已经能够解决过去 25 年中 83% 的 IMO 几何问题，而它的“前身”仅能解决 53%。
“深度思维”公司 AI 科学副总裁普什米特·科利指出，这是 AI 系统首次达到获得 IMO 奖牌级别的性能。IMO 主席格雷戈尔·多利纳尔也表示，AI 最终将能比人类更好地解决大多数数学问题，其进步速度令人惊叹。
几乎在同一时间，软件公司 Numina 的科学家使用语言模型赢得了 AI 数学奥林匹克奖 (AIMO) 的首个“进步奖”。
但 Numina 团队在获奖后表示，要解决更难的数学问题，仅靠语言模型可能还不够。
与自己对抗
AlphaProof 是一个自学习系统，其核心创新在于将预训练语言模型与 AlphaZero 强化学习算法的策略相结合。强化学习是机器学习领域中一种重要的学习范式，系统可以通过多次尝试找到自己的解题方法。
这种方法需要用 AI 可以理解和验证的语言编写大量问题，而大多数 IMO 问题都是用英语编写的。为了解决这个问题，“深度思维”团队的托马斯·赫伯特及其同事使用了谷歌的大型语言模型 Gemini，将这些问题翻译成一种名为 Lean 的编程语言，以便 AI 进行学习。
AlphaProof 使用经过微调的 Gemini 模型，自动将数学问题转换为 Lean 语言，从而创建了一个涵盖不同难度级别的大型问题库。在强化学习阶段，系统每验证一个证明，就用它来强化 AlphaProof 的语言模型，提高其解决后续更具挑战性问题的能力。
赫伯特表示，在挑战围棋游戏时，他们也采用了类似的方法：AI 通过与自己对抗，来学习如何更好地玩游戏。结果表明，在某些情况下，AlphaProof 能够在无限的可能性中迈出正确的一步，展现出“灵光一闪”的能力。
仍有改进空间
尽管 AlphaProof 的表现令人印象深刻，但其速度相对较慢，解决 3 个问题耗费了 3 天时间，而人类参赛者仅需 4 个半小时。此外，它也未能回答两个与组合数学有关的问题。
英国数学家约瑟夫·迈尔斯审查了 AI 在本次 IMO 比赛中给出的答案。他指出，AlphaProof 采用的这些技术能否得到完善还有待观察。
英国伦敦数学科学研究所的何杨辉称，AlphaProof 这样的系统对于帮助数学家证明问题非常有用，但它无法帮助研究人员确定需要解决和研究的问题。
“深度思维”团队表示，他们正在继续探索多种用于推进数学推理的 AI 方法。未来，数学研究人员将与 AI 合作验证假设，尝试新方法来解决长期未解决的数学难题。他们也希望 AlphaProof 能够通过减少错误响应，帮助改进谷歌的大型语言模型。
免责声明：本网站内容主要来自原创、合作伙伴供稿和第三方自媒体作者投稿，凡在本网站出现的信息，均仅供参考。本网站将尽力确保所提供信息的准确性及可靠性，但不保证有关资料的准确性及可靠性，读者在使用前请进一步核实，并对任何自主决定的行为负责。本网站对有关资料所引致的错误、不确或遗漏，概不负任何法律责任。任何单位或个人认为本网站中的网页或链接内容可能涉嫌侵犯其知识产权或存在不实内容时，可联系本站进行审核删除。
