核心观点 - 字节跳动旗下Seed AI4Math团队发布数学推理专用模型Seed Prover 1.5，在Scaling Law和强化学习加持下，其数学推理能力达到国际顶尖水平，在IMO竞赛中取得金牌成绩，并在多项基准测试中刷新SOTA记录 [1][4][5][6] 模型性能与成就 - Seed Prover 1.5在16.5小时内解决了IMO 2025的前5道题目，仅失一题，获得35分，达到今年IMO金牌线 [1] - 该成绩与谷歌Gemini的IMO金牌成绩持平，并大幅超越了其前代模型（前代模型耗时3天完成4道题及一道题的部分证明，仅获银牌成绩）[3] - 模型在北美本科级别数学竞赛Putnam基准上，大幅刷新了SOTA成绩 [4] 技术架构与创新 - 模型采用“Agentic Prover”架构，这是一种新的形式化数学推理范式，将Lean等形式语言视为工具，允许模型在证明过程中自主调用多种工具进行交互和验证 [12][13][14] - 核心创新之一是引入了“Sketch Model”，它模拟人类数学家的工作方式，先将自然语言证明转化为非形式化的逻辑草稿和引理结构，从而将复杂问题拆解为更易解决的子目标 [14][22][23] - 工作流采用分层级的多智能体协作系统：Natural Language Prover提供高层数学直觉，Sketch Model转化为形式化引理结构，Agentic Prover并行攻克各个引理 [37] - 模型采用基于引理的交互式证明方式，既非低效的逐步证明，也非高风险的一次性完整证明，提升了推理的并行度和成功率 [15][17] 训练方法与效率提升 - 模型进行了大规模的Agentic强化学习训练，随着训练步数增加，模型在训练集上的证明通过率从初始的50%提升至接近90% [18][19] - 强化学习带来了显著的效率提升，Seed Prover 1.5仅需少量计算资源，就能在Putnam等高难度数据集上击败消耗大量算力的上一代模型 [19] - 实验数据对比显示，在Putnam数据集上，Seed-Prover 1.5（agentic prover only）以特定的测试配置（pass@8 × 8）取得了57/100的成绩，优于前代模型（35/100）及其他竞品 [20] - 研究验证了测试时Scaling的有效性，即投入更多计算资源（测试时）能显著提高解题率，且解决率随计算资源投入呈对数线性增长 [5][28][29] 模型规格与背景 - Seed Prover 1.5的参数规模为230B总参数，23B激活参数，与其基础模型Seed 1.6相同 [8] - 该研究团队为字节跳动Seed AI4Math团队，核心成员包括来自清华大学、牛津大学、卡内基梅隆大学等背景的研究人员 [30][32][33][34]