OpenAI IMO 团队：为什么模型终于能解决精英级数学
摘要
OpenAI 的模型在国际数学奥林匹克竞赛 (International Math Olympiad, IMO) 中首次取得了金牌级别的成绩，这是通往人工超级智能 (Artificial Super Intelligence) 道路上最重要的里程碑之一。本期对话邀请了该突破背后的三位核心成员 Alex Weey、Cheryl Sue 和 Noam Brown，深入剖析了这一成就背后的技术架构。
真正令人兴奋的不仅是模型的数学能力本身，而是底层的通用技术：用于扩展测试时计算 (test-time compute) 和解决难以验证任务 (hard-to-verify tasks) 的方法，这些能力远超竞赛数学的范围。仅仅一年前，模型还只能进行约 0.1 分钟的推理；如今，系统已经可以持续集中思考长达 100 分钟。团队始终将"通用性"作为最高优先级——与多年前耗费数年构建专用系统（如扑克 AI 或外交 AI）不同，他们刻意避免为 IMO 定制任何特殊性方案。
对话还揭示了模型在证明中的"外星语言"风格、团队如何在 IMO 当日熬夜等待结果的紧张氛围、以及模型在面对无法解决的问题（第六题）时表现出的令人鼓舞的"自知之明"——它选择承认"无法回答"而非胡编乱造。
正文
起源：一个只有三个人的团队
Alex 回忆道，他在 OpenAI 的第一周，Noam 就问他"你认为模型什么时候能拿到 IMO 金牌？"当时 Alex 觉得 2025 年不太可能。但这个问题一直萦绕在团队心中。
具体到这次冲刺：核心想法在大约六个月前开始成型，而真正的"最后一公里"——为当年 IMO 做准备——只花了几个月时间。令人惊讶的是，核心团队实际上只有三个人（Alex、Cheryl 和 Noam），当然，他们"站在巨人的肩膀上"——依赖了大量从事推理基础设施、预训练和 RL 训练的同事的工作。
Noam 补充说，大部分技术工作是由 Alex 完成的，他和 Cheryl 是在接近 IMO 时加入协助的。
内部氛围与赌约
当被问及内部是否乐观时，团队的回答颇具戏剧性。Noam 回忆说，在比赛前两个月，另一位 OpenAI 研究员认为模型获胜的概率不到三分之一，愿意以 2:1 的赔率赌模型不会赢——但他最终没有下注，因为"押注团队输太不吉利了"。而 Alex 则一直默默地在后台努力改进模型。
Cheryl 透露，在一两个月前，模型确实还需要大幅改进。但技术的进步速度超出了大部分人的预期——这正是 Alex 在推特上强调的观点：仅仅几年前，这些模型还在与小学数学题（GSM8K）较劲；到 2024 年，GSM8K 已成为过时的基准；紧接着是 AMC，再然后是 USA Math Olympiad——模型以惊人的速度"扫荡"了所有数学基准测试。
来自外星人的证明风格
Alex 坦率地承认，模型输出的证明风格"有些糟糕"（atrocious），但 Noam 则更温和地称之为"像外星语言"。由于这次是小型冲刺式的努力，团队没有花太多精力优化人类可读性——但他们知道如何做到这一点（类似 ChatGPT 那样使输出更可读）。
关于验证过程：每个证明由三位前 IMO 奖牌获得者独立评分，并达成一致意见。有趣的是，Noam 和 Cheryl 都承认自己无法理解模型的证明——这反而更凸显了模型的能力水平。
第六题的"自知之明"
IMO 的第六题（通常是最难题）是组合数学 (combinatorics) 问题。没有任何模型在本届 IMO 上解决第六题，OpenAI 的模型甚至没有尝试回答。但团队认为这反而是个积极信号：模型没有试图编造答案——它诚实地输出了"无法回答"。
Noam 回忆起一个普遍痛点：推理模型发布后，如果问它们一个它们不知道答案的问题，模型会输出一个极具说服力但完全错误的答案——教授和研究人员必须逐行检查才能发现某个被悄悄翻转的不等式。而新模型不仅能力更强，更重要的是——它学会了在不知道时说"不知道"。
Alex 分析认为，组合数学之所以比几何更难，是因为它更抽象、更高维，常常需要一种"信念之跃"式的洞察力，而模型更擅长需要大量小步骤逐步推进的问题。
通用技术，而非特化方案
这或许是整场对话中最重要的一点。Noam 强调，团队刻意避免了为 IMO 构建专用系统。他本人曾在扑克 AI 项目上耗费多年，Alex 曾参与外交 AI（Cicero）——这些项目虽然令人自豪，但在 AI 进步如此迅速的时代，"花几年做一个只能做一件事的定制系统"已不再是最好的时间投资。
因此，所有技术——扩展思考时间、处理难以验证的任务、并行计算——都是通用技术，已经或计划应用于其他系统。这也是团队选择不使用 Lean（形式化验证工具）而坚持自然语言推理的原因：Lean 虽然有价值，但在通用推理能力方面有局限性。
关于形式化验证 vs. 非形式化推理：团队认为这两者是正交的 (orthogonal)。非形式化数学之所以是一个有趣的挑战，是因为它代表了扩展测试时计算和解决难以验证任务的"困难内核"——而这些困难广泛适用于各种通用任务。Lean 更狭窄——世界上可以用形式化方法处理的事物远少于可用非形式化推理处理的事物。
Alex 重申：扩展测试时计算的这些技术将被整合到 OpenAI 的通用模型中，以全面提升推理能力，但这需要一些时间来部署。
从 0.1 分钟到 100 分钟，再到 1500 小时
Noam 提出了一个令人深思的计算：如果将推理时间作为横轴，我们经历了从几秒钟（GSM8K）到 1.5 小时（IMO 问题）的跨越——这是约 1000 倍的提升。但研究级数学问题需要这些顶尖学生在成长为研究人员后花费约 1500 小时。而千禧年大奖问题 (Millennium Prize Problems) 则需要整个领域几代人的集体思考。
这既是激动人心的，也是令人谦卑的——从 1.5 小时到 1 万小时甚至 10 万小时，还有很长的路要走。
Noam 也指出了一个实际的瓶颈：如果你想评估一个需要思考 1500 小时的模型，那么评估本身就需要 1500 小时——实验的迭代速度将受到根本性限制。
IMO 当日的氛围
IMO 比赛当天，题目在参赛者完成考试后才会公布。大约凌晨 1 点，团队将题目输入模型。Cheryl 选择去睡觉（毕竟需要四个半小时才能出结果），而 Alex 和 Noam 则熬夜守候。Alex 在等待过程中焦虑地实时检查模型的中间输出，用手工验证证明的正确性。
Noam 分享了一个有趣的观察：虽然他自己无法理解证明内容，但模型在思考过程中会用自然语言表达其信心水平——反复说"good"表示自信，"？"表示不确定。这样，即使不懂数学的人也能大致感知模型的"情绪"。
下一步：从解题到命题
团队认为，Putnam 竞赛的题目（时间更短、更偏知识型）实际上对模型来说比 IMO 更容易——所以竞赛数学的边界已经不再是"计时解题"，而是需要更深层次、更长时间思考的问题。
关于"发现新定理"：Alex 认为需要正视从 1.5 小时到 1500 小时的差距。但 Noam 不认为存在根本性障碍——当 LLM 刚出来时，问题是"如何让它们推理"；有了推理之后，问题是"如何解决难以验证的任务"；现在这个问题也解决了，下一个问题是"如何让它们提出新颖的问题"——就像创建一个 IMO 问题本身也需要顶尖数学家的巨大努力一样。
关于 AI 是否应该擅长出题（而不仅仅是解题），Alex 认同 Demis Hassabis 的观点：最难的部分确实是提出有趣的问题。但 Noam 乐观地表示，团队没有看到阻碍进一步进展的根本性障碍。