字节小组发布原创自动定理验证工具 Seed-Prover，有效迎战 IMO2025难题
发布时间：2025-08-04 12:22:27 | 责任编辑：张毅 | 浏览量：5 次
在最近的国际数学奥林匹克（IMO2025）比赛中，ByteDance Seed 团队的自动定理证明系统 Seed-Prover 表现出色，成功解决了比赛中的四道题目。这一成果标志着 Seed-Prover 在数学证明领域的重要进展，并展示了人工智能在复杂数学问题求解中的潜力。
Seed-Prover 是 ByteDance Seed 团队的一项重要研究项目，旨在通过深度学习和广泛推理技术，提升自动定理证明的能力。在 IMO2025比赛中，该系统在紧张的竞赛环境中表现优异，成功解决了以下题目:
尽管 Seed-Prover 在比赛中取得了显著的成绩，但目前该项目尚未公开其模型权重，用户仅能访问项目资料和相关论文。团队计划在未来进一步发布更多信息，以便于学术界和开发者们能够更好地理解和应用这一系统。
ByteDance Seed 团队的这一成就不仅为自动定理证明领域注入了新的活力，也为数学研究提供了新的工具，期待未来能够看到更多的应用与发展。
论文地址:https://arxiv.org/abs/2507.23726
repo地址:https://github.com/ByteDance-Seed/Seed-Prover
字节跳动 Seed 团队开发的自动定理证明系统 Seed-Prover 于 IMO 2025 比赛中表现出色，成功解决了 6 道题目中的 4 道（包括部分第 5 题），最终获得 IMO 官方认证的 30 分，相当于银牌成绩（得分分布为 2/7/7/7/7/0）。具体表现如下：
-
第 2 题（几何）：2 秒内完成证明。
-
第 3 题（数论） 和 第 4 题（数论）：分别耗时 3 天，生成 2000 行和 4000 行形式化证明。
-
第 5 题（组合学 / 代数）：1 天内完成，其证明方法与人类已知解法略有不同。
-
第 1 题（组合学）：赛后通过额外 4 天搜索完成完整证明（4000 行形式化证明）。
Seed-Prover 基于 Lean 验证器构建，通过 多阶段强化学习训练 和 多层次测试时扩展策略（轻量级、中量级、重量级）实现复杂数学问题的长链思维推理。此外，Seed-Prover 还在多个形式化推理基准测试中表现优异，成功证明了 79% 的此前已形式化的 IMO 题目，并解决了 MiniF2F 基准中的大部分问题及北美大学级别 Putnam 竞赛题中过半数的问题。
尽管目前模型权重尚未公开，团队计划未来进一步发布更多信息，以供学术界和开发者参考。
本网站(https://aigc.izzi.cn)刊载的所有内容，包括文字、图片、音频、视频等均在网上搜集。
访问者可将本网站提供的内容或服务用于个人学习、研究或欣赏，以及其他非商业性或非盈利性用途，但同时应遵守著作权法及其他相关法律的规定，不得侵犯本网站及相关权利人的合法权利。除此以外，将本网站任何内容或服务用于其他用途时，须征得本网站及相关权利人的书面许可，并支付报酬。
本网站内容原作者如不愿意在本网站刊登内容，请及时通知本站，予以删除。
