编辑:编辑部
谷歌DeepMind奥数夺金了,得到IMO官方认证!新模型Gemini Deep Think仅用自然语言,在4.5小时攻克了5题,拿下35分。这次,具体解题过程也一并公开了。
今天,谷歌DeepMind正式官宣拿下IMO金牌!
他们凭借Gemini Deep Think(高阶版),一个通用模型,成功破解前5题,斩获35分(满分42分)。
而且, AI在极限4.5小时之内,就达到了IMO金牌标准。
最最重要的是,Gemini仅用纯自然语言——英语完成了解题。
与OpenAI不同的是,这一结果得到了IMO组委会官方认证。
Demis Hassabis连发两弹,一再强调「谷歌模型是首个获得官方金牌级别认可的AI系统」。
谷歌DeepMind,正式摘金
作为数学界的奥林匹克,IMO自1959年以来每年举办一次,每年吸引了全球各界优秀的学生参与。
参赛者需在4.5小时内解决6道极具深度的数学问题,涵盖代数、几何、组合数学和数论。
而且只有排名前8%的选手才能摘得金牌,象征着无上的学术荣耀。
近年来,IMO逐渐成为AI能力的试炼场。数学问题不仅需要逻辑推理,还考验创造性思维和严谨性,这对AI系统提出了极高要求。
2024年,AlphaProof和AlphaGeometry 2破解了6题中的4题,获得28分,达到了银牌水平。
这一突破利用专业的「形式语言」,表明AI开始接近顶尖人类的数学推理能力。
今天,Gemini Deep Think再创里程碑,完美破解5道题,跻身金牌行列。
那么,这款模型是如何做到的呢?
我们在此确认,谷歌DeepMind已经达成了一个万众瞩目的里程碑,在满分42分的竞赛中取得了35分的成绩——这足以摘得金牌
他们的解法在诸多方面都堪称惊艳。IMO的评委认为,这些解法思路清晰、表述精确,且大部分内容都简单易懂。
——IMO主席Gregor Dolinar教授
自然语言解题,端到端推理
AlphaProof和AlphaGeometry 2解决IMO难题前,需要专家将问题翻译为「形式语言」,如Lean。
而且,证明过程也是如此,且需要两到三天的计算时间。
今年,Gemini Deep Think完全以自然语言端到端运行,直接从官方问题描述中生成严谨的数学证明,并在4.5小时的比赛时间限制内完成。
借用Karpathy经典语录,「英语是热门的编程语言」。如今看来,确实如此。
Deep Think模式
之所以能够取得金牌,团队使用了Gemini Deep Think的高级版本——一种针对复杂问题的增强推理模式。
并且,结合并行思考技术,允许模型同时探索多种解题路径,最终整合出最优答案。
这种多线程推理方式,突破了传统单一线性思考的局限。
为了充分发挥Deep Think的推理能力,谷歌还对Gemini进行了新颖的强化学习训练,让其利用更多多步推理、问题解决和定理证明数据。
此外,谷歌研究团队还通过以下方式,进一步升级了Gemini版本:
更多思考时间
获取过往问题的一系列高质量解决方案集
提供解决IMO问题的通用提示与技巧
这种「训练+知识库+策略」的组合,让Gemini在IMO的舞台上大放异彩。
值得一提的是,接下来,谷歌将向一部分数学家等测试者提供这个版本的Deep Think模型,随后向Google AI Ultra订阅者推出。
解题过程
那就让我们来看看,这次谷歌Gemini Deep Think具体的解题过程吧。
官方报告:https://storage.googleapis.com/deepmind-media/gemini/IMO_2025.pdf
对于第一题这道解析几何题,模型的解法是设n>3是一个给定的整数。
证明思路是将问题简化到n=k且所有直线必须是阳光线的这一特定情况。具体来说,设C(k)表示「P可被k条不同阳光线覆盖」,定义P_0=ø。
然后模型设定了一个引理:在集合L中,所有N_v竖直直线必须是{x=1,2,...,N_v},所有N_H水平线必须是{y=1,2,...,N_H},所有N_D对角线必须是形如x+y=s的直线,s的取值范围为n+2−N_D,...,n+1。
然后,模型对这个引理进行了证明。
接下来,模型证明了定理1:当n≥3且0≤k≤n时,若存在一个由n条不同的直线组成的集合,刚好覆盖点集P_n,且其中恰好有k条阳光线,那么充要条件便是命题C(k)为真。
接下来,模型对核心问题C(k)展开了分析:对于哪些k>0,点集P_k可以恰好被k条阳光线覆盖。
最终,模型成功证明了C(k)成立的充要条件是k∈{0,1,3},由此证明了唯一可能的阳光线数量为:0、1或3条。
对于第二题这道平面几何题,模型把证明过程分成了五步。
步骤1:确定点P是△AMN的旁心。
步骤2: 求∠EBF。
步骤3: 引入辅助点V及其性质。
步骤4: 点V落在外接圆Σ上。
步骤5: 垂心H与切线条件。
最终,模型证明了直线VH是圆Σ在点V处的切线,由此证毕。
第三题是一道函数题。
在解题过程中,模型将关键步骤分为三步。
首先,是确定Bonza函数的性质与分类。
第二步和第三步中,模型分别完成了上界证明c≤4,以及下界证明c≥4。
最终结论可得:满足条件的最小实数常数c为c=4。
第四题是一道数论题,前提给出了一个真因数的定义,对于一个正整数N,除了N本身以外的正整数因数,都叫作N的真因数。
数列中,每一个数a_n都是正整数,且都至少有3个真因数,先找出a_n的三个最大的真因数,再把它们相加得到下一项a_{n+1}。
问题是,起始值a_1有哪些数值可以取?
谷歌Gemini Deep Think给出了5个解题步骤,想要确定a_1取值,前提是让a_n+1=S(an) 定义的序列是无限正整数。
步骤1:证明对所有n,a_n都是偶数。
步骤 2: 证明对所有n,a_n都能被3整除。
步骤 3: 当6∣N时,分析序列的动态行为。
步骤 4: 研究序列的演变过程并给出对a_1的限制条件。
步骤 5: 对起始值a_1进行全面刻画与分类。
整体过程亮点,在于化繁为简,用不变性和增长率把大范围枚举压缩到独一无二的固定点。
第五题,是一道组合博弈+不等式分析题。
简单来说,题干要求:
轮到Alice(奇数回合)时,她必须给出一个非负数,使得目前所有数的总和≤ λ×当前回合数;
轮到Bazza(偶数回合)时,他必须给出一个非负数,使得目前所有数的平方和≤当前回合数。
谁在自己回合找不到合法数就输;若双方都能一直出数,游戏无胜负。
题目要找出哪些 λ 能保证Alice必胜,哪些 λ 能保证 Bazza必胜?
Gemini Deep Think在解题时假设了2种情况,如下所示:
前者巧妙之处在于,把连续参数问题瞬间离散化:只要在λ
而后者关键点是「先蓄力,再一击致命」,具体来说,让Alice把总和一次性抬高,让Bazza下一回合无法去满足平方和条件,于是当场获胜。
最终,Gemini得出如果λ=1√2时,两者都不会赢。只有当λ>1√2,Alice获胜;当0<λ<1√2时,Bazza获胜。
对此,来自Anthropic AI研究员点评道,「乍一看,它们的解法比OpenAI要清晰得多」。
团队介绍
Thang Luong
官博称,Gemini Deep Think整体技术方向由Thang Luong带队,现任Google DeepMind高级主任研究员,曾任Google Brain研究员。
他于2016年获得斯坦福大学计算机科学博士学位,在读博期间开创了深度学习在机器翻译领域的应用先河。
在Google DeepMind工作期间,Thang Luong构建了多个语言(QANet、ELECTRA)和视觉(UDA、NoisyStudent)领域的尖端模型。
2020年,他推出全球最强聊天机器人Meena项目,该项目后续发展为Google LaMDA、Bard及现Gemini系列,也是经典注意力机制「LuongAttention」的发明者。
自2022年起,Thang Luong共同领导Bard多模态功能的开发,并担任能解决IMO级别几何题的AlphaGeometry项目负责人。
所有成员名单如下:
上下滑动查看
AI+数学未来
谷歌DeepMind长期与数学界保持着合作,但AI为数学做出贡献的潜力才刚刚崭露头角。
通过训练Gemini学会更灵活、更直观地推理,谷歌正逐步构建出能够解决更复杂、更前沿数学问题的AI。
今年,夺下IMO金牌虽然完全基于Gemini自然语言能力,但团队也在AlphaGeometry和AlphaProof等形式化系统方面也取得了持续的进展。
谷歌坚信,那些能够将流畅的自然语言能力与严谨的推理能力(包括形式化语言中的可验证推理)相结合的AI智能体,将成为数学家、科学家、工程师和研究人员不可或缺的工具。
在通往AGI的道路上,AI将推动人类知识的进步。
OpenAI回应了!
其实,谷歌DeepMind早在7月19日周五下午就拿下了金牌,只是在等内部验证流程才未对外公布。
与之形成鲜明对比的是,赶在周六凌晨抢发的OpenAI不仅不讲武德,金牌也完全是「自封」的,并未经过任何IMO官方的独立验证和评分。
谷歌DeepMind超级推理团队的Thang Luong表示:因为IMO内部有一份官方评分指南,外界根本无法获取。
要知道,OpenAI自评的金牌成绩只是刚刚过35分的线而已,如果有微小的扣分,都会让成绩从金牌跌到银牌。
而且IMO组委会还特地明确要求,希望各个大模型公司在闭幕式一周后再公布成绩,不要抢走孩子们的风头。
但OpenAI的Naom Brown却表示,他们的确尊重了IMO的要求,是等闭幕式之后才发布的。
就在谷歌DeepMind官宣夺金之后,Naom Brown又双叒代表OpenAI发声了,还是连发7推。
他首先肯定了GDM的成就,并指出OpenAI与之并行取得的成功,印证了AI进化的迅速。
不过,在具体测试中,两家的方法各有千秋。
在总结自家模型结果的思考前,Naom Brown澄清了,早在2个月前,IMO组委会曾电邮邀请OpenAI参与基于Lean语言的正式竞赛。
然而,当时OpenAI正忙于自然语言通用推理研究(不受Lean约束),就给婉拒了。
他特别强调了,OpenAI通用模型参赛IMO时,并没有使用任何RAG等工具。
而且,团队提交的证明均由三位外部 IMO 奖牌获得者进行了评分,并且在正确性上达成了完全一致的意见。
接下来,Naom再次重申,「OpenAI是在开幕式结束之后公开的结果」。
昨日澄清的那一套话,再次公开陈述了一遍。
另一位OpenAI研究员Aidan McLaughlin还讥讽GDM,「他们为模型提供上下文,纯属带着小抄进入了考场作弊」。
但现在事实已经摆在眼前——
一边是谷歌经IMO官方认证的成绩,模型即将在未来可用;一边是OpenAI不讲武德提前邀功,模型是未公开版本,以后很可能也不会公开。
这一轮过后,OpenAI急功近利的做法,更加失了民心。