谷歌DeepMind的目标是打造世界上最强大的AI数学家。
Perplexity AI的CEO大胆预测，如果DeepMind继续研究下去，也许可以创造出一个“AI陶哲轩”！
这个预测确实相当大胆。陶哲轩在IMO竞赛圈乃至整个数学界都是传奇般的存在，被誉为“天才少年”和“数学界莫扎特”。他首次参加IMO竞赛时只有10岁，是迄今为止最年轻的参赛者。
从10岁获得铜牌，到11岁获得银牌，再到12岁获得金牌，他一路高歌猛进，成为IMO历史上最年轻的金牌获得者。
AI大佬做出如此大胆的预测，并非空穴来风。DeepMind的AlphaProof和AlphaGeometry 2在今年的IMO竞赛中，与来自世界各地的优秀人类选手同台竞技，最终取得了银牌的好成绩，在6道题目中共同做对了4道，距离金牌仅差一分。
其中，AlphaGeometry 2更是展现出惊人的实力，仅用19秒就破解了一道几何题目。
这一消息在AI界和数学界引起了巨大反响，许多大佬纷纷发表了自己的思考和感悟。
数学大佬怎么看？
陶哲轩作为被“cue”的当事人，也发表了自己的看法。他并未关注“AI陶哲轩”的称号，而是延续了自己一贯的关注点，分析了AI和数学将如何共同发展。
陶哲轩首先肯定了DeepMind取得的成就，认为它突破了AI辅助/全自动化方法在基准挑战上的能力边界，再次颠覆了人们的预期。他指出，IMO级别的几何问题已成为专门AI工具的实际可解问题。目前看来，能够形式化并可以用强化学习过程找到形式化证明的IMO问题，至少在某种程度上都可以被AI攻克，尽管每个问题都需要相当程度的算力以及形式化过程中的协助。
他认为，这种方法的好处在于可以更容易地实现形式数学的自动化，从而有助于包含形式化成分的数学研究。特别是，如果创建一个包含形式化证明过程的数据库并公开共享，将成为非常有益的资源。
陶哲轩认为DeepMind这次的研发路径非常巧妙，它更多地基于强化学习，而非大语言模型，继承了AlphaGo的精神，并强调形式化方法。他指出，一旦原理被解释清楚，AI就不再被视为“类人智慧”的展现，但这依旧扩展了AI辅助工具的能力。
陶哲轩还提到了“AI效应”，即一旦AI项目取得了成功，相关任务就不再被视为AI领域的一部分。他认为，AlphaProof/AlphaGeometry 2与近期获得AIMO冠军的NuminaMath模型不能直接比较，因为后者是完全自动化的，资源效率高出几个数量级，并采用了完全不同的思路，即通过LLM生成Python代码对数字答案进行暴力破解。NuminaMath在数学解题的不同部分中尝试用AI协助或自动化，展示了挑战本身的多维性质。目前，NuminaMath模型已在HuggingFace上开源。
仓库地址：https://huggingface.co/AI-MO/NuminaMath-7B-TIR
CMU数学教授罗博深（Po-Shen Loh）也对AI在IMO上的表现感到震惊，他甚至表示“人类文明需要进入高度戒备状态”。他一直期待这种水平的AI出现，但认为至少还需要几年时间才能实现。罗博深对IMO竞赛有着深入的了解，他曾在1999年获得IMO银牌，并从2002年开始担任美国IMO国家队训练营的助理教练，长达21年。2014年，他正式担任总教练，并带领美国队在2015年、2016年、2018年和2019年获得冠军，让美国IMO国家队重回巅峰。罗博深对IMO的出题流程非常熟悉，他知道IMO专门选择非标准化问题，并避免任何类似题目。这种题目的创新性让很多人类学生感到难以上手，因为他们习惯于从例题中学习，记住解题步骤，并用来解决相似问题。本届IMO的6道题目远远超出了任何课程标准，需要找到解题路径，即使有一整年时间思考也可能拿不到任何分数。
因此，DeepMind模型在IMO上的胜利与GPT-4在标准化测试上通过“模式匹配”获得高分有着完全不同的意义。尽管AI花费的时间远远超过比赛规定，但实现软硬件加速只是时间问题，模型能够解决这些问题本身就是一个重大进步。
罗博深教授长期致力于数学教育，他认为AI的强大数学能力意味着人类需要大幅提升自身智慧，首先要关注其对就业动态的影响。他认为，AI出现之前，个别有非凡能力的人不会真正损害就业，因为这样的人终究是少数。即使这些天之骄子会占据一些职位，但余下的工作依旧很多。然而，一旦AI的能力超越人类，它就可以通过大规模复制夺走所有工作。这与之前的逻辑完全不同。AlphaProof/AlphaGeometry 2在IMO中的表现已经证明AI具备了发现新事物的能力，这是最有价值的技能之一，因此整个教育方法都需要快速变革。当前的教育结构很大程度上受到考试的影响，是为了测试学生在预定义标准上的熟练程度。但是，每个人都必须学会如何解决从未见过的新问题，否则就无法跟上AI的步伐。
此外，技术越强大，我们就越需要努力保持人类文明中的人性。这意味着，我们需要建立一个让人们共同合作、互相支持的社区，而不是在“丛林竞争”中互相争斗。分裂则亡。对于罗博深教授来说，这与构建人类的分析性才能密切相关，因为培养一个试图击败他人而非帮助他人的天才，很可能是有害的。
这些观点并非罗博深教授的“纸上谈兵”，他基于十多年的数学教育工作经验进行深入思考，并试图提出一些启发性的解决方案。
DeepMind的AI数学家
DeepMind伦敦总部的实验室有一个传统，在庆祝每次AI里程碑时，敲响大锣。2016年AlphaGo在围棋比赛中取得优异成绩时，锣声响起；2017年AlphaZero征服国际象棋时，锣声再次回荡。每次锣声响起，都代表着算法击败了人类冠军。AlphaProof和AlphaGeometry 2在IMO 2024夺得银牌的那天，伦敦总部再次敲响了铜锣。
这篇报道深入团队内部，让我们对这位AI数学家有了更深一层的了解。文章表示，AI越来越擅长数学，并且很快就会成为人类最值得合作的伙伴。DeepMind数学计划负责人之一Alex Davies表示，这是AI在数学推理方面取得的重大突破。
IMO 2024在伦敦以西约100英里的巴斯大学举行，被公认为是世界上“最聪明的数学天才”参加的顶级数学竞赛。来自108个国家的609名高中生参加了比赛，并获得了58枚金牌、123枚银牌和145枚铜牌。
谷歌AI在答题的过程中，解决了6个问题中的四个，总得分28分，与金牌仅差一分。对此，谷歌DeepMind研究副总裁Pushmeet Kohli在接受采访时表示，这并不完美，我们沒有解决所有问题。我们的目标是做到完美。
尽管如此，Kohli博士将这一结果描述为一种“相变”，即在数学中使用AI以及AI系统进行数学运算能力的一种革命性的变化。DeepMind实验室邀请两位独立专家来评判AI的表现，他们是剑桥大学数学家、菲尔兹奖得主Timothy Gowers和软件开发人员Joseph Myers，他们都曾是IMO竞赛获奖者，并对AI的表现表示印象深刻。
Gowers在过去25年一直对AI与数学的结合感兴趣，他认为“AI已经找到了解决问题的神奇钥匙”。
铜锣敲响
每年IMO，人类选手都要经过几个月的严格训练，去参加两场奥数考试（共9小时）。每天仅需做答三题，涉及了代数、组合学、几何和数论。与此同时，AI数学家也在伦敦实验室里埋头苦干。研究科学家David Silver说，“每次系统解决一个问题，我们就敲锣庆祝”。
IMO结果公布那天，中国队中的Haojia Shi是唯一一位获得满分（42分）的参赛者，6道题目分别拿了7分满分成绩。
总榜成绩中，美国队以192分获得第一名，中国以190分获得第二名。
谷歌AI成功破解了4道题——2道代数题、1道几何题和1道数论题，得分28分。它在另外两个组合学问题上失败了。与人类选手不同的是，AI答题完全不限时间。对于某些问题，AI需要长达三天的时间，而学生在每场考试中仅有4.5小时。
Silver博士解释道，“对于谷歌DeepMind团队来说，速度是整体成功的次要因素，因为这实际上只是取决于算力的投入”。他继续称，“我们能够达到这个阈值，能够解决这些问题，这代表了数学史上的一个重大变化。但也希望能成为一个转折点，让计算机从只能证明简单问题，到证明人类无法证明的问题”。
两大团队，两个AI数学家
几年来，将AI应用于数学一直是DeepMind的使命之一，而且通常是与世界级的研究数学家合作。Davies博士表示，数学需要抽象、精确和创造性推理的有趣结合。他指出，部分原因是这种能力组合，使数学成为达到所谓的AGI这一最终目标的良好试金石，这也是OpenAI、Meta AI、Xai等公司一直在追逐的目标。因此，奥林匹克数学题已成为公认的一个基准。
今年年初，谷歌DeepMind首次发布AlphaGeometry，解决了奥林匹克抽样的几何问题，水平相当于人类金牌获奖者。
论文地址：https://www.nature.com/articles/s41586-023-06747-5
首席研究员Thang Luong在电子邮件中表示，AlphaGeometry 2在解决IMO问题上已经超过了金牌得主。
借着这股势头，谷歌DeepMind为这项挑战组建了两个团队：一个由伦敦的研究工程师Thomas HuBERT领导，另一个团队由位于美国Mountain View实验室的Luong博士和Quoc Le领导，每个团队约有20名研究人员。
Luong博士领导的团队名为“超人类推理团队”，目前为止招募了十几名IMO奖牌获得者。他自豪地表示，这是目前为止谷歌内部“IMO密度最高”的团队。
大约20年前，我全身心投入奥数竞赛，在全国获得银牌（当时排名第8），但我没能进入2005年的IMO比赛…..，时光荏苒，我非常高兴谷歌最新的AI系统（AlphaGeometry2+AlphaProof）帮我实现了“赢得”IMO奖牌的梦想！
时隔半年，谷歌推出了迭代后的AlphaGeometry 2，仅用19秒就解决了IMO 2024的几何问题。另一波在伦敦总部的团队，由Hubert领队，开发了全新模型AlphaProof。它具有可比性，更加通用，目标是为了解决更广泛的数学问题。
背后的算法揭秘
简言之，AlphaGeometry和AlphaProof利用了多种不同的AI技术。
非形式推理系统
AlphaProof是用自然语言表达的非形式推理系统（informal reasoning system）。它基于谷歌Gemini打造，使用已公开的问题、证明等英文语料库作为训练数据。非形式系统擅长识别模式，以及提出下一步建议。而且它富有创造性，以一种自然语言可以理解的方式谈论想法。当然，LLM倾向于编造内容，这对诗歌可能行得通，但对数学肯定不行。在数学这种情况下，大模型似乎表现出了克制。但这并不是说，它完全免疫于“幻觉”，但频率有所降低。
形式推理系统
AlphaGeometry是基于逻辑并用代码表达的形式推理系统。它使用了名为Lean的定理证明器和证明助手软件。该软件可以确保，如果AI认为证明是正确的，那么它确实是正确的。Hubert表示，“我们可以准确地检查证明是否正确，因为每一步都保证在逻辑上是合理的”。
另一个关键组件是AlphaGo和AlphaZero谱系中的强化学习算法。谷歌DeepMind负责强化学习的副总裁Silver博士说，“AI可以自主学习，无限扩展”。由于RL算法不需要老师，所以它可以不断地学习，一直学习，直到最终它能够解决人类可以解决的最困难的问题。这也是AlphaZero所经历的现实，从0开始学习，仅通过玩游戏，在不到一天时间内，就能重新发现国际象棋中的所有知识。在大约一周的时间，它便发现了围棋的所有知识。所以我们想，把这个AI能力应用到数学中。
数学家，会被AI取代吗？
菲尔兹奖得主Gowers并不担心AI数学家带来的长期后果。我们无法预测这种情况，如果计算机在数学家目前做的所有事情上都变得更好、更快，那么数学家就基本上没什么可做的了。不过，
