在人工智能不断发展的当下，自动化定理证明（Automated Theorem Proving, ATP）领域取得重要进步。作为形式化数学推理的核心任务，ATP的目标是利用计算机自动构建严谨的数学证明。Kimina-Prover作为最近兴起的基于大型语言模型和强化学习的形式化定理证明系统，以其在miniF2F标准测试集上达到92.2%的最高通过率，引起了学术界和工业界的广泛关注。该系统不仅刷新了基准成绩，也开创了测试时强化学习（Test-Time Reinforcement Learning, TTRL）在数学推理中的实际应用。Kimina-Prover基于强大的Qwen系列大模型，并结合了诸多创新技术，使其成为当前最先进的自动证明工具之一。Kimina-Prover的核心突破在于其测试时强化学习搜索框架，赋予模型在推理过程中能够自主发现、筛选和组合多个中间引理，从而逐步构建出复杂的多阶段公式证明。
传统的神经定理证明模型多集中于单步生成策略，面对长逻辑链条和多层推理时往往力不从心。TTRL框架通过引入引理启用模式，指导模型主动利用潜在有用的引理显著提升了推理深度和质量，尤其在处理需要多重分解的难题时表现尤为出色。引理启用模式是Kimina-Prover设计中的一个关键创新。在强化学习训练阶段，向模型输入中随机加入一至三个潜在引理，使模型具备识别及利用中间引理的能力。更重要的是通过偏好奖励机制加强模型倾向于选择并正确应用引理，将引理的利用率稳定提升至30%至40%。这一设计不仅模拟了人类数学家利用已知定理辅助证明的过程，也让模型学会了“合理取舍”，提升推理效率，使其更接近人类的解决问题习惯。
除了引理发现与应用，Kimina-Prover另一项突破性的能力是其错误修正机制。Lean 4作为严格的定理证明助手，会在证明代码出现错误时生成详细的错误信息。Kimina-Prover能够读取、理解并根据反馈迭代修改证明内容。为此，团队构建了专门的有监督微调数据集，包含错误证明、Lean错误反馈及对应正确修正的样本，同时融入了由大语言模型生成的逐步修正推理链，增强模型理解与修正复杂错误的能力。在实际操作中，通过“批量失败重放”训练策略，模型稳定提升了错误修正的成功率，逐步能够修正从语法到逻辑的大量错误，显著减少了无效反复尝试的计算资源浪费。Kimina-Prover所采用的强化学习训练流程亦体现了对数据的精细打磨。
团队精选了约9万条以奥林匹克竞赛级别为主的高质量数学证明问题集，对问题进行动态筛选与分解，使训练任务保持合理难度和挑战性。充足且多样化的训练数据为模型提供了广泛的数学知识基础，有助于其在测试时灵活应对不同数学问题。此外，团队还利用了持续预训练技术，加强模型对Lean语言的理解能力，构建了一个涵盖在线代码仓库、大规模强化学习生成数据及丰富状态转换信息的6亿词元数据集，以提升模型的语境理解和推理连贯性。为了充分利用大量缺乏完整推理步骤的人类标注证明，Kimina-Prover引入了随机证明截断与推理填充策略。通过截断证明的最终部分，或者在证明任意位置以占位符替代，使模型必须补全缺失的步骤。这一方法有效促进了模型在局部推理重构与整体证明完成之间的协调，为模型打开了处理不完整数据的通道，提升了实际应用中的鲁棒性。
Kimina-Prover同样创新地实现了非证明问题求解，如某些题目只需给出最终答案。模型先自动推导结果，再生成完整证明以论证此答案正确性，确保了结果与过程的内在一致性，增强了模型整体的逻辑严密性。Kimina-Prover不同规模的模型都取得了显著成绩，其中基于Qwen2.5-72B的Kimina-Prover-72B版本在miniF2F测试集上的pass@1达到63.9%，pass@32达到84%, 并通过一轮错误修正提升至约86.4%，在更大采样预算下达到87.7%。整合完整测试时强化学习搜索后，最终突破92.2%的历史最高通过率，远超过去深度学习定理证明模型的表现。性能提升并非单纯依赖大量采样，而是因应复杂推理需求引入了更为高效的搜索策略，避免了无用推理路径的资源浪费。同时，对产生的引理进行负否定证明检测步骤，保障了推理过程的逻辑一致性，避免了不正确或矛盾引理对整体证明的破坏。
Kimina-Prover的诞生标志着神经定理证明进入了一个新的阶段，不再像过去那样局限于单步推理或盲目生成，而是逐步迈向了具备自主规划推理结构、基于反馈修正错误以及动态利用中间信息的智能化系统。展望未来，这类系统有望在定理发现、复杂数学推导乃至科学计算中扮演更为重要的角色。结合强化学习的自适应搜索策略与错误修正能力，Kimina-Prover展示了实现持续提升的巨大潜力。进一步优化样本利用效率、引理筛选机制以及推理搜索策略，将成为推动下一代自动证明系统前进的关键。Kimina-Prover项目不仅在技术层面展现了强大的创新力，也推动了开源社区的协作精神。团队已发布多个模型版本及示例证明代码，供研究者和开发者借鉴和扩展，促进自动定理证明技术的普及和产业化应用。
总结而言，Kimina-Prover通过测试时强化学习框架、引理启用设计和错误修正机制，成功提升了自动数学定理证明的性能和效率，在miniF2F这一权威测试平台上实现了92.2%的突破，成为当前最具代表性的智力AI系统之一。这项成果不仅拓展了大型语言模型在形式化数学领域的边界，也为未来智能推理系统的发展奠定了坚实基础。随着自动证明技术日趋成熟，无疑将为科研创新、教育辅助以及自动化推理系统带来深远影响。
