Kimina

Kimina-Prover简介

Kimina-Prover是由月之暗面与Numina团队联合开发的大型数学定理证明模型，采用大规模强化学习技术进行训练，能够在Lean 4语言中以类似人类的方式进行逻辑推理并严谨地证明数学定理。该模型引入了“形式化推理模式”，在推理过程中结合非形式化推理和Lean 4代码片段，更贴近人类解决问题的策略。在miniF2F基准测试中，Kimina-Prover取得了80.7%的准确率，超越了此前最佳水平10.6%，表现突出。随着模型规模和计算资源的增加，其性能显著提升，展现出良好的可扩展性和样本效率。目前，1.5B和7B参数版本已开源。

主要功能

• 基于强化学习：Kimina-Prover是首个通过大规模强化学习训练的形式化推理模型，能够以类人方式在Lean 4中进行数学定理证明。
• 结构化推理模式：模型采用“形式化推理模式”，在推理过程中结合非形式化推理与Lean 4代码片段，模拟人类解题策略。
• 高样本效率：即使在有限采样条件下，也能取得良好结果，且性能随计算资源增加而显著提升。
• 性能与规模正相关：相比以往模型，Kimina-Prover的性能随模型规模扩大而明显增强。

技术原理

• 自动形式化：研究人员训练模型将自然语言问题自动转换为Lean 4代码，并以占位符证明结尾，构建多样化问题集。
• 强化学习训练：在监督微调后，模型通过强化学习进一步提升形式化定理证明能力，每次迭代从问题集中采样并生成候选解决方案，由Lean编译器验证正确性。

性能表现

• 基准测试成绩：Kimina-Prover在miniF2F基准测试中获得80.7%的准确率，超过SOTA模型10.6%。
• 对比通用大模型：在miniF2F及其子集（如IMO、AIME）中，Kimina-Prover的表现优于OpenAI的o3和Gemini 2.5 Pro等通用模型。

项目信息

• 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

应用场景

• 科研辅助：可用于数学研究中验证复杂定理，提供严谨的证明流程。
• 软件测试：支持验证软件逻辑正确性，提升系统稳定性。
• 算法验证：用于验证人工智能算法的理论正确性。
• 风险评估：在金融领域验证模型的数学基础。
• 工程设计验证：用于建筑、机械等领域验证设计的数学模型。