人工智能的发展正在不断突破人类的想象！！！
第65届国际奥林匹克数学赛（IMO）刚刚在英国巴斯落下帷幕，但事情还远远没有结束。
2024IMO美国队夺冠
在这一次 “全世界最聪明的人类”的集会背后，还有一股神秘力量的参与——人工智能！
7月16-17日，来自世界各地的人类选手们正在现场浑然未觉的投入比赛解题中，而在120英里以外英国伦敦的实验室里，谷歌DeepMind团队的科学家们正猫在一起，静静等待着实验室新开发的人工智能的对于IMO问题给出的解答。
在几个小时后，这两个最新的超级数学模型， AlphaProof 和 AlphaGeometry 2，也展现了令研究人员喜笑颜开，令旁观者瞠目结舌的炸裂表现——它们成功解出了4道IMO的超高难度题目！
让我们先来看比赛成绩。
IMO共6道题目，每道题目满分7分。
今年IMO金牌的分数线是29分。银牌的分数线是22分。
而AlphaProof 和 AlphaGeometry 2解出的四道题目获得28分。
达到了银牌中的高阶银牌（High Silver）水平！已经无限逼近金牌！！！
人工智能的比赛成绩接近IMO金牌选手
图源：谷歌DeepMind AlphaProof 和AlphaGeometry 项目组
于2024年7月25日发表的
《AI achieves silver-medal standard solving International Mathematical Olympiad problems》
（《人工智能在解决国际数学奥林匹克问题上达到银牌标准》）一文
01、AlphaProof
AlphaProof 是一个通过 Lean 语言来证明数学命题的模型。（*Lean 是一种用于形式化数学和计算机科学的证明辅助和编程语言。它由 Microsoft Research 开发，旨在帮助用户构建和验证数学证明）。
AlphaProof结合了预训练语言模型（pre-trained language model）和AlphaZero强化学习算法（reinforcement learning algorithm），后者就是那个大家熟知的，那个征服了国际象棋的模型（AlphaGo超进化版）。
利用形式化数学语言来进行数学证明的优势在于，尽管相比自然语言可以访问的数据量级更少，但是却可以确保数学证明的每一步推理都是正确的，并且可以被计算机程序验证。（形式化数学是使用精确的符号和严格的逻辑规则来定义和证明数学概念、定理和推理过程的方法。）
谷歌DeepMind研究人员为了弥合程序语言和自然语言在数据量级之间的鸿沟，通过微调 Gemini 模型，成功地将自然语言问题转换为形式化问题，创建了一个包含各种难度问题的大型问题库。
在实际应用中，AlphaProof 能够生成候选解决方案，并通过不断搜索库中的证明步骤来验证或驳斥这些候选答案。每当一个证明被证实，都会进一步强化 AlphaProof 模型，提高其解决更具挑战性问题的能力。
在今年IMO比赛前的几周内，谷歌的科学家们通过数百万道题目的证明和反证来训练 AlphaProof，使其在竞赛中表现优异。
02、AlphaGeometry
AlphaGeometry 2 仅用19秒，就解出了今年IMO第四题，它是谷歌几何求解系统的显著升级版，毫无疑问，它比AlphaGeometry 1速度更快，解决问题的效率更高。
它基于 Gemini 语言模型，使用了比前版本多一个数量级的合成数据进行训练。这使得AlphaGeometry 2 能够解决更加复杂的几何问题，包括涉及物体运动、角度、比例和距离方程的问题。
新的符号引擎使 AlphaGeometry 2 的速度比前版本快两个数量级。在面对新问题时，它采用了一种全新的知识共享机制，使不同搜索树的高级组合能够应对更复杂的挑战。
在今年的比赛之前，AlphaGeometry 2 已经能够解决过去25年间IMO所有几何问题中的83%，而其上一代模型的解决率为53%。在2024年IMO竞赛中，AlphaGeometry 2 在接收到问题形式化表述后的19秒内解决了第4题，更加展示了其强大的问题解决能力。
03、AI迎战国际数学奥林匹克的挑战
如果说在今年1月，人们已经对《纽约时报》所报道的能解出IMO几何题的AlphaGeometry感到惊异，那么这次联手解出四道IMO题目的AlphaProof和AlphaGeometry 2 模型则足以带来颠覆人类认知的震撼。两大模型可谓是目前AI届横空出世的，最不可思议的存在。
在《纽约时报》发表文章介绍AlphaGeometry时，曾有人质疑道：“几何是最具结构化的奥数学科，AI能解出来不足为奇。”
《纽约时报》1月发表文章介绍AlphaGeometry
理论上来说，几何类题目涵盖的定理内容确实相对有限，让AI足以通过题库搜索调用定理来解题。
但是如今，AI成功解出的另外3道IMO非几何类题目，真正证明了其势不可挡的实力。
与几何问题不同，这三道题目并没有证明空间可以供AI进行简单搜索。举例来说，假设由你来为IMO试卷打分，即使解题步骤是用你不懂的语言书写的，你仍可以通过各种代表不同几何概念的符号等信息来理解选手写的几何证明。但当你看其他类型的数学问题的答卷时，你所需要评判的内容则远比辨别字母符号更多。
04、AI甚至超越前美国奥数队总教练罗博深，他怎么说？
前美国奥数队总教练罗博深教授曾在1999年代表美国队参加IMO，曾获得“低阶银牌”（Low Silver）成绩。
罗博深高中时期夺得IMO银牌，Radu Gologan为他颁奖
用他的话来说：“现在，AI 达到了IMO高阶银牌水平，这已经超越了我当年的成绩。在亲自尝试解答这些题目后，我必须承认解出其中一些题目花了我好几个小时。一些非几何题目非常难，几乎让人无从下手。当我阅读IMO竞赛题目时，我对一些奥数领域的同事说，这次考试对 AI 来说会很难，因为只有一道几何题，其他题目非常打破常规。然而，让我出乎意料的是，AI竟然做到了。这是非常伟大的进步。”
罗教授说，“有些人可能会抱怨 ‘比赛不公’，因为AI 有超过 9 小时的时间来解决这些问题，并在计算过程中使用了大量资源。然而，从计算机工程的历史来看，解题耗时长的情况，迟早都会得到解决。
很巧，我昨天刚在布莱切利庄园主持了 IMO 校友聚会，我们参观了看到二战期间使用的计算机，它们非常庞大，一台计算机的大小相当于一整个房间，而且耗能巨大，还几乎没有什么计算能力。然而仅仅过去了数十年，智能手机已经能够让我们在股掌之间，数秒之内，轻轻松松获取自己需要的信息。”
05、AI征服IMO，教育行业将发生哪些变革？
IMO是全球最负盛名的数学竞赛，自1959年起每年举办，吸引了全世界顶尖的年轻数学家。参赛者们需要经过数千小时的训练，解决代数、组合学、几何学和数论领域的极其困难的六道题目。
许多菲尔兹奖得主都曾在年轻时参加过IMO，这一竞赛也成为衡量AI系统高级数学推理能力的理想化基准。
由于数学竞赛天生具备的选拔性，许多人也因此不自觉的加入了“内卷”之中。
从追求AMC 8满分，变成追求4年级就拿到AMC 8满分；从努力quilify for AIME，变成追求入选AIME很多次。也因此，很多教培机构应运而生，通过给学生灌输解题技巧来帮助学生迅速获取“一次性”的高分。
然而，数学竞赛真正的意义到底是什么？在罗教授看来，如果你仅仅追求的一个阶段性的“解”，无论是在某个竞赛取得高分，或是进入顶尖私立高中，或者是爬藤，都可能会让你忽视这一切真正的价值和乐趣。
数学的最本质的意义是思考和逻辑，参与竞赛，一方面是让每个孩子能接触更复杂，更有趣，更挑战思维能力的数学题目，另一方面，则是培养孩子思考和解决问题的勇气，面对新的问题勇于尝试而非胆怯止步，并从中得到真正的成就感和满足感，这样的能力才是真正长远有益于学生的。
在罗教授看来，学生应该通过思考和尝试，探索问题的解决方法，而不是通过重复性训练套用已有的答题技巧。如果一个孩子参与数学竞赛只是为了熟悉题目和技巧，以便在比赛中打败其他人，从而获得更高的排名以证明自己的能力，那这就只是无意义的内卷。
这一次AlphaProof和AlphaGeometry 2的出现，也让一直深耕数学教育行业的罗教授开始思考，奥数考试系统化培训是否还有其价值。
在能够解决IMO级别问题的AI出现之后，通过训练达到的同样能力的人，是否还会一样会在未来受到大企业的青睐？如果计算机能够比人更快地解决题目，我们的优势何在？未来的科学研究结构将发生怎样的巨大变化？
罗教授认为，极强的学术技能将不再是一人独有的硬核技术。而拥有能够认识未来世界的全局的洞察力和应变力将变得至关重要。学会发现问题提出问题，学会整合和利用资源，理解那些在完成目标的过程中遇到的一个个小问题，才是一个人能够有策略地解决任何难题的关键。
按照目前的发展趋势，人类无法在速度和准确性上击败计算机，但更加迫在眉睫的是，我们需要找到属于自己的那条，旁人和人工智都能未曾踏入的河流。
06、孩子的未来将何去何从？
罗教授说：“随着人工智能变得越来越强大，大规模提升人类智能变得越来越重要。许多人可能一开始还没有意识到这一点，但正在真实发生的是，人工智能已经很大程度上影响了人们的就业选择。
过去，一个IMO金牌选手这样能力卓群的人的存在，可能并不会真正影响大多数人就业状况——因为我们都知道，这样的人已经是金字塔顶端的凤毛麟角。然而，一旦任何AI在某项工作上达到了比人类更高的能力，它便可以大规模复制并占据所有相关工作岗位。
现在，AI已经能够解决IMO问题，这意味着它们已经学会了解决没有见过的新问题，这几乎是人类最有价值的技能之一，因此，现有的教育方法需要快速改变。不管人们是否愿意承认，我们的教育结构目前深受标准化考试影响，学生仍然在“被迫”追求解题的熟练程度。但现在，每个人都需要学习如何解决他们以前从未见过的问题，以跟上AI的发展。
此外，技术越强大，我们就越需要努力保护人类文明和人性的光辉。我们需要建立一个人们愿意共同友好合作，相互支持的，让人类感到安全和进步的社群，而不是成为一个个为了竞争在内卷中彼此争斗打压的个体。分裂则衰。对我来说，这与建立人类智能密切相关，如果我们培养一个寻求打败他人的“人才”而不是帮助他人的人才可能是有害的。”
【竞赛报名/项目咨询请加微信：mollywei007】
