刚刚，谷歌DeepMind最新数学模型在IMO 奥数竞赛中斩获银牌！它不仅以满分成绩完成了6道题中的4道，距离金牌仅差1分，而且在第4题上仅用了19秒便解出，令评委震惊不已。
AI 系统成功完成了6道题中的4道，并且每道题都获得了满分，获得了银牌的最高分——28分。
正式比赛中，人类选手需要分两次提交答案，每次限时4.5个小时。
有趣的是，AI 只用了几分钟就解出了一道题，但剩下的问题却花了整整三天时间，可谓是严重超时了。
这次成功背后的功臣是两款AI 系统——AlphaProof 和 AlphaGeometry 2。
值得注意的是：2024 年IMO 竞赛题目并没有包含在两个AI 系统的训练数据中。
其实，早在今年1月份，谷歌DeepMind 的第一代 AlphaGeometry 就登上了Nature 杂志。当时，它成功解出了IMO 30道几何题中的25道。
AlphaGeometry 2 的创始人之一 Scott Wu（IOI 三枚金牌得主）感叹道：「当我还是个孩子的时候，奥林匹克竞赛就是我的全部。然而，仅仅10年后，它们就被AI 解开了，这真是不可思议！」
今年的IMO 竞赛共有六道赛题，涉及代数、组合学、几何和数论。AI 成功解出了其中的四道，展现了令人惊叹的数学能力。
众所周知，过去的AI 在解决数学问题方面一直表现不佳，主要原因在于推理能力和训练数据的限制。
而今天登场的两位AI 选手突破了这一限制。它们分别是——
– AlphaProof，基于强化学习的形式数学推理新系统
– AlphaGeometry 2，第二代几何解题系统
这两位AI 给出的答案，由著名数学家 Timothy Gowers 教授（IMO 金牌得主和菲尔兹奖得主）和 Joseph Myers 博士（两次IMO 金牌得主、IMO 2024 问题选择委员会主席）根据规则进行评分。
最终，AlphaProof 正确解出了两个代数题和一个数论题，其中一个最难的问题，在今年IMO 中只有5名人类参赛者解出；AlphaGeometry 2 则解出了一道几何题。
Timothy Gowers 教授在评分过程中，也被深深地震撼了——
程序能够提出这样一个非显而易见的解法，实在令人印象深刻，远超出我对当前技术水平的预期。
AlphaProof 能够在形式化语言 Lean 中证明数学命题。
它结合了预训练的大语言模型和 AlphaZero 强化学习算法，后者曾自学掌握了国际象棋、将棋和围棋。
形式化语言的一个关键优势，就是可以对涉及数学推理的证明进行形式化验证。然而，由于人类编写的相关数据量非常有限，它们在机器学习中的应用一直受到限制。
相比之下，基于自然语言的方法尽管可以访问大量数据，但却可能产生似是而非、但不正确的中间推理步骤和解决方案。
为了克服这一问题，谷歌DeepMind 研究人员通过微调 Gemini 模型，将自然语言问题陈述自动翻译成形式化陈述，建立了一个包含不同难度的形式化问题的大型库，从而在两个互补领域之间架起桥梁。
解题时，AlphaProof 会生成候选的解决方案，并通过在 Lean 中搜索可能的证明步骤，来证明或反驳它们。
每个被找到并验证的证明，都被用于强化AlphaProof 的语言模型，使其能够在后续解决更难的问题。
为了训练AlphaProof，研究人员证明或反驳了几百万个问题，涵盖了从比赛前几周到比赛期间广泛的难度和数学主题领域。
在比赛期间，他们还应用了训练循环，通过强化自生成的比赛问题变体的证明，直到找到完整的解决方案。
AlphaProof 强化学习训练循环的流程信息图：大约一百万个非正式数学问题由形式化网络翻译成形式化数学语言；接着，求解网络通过搜索这些问题的证明或反驳，并利用AlphaZero 算法逐步训练自己，以解决更具挑战性的问题
AlphaGeometry 的升级版AlphaGeometry 2，是一个神经符号混合系统，基于Gemini 的语言模型从头开始训练。
基于比上一代多了一个数量级的合成数据，它能够解决难度更高的几何问题，包括涉及物体运动、角度、比例和距离方程等等。
此外，它还采用了比前一代快两个数量级的符号引擎。当遇到新问题时，它会用一种新颖的知识共享机制，使不同搜索树的高级组合能够解决更复杂的问题。
在今年参加IMO 之前，AlphaGeometry 2 已战绩累累：它能解出过去25 年IMO 几何赛题中的83%，而第一代只能解出53%。
在这届IMO 中，AlphaGeometry 2 的神勇速度更是震惊了众人——在接收到形式化问题的19秒内，它就把问题4 做出来了！
问题4 要求证明∠KIL 和∠XPY 之和等于180°。AlphaGeometry 2 建议在BI 线上构造一个点E，使得∠AEB=90°。点E 有助于确定AB 的中点L，形成了许多类似的三角形对，如ABE ~ YBI 和 ALE ~ IPC，从而证明结论
值得一提的是，这些问题首先会被人工翻译成正式的数学语言，然后才会投给AI。
P1
一般来说，每届IMO 试题中第一题（P1）相对来说，是比较容易的。
网友表示，「P1 仅需要高中数学知识就够了，人类选手通常会在60分钟内完成」。
IMO 2024 第一题主要考察了实数α 的性质，并要求找出满足特定条件的实数α。
AI 给出了正确答案——α 是偶整数。那么，它具体是如何解答的呢？
解题第一步，AI 先给出了一个定理，左右两边集合相等。
左边集合表示，所有满足条件的实数α，对于任何正整数n，n 能整除从1 到n 的⌊i*α⌋；右边集合表示，存在一个整数k，k 是偶数，实数α 等于k。
然后，再证明左边集合，是右边集合的子集（困难方向）。
直到代码结束时，AI 提出了一个关键等式⌊(n+1)*α⌋ = ⌊α⌋+2n(l-⌊α⌋)，使用等式来证明α 必须是偶数。
最后，DeepMind 总结了AI 在解题过程中，依赖的三个公理：propext、Classical.choice，以及Quot.sound。
以下是P1 的完整解题过程：https://storage.Googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P1/index.html
免责声明：本网站内容主要来自原创、合作伙伴供稿和第三方自媒体作者投稿，凡在本网站出现的信息，均仅供参考。本网站将尽力确保所提供信息的准确性及可靠性，但不保证有关资料的准确性及可靠性，读者在使用前请进一步核实，并对任何自主决定的行为负责。本网站对有关资料所引致的错误、不确或遗漏，概不负任何法律责任。任何单位或个人认为本网站中的网页或链接内容可能涉嫌侵犯其知识产权或存在不实内容时，可联系本站进行审核删除。
