字节模型拿下IMO银牌字节数学模型能复现全过程字节的数学推理模型SeedPro

字节模型拿下IMO银牌字节数学模型能复现全过程

字节的数学推理模型Seed Prover，杀进国际数学奥林匹克（IMO 2025），拿下了银牌。

赛后它还顺手把第1题补了，等于解完了6道题中的前5题。

其中第3题和第4题，模型各花了3天，写出几千行形式化代码，真的是一行一行“死磕”的那种。

背后靠的是引理（Lemma）链（引理是比定理更次要的结果）。

通俗讲，这就是把一道大题拆成几十个小结论，每个结论都能自动验证，像搭积木一样，一层一层往上垒，直到最终通关。

而且这不是靠堆算力硬解的，Seed Prover的“重量级模式”，能自己构造新猜想、反复试错、建出一个引理池，再用里面的关键引理反向喂给自己继续推理。

相比之下，尽管DeepMind在本届IMO中解出5题拿下金牌，OpenAI实验性模型也实现类似水平，但Seed Prover的优势是“可验证”——每一行代码都能形式化复现，不存在跳步。

目前它在多个公开数学测试上都吊打SOTA（最先进模型），Putnam赛题得分翻了5倍，MiniF2F测试基本满分，就连大学组合数学题也能搞定。

Seed Prover已开源部分题目的形式化代码：

- 第 1 题证明：

- 第 2 题证明：

- 第 3 题证明：

- 第 4 题证明：

- 第 5 题证明：