Kimi 新模型数学反超 DeepSeek！北大校友刘征瀛等领衔

Kimi 新模型数学超越 DeepSeek 了！

在定理证明这块，即便模型参数 72B 也能超越 DeepSeek-Prover-V2 的 671B 版本，实现 SOTA。

这一新模型来自 Numina 组织和 Kimi 团队联合打造，前者曾在 AI-MO 竞赛中荣获进步一等奖，陶哲轩亲自为他们颁奖。

有意思的是，这俩 AGI 团队不是第一次交手。

两个月前 DeepSeek 刚发布了 DeepSeek-Prover V2 版本，然后直接在普特南测试上将记录刷新到49 道。

当时第一名正好是 Kimina-Prover，而它只能做出 10 道题。

现在 Numina 组织和 Kimi 团队这边，再次又在 miniF2F-test 胜了一筹。

双方真是，打得有来有回的 ~

此次模型是基于 Qwen2.5-72B 打造、采用 Kimi k1.5 强化学习训练流程打造。

主要有两大技术创新，分别是提出了一种可训练的代理证明框架；还提出了一种有针对性的错误修复方法。

新模型还有两个精简版本：Kimina-Prover-Distill-8B 和 1.7B，他们分别基于 Qwen3-8B 和 Qwen3-1.7B。

官方有 Demo 可以体验 ~

Kimi 定理证明模型超越 DeepSeek

那就来看看这次 Kimi 定理证明模型是如何超过 DeepSeek 的吧。

据他们介绍，主要有两大技术创新。

首先是引入测试时强化学习（TTRL）搜索框架。

此前他们已经验证推理范式的可行性。其结构化的推理模式可以实现高效的证明搜索，并模拟了类似人类的问题解决策略。

但是单步推理对于解决需要长篇、多阶段证明的复杂问题仍然不足。

新的框架能让模型自主发现、组合和复用多个中间引理，通过将难题分解为可重用的子组件，支持更深层次、更长远的推理。

△IMO 1969 p2 证明依赖关系图

它主要包括三个部分：强化学习训练、子引理生成和否定过滤。

子引理生成并形式化后，通过动态评分和剪枝集成到训练循环中。否定过滤器通过丢弃无效引理来确保逻辑一致性。

TTRL 搜索的一个关键要素是引理启用模式，它允许模型识别并应用中间引理作为其证明构建过程的一部分。

（引理，也可以叫做辅助定理，为了得到某些更好的结论而作为步骤被证明的命题）。

这种对中间结果的结构化复用显著扩展了模型的解决问题能力，使其超越了单步生成。

TTRL 的一个关键特性是递归搜索机制，搜索范围不仅限于原始定理，也适用于每个引理，这使得框架能够将问题递归地分解为更小的子问题。并行的子引理生成过程贯穿始终，每当一个定理或引理在 N = 128 次尝试后仍未找到证明时，就会生成新的候选子引理。

此外，还引入了一个否定证明过程：对于每个新生成的引理，都尝试证明其逻辑否定。如果否定语句可证明，则表明原始引理在逻辑上不一致，并立即被丢弃。此步骤确保了整个证明构建过程的可靠性和健全性。

回看近期发布的定理证明模型，他们的一个关键限制是，缺乏根据证明助手的反馈来修正证明的能力，这却是人类经常使用的能力。

为了弥补这一缺陷，他们开发了个专门的框架，将错误修复机制集成到模型中，它可以解读 Lean 的错误信息并提出有针对性的修正建议，通过迭代反馈来优化其输出，从而提高证明的可靠性和整体样本效率。

为此，他们构建了个专门用于纠错的 SFT 数据集，还设计了个批量化失败重演策略。

在 RL 的第 N 轮迭代中，系统暂不立即纠正错误，而是完整收集所有失败的证明尝试。进入第 N+1 轮迭代时，训练批次由固定数量的历史失败样本（例如 500 条）与提示集中的标准问题（例如另 500 条）共同组成。这种设计确保模型在每一步训练中都能稳定、高频地接触纠错任务，从而以数据高效的方式逐步掌握有效的错误处理能力。

除此之外，团队还开发了其他几种新技术来增强模型学习过程和解决问题的能力。

比如随机证明切割数据增强、非证明问题求解等。

结果在 miniF2F 基准测试中，Kimina-Prover 在 pass@32 时通过率为 84.0%，在增加一轮纠错后通过率为 86.4%。

在 pass@1024 时，通过率达到 87.7%。

应用完整的测试时强化学习 ( TTRL ) 搜索框架后，最终通过率为 92.2%。

然而，由于当前采样的很大一部分用于证明无用或冗余的引理，在未来版本中他们计划大幅优化此通过次数预算。

来自 Numina&Kimi 团队

这一成果来自 Numina&Kimi 团队联合完成。

Numina 团队是一个非盈利组织，其使命是促进人类和 AI 数学的发展。

官网显示，他们受到 MistralAI、抱抱脸、Anthropic、Meta、北京国际数学研究中心等企业或机构的支持。

此前，他们推出的 Numina Math 7B 模型获得了 AI-MO 竞赛进步一等奖，解答了学生备战奥林匹克竞赛的专用数学难题集中超过一半的题目。

此次项目也有 16 位组织成员参与，其中还有不少华人。

像 Haiming Wang，中山大学博士生，月之暗面研究员，Numina 团队负责人。

Xiaohan Lin，中山大学硕士研究生。

Flood Sung，月之暗面研究员。

刘征瀛，本科毕业于北京大学元培学院，主修物理学和数学，博士毕业于巴黎萨克雷大学，主修 AutoML，加入月之暗面前，原华为诺亚方舟实验室 AI 基础理论团队研究员，现带领团队探索数学和推理方向。

李嘉，Numina 联合创始人，Mistral 前 AI 科学家，Cardiologs 联合创始人兼前 CSO。

好了，接下来就看 DeepSeek 如何应对。（Doge）

Demo 演示：

https://demo.projectnumina.ai/

参考链接：

[ 1 ] https://x.com/JiaLi52524397/status/1943293969745743907

[ 2 ] https://huggingface.co/blog/AI-MO/kimina-prover