导读： 据学者观察，大型语言模型在形式语言中进行定理证明仍然面临挑战，且计算成本高昂。近日，字节跳动 Seed 团队今日宣布推出新一代形式化数学推理专用模型 Seed Prover 1.5，该模型通过大规模智能强化学习进行训练，并配备了高效的测试时扩展（TTS）工作流程。通过和其他工具的广泛交互，该模型在强...

据学者观察，大型语言模型在形式语言中进行定理证明仍然面临挑战，且计算成本高昂。

近日，字节跳动 Seed 团队今日宣布推出新一代形式化数学推理专用模型 Seed Prover 1.5，该模型通过大规模智能强化学习进行训练，并配备了高效的测试时扩展（TTS）工作流程。

通过和其他工具的广泛交互，该模型在强化学习过程中不断积累经验，从而显著提升了形式定理证明的能力和效率。

此外，TTS 工作流程有效地弥合了自然语言和形式语言之间的鸿沟。与现有方法相比，Seed-Prover 1.5以更小的计算预算实现了更优异的性能。该系统能够解决 PutnamBench（本科水平）88%的问题、Fate-H（研究生水平）80%的问题以及 Fate-X（博士水平）33%的问题。

值得注意的是，利用该系统，Seed 团队在9 小时内解决了 Putnam 2025 中的 12 道题中的 11 道。研究结果表明，以高质量形式化反馈为驱动的经验学习规模化，对未来形式化数学推理的发展具有巨大的潜力。

训练方法

与之前的智能体证明器不同，团队提出了一种更高效的策略，通过增量调用多个工具来逐步构建形式化证明。一旦引理编译成功，它就会被缓存到内存中，并在后续的推理步骤中重用，从而无需重新生成先前已验证的代码。

与基于完整证明生成的方法相比，这种增量缓存机制能够更有效地利用上下文窗口。这种表示方法具有以下几个优点：

• 与模态证明的一致性：与之前提出的引理式证明无缝衔接。

• 复杂度分解：减轻了模型生成完整证明的必要性。相反，模型可以专注于解决眼前的子目标

• 上下文效率：通过顺序缓存有效引理，与必须迭代地重新生成完整证明历史的方法相比，显著降低了上下文开销。

• 灵活的推理控制：能够实现各种推理策略，例如剪除不相关的中间步骤或回溯到特定点重新开始对话。

研究人员设计了几种强化学习训练任务形式，包括直接从形式化语句进行证明、基于自然语言证明概要进行证明，以及基于先前失败尝试的总结进行证明。

他们还提出训练一个草图模型。该模型从形式化语句及其自然语言证明中合成一个引理风格的 Lean 草图。

为了训练这个草图模型，研究团队使用了 VAPO 和混合奖励信号。Lean 编译器确保草图结构的正确性，而 LLM 作为评判标准则作为语义价值模型，采用长链思维 (Long-CoT) 来实现比基于标量模型更好的泛化能力。

Seed-Prover 1.5 协调三个专门的 Agents，包括：

1. 自然语言证明器：一个针对自然语言证明优化的 LLM。

2. Sketch 模型：一种经过训练的翻译代理，可以将自然语言证明转换为 token 的 Lean 草图，有效地弥合非正式推理和正式语法之间的差距。

3. 智能精益证明器：工具集成代理，负责验证每个单独的引理。

实验结果

强化学习训练的准确率从初始化时的约 50% 提升至 1000 步后的近 90%。这一提升主要归功于精心挑选的训练数据集与来自 Lean 验证的准确奖励信号。

平均函数调用次数从约15 次下降到 10 次，这与平均序列长度的持续减少相一致。这表明模型正在学习更策略性地使用工具，避免冗余或“试错”调用。

尽管调用次数有所减少，但模型的推理能力却有所提升。优化步骤的改进表明，智能体处理复杂、长时程问题的能力也日益增强。然而，在 32K–64K 范围内持续存在负分表明，有效处理极长上下文仍然是一个挑战。

Seed-Prover 1.5 在 PutnamBench 上解决了 87.9% 的问题，在 Fate-H 上解决了 80% 的问题，证明了其在处理本科和研究生水平数学形式化证明方面的能力。然而，该系统在处理博士及更高级别的问题时仍然面临挑战，这主要是由于问题复杂性的增加以及 Mathlib 支持的限制。

研究人员表示，系统目前还无法做出与人类专家相媲美的重大数学贡献，这一局限性源于前沿数学研究中固有的关键依赖性问题。

关键的区别在于数学任务的性质：IMO 或 Putnam 数学竞赛的问题经过精心设计，求解者无需了解特定的先前研究论文，而推动数学领域取得重大进展通常依赖于对众多相关论文的综合分析。

要取得这样的进展，需要应对三个相互关联的挑战：

1. 首先，识别最具影响力和最相关的论文；

2. 其次，基于这些论文进行自然语言证明；

3. 第三，开发可扩展的方法，将论文本身及其推导出的结果形式化。

解决这三大挑战将能够大规模生成形式化的数学研究——这一进步最终可能有助于解决某些悬而未决的数学猜想。

参考资料：

https://arxiv.org/abs/2512.17260