字节跳动Seed-Prover：自动化数学证明领域的SOTA突破

大型语言模型（LLMs）在数学推理方面取得了显著进展，通常利用其自然语言能力来提高在MATH和AIME等基准测试上的表现。然而，使用强化学习（RL）训练这些模型的一个关键挑战是难以验证自然语言证明的正确性，这通常需要对每一步进行细致的手动检查。这一限制阻碍了RL在开发数学定理证明模型方面的更广泛应用。虽然Lean等形式语言提供了自动的正确性验证，但当前基于LLM的形式证明器仍然面临局限性。例如，步级证明器可以逐步生成代码，但通常需要特定的结构支持，并且难以进行高层次推理。

为此，字节跳动的Seed团队推出了Seed-Prover，这是一种新颖的引理式全证明推理模型。Seed-Prover通过整合来自Lean的反馈、利用先前已建立的引理以及采用自我总结，迭代地完善证明。它在测试时集成了三种专门的推理策略，从而实现了深入而广泛的推理能力，能够解决复杂问题，包括国际数学奥林匹克（IMO）中的问题。其核心创新在于采用引理式证明方法，将推理过程集中于引理，而非传统的逐步骤或单一全证明生成方法。作为补充，Seed-Geometry也同时推出，它是一个专门的几何推理引擎，旨在克服Lean在处理几何问题方面的局限性。

Seed-Prover与Lean之间的交互由一个基于VAPO的多阶段、多任务强化学习框架促进。训练数据集结合了公开数据集和字节跳动内部的形式化问题。一个“提议器”组件用于生成困难任务的简化变体，而过于简单的问题（证明率高于25%）则被排除。Seed-Geometry的后端支持大规模问题生成，在七天内识别了超过2.3亿个独特问题，搜索效率提高了八倍。尽管训练了单独的策略模型和价值模型，但广泛测试表明，价值模型有时会因估计误差而降低性能，因此在分布式设置中采用了带束搜索的逐步生成方法。

Seed-Prover在多项数学基准测试中取得了最先进的成果。在2025年IMO中，Seed-Prover成功解决了6道题目中的5道；具体来说，Seed-Geometry即时解决了第2题，而Seed-Prover则使用各种推理设置推导了其余问题的证明。在过去的IMO问题上，它在155个任务中证明了121个，在所有难度级别上取得了78.1%的成功率。这一表现包括解决了55道简单问题中的47道，56道中等问题中的47道，以及44道难题中的27道。分学科的成功率也很高，代数85道中72道，数论55道中42道，组合学14道中7道。

在MiniF2F基准测试中，研究人员报告称，在中等设置下，验证集和测试集的证明率均达到99.6%，成功解决了IMO 1990 P3等具有挑战性的问题。PutnamBench的结果显示，从轻量级推理设置升级到中等设置后，在657个问题中，解决的问题数量从201个显著提高到331个，这标志着相对于之前的本科级别数学推理系统有了显著的性能飞跃。尽管Seed-Prover在CombiBench上解决了100个组合学问题中的30个，超越了现有方法，但结果也凸显了组合推理方面持续存在的挑战。此外，Seed-Prover在MiniCTX-v2上取得了81.8%的成功率，展示了超越特定竞赛问题的强大泛化能力，并超越了o4-mini基线在Pass@8上的44.3%。

总而言之，字节跳动的Seed团队推出了Seed-Geometry和Seed-Prover，这两种形式化推理方法有效地整合了LLM的能力。Seed-Geometry为几何问题提供了加速验证和增强搜索机制，而Seed-Prover则利用迭代细化和复杂的测试时推理策略进行通用数学证明。在2025年IMO中解决6道题目中的5道的成就，凸显了这些方法在应对精英数学竞赛方面的实际效用。采用Lean等形式语言提供了快速的证明验证，这比人类专家更具成本效益，也比基于LLM的评判系统更可靠。未来的研究将致力于进一步结合形式系统与LLM，以解决开放的数学猜想。