白交 发自 凹非寺
量子位 | 公众号 QbitAI
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/
（文：量子位）