月之暗面Kimi开源数学定理证明模型Kimina-Prover
发布时间：2025-04-17 08:59:42 | 责任编辑：字母汇 | 浏览量：15 次
Moonshot AI开放平台的API接口Kimi 技术团队近日发布了 Kimina-Prover 预览版的技术报告，并开源了1.5B 和7B 参数的模型蒸馏版本、用于数据生成的 Kimina-Autoformalizer-7B 模型以及修订过的 miniF2F 基准测试数据集。Kimina-Prover 是由 Numina 和 Kimi 团队联合研发的一款数学定理证明模型，它在形式化定理证明领域采用了一种新颖的、由推理驱动的探索范式，展现出极佳的性能。
Kimina-Prover 基于 Qwen2.5-72B 模型，并结合 Kimi k1.5的大规模强化学习（RL）流程进行训练。在权威的 miniF2F 形式化数学基准测试中，Kimina-Prover 预览版以更低的采样预算(pass@8192)达到了80.7% 的通过率，显著超越了之前的最佳结果:BFS Prover 的72.95%(pass@2048×2×600+)和 DeepSeek-Prover 的50.0%(pass@65536)。
形式化定理证明是数学和计算机科学领域的一个重要方向，它应用严格的数学逻辑和计算机程序来验证数学定理的正确性。然而，让 AI 掌握形式化证明极具挑战，传统方法往往难以应对复杂、需要深刻洞察力和创造力的数学问题。近年来，大语言模型（LLM）的兴起为这一领域带来了新的希望，但现有方法大多存在局限，如依赖外部搜索、难以捕捉深度推理、缺乏模型规模效应等。
为了克服这些局限，Kimina-Prover 采用了新的路径，将大规模强化学习（RL）与“形式化推理模式”深度结合，直接优化模型生成完整证明的内部“策略”。这种方法使得模型能够在生成 token 的过程中隐式地探索庞大的证明空间，自主地导航推理路径，极大地降低了计算开销，并赋予了模型更灵活、更接近人类直觉的探索方式。此外，Kimina-Prover 还引入了基于最终结果的奖励信号，强化学习的训练过程是目标导向的，只有完全正确、能通过编译的证明才能获得正奖励。
Kimina-Prover 的初步研究成果取得了显著进展。在 miniF2F 基准测试中，Kimina-Prover 达到了80.7% 的通过率，显著超越了之前的最佳结果。它还展现出极高的样本效率，即使在极少采样次数下也能取得有竞争力的结果。此外，Kimina-Prover 的性能随着模型参数规模的增大而持续提升，这是首次在形式化数学领域的神经定理证明器中观察到如此明确的规模效应。与顶尖的通用推理大模型相比，Kimina-Prover 在形式化数学任务上展现出压倒性优势，能够稳定生成形式正确、可通过 Lean 编译器检查的证明。
Kimina-Prover 的思考过程具有很高的可解释性，用户可以查看模型是如何一步步推导出证明的，这为理解模型行为、诊断失败原因提供了便利，也使其具备成为数学教育辅助工具的潜力。研究团队表示，Kimina-Prover 的性能能够随着模型规模和上下文长度的增加而显著扩展，初步验证了“基于推理的神经证明器”的潜力。这种结合了大规模强化学习和类人推理模式的方法，将为自动化推理乃至通用人工智能（AGI）的发展开辟新思路。
为了推动社区的参与和研究进展，Kimi 技术团队开源了 Kimina-Prover 的1.5B 和7B 参数的蒸馏版本，用于数据生成的 Kimina-Autoformalizer-7B 模型，以及修订过的 miniF2F 基准测试数据集。
Arxiv 技术报告:https://arxiv.org/abs/2504.11354
月之暗面与 Numina 团队合作推出了数学定理证明模型 Kimina-Prover，以下是关于该模型的详细介绍：
模型概述
Kimina-Prover 是一款大型数学定理证明模型，采用大规模强化学习训练，能够以类似人类的方式进行推理，并在 Lean 4 语言中严谨地证明数学定理。它开创了一种新颖的由推理驱动的探索范式，通过独特的“形式化推理模式”，在推理过程中穿插非形式化推理和 Lean 4 代码片段，模拟人类解决问题的策略。
技术原理
- 自动形式化：研究人员训练了一个模型，将自然语言问题陈述自动翻译成 Lean 4 代码，并以占位符证明结束，从而构建多样化的问题集。
- 强化学习训练：在监督微调（SFT）阶段之后，模型通过强化学习进一步增强其形式化定理证明能力。在每次迭代中，模型会从问题集中采样一批问题，并生成多个候选解决方案，然后使用 Lean 编译器验证这些解决方案的正确性。
性能表现
- 基准测试成绩：在 miniF2F 基准测试中，Kimina-Prover 取得了 80.7% 的成绩，超过此前最佳水平（SOTA）模型 10.6%，创下新高。
- 样本效率高：即使在采样次数较少的情况下，Kimina-Prover 也能取得较好的结果，随着计算资源的增加，性能会显著提升。
- 模型规模与性能正相关：与以往的神经定理证明器不同，Kimina-Prover 的性能随着模型规模的增大而显著提高。
开源信息
Kimina-Prover 的 1.5B 和 7B 参数的蒸馏版本已开源，开源内容还包括用于数据生成的 Kimina-Autoformalizer-7B 模型以及修订过的 miniF2F 基准测试数据集。开源地址如下：
- GitHub 代码库：
- Hugging Face 模型下载：
应用场景
- 科研辅助：帮助数学家和研究人员快速验证复杂的数学定理，提供严谨的证明过程。
- 软件测试：在软件开发过程中，验证软件的逻辑正确性，确保软件的可靠性和稳定性。
- 算法验证：在人工智能和机器学习领域，验证算法的正确性和可靠性。
- 风险评估：在金融领域，验证风险评估模型的数学基础，确保这些模型的准确性和可靠性。
- 工程设计验证：在工程设计中，验证设计的数学模型和公式，确保设计的稳定性和安全性。
本网站(https://aigc.izzi.cn)刊载的所有内容，包括文字、图片、音频、视频等均在网上搜集。
访问者可将本网站提供的内容或服务用于个人学习、研究或欣赏，以及其他非商业性或非盈利性用途，但同时应遵守著作权法及其他相关法律的规定，不得侵犯本网站及相关权利人的合法权利。除此以外，将本网站任何内容或服务用于其他用途时，须征得本网站及相关权利人的书面许可，并支付报酬。
本网站内容原作者如不愿意在本网站刊登内容，请及时通知本站，予以删除。
