OpenAI与谷歌模型斩获IMO金牌纯语言推理破逻辑壁垒

硅谷101

大模型虽突破自然语言逻辑难题并斩获IMO金牌，但攻克封闭竞赛题仍不等于掌握开放式数学研究能力。

AI-assisted summary of AI拿下奥数IMO金牌，但数学界的AlphaGo时刻还没来【101 Weekly】 — original source. Check the original for full context.

Source published: 2025-07-30

Detailed notes

## Background 本内容由 Bilibili 频道的“硅谷101”于 2025 年 7 月 30 日发布。视频主要探讨了 OpenAI 与谷歌 DeepMind 的 AI 模型在国际数学奥林匹克竞赛（IMO）中斩获金牌的技术突破、前 IMO 金牌得主对 AI 解题思路与风格的评价，以及这一成果对未来数学研究与 AGI 发展方向的深远影响。

## TL;DR 今年 IMO 竞赛闭幕后，OpenAI 与谷歌 DeepMind 几乎同时宣布其模型达到了 35 分的 IMO 金牌标准。与过去依赖 Lean 等编程语言进行形式化证明不同，本次 DeepMind 的 Gemini DeepSync 实现了完全基于纯自然语言的输入与推理，打破了过去关于大模型缺乏严谨数学逻辑的质疑。前 IMO 中国国家队成员解析发现，AI 模型在解题上既能进行复杂的解析几何“暴力计算”，也展现出了如讲题老师或严谨论文般的个性化表达。尽管成绩亮眼，但这仍属于封闭环境下的竞赛解题，距离解决开放性数学难题还有差距，同时也引发了数学界对于 AI 工具化与数学创造力本质的讨论。

## Atmosphere & style 视频整体呈现出一种兼具戏剧张力与专业理性的科技洞察风格。前半段展现了两大 AI 巨头紧锣密鼓抢发成果、高层隔空暗讽以及人才争夺战的戏剧性博弈，氛围紧张而热闹；后半段则通过前国家队选手的专业视角与数学家们的观点碰撞，将情绪沉淀至冷静严肃的学术思考。听众在感受 AI 技术飞速跃迁的震撼之余，也能体会到面对技术变革时数学界对于人类智慧与自由创造力的深沉思辨。

## Key takeaways - [00:00](https://www.bilibili.com/video/BV1hj8fzrEey?t=0s) OpenAI 与 Google DeepMind 在 2025 年 IMO 闭幕前后相继宣布其 AI 模型达到金牌标准（答对 5/6 题，斩获 35 分）。 - [00:00](https://www.bilibili.com/video/BV1hj8fzrEey?t=0s) OpenAI 抢先公关发布未获官方背书的结果，而 DeepMind 的成绩则得到了 IMO 官方组委会的独立验证与好评。 - [00:00](https://www.bilibili.com/video/BV1hj8fzrEey?t=0s) 顶尖 AI 实验室间的人才争夺战异常激烈，DeepMind 金牌团队中的 3 名核心研究员在发布后不久即被 Meta 挖走。 - [00:00](https://www.bilibili.com/video/BV1hj8fzrEey?t=0s) 此次成绩尚算不上数学界真正的“AlphaGo 时刻”，因为人类顶尖选手仍能拿到满分，AI 在综合能力上超越人类尚为时过早。 - [02:30](https://www.bilibili.com/video/BV1hj8fzrEey?t=150s) 相较于去年依赖 Lean 形式化证明语言的模型，Gemini DeepSync 实现了全程纯自然语言的理解与推理作答。 - [02:30](https://www.bilibili.com/video/BV1hj8fzrEey?t=150s) 纯自然语言推理打破了 Gary Marcus 等学者关于大模型缺乏逻辑、必须依托结构化代码才能进行严谨数学推理的质疑。 - [06:00](https://www.bilibili.com/video/BV1hj8fzrEey?t=360s) 在几何题解法上，DeepMind 偏向人类常规的纯几何构造法，而 OpenAI 则利用算力优势进行高强度的代数解析“暴力计算”。 - [06:00](https://www.bilibili.com/video/BV1hj8fzrEey?t=360s) 语言表达风格上，OpenAI 呈现出充满鼓励性词汇的“讲题老师”风格，DeepMind 则呈现严谨规范的“学术论文”风格。 - [09:00](https://www.bilibili.com/video/BV1hj8fzrEey?t=540s) IMO 竞赛属于封闭且有标准答案的环境，攻克竞赛题并不代表 AI 已具备解决现实中开放性（open-ended）数学难题的能力。 - [09:00](https://www.bilibili.com/video/BV1hj8fzrEey?t=540s) 以陶哲轩为代表的“拥抱派”对 AI 抱有信心，预测到 2026 年 AI 将成为数学研究中值得信赖的合作者。 - [09:00](https://www.bilibili.com/video/BV1hj8fzrEey?t=540s) 以 Michael Harris 为代表的“批判派”则担忧将数学机械化会剥夺自由创造力，并警惕资本与实用主义对数学研究内在价值的侵蚀。

## Detailed walkthrough 以下是本期视频的详细内容梳理与深度解读：

[00:00](https://www.bilibili.com/video/BV1hj8fzrEey?t=0s) IMO 赛场上的 AI 戏剧性对决

今年国际数学奥林匹克竞赛（IMO）在澳大利亚闭幕后，AI 圈迎来了一场针锋相对的戏码。OpenAI 与谷歌 DeepMind 先后宣布自己的 AI 模型达到了 IMO 金牌标准，两家发布时间仅相差两天，过程充满剧情转折。竞赛于 7 月 20 日（周日）闭幕，但 OpenAI 早在 7 月 18 日（周五）晚就抢先官宣。研究员 Alexander Wei 在 X 上发文称，OpenAI 最新的实验性推理大模型攻克了 AI 领域长期以来的重大挑战，在 IMO 的 6 道题目中解出 5 道，斩获 35 分（满分 42 分，35 分恰好达到金牌门槛）。

然而两天后，DeepMind 也下场宣布其 Gemini DeepSync 的进阶版本同样拿下了 35 分的金牌成绩。与 OpenAI 不同的是，DeepMind 的解答获得了 IMO 官方组委会的背书。IMO 主席 Gregor Dolina 评价 DeepMind 的解题“在许多方面都令人惊叹”，阅卷官也认为其解答清晰严谨且易于理解。DeepMind CEO Demis Hassabis 更是亲自在 X 上暗讽 OpenAI，称 DeepMind 之所以没有在周五抢先发布，是尊重 IMO 组委会的请求——即所有 AI 实验室都应在官方成绩经过独立专家验证、且参赛学生获得表彰之后再公开结果。Hassabis 强调自己的模型才是“第一个获得官方金牌水平评级的 AI 系统”。戏剧性的是，隔天媒体便爆出 DeepMind 这支金牌团队中的 3 名核心研究员已被 Meta 挖走，而在此前 6 个月内，已有约 20 名 DeepMind 员工跳槽至微软，足见顶尖实验室间的人才争夺战愈演愈烈。

* **IMO 算分与成绩**：共 6 道题，满分 42 分，金牌线为 35 分。今年共有 72 位高中生选手达到金牌标准，其中 5 位获得 42 分满分；而两个 AI 模型均做对了 5 道题，拿到 35 分。 * **AlphaGo 时刻的对比**：虽然成绩亮眼，但这还算不上数学界的“AlphaGo 时刻”。当年 AlphaGo 击败李世石震撼全球，是因为围棋曾被视作人类智慧最难被攻克的堡垒；2022 年底 Meta 的 AlphaFold 准确预测蛋白质结构也被誉为生物学的 AlphaGo 时刻。如今 AI 仅做对 5 题，而人类顶尖高中生能做到全对，说明 AI 在综合数学能力上超越人类尚为时过早。

---

[02:30](https://www.bilibili.com/video/BV1hj8fzrEey?t=150s) 从 Lean 形式化证明到纯自然语言推理

要理解这次的技术突破，需要回顾一年前 DeepMind 推出的 AlphaGeometry 和 AlphaProof。去年这两个模型在 IMO 中解出 4 道题，达到了银牌标准。但当时它们并非直接理解和输出自然语言，而是依赖“形式化证明”（Formal Proof）。

所谓的形式化证明，是借助一种类似编程语言的系统（如 Lean），将自然语言的数学题先翻译成机器能看懂的逻辑语言，由 AI 生成一步步严谨可验证的代码解答，最后再人工翻译回人类可读的语言。这一套流程极其耗费计算资源，当时解题长达 3 天，远超 IMO 竞赛两天共 9 小时的时间限制。

而本次 Gemini DeepSync 最大的技术飞跃在于：**完全使用自然语言进行输入与输出**。AI 独立阅读自然语言题目、用自然语言逻辑作答，全程没有借助 Lean 或任何形式化工具。

* **打破 Gary Marcus 等学者的质疑**：此前以纽约大学教授 Gary Marcus 为代表的 AI 学者一直断言，语言模型本身缺乏逻辑，不具备独立完成高难度数学推理的能力（例如让大模型数 "strawberry" 里的 'r' 经常出错）。Gary Marcus 曾认为，AI 必须依托像 Lean 这样的形式化语言输出机器可验证的结构，再人工转为自然语言，才能用于严谨的数学研究。 * **纯自然语言推理的意义**：Gemini DeepSync 的成功证明了语言模型自身即可承载极其复杂的数学逻辑逻辑，直接打破了以往“电脑辅助数学必须等同于形式化方法”的固有认知。

---

[06:00](https://www.bilibili.com/video/BV1hj8fzrEey?t=360s) 真实作答体验：解析几何暴力计算 vs 讲题老师风格

为了客观评估 AI 的解题水平，节目邀请了一位前 IMO 中国国家队成员对两个模型的作答过程进行了专业打分与对比。嘉宾指出，在 AI 做对的 5 道题中，其逻辑线条完整、思路清晰，拿满分实至名归，但两者的作法与语言风格展现出有趣的差异。

以第二题平面几何题为例，平面几何本是 AI 最擅长的领域之一，但两者的策略截然不同：

在语言表达与排版习惯上，AI 也展现出了独特的“职业病”与个性： * **符号系统**：两个 AI 都极度喜欢在解答过程中不断引入新符号来定义新概念或公式。这种习惯在大学的高等数学中很常见，但在高中竞赛中反而增加了人类理解思路的难度。 * **OpenAI 的风格**：带有强烈的互动感和口语化色彩。解答中频繁出现如 "so far so good"（到目前为止都不错）、"nice"（太棒了）、“这是个漂亮的结论”等鼓励性词汇，听起来非常像一位在课堂上引导学生、巡巡善诱的讲题老师。 * **DeepMind 的风格**：极其书面化与严谨，文字排版流畅，阅读体验更像是一篇正规的数学论文。

---

[09:00](https://www.bilibili.com/video/BV1hj8fzrEey?t=540s) 竞赛解题 vs 现实研究：数学界的两派阵营

虽然大模型在竞赛上实现了质的飞跃，但前国家队嘉宾提醒，IMO 毕竟只是在一个封闭、已知的环境里寻找固定答案，这既不是日常买菜的数学，也不是数学家穷尽一生探索的目标。真正的数学研究往往是开放式的（open-ended），研究者在做出突破前甚至不知道自己能发现什么。因此，攻克竞赛题对 AI 而言是当前更可及的目标，但距离解决真正的开放性数学难题（Open Questions）仍有距离。

随着 AI 深入数学领域，数学界内部也逐渐分化为两大派别：

> **拥抱派（以陶哲轩为代表）**： > 澳籍华人数学家陶哲轩指出，早在 2023 年 AI 就已经能为职业数学家提供有启发性的提示和思路。他预测，当 AI 与形式化证明、验证搜索引擎以及符号数学工具深度结合后，到了 **2026 年，AI 将成为数学研究中值得信赖的合作者**。

> **批判派（以 Michael Harris 为代表）**： > 哥伦比亚大学数学家 Michael Harris 在其 Substack 博客中发文批判。他认为数学的真正价值在于自由探索与内在洞见，而非沦为市场逻辑下的技术工具。像 Lean 这样的代码语言将数学简化为机器逻辑，剥夺了数学的自由创造力与思辨美感。同时他极度担忧数学研究资本化的趋势，批评像 Google、NSA 等资助方倾向于用实用价值衡量数学，忽略了其内在价值；他也反思当前关于“AI 助教”的讨论过分关注“它管用吗/能否带来效益”，却忽视了“对谁有利”、“为什么需要它”等根本性伦理问题。

对于那些在顶级赛场被 AI 追赶甚至超越的数学家来说，这是否会像当年李世石被 AlphaGo 击败后选择退役一样，让人类开始怀疑研究数学本身的意义？DeepMind 的 Pushmeet Kohli 在去年 AlphaProof 拿到银牌时曾表示，他相信这终将促进学术研究的发展，但如何平衡技术工程与科学探索，依然留给全社会无限的思考空间。

## Notable quotes > [00:00](https://www.bilibili.com/video/BV1hj8fzrEey?t=0s) 在许多方面都令人惊叹 — Gregor Dolina

> [00:00](https://www.bilibili.com/video/BV1hj8fzrEey?t=0s) 第一个获得官方金牌水平评级的 AI 系统 — Demis Hassabis

> [06:00](https://www.bilibili.com/video/BV1hj8fzrEey?t=360s) so far so good — OpenAI 模型

> [06:00](https://www.bilibili.com/video/BV1hj8fzrEey?t=360s) nice — OpenAI 模型

> [06:00](https://www.bilibili.com/video/BV1hj8fzrEey?t=360s) 这是个漂亮的结论 — OpenAI 模型

> [09:00](https://www.bilibili.com/video/BV1hj8fzrEey?t=540s) 2026 年，AI 将成为数学研究中值得信赖的合作者 — 陶哲轩

> [09:00](https://www.bilibili.com/video/BV1hj8fzrEey?t=540s) 它管用吗/能否带来效益 — Michael Harris

> [09:00](https://www.bilibili.com/video/BV1hj8fzrEey?t=540s) 对谁有利 — Michael Harris

> [09:00](https://www.bilibili.com/video/BV1hj8fzrEey?t=540s) 为什么需要它 — Michael Harris

## Mentioned OpenAI, 谷歌 DeepMind, DeepMind, IMO, 国际数学奥林匹克竞赛, AlphaGo, Alexander Wei, Gemini DeepSync, Gregor Dolina, Demis Hassabis, Meta, 微软, 李世石, AlphaFold, AlphaGeometry, AlphaProof, Lean, Gary Marcus, 纽约大学, 陶哲轩, Michael Harris, 哥伦比亚大学, Google, NSA, Pushmeet Kohli

## 弹幕氛围 (Danmaku mood) — 152 条观众互动氛围十分热烈且充满调侃与思考。开局弹幕大量刷数字打卡，随后针对 AI 配音自然度、AI 与人类智力（如 IMO 金牌、显卡 vs 人类成本）的对比展开理性探讨与幽默吐槽。中段在特定节点密集刷“算/不算”形成互动高潮，后续则围绕 DeepMind 与 OpenAI 的对比、AI 解题思路以及说话口音（如印度咖喱味）进行了丰富的梗与观点输出。

**整体情绪**：😊 正面 30% · 😐 中性 50% · 😞 负面 20%

**热议点** - **弹幕开场打卡与刷屏互动** —— “5” - **探讨 AI 与人类成本及智力的对比** —— “ai只需要几张显卡，人需要吃喝拉撒一辈子，还要后天的教育培养，甚至少数人才学的会” - **对视频中判别标准表达不同意见的“算/不算”刷屏** —— “不算” - **对比 OpenAI 与 DeepMind/谷歌的技术路径与表现** —— “这就有意思了啊，谷歌在学人，openai在超人” - **调侃视频中出场人物的印度口音** —— “纯正咖喱味” - **思考 AI 对数学竞赛及人类未来价值的影响** —— “AI始终只能用来辅助。”

**代表弹幕** > 别的不说，这个AI配音倒是挺真实自然的

> ai只需要几张显卡，人需要吃喝拉撒一辈子，还要后天的教育培养，甚至少数人才学的会

> 绝不忘阴阳怪气一下

> 已经比90%的人类强了

> 这就有意思了啊，谷歌在学人，openai在超人

> 纯正咖喱味

> 人类没有价值了

[Source](https://www.bilibili.com/video/BV1hj8fzrEey)

中文简报

OpenAI与谷歌模型斩获IMO金牌纯语言推理破逻辑壁垒大模型虽突破自然语言逻辑难题并斩获IMO金牌，但攻克封闭竞赛题仍不等于掌握开放式数学研究能力。今年 IMO 竞赛闭幕后，OpenAI 与谷歌 DeepMind 几乎同时宣布其模型达到了 35 分的 IMO 金牌标准。与过去依赖 Lean 等编程语言进行形式化证明不同，本次 DeepMind 的 Gemini DeepSync 实现了完全基于纯自然语言的输入与推理，打破了过去关于大模型缺乏严谨数学逻辑的质疑。前 IMO 中国国家队成员解析发现，AI 模型在解题上既能进行复杂的解析几何“暴力计算”，也展现出了如讲题老师或严谨论文般的个性化表达。尽管成绩亮眼，但这仍属于封闭环境下的竞赛解题，距离解决开放性数学难题还有差距，同时也引发了数学界对于 AI 工具化与数学创造力本质的讨论。 OpenAI 与 Google DeepMind 先后宣布其 AI 模型在 2025 年 IMO 国际奥数竞赛中达到金牌线（答对 5/6 题获 35 分），但鉴于顶尖人类选手仍斩获满分，目前尚算不上数学界真正的“AlphaGo 时刻”。 (0:00) 相较于去年依赖 Lean 形式化代码且耗时数天的模型，本次 Gemini DeepSync 实现了全程纯自然语言推理作答，直接打破了大模型缺乏严谨数学逻辑能力的学术质疑。 (2:30) 解题风格上，DeepMind 倾向于贴近人类常规思维的纯几何构造与严谨论文格式，而 OpenAI 则利用算力进行代数“暴力计算”，并呈现出充满鼓励性口语的讲题老师风格。 (6:00) 针对 AI 进军数学领域，学界分化为陶哲轩领衔的“拥抱派”（预言 2026 年 AI 成为可信合作者）与 Michael Harris 代表的“批判派”（担忧商业化与工具主义剥夺数学探索之美）。 (9:00)

Reading summary

OpenAI与谷歌DeepMind的大模型在国际数学奥林匹克竞赛（IMO）中相继达到金牌分数线，标志着AI实现了纯自然语言数学推理的质变，但其离真正超越人类研究者的“AlphaGo时刻”仍有差距。达到金牌门槛但尚未超越人类巅峰 (0:00) 在澳大利亚举办的IMO竞赛闭幕前后，OpenAI与DeepMind的模型均在6道题中解出5题，斩获35分（满分42分）达到金牌线。OpenAI于7月18日抢先发布其实验性推理模型成绩，而DeepMind随后于7月20日宣布其Gemini DeepSync进阶版本同样达到35分，并获得了IMO官方组委会与阅卷官对其解题严谨清晰的官方背书。伴随成绩公布的是激烈的人才竞争，DeepMind金牌团队已有核心研究员跳槽至Meta与微软。尽管成绩亮眼，节目认为这仍算不上数学界的AlphaGo时刻。今年共有72位人类高中生获得金牌，其中5位斩获42分满分；相比当年AlphaGo击败李世石或AlphaFold预测蛋白质结构，AI目前仅做对5道题，在综合数学能力上全面超越顶尖人类选手尚为时过早。推理范式跨越：摆脱形式化代码证明 (2:30) 回顾前一年DeepMind推出的AlphaGeometry和AlphaProof，两者在IMO获得银牌时严重依赖类似编程语言的Lean形式化证明系统，需经历“题目转代码、AI代码解答、人工转回自然语言”的漫长链路，单次解题耗时长达3天。本次Gemini DeepSync的核心突破在于完全采用自然语言进行端到端的输入与输出，全程未借助Lean等形式化工具。这一进展直接打破了学者Gary Marcus等人此前的质疑。Marcus等学者曾认为语言模型本身缺乏严密逻辑、无法独立完成高难度数学推演，必须依托机器验证的形式化语言。Gemini DeepSync的表现证明语言模型自身即可承载复杂的数学逻辑推理，颠覆了电脑辅助数学必须依赖形式化方法的固有观念。解题路径分野：暴力代数计算与论文严谨论述 (6:00) 前IMO中国国家队成员对两家模型作答评估后指出，两者解题思路清晰且拿满分实至名归，但策略与语言风格迥异。以第二道平面几何题为例，DeepMind采用符合人类选手常规思维的纯几何构造法；OpenAI则直接建系进行代数化“暴力计算”，其承受的高强度计算量在考场上极难由人类完成，但极其契合AI的计算效率优势。在表达习惯上，两家AI均表现出频频引入新符号的学术习惯，增加了高中竞赛层面的阅读负担。风格方面，OpenAI答卷充满“so far so good”、“nice”等口语化互动，类似引导课堂的讲题老师；DeepMind则行文严密、排版规整，展现出类似正式学术论文的书面化风格。竞赛局限与真实科研鸿沟引发学界分歧 (9:00) 专业嘉宾指出，IMO竞赛是在已知、封闭的环境中求解确定答案，而现实中的前沿数学研究多为开放性探索（open-ended），数学家在突破前往往无法预知结论，因此竞赛解题的成功距离解决未知的开放性数学难题仍存在巨大鸿沟。 AI的介入也使数学界分化为两大阵营：以陶哲轩为代表的拥抱派认为AI在2023年已能提供启发，并预测到2026年AI与形式化验证、符号工具结合后将成为可信赖的科研合作者；而哥伦比亚大学数学家Michael Harris等批判派则质疑将数学简化为机器逻辑剥夺了其自由创造力与思辨美感，同时对科技巨头与资本导向侵蚀数学内在价值及伦理机制表达了深切忧虑。尽管DeepMind等技术团队看好AI对学术研究的促进作用，但在封闭赛题被AI逐一攻破的背景下，如何界定机器辅助与人类自由探索的界限、应对科研范式转变，仍是数学界面临的长期追问。

Source quotes

[0:00] Gregor Dolina: 在许多方面都令人惊叹 [0:00] Demis Hassabis: 第一个获得官方金牌水平评级的 AI 系统 [6:00] OpenAI 模型: so far so good [6:00] OpenAI 模型: nice [6:00] OpenAI 模型: 这是个漂亮的结论 [9:00] 陶哲轩: 2026 年，AI 将成为数学研究中值得信赖的合作者 [9:00] Michael Harris: 它管用吗/能否带来效益 [9:00] Michael Harris: 对谁有利 [9:00] Michael Harris: 为什么需要它

Original transcript

[0:00] 当AI能赢下奥数比赛的时候我们离AGI还有多远一觉醒来啊我以为我船也回高中了朋友圈呢竟然有人提起IMO也就是中学生国际数学奥林匹克这个竞赛记得当年啊还是万里挑一的学霸才能参加这个比赛今年呢竟然被AI拿下了OpenAI和谷歌DMine前后宣布他们的模型达到了IMO精彩的标准这个前后虽然只差了两天啊但却是充满了drama今年的IMO是7月20日周日在澳大利亚比目而OpenAI在周五也就是7月18日晚上就早早宣布了这个消息研究员Alexander Wei在X上说OpenAI最新的实验性推理大模型实现了人工智能领域长期以来的一项重大挑战在IMO竞赛的6道题目当中解除了5道并且最终获得了35分IMO的满分是42分而35分恰好就达到了金牌的门槛不过两天之后DeepMind也下场宣布Gemini DeepSync的进阶版本模型也达到了这一成就DeepMind的模型在整个过程中完全使用自然语言操作最后同样获得了35分的成绩并且IMO官方组委会也证明了这一成绩IMO主席Gregor Dolina说DeepMind的解题在许多方面都令人惊叹月卷官认为这些解答清晰严谨而且大多数都很容易理解这个组委会亲自背书的待遇却没有给到OpenAIDemis Hassabis甚至特意下场在X上表示我们之所以没有周五公布是因为我们尊重IMO组委会最初的请求所有AI实验室都应该在官方成绩经过独立专家验证而且参赛学生已经获得应有的表彰之后才公开各自的结果他还说我们的模型是第一个获得官方金牌水平评级的AI系统简直是就差点OpenAI的名了这下OpenAI之前的欢呼好像就没有那么名正言顺了但更戏剧性的是隔天媒体就爆出DeepMind这一金牌模型背后的研究团队中有三名研究员已经被卖的挖走了在此之前的六个月内DeepMind已经有20名员工被挖去了微软看来这场顶尖实验室之间的斗争还在愈演愈烈那在吃瓜的同时我们还是回到IMO竞赛这个话题上AI达到金牌水平到底意味着什么首先要知道的是这还远远说不上是数学领域的AlphaGo时刻当年AlphaGo击败了世界围棋冠军李适时震惊全球最核心的原因是围棋被认为是人类智慧最难被机器超越的领域之一2022年底卖的AlphaFold准确预测蛋白质结构也被称为是生物学的AlphaGo时刻我们硅谷101在去年的一期视频里详细解读了它的重要性但是这次有72位高中生的成绩也达到了金牌标准其中五位呢获得了42分满分的成绩也就是完美的解答了六道问题但两个AI模型都只做出来了五道所以要说AI在数学能力上已经胜过人类还为时过早但即使没有达到AlphaGo的标准IMO金牌的成绩也足以证明大模型的数学能力了纽约大学的计算机教授Gary Marcus和Ernest Davis就说非常了不起将解答IMO题目作为评估AI能力的标准啊其实早有先例去年Demind发布了两个专门为数学设计的模型Alpha Geometry和Alpha Proof在IMO的六道题里面他们解除了四道成为第一批达到银牌标准的AI系统不过这两个模型当时并不是用自然语言来解题而是结合了一种叫形式化证明的方法简单来说形式化证明就是把数学问题转成了机器能看懂的语言,再由AI用这种形式化语言一步步写出逻辑严谨可验证的解答。而这套语言的写作工具叫做Lean,类似一种编程语言。为了让AI解题,研究者得先把自然语言题目翻译成Lean,让AI去处理,再转回人类可读的答案。整个过程耗时长达三天远超过IMO给高中生两天共9小时的比赛限制但这一次DeepMine最新的Gemini DeepSync模型在完全使用自然语言输入输出的条件下达到了IMO的金牌标准也就是说呢AI完全使用自然语言独体用自然语言作答没有借助Lean或者其他的形式化工具这背后的意义很重要一直以来呢很多人都认为语言模型不具备真正的推理能力比如问他strawberry这个词里面有几个r它可能就会开始内耗反复计算还出错因为自然语言里没有明确的逻辑结构推理过程也就不稳定这也是为什么过去像alpha proof那样的模型需要把自然语言转化成lean绕开语言的不确定性但现在deepmind证明了语言模型本身也可以完成高难度的数学推理虽然deepmind和open ai都没有 [4:59] 公开两个模型的具体训练过程但和一年前相比这确实是一次重大的进展现在这个AI大家都知道是从很多数据当中学习出来的一些参数这样的一个结果就不是说我们预先给定了很多国际规则然后它去执行同理在这个数学上最早期的用电脑来做数学的人会认为把这个数学全部都形式化然后运用这些规则是解决这个数学问题的方法但是现在我们更多的看到这些公司会想办法把两者结合起来甚至是直接使用这个预言模型去输出这个自然语言的数学而完全不借助于这个形式化系统此前以Garen Marcus为代表的AI学者一直认为语言模型无法独立完成真正的数学推理在他的设想中AI模型必须依托像Lin这样的形式化语言输出可以接其验证的逻辑结构最后再人工转化成自然语言也就是说只有像AlphaProof这样的混合模型才有可能达到数学研究的标准因此 Gemini DeepSync 的成功无疑在一定程度上挑战了 Gary Marcus 的观点你可以看到 DeepMind它发布了自己的模型生成出来的解答这个解答就完全是自然语言就没有一些代码什么之类的但是相比于去年他们使用的那一套系统就是它可能最终输出也是自然语言的但是它需要先把这些东西翻译成一个逻辑语言然后进行一些形式化的证明之后再输出可能过往数学家会把这个用电脑辅助数学跟这个形式化方法等同起来但是经过了这些语言模型的发展以及他们证明了自己能够显示出一定的数学能力之后他们可能会改变这个想法为了让大家有一个直观的感受对比AI和人类选手的回答我们邀请了一位IMO前中国国家队成员为我们分享他对AI作答的感受他告诉我们在AI作答的五道题当中逻辑线条完整解题思路清晰获得满分纸实之名归的但在具体题目里对比两个AI的回答还是能发现一些有意思的情况就比如第二题移到平面几何题那么平面几何题对于AI来说算是最容易做的提醒之一了在这里呢这个两个AI也给出了不一样的作法那么DeepMind的这个解法呢是一个更加几何的更加自然的一个解法然后我觉得也是更接近于正常人类选手可以想到的做法但是相比起来呢这个OpenAI的做法就非常的暴力因为它直接使用了这个解析几何的手段用解析几何的办法直接把这道几何题转化成了一道代数题并且在它的解答过程当中出现了巨量的计算通常来说呢人类选手在考场上并不会花时间做这么大量的计算所以说这个方法可能对于AI来说也许执行起来要比人类选手要更加容易他还提到两个AI作答的时候所使用的语言风格也和人类选手不太一样两个AI的一个共同点就是他们的解答过程中会不断地引入新的符号来定义一些概念或者是一些公式那么这个现象在我上大学之后的高等数学的学习中比较经常的出现但是在我以前的竞赛生涯中不太经常的出现原因是这个高度的竞赛题其实没有那么的复杂如果在解答过程中不断的引入一些新的符号呢其实反而会增加我们理解解答过程以及这个解答思路的难度两个AI的语言风格也有非常明显的区别比如说这个OpenAI呢在它的解答过程中会经常出现一些人性化的描述词比如说这个什么什么然后so far good或者说什么什么什么我们完成了这一步nice之类的这些词汇所以总的来说呢看给我的感觉就像是一个在课堂上给学生讲题的老师所以他会经常使用一些口语化的语言来鼓励学生寻寻善用比如说他会说我们已经完成了关键的一步非常的棒或者说我们得到了这个结论真是漂亮的一个结论之类的事情来强调的一些故事中的关键的部分而相比之下呢DeepMine所用的语言则更加书面化像是在阅读一篇数学论文虽然和之前相比啊大模型在IMO竞赛当中的表现已经达到了质的飞跃但我们的采访嘉宾告诉我们啊IMO竞赛终究只是数学能力的一个侧面它是在一个现实封闭的环境中需要参赛者进行巧妙的思考从而找到固定答案的一项竞赛这既不是我们在现实生活中买菜逛街所要用到的数学也不是数学家要穷尽一身思考的目标相比于真正的数学研究有时候这个目标可能是更加的开放式就是open-ended比如说有些人可能会觉得自己做这个研究的目的 [10:00] 输出一种现象或者是发现出一些就规律性的结构但是在你真正做出这些发现之前你能发现出什么是不知道的所以说相比于解决这个真正的数学open quest可能解决这个竞赛问题对于这些模型来说现在是更可及的在AI不断发展的过程中数学学界也分裂成了两派有人认为AI在数学和推理能力上的进展已经能够在一定程度上帮助数学家比如澳籍华人数学家陶哲轩就说2023年AI已经能够为职业数学家生成有启发式的提示和有前景的思路当他与形式化证明及验证搜索引擎符号数学工具等结合使用的时候2026年的AI将会成为数学研究中值得信赖的合作者但与此同时也有数学家对AI不那么信任哥伦比亚大学的数学家Michael Harris就在自己的Substack博客中提出了对AI数学的批判他提出数学的真正意义在于自由探索和内在洞见而不是将其沦为市场逻辑下的技术产品而像Lean这样的计算机语言却将数学简化成机器能看得懂的逻辑让他钟爱的数学失去了自由创造和思辨力同时他十分关注数学研究资本化的趋势担心类似Google NSA这样的资助者倾向于以应用价值衡量数学而忽略其内在价值他批评当前关于AI助理教学的讨论过分关注他管用吗会带来效益吗却忽略了对谁有意为什么需要他这类值得探讨的根本问题我们知道李世时在被AlphaGo击败之后选择提前退役那么顶尖的数学家们会因为AI在数学上的成就而怀疑自己研究的意义吗DeepMind的Pushman Coley在去年AlphaProof达到IMO银牌标准后就说他认为这会促进学术研究的发展这是一个很难的问题而这些数据的数据和系统像这个DVU是一个很大的工程去助于那大大事件那些数据和科技人就是要求世界的评论你怎么看待这些不同的意见呢欢迎在评论区告诉我你们的想法以上就是这次101weekly的全部内容我是一文我们下期再见优优独播剧场——YoYo Television Series Exclusive

OpenAI与谷歌模型斩获IMO金牌 纯语言推理破逻辑壁垒