北京 – 人工智能领域再传捷报，中国人工智能公司月之暗面（Moonshot AI）联合Numina团队，推出了一款名为Kimina-Prover的大型数学定理证明模型。该模型采用大规模强化学习训练，能够在Lean 4语言中严谨地证明数学定理，并在miniF2F基准测试中取得了80.7%的优异成绩，超越了此前最佳水平10.6%，刷新了该领域的纪录。
Kimina-Prover：AI形式化推理的新突破
Kimina-Prover的独特之处在于其“形式化推理模式”，该模式允许模型在推理过程中穿插非形式化推理和Lean 4代码片段，从而模拟人类解决问题的策略。这种结构化的推理方式，使得模型能够更有效地理解和解决复杂的数学问题。
据了解，Kimina-Prover是首个通过大规模强化学习训练的大型形式化推理模型。与以往的神经定理证明器不同，Kimina-Prover的性能随着模型规模的增大而显著提高，展现出高样本效率和良好的可扩展性。目前，该模型的1.5B和7B参数版本已开源，为学术界和工业界的研究人员提供了宝贵的资源。
技术原理：自动形式化与强化学习
为了构建一个多样化的问题集，研究人员训练了一个模型，将自然语言问题陈述自动翻译成Lean 4代码，并以占位符证明结束。在监督微调（SFT）阶段之后，模型通过强化学习进一步增强其形式化定理证明能力。在每次迭代中，模型会从问题集中采样一批问题，并生成多个候选解决方案，然后使用 Lean 编译器验证这些解决方案的正确性。
性能表现：超越通用大模型
在miniF2F基准测试中，Kimina-Prover不仅取得了80.7%的成绩，超过了此前的最佳水平，而且在IMO和AIME等子集中，也显著优于OpenAI的o3和Gemini 2.5 Pro等通用推理模型。这一结果表明，Kimina-Prover在数学定理证明领域具有显著的优势。
应用场景：潜力无限
Kimina-Prover的应用前景广阔，不仅可以作为科研辅助工具，帮助数学家和研究人员快速验证复杂的数学定理，提供严谨的证明过程，还可以在软件测试、算法验证、风险评估和工程设计验证等领域发挥重要作用。例如，在软件开发过程中，Kimina-Prover可以用于验证软件的逻辑正确性，确保软件的可靠性和稳定性。
开源地址：
- Github仓库：https://github.com/MoonshotAI/Kimina-Prover-Preview/tree/master
- HuggingFace模型库：https://huggingface.co/collections/AI-MO/kimina-prover-preview
- arXiv技术论文：https://arxiv.org/pdf/2504.11354
结语
Kimina-Prover的推出，标志着人工智能在形式化推理领域取得了重要进展。随着模型规模的不断扩大和技术的不断完善，Kimina-Prover有望在数学研究、软件开发、算法验证等领域发挥更大的作用，推动人工智能技术的进一步发展。
参考文献
- Moonshot AI. (2024). Kimina-Prover-Preview. GitHub. Retrieved from https://github.com/MoonshotAI/Kimina-Prover-Preview/tree/master
- AI-MO. (n.d.). Kimina-Prover-Preview. Hugging Face. Retrieved from https://huggingface.co/collections/AI-MO/kimina-prover-preview
- (请注意：由于提供的arXiv链接为虚构，此处无法提供真实的论文引用。如果未来有相关论文发表，请替换为正确的arXiv链接。)
（完）
Views: 0