谷歌 DeepMind 在所有方面都击败了人类之后，从 玩转到策略棋盘游戏,
它现在声称在解决数学问题方面即将击败世界上最好的学生。

总部位于伦敦的 机器学习 该公司于 7 月 25 日宣布，其人工智能 (AI) 系统解决了 2024 年英国巴斯国际数学奥林匹克 (IMO) 学生提出的六道题中的四道。该人工智能提供了严格的、逐步的证明，并由两位顶级数学家评估，并获得了 28/42 的分数——距离金牌仅差一分。

“这显然是一个非常重大的进步，”来自英国剑桥的数学家约瑟夫·迈尔斯 (Joseph Myers) 说道，他与菲尔兹奖得主蒂姆·高尔斯 (Tim Gowers) 一起审查了解决方案，并帮助选择了今年 IMO 的原始问题。

DeepMind 和其他公司正在竞相最终为机器提供重要的证据 解决数学研究问题 。该公司表示，IMO（世界领先的年轻数学家竞赛）上提出的问题已成为实现这一目标的基准，并被认为是机器学习的“巨大挑战”。

DeepMind 人工智能科学副总裁 Pushmeet Kohli 在新闻发布会上表示：“这是人工智能系统首次实现奖牌级性能。” “这是建立先进证据调查人员的一个重要里程碑，”科利说。

扩大

就在几个月前，一月份，DeepMind 系统 AlphaGeometry 奖章级成就 在解决一类 IMO 问题（即欧几里得几何问题）中取得的成就。第一个在整体测试中表现出金牌水平的人工智能——包括代数、组合学和数论问题，通常被认为比几何更具挑战性——将有资格获得 500 万美元的奖金，即人工智能数学奥林匹克奖（AIMO）。 （该奖项有严格的标准，例如公开源代码和使用有限的计算能力，这意味着 DeepMind 目前的努力不符合资格。）

在他们的最新尝试中，研究人员使用 AlphaGeometry2 在 20 秒内解决了几何问题； DeepMind 计算机专家 Thang Luong 表示，人工智能是其记录系统的改进版，速度更快。

对于其他类型的问题，团队开发了一个名为 AlphaProof 的全新系统。 AlphaProof 解决了比赛中的两道代数问题和一道数论问题，历时三天。 （实际IMO的参与者有两节课，每节课4.5小时。）它无法解决组合数学中的两个问题，组合数学是数学的另一个领域。


Nahaufnahme einer Goldmedaille, gewonnen bei der 63. Internationalen Mathematik-Olympiade von einem rumänischen Teilnehmer.

研究人员在使用语言模型（为 ChatGPT 等聊天机器人提供支持的系统）回答数学问题时得到了不同的结果。有时模型给出了正确的答案，但无法合理地解释其推理，有时 他们胡言乱语 。

就在上周，来自软件公司 Numina 和 HuggingFace 的研究团队使用语言模型赢得了基于 IMO 问题简化版本的 AMIO 中级“进步奖”。这些公司已将整个系统开源并可供其他研究人员下载。但获奖者表示自然，仅靠语言模型可能不足以解决更困难的问题。

仅班级

AlphaProof 将语言模型与强化学习技术相结合，该技术使用“AlphaZero”引擎，该公司已成功用于围棋等攻击游戏和一些游戏。 具体的数学问题 用过的。在强化学习中，神经网络通过反复试验来学习。当可以使用客观标准评估他的答案时，这种方法很有效。为此，AlphaProof 接受了使用名为 Lean 的正式语言读写证明的训练，该语言用于数学家流行的同名“证明助手”软件包中。为此，AlphaProof 通过在 Lean 包中运行来测试其输出是否正确，这有助于填写代码中的一些步骤。

训练语言模型需要大量数据，但精益中几乎没有可用的数学证据。 DeepMind 机器学习研究员、AlphaProof 开发共同领导者托马斯·休伯特 (Thomas Hubert) 表示，为了克服这个问题，该团队开发了一个额外的网络，试图将现有的一百万个问题记录转化为 Lean，该记录是用自然语言编写的，但没有人工编写的解决方案。 “我们的方法是，即使我们最初没有接受人类编写的证明训练，我们也能学会证明吗？” （该公司对围棋采取了类似的方法，其人工智能通过与自己对弈来学习下棋，而不是学习人类的方式。）

魔术键

许多精益翻译没有意义，但足够好，足以让 AlphaProof 达到可以开始强化学习周期的程度。高尔斯在新闻发布会上表示，结果比预期要好得多。在巴黎法兰西学院工作的高尔斯说：“IMO 的许多问题都具有这种神奇的钥匙属性。这个问题一开始看起来很困难，直到你找到一把可以打开它的神奇钥匙。”

在某些情况下，AlphaProof 似乎能够通过从无限大的可能解决方案中提供一个正确的步骤来提供额外的创造力。但高尔斯补充说，还需要进一步分析来确定答案是否没有看上去那么令人惊讶。在令人惊讶的言论之后出现了类似的言论 “37号列车” ，他的 DeepMinds AlphaGo 机器人 2016 年著名战胜世界最佳人类围棋棋手 制造——人工智能的转折点。

迈尔斯在新闻发布会上表示，这些技术是否可以完善以应用于数学研究水平还有待观察。 “它可以扩展到可能没有数百万个问题训练的其他类型的数学吗？”

DeepMind 计算机专家、2010 年代中期开发 AlphaGo 的首席研究员 David Silver 表示：“我们现在不仅可以证明开放性研究问题，还可以证明对世界上最优秀的年轻数学家来说非常具有挑战性的问题。”