Kimina-Prover:不挂搜索树,靠整证生成 RL 把 miniF2F 推到 92.2%
kimina-prover
Moonshot AI 与 Numina 的 Lean 4 定理证明线,立场逆主流:训练与推理均无 prover 中间反馈,不用 MCTS、价值函数与过程奖励模型(arXiv:2504.11354),搜索内化成一次整证生成;Formal Reasoning Pattern 先写结构化自然语言草稿再落 Lean 代码,把稀疏二值奖励重述成语言问题。底座 Qwen2.5-72B、上下文 32K。两代分开读:Preview(2025-04)miniF2F-test 80.7%(pass@8192);72B(2025-07-10)加 TTRL 搜索与错误修复后 92.2%,是收录时最高公开读数,卡片取此数,同口径 pass@1 仅 63.9%。等预算 pass@1/32/1024 为 63.9/84.0/87.7,三档全领先 671B DeepSeek-Prover-V2(61.9/82.4/86.6)。打折:对照表由 Kimina 团队发布、DeepSeek 两行为其复跑;仓库未声明许可证;miniF2F 仅 244 题且已过 92%,区分度在衰减。该域无第三方榜,读数只读作方向。置信度 C(厂商宣称):未在固定 commit 复算。
- 置信度
- 厂商宣称
- 只有官方模型卡/发布会,无独立复测
- 关键指标
- miniF2F(TTRL 搜索后)
- 厂商宣称 · 2025-07
- 成熟度
- 研究
- 研究 → 演示 → 产品 → 生产
编辑判断评为 C 档(厂商宣称)。判断逻辑和 DeepSeek-Prover-V2 那条一模一样:证明文本可机械核验,但那个 92.2% 没跑过。仓库公开、蒸馏模型可下载、证明 ZIP 可逐条喂给 Lean,任何人有算力都能复核;这件工作没做,所以不把自己没验过的数字升成 A。C 档在这里是诚实,不是贬低。
它最有价值的贡献不是分数,是两条被数据支撑的路线判断。第一,规模效应在神经定理证明上成立:Preview 之前这条曲线没被清楚观察到,72B 打赢 671B 的 DeepSeek-Prover-V2(pass@1 63.9 对 61.9、pass@1024 87.7 对 86.6)进一步说明RL 配方比底座参数量更值钱——这对资源有限的团队是极其重要的信号,它意味着不必先有一个 671B 才能做前沿证明器。第二,Formal Reasoning Pattern 把稀疏奖励问题重新表述成了语言问题,这是他们敢不用 PRM 与 MCTS 的底气所在。
但这条线自己的演化说明「无反馈整证生成」不是终局:72B 那一代把 prover 报错读回来了,也引入了测试时搜索(TTRL + 引理复用)。Preview 到 72B 的三个月里,先前被刻意省掉的机制按需加了回来——这在工程上是正常路线,但读者不该把 Preview 的立场当成这个域的结论。读数要读结构而不是读单点:pass@1 63.9% 到 pass@1024 87.7% 之间那 23.8 个百分点,才是这个模型的真实成本曲线;而 miniF2F 被推到 92%+ 之后,这个基准对区分前沿模型的信息量已经接近耗尽。最后两点风险必须摆在明面上:仓库没有 LICENSE 字段,商用复用前要逐个确认 Hugging Face 上的模型许可;那张漂亮的等预算对照表是 Kimina 团队自己复跑的,DeepSeek 与 DSP+ 的行不是原厂口径。
它解决的问题:把证明搜索从符号系统搬进语言模型
自动定理证明有两条老路。一条是符号搜索(dsuper、tactic 级的树搜索),可靠但每换一类命题就要重写启发式;另一条是端到端神经模型,泛化好但在 Lean 4 上长期停在 50%-70% 的通过率,因为训练信号太稀疏——一道竞赛题要么整证通过要么全错,中间没有梯度可学。Kimina-Prover 的选择是第三条:把大规模强化学习直接做在整证生成上,不给模型任何 prover 中间反馈,让它像人一样先写推理草稿、再落成 Lean 代码。
这条路线的赌注是:只要模型够大、上下文够长、RL 规模够大,「搜索」这件事可以被内化成一次生成,而不需要外挂一棵搜索树。Preview 那篇技术报告(arXiv:2504.11354)明确写了这个立场——他们刻意不用蒙特卡洛树搜索、不用价值函数、不用过程奖励模型(PRM),与 Kimi k1.5 的结论一致。这在当时是逆主流的:AlphaProof 那条线正是靠海量搜索换质量。
两代读数:Preview 的 80.7% 与 72B 的 92.2%
Kimina 有两代公开读数,时间相隔不到三个月,必须分开写清楚,否则很容易把两个数混成一个。
- Kimina-Prover Preview(2025-04):在 miniF2F-test 上拿到 80.7%(pass@8192),是当时公开结果里第一个越过 80% 的,超过此前的 SOTA BFS-Prover(72.9%),也超过 Hunyuan-Prover、DeepSeek-Prover 与 Leanabelle-Prover。它在小采样预算下同样站得住:pass@32 68.85%、pass@8 65.16%,这一点比只看 pass@8192 的读数更有说服力。
- Kimina-Prover-72B(2025-07-10):加上 TTRL 搜索与错误修复后,miniF2F 通过率达到 92.2%,是本站收录时这个基准上的最高公开读数。
72B 那篇博客给了一张等采样预算的对照表,这是整个域里少有的、把不同模型放在同一横轴上的数据,值得逐行读:
| 模型 | pass@1 | pass@32 | pass@1024 |
|---|---|---|---|
| Kimina-Prover-1.7B | 46.7 | 73.4 | — |
| DSP+ | 52.5 | 71.3 | 80.7 |
| DeepSeek-Prover-V2-7B | 58.6 | 75.6 | 79.9 |
| Kimina-Prover-8B | 61.1 | 78.3 | — |
| DeepSeek-Prover-V2-671B | 61.9 | 82.4 | 86.6 |
| Kimina-Prover-72B | 63.9 | 84.0 | 87.7 |
三件事从这张表里读出来。第一,72B 打赢了 671B:用不到十分之一的参数在三个预算档上全部领先,这是「RL 配方比底座规模更值钱」的直接证据。第二,pass@1 到 pass@1024 涨了 23.8 个百分点(63.9 → 87.7),说明这个模型的能力有很大一部分要靠采样买回来,单次调用的真实水位是 63.9%。第三,8B 蒸馏版(61.1)已经接近 671B 的 DeepSeek-Prover-V2(61.9),小模型部署这条路是通的。
⚠ 这张表由 Kimina 团队自己发布,表里的 DeepSeek 两行是他们的复跑结果,不是 DeepSeek 官方口径。DeepSeek 自己报的 MiniF2F-test 是 88.9%(更高采样预算),两个数字并不矛盾,只是横轴不同。本站因此把两条资产并列收录而不排名次。
技术路线的四个选择
| 选择 | 具体做法 | 代价与收益 |
|---|---|---|
| 整证生成,无 prover 反馈 | 训练与测试阶段都不给中间反馈,一次生成完整证明 | 工程简单、可端到端 RL;代价是样本效率低,要靠大预算采样补 |
| 模型规模 scaling | 底座 Qwen2.5-72B,证明「神经定理证明器也存在规模效应」 | 此前学界普遍没观察到这条曲线,是 Preview 的主要科学贡献之一 |
| 长上下文 | RL 训练与推理上下文最长 32K tokens | 当时神经定理证明社区最长;长证明与 mathlib 引理签名装得下 |
| Formal Reasoning Pattern | 自定义推理格式,在形式化验证与非形式化数学直觉之间搭桥 | 让模型先写「人话草稿」再落 Lean,是 RL 能收敛的关键设计 |
其中 Formal Reasoning Pattern 是最容易被忽略、但实际影响最大的一环。纯 Lean 输出对 RL 来说几乎是不可学的:动作空间是战术语法,奖励是稀疏二值。让模型先产出一段结构化的自然语言推理、再翻译成形式化代码,等于把稀疏奖励问题重新表述成语言模型本来就擅长的问题。这也解释了为什么他们敢不用 PRM——推理草稿本身就承担了过程监督的一部分职能。
72B 那一代新增的两件事
Preview 到 72B 之间,单一整证生成的天花板暴露了出来:需要长链条、多阶段引理的难题,一步生成解不出来。72B 的两个新增正是针对这个:
- TTRL 搜索(Test-Time Reinforcement Learning)+ lemma-enabled pattern:一个可训练的 agentic 证明框架,让模型在测试时递归地发现、组合、复用多个中间引理。它不是外挂的符号搜索器,而是把「拆引理」这件事也变成了模型学得会的动作。84.0% 的 pass@32 读数就是在这套框架下拿到的。
- 错误修复能力:模型能读懂 Lean 的报错信息并给出定向修补。博客给的对照是:pass@32 84.0% → 加一轮错误修复 86.4% → pass@1024 87.7% → 完整 TTRL 搜索 92.2%。关键在于修一条错证明比从零重生成便宜得多,这直接改善的是样本效率,而不是单点准确率。
注意这两个新增的方向恰好和 Preview 的立场相反:Preview 强调「不需要 prover 反馈」,72B 开始读 prover 的报错;Preview 强调「不需要搜索」,72B 引入了测试时搜索。这不是自相矛盾,而是一条很典型的路线演化——先用最简配方把基线推到 80%,再把省掉的那些机制按需加回来。本站把两代写在同一条资产里,就是为了让这个演化过程可见。
开源面:比模型本身更有复用价值的部分
- 蒸馏模型:Kimina-Prover-Distill-8B(底座 Qwen3-8B)与 1.7B(底座 Qwen3-1.7B),Preview 那一代是 7B 与 1.5B。8B 蒸馏版在 miniF2F 上 61.1% pass@1,是单卡可跑的水位。
- autoformalization 模型:把自然语言命题翻译成 Lean 陈述。这是整条流水线里唯一没有通过率光环、但实际使用中最先失败的一环,单独放出来很有价值。
- Kimina Lean Server(project-numina/kimina-lean-server,约 211 stars):他们整个训练过程用的 Lean 服务与客户端 SDK。做形式化 RL 的团队真正缺的往往不是模型,是一个能扛住高并发检查请求的 Lean 服务,这一件的工程复用价值最高。
- 修正版 miniF2F-test:他们发现原基准至少 5 道题形式化写错了,并发布了修正版。这是「模型强到开始反过来审基准」的实例——任何还在用原版 miniF2F 的读数都和修正版不可直接比。
- 证明文本:Preview 在 miniF2F-test 上找到的全部证明以 ZIP 发布(压缩以防污染训练数据)。
边界
- 92.2% 是搜索后的读数,不是单次调用:pass@1 只有 63.9%。生产成本要按「采样 + 搜索 + 错误修复轮次」算,不是按一次 API 调用算。
- miniF2F 已接近饱和:一个 244 道题的高中/竞赛级基准被推到 92%+,它对区分前沿模型的信息量正在迅速衰减。这个域下一步的尺子应该是 PutnamBench、Erdős 问题这类真正难的集合,而本站目前还没有接入。
- 仓库未声明开源许可证:实测 GitHub 的 license 字段为空。技术报告、README、证明 ZIP 都能读,但代码与权重的法律复用边界不清,商用前必须单独确认 Hugging Face 上各模型的许可条款。
- 对照表是自家复跑:表里 DeepSeek 与 DSP+ 的行由 Kimina 团队执行,协议细节(采样温度、mathlib 版本、Lean 版本)未逐项公开,严格说属于厂商宣称档次的横向比较。
- 只覆盖 Lean 4:Isabelle、Coq 不在能力面内;autoformalization 那一步的错误率也不在任何通过率数字里。
我们的核验状态
事实来自三处实读:MoonshotAI/Kimina-Prover-Preview 的 GitHub README 全文(376 stars / 32 forks,默认分支 master,最后推送 2025-07-10)、Hugging Face 博客《Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models》(2025-07-10,含上表逐行数据)、以及技术报告 arXiv:2504.11354。仓库、证明 ZIP、蒸馏模型都是公开的,任何人都可以在 Lean 4 里独立核验证明文本。
置信度记 C(厂商宣称),理由和 DeepSeek-Prover-V2 那条完全一致:本站没有跑过这些证明。我们没有在固定的 Lean 4 + mathlib 版本上复算 92.2%,没有复跑那张对照表里 DeepSeek 的两行,也没有在修正版 miniF2F-test 上把两家重新拉到同一横轴。要升到 A 档,需要:锁定 Lean 4 与 mathlib 的 commit、下载证明 ZIP 逐条喂给检查器统计真实通过率、在等采样预算下同时复跑 Kimina 与 DeepSeek-Prover-V2、并把 pass@1 与 pass@8192 两个口径都报出来。
另外要说清一件我们做不到但读者该知道的事:这个域没有第三方榜。本站同步的 12 个第三方榜单里没有任何形式化数学基准,所以这里的所有读数都来自各家自报,横向比较只能读作方向。