核心观点 - 谷歌DeepMind的Gemini Deep Think模型在IMO竞赛中以自然语言方式破解5道题，获得35分（满分42分），达到金牌标准[3][4][22] - 该成绩获得IMO组委会官方认证，成为首个获此认可的AI系统[6][7][24] - 模型突破在于完全使用自然语言端到端推理，无需形式语言翻译，且在4.5小时比赛时限内完成[26][29] - 相比2024年AlphaProof和AlphaGeometry 2解决4题获28分（银牌）的表现有显著提升[17][19] - 技术核心是Deep Think增强推理模式，结合并行思考技术和强化学习训练[32][33][35] 技术实现 - 采用并行思考技术，同时探索多种解题路径并整合最优答案[33][34] - 通过新颖的强化学习训练，利用多步推理和定理证明数据提升能力[35] - 提供高质量数学问题解决方案集和IMO解题技巧作为知识库[42] - 模型即将向数学家测试者和Google AI Ultra订阅者开放[39] 解题案例 - 第一题（解析几何）：通过设定引理和分类讨论，证明阳光线数量只能是0、1或3条[44][45][52] - 第二题（平面几何）：分五步证明，包括确定旁心位置和引入辅助点性质[54][55][59] - 第三题（函数）：通过上界证明c≤4和下界证明c≥4确定最小实数常数为4[65][66][67] - 第四题（数论）：用五步证明序列性质，包括偶数性分析和动态行为研究[73][74][78] - 第五题（组合博弈）：通过离散化策略和蓄力战术，确定Alice与Bazza的必胜条件区间[84][85][86] 行业影响 - IMO成为AI能力试炼场，数学推理能力接近顶尖人类水平[16][19] - 自然语言与形式化推理结合的AI将成为科研人员重要工具[105] - 谷歌与OpenAI的竞争凸显技术路线差异：官方认证vs自评结果[108][109][129] - OpenAI被质疑未获官方认证且提前公布结果，影响行业声誉[109][112][130] 团队背景 - 项目由Thang Luong领导，他是机器翻译深度学习先驱和注意力机制发明者[95][96][97] - 团队曾开发AlphaGeometry、LaMDA、Bard等知名项目[98]

模型发布与版本 - DeepSeek在Hugging Face正式发布DeepSeek-Prover-V2，同步上线模型卡及示例代码，共推出两个版本：7B和671B [1][4] - DeepSeek-Prover-V2-7B基于上一代V1.5模型，支持最长32K上下文输入 [4] - DeepSeek-Prover-V2-671B在DeepSeek-V3-Base基础上训练，推理性能最强 [4] 训练方法与技术 - 训练核心采用"递归+强化学习"组合，由DeepSeek-V3拆解复杂定理生成子目标和推理思路，再通过GRPO算法从候选方案中学习最优解 [3] - 训练分为两阶段：第一阶段采用"专家迭代"方法，模型通过解决难题反哺自身 [5]；第二阶段迁移DeepSeek-V3数学知识并引入形式化数据，构建复杂推理路径 [6] - GRPO强化学习算法引导模型在32个候选证明方案中选择被Lean验证系统判定为正确的答案（奖励1分，否则0分） [8][9] 模型能力与特点 - 671B模型能力被"蒸馏"到7B模型，使小模型在资源有限设备上获得接近大模型的数学推理能力 [10][11] - 提供两种解题风格：快速模式（non-CoT）直接生成精炼答案；逻辑模式（CoT）详细展示推理过程 [12] - DeepSeek-V3负责拆解定理生成推理草图，7B模型完成子证明并拼接完整推理，形成"模糊思考+精确证明"机制 [14][15] 性能评估与数据集 - DeepSeek-Prover-V2-671B在MiniF2F测试中通过率达88.9%，成功解出PutnamBench数据集49道难题 [17] - 推出全新数学形式化数据集ProverBench，包含325道题目，涵盖AIME竞赛题、数论、代数、微积分等10个领域 [18][19] - 在15道AIME竞赛题中，DeepSeek-Prover-V2解出6道，DeepSeek-V3通过多数投票解决8道 [20] 行业趋势与方向 - 大型语言模型在"非正式数学推理"与"正式数学推理"间的表现差距明显缩小，逐步学会写出规范可验证的数学证明 [21][22] - 模型从生成内容迈向生成结构化逻辑，可能最早触碰通用人工智能的底层结构，推理能力成为知识系统边界的关键 [32][33][34] 商业化与部署 - 新模型遵循公开许可证，可通过Hugging Face平台免费下载并支持Transformers接口部署 [23][24] - Novita AI成为首批上线Prover-V2-671B推理服务的第三方提供商 [24]