来源： Invited Talk 07 · Zheng Yuan 播客： ICML 2026 · AI4Math 分类： AI 研究 原文发表： 2026-07-11 纪要生成： 2026-07-13
介绍 ByteDance Seed 的三项形式数学工作——Seed Prover（引理式整证 + 深广搜索 + 多阶段 RL）、APE-Bench（repo 级"Lean 版 SWE-bench"证明工程基准）、Seed Prover 1.5（大规模 agentic RL，三工具、稀疏奖励）；核心信条是"模型改进比 harness 改进更重要、RL 在 Lean/形式推理上极其有效（有无限数据的清晰 ground-truth 奖励）"。
ByteDance Seed 在形式数学做了成体系工作，讲者先列出团队全貌：
本讲聚焦其中三项：Seed Prover、APE-Bench、Seed Prover 1.5。
核心思路：Seed Prover 是由领域专用大模型（formal reasoning 模型）驱动的 Lean 定理证明系统。此前整证生成"总出错"——给一个定理、让模型一次输出一大块代码；但让大模型一次生成上百到两千行的正确证明很难。改进：让模型生成小引理（small lemma）、并复用小引理往上搭。这借由"模块化证明构造 + 与 Lean 验证的交互式训练"实现长程推理；再用多阶段推理时扩展（inference scaling）让模型突破能力。核心工作流：propose（提议）→ prove（证明）→ summarize errors（总结你遇到的错误）→ refine（精炼），循环可攻克很难的问题。
训练：多阶段 RL + 课程式难度。训练数据混合开源 Lean 数据集与内部形式化问题；以课程（curriculum）方式控制难度：排除过易题（证明率超过某比例，如"四分之三"以上）；对过难题（采样很多次仍得不到正确证明）——用一个通用 LLM 作 proposer 生成更易的变体纳入训练，先学易版，后期训练时再纳入原题、此时模型更强能解出。推理时可在 prompt 前拼接自然语言提示或已证引理。RL 训练与推理时都可包含这些要素：自然语言提示、已证/失败引理、编译器检查反馈。
测试时扩展（test-time scaling）三档（论文里的 light / medium / heavy 推理设置）。heavy（IMO 时用）：从一个空引理池起，构建一个约 5000 个猜想（conjecture）的池——用通用 LLM 提猜想、Seed Prover 用 light 设置逐一证/否每个猜想；证出很难的引理后，可用它们提出新猜想加入猜想池。IMO 期间该流程跑数天。始终按证明难度给引理排序——一个有趣发现：证明难度越高，通常意味着该引理对解原题越重要。最终解 IMO 题时，取 top ~100 个排序引理作 prompt、以 medium 推理循环完成主证明。讲者调侃：这在今天术语里就叫"harness + 高算力（ultra code effort）"，只是去年还没这些词、当时只叫 medium/heavy inference。
性能：除 2025 IMO 外，在历届 IMO 上可证约 80%；MiniF2F（形式数学标准基准）几乎全解；PutnamBench 表现优异（但 Putnam 这些天也被解了——"有基准，几个月内就会被解"）。也能泛化到 MiniCTX（针对其他 Lean 库的基准）。但 MiniF2F/MiniCTX 只是孤立的定理证明题——真实库（如 mathlib）需要重构、修 bug、加新特性，现有基准忽略了这些迭代式工程流程。
动机：真实世界的形式库建设涉及重构、修 bug、实现新特性；现有基准（如 MiniF2F 给你一个定理陈述让你证）忽略这些。APE-Bench：给你一个大 commit 与"你应该做什么"的指令，任务不是证一个题，而是在这个大 commit 上做证明工程。数据采集很直接：从 GitHub 真实 PR 抽取，与 SWE-bench 很像——可以说 APE 是"Lean 版 SWE-bench"，只是工作在 Lean 而非 Python。双层评测（dual-layer）：一是 Lean 编译器判、二是 LLM-as-judge 判"你是否按指令正确修改"，两关都过才算通过。模型分 easy / medium / hard 三级：hard 题当时所有模型都拿不到分；easy 约 30–50%。但讲者强调这些是较老模型、今日模型会好得多；且 APE-Bench 现在是单文件任务，未来真实工作是多文件——编辑多个文件、走向"自动化库构建 agent"而非单一 prover。
为何 1.5 才是真正 agentic：Seed Prover 1 本质非真正 agentic——每轮把一切塞进 prompt、模型想很多、生成一段 Lean 代码在 Lean 环境跑，但不把编译结果回传给它，而是重开一个新 prompt；所以 1 不是 agentic 模型。Seed Prover 1.5 是真正的多轮 agentic 模型。主工作流：先生成自然语言证明 → 调 lemma sketch 模型生成引理草图（每个引理只给陈述、无证明）→ agentic prover 为每个引理写证明、每写一个引理就交 Lean 编译器得到编译信息（含 error 或 info）→ agent 读取后改写引理并迭代 → 最终解决问题。它以远少于 Seed Prover 1 的测试时算力取得当时 SOTA。
三个工具：(1) Lean 编译器——输入引理代码、返回错误信息；(2) Python 工具——做计算，因为有些数学题需要计算、而当时的大模型不擅长很复杂的数学计算，Python 是刚需；(3) 语义搜索工具——在 mathlib 内做语义搜索；mathlib 东西太多，没有搜索工具就只能靠 apply/exact 盲搜，有了它就能知道 mathlib 里有什么。
大规模 RL 细节：Lean 是做 RL 的好地方——有无限数据的 ground truth；但需冷启动（cold start）——若不冷启动，RL 里很难 rollout 出一个正信号；SFT 过程教模型如何用工具、如何做多轮交互。与 Seed Prover 1 类似，有课程式难度控制：过易题直接丢弃、过难题分解或提出更易版让模型尝试。奖励很简单/稀疏：解出题 +1、没解出 −1，不做过程奖励（process reward）——因为"没解出时你真不知道自己走了多远"，所以直接给 −1。训练曲线（约 1200 步）：训练准确率从 50% 升到约 90%（转写此处写作"19 percent"，据上下文应为 ~90%，待核）；有趣的是平均工具调用次数下降——模型变强则出错更少，因而调用少、序列长度也随之下降。有 held-out 的 Putnam 测试子集监测：性能随训练提升；Seed Prover 1.5 取得当时 SOTA，且算力远低于 1.0、能力更高。
持续改进的信条：prover 能力由两要素决定——模型与 harness。团队一直用 RL 提升模型，且同时提升非形式与形式数学推理能力——因为发现"形式推理有时被非形式推理卡住，而非形式推理有时又被形式推理改善"，两者都重要。也一直改进 harness，主张是"少给控制、多给上下文（less control, more context）"：别规定它何时做这、何时做那，只给工具与它所需的全部上下文，让模型自己判断该做什么；因此模型对不同 harness（无论 claude code 还是自研）都很稳健、都能在形式数学推理上表现很好。
可及性与近况：Seed Prover 1/1.5 对多数人无公开访问；但现在可用 Seed 2.5 Pro / Turbo——ByteDance 训练的语言模型，不只是 prover，含多种能力、很擅长多模态推理，已整合了最新的形式推理能力；想试就把它接入你的 harness（如 claude code）去形式化你喜欢的东西，会给"很惊艳的结果"。目前 Seed Prover 在 Lean 社区官方基准 LeanEval 上评测，数月内证了约 116 题（LeanEval 持续加新题，一有新题就测，已证约一半）；证出了 Jordan–Brouwer、Lindemann–Weierstrass 等重要且传统的数学结果。讲者认为：形式推理的一大阻碍是"你想形式化最新证出的猜想，却发现所依赖的项不在 mathlib 里——很令人沮丧"；因此大规模形式化传统数学定理并回馈 mathlib 会极大改善形式数学推理。
两点 takeaway：(1) 模型改进 > harness 改进——一旦训出新模型、性能提升很惊艳，上一版遇到的问题就会消失；(2) RL 非常有用——它持续改进模型；Lean/形式推理是做 RL 的最佳场所，因为总有清晰的正/负信号，而非形式数学推理总要担心"是否破坏了奖励模型"之类。
Q1： 关于 Seed Prover 1.5，你说即使对很长程的任务也只用稀疏奖励。那么 RL 中模型如何学到有效的 credit assignment（信用分配）？为何模型在学会证越来越难的题的同时、轨迹反而变短？ A1： credit assignment 在当下的长程 RL 工作里确实很重要；但 Seed Prover 1.5 其实不算很长程——大约 60k tokens，按如今标准不长。对真正跨天的长程任务，credit assignment 很难，我们也在找解法、目前没有标准答案。
Q2（两个关于 Seed Prover 1.5 的细节问题）： ① 你说用 RL 训练、模型持续改进，还提到"非形式推理"和"形式推理"——能否多讲讲二者的实现？是联合进行的吗？② 能否多解释一下 harness——什么是 harness，它与之前说的 easy/medium/hard 分级有何不同？ A2： ① 关于"如何同时训练非形式与形式数学推理"——这个问题不好答，因为我们没写进 tech report，公司不希望我们在 tech report 里谈，所以这是个难题。② harness 这个可以答：harness 指"你如何约束模型去行动"。如今我们称 Codex / claude code / open code 之类为 harness——它由一个系统提示 + 一组工具定义（你定义一些工具，如编辑文件、读文件等，这组工具就是 harness）。Seed Prover 1 的 harness 是那套 workflow；Seed Prover 1.5 的 harness 只有三个工具（Python、Lean、mathlib 搜索）；而如今用 claude code 你会有约 20 个工具，最新的 Seed Prover 也不止三个工具、可想象成 claude code 或某种通用代码 agent。所以 harness 就是"你定义模型可用的工具集"。我的观点是：给它更少控制是好的、给它更多上下文——真正意味着它能利用你提供的一切（整个 mathlib 文件、Docker、互联网……它想要的一切）。
Q3： 关于 RL 训练用的数据集规模：能谈谈适配该规模的算法、以及你们如何最终定下这个训练数据量吗？ A3： 数据方面：包含开源数据集（如 Numina 或一些非形式数学推理开源集，如 ByteDance 的 豆包/"double" 数据集，我们会自动形式化它）；也自动形式化内部数据集——论文里写了我们自动形式化了许多 GTM（研究生数学教材）问题，因为不想做"只刷基准"的模型、想要广覆盖数学主题，GTM 是很好的代表、非常广。所以数据主要来自这里。算法上——其实就是带 value 预训练的 PPO，用 PPO 做 RL，"算法上没什么特别"；但要把大规模 RL 跑得很顺，需要花很多时间调超参。（主持人随后致谢 Zheng Yuan，进入 workshop 闭幕致辞：感谢所有 keynote 讲者、论文展示者、challenge 参赛者、审稿人、赞助商与志愿者，并提醒下午 4 点开始 Poster Session 2。）