Seed-Prover：用于自动定理证明的深度和广度推理

大型语言模型（LLMs）通过利用强化学习和长思维链，展现了强大的数学推理能力，但由于仅使用自然语言时缺乏明确的监督信号，它们在定理证明方面仍然存在困难。像 Lean 这样的专用领域语言通过对证明进行形式化验证来提供清晰的监督，从而能够通过强化学习进行有效训练。在这项工作中，我们提出了 Seed-Prover，一个引理式的全证明推理模型。Seed-Prover 可以根据 Lean 的反馈、已证明的引理和自我总结来迭代地优化其证明。为了解决国际数学奥林匹克（IMO）级别的竞赛问题，我们设计了三种测试时推理策略，以实现深度和广度推理。Seed-Prover 证明了 78.1% 的形式化往届 IMO 问题，在 MiniF2F 数据集上达到了饱和，并在 PutnamBench 上取得了超过 50% 的成绩，大幅超越了之前的最先进水平。为了解决 Lean 中缺乏几何支持的问题，我们引入了一个几何推理引擎 Seed-Geometry，其性能优于之前的形式化几何引擎。我们使用这两个系统参加了 2025 年的 IMO，并完全证明了 6 个问题中的 5 个。这项工作代表了自动化数学推理领域的一项重大进展，展示了形式化验证与长思维链推理相结合的有效性。