Kimina-Prover Preview：面向大规模形式推理模型的强化学习方法
人工智能
2025-04-16 v1
摘要
我们介绍 Kimina-Prover Preview，这是一种大型语言模型，标志性地采用一种新颖的以推理为导向的探索范式进行形式定理证明，如本预览版所示。该模型基于 Qwen2.5-72B 训练，Kimina-Prover 在 Lean 4 证明生成中展现出强大的性能，通过采用我们称之为 "形式推理模式" 的结构化推理模式实现。该方法使模型能够模拟人类在 Lean 中的问题解决策略，迭代生成和细化证明步骤。Kimina-Prover 在 miniF2F 基准测试上取得了新的最先进成绩，达到 80.7%（pass@8192）。除了改进的基准性能之外，我们的工作还带来了若干关键见解：（1）Kimina-Prover 具有高样本效率，即使在最小采样（pass@1）情况下也能取得强劲结果，并能随计算预算有效扩展，源于其独特的推理模式和 RL 训练；（2）我们展示了模型规模与性能的明确扩展趋势，这一以前在神经定理证明器用于形式数学中未观察到的趋势；（3）所学到的推理风格，不同于传统搜索算法，显示出桥接形式验证与非形式数学直觉的潜力。我们开源了规模为 1.5B 和 7B 参数的 Kimina-Prover distilled 版本。
引用
@article{arxiv.2504.11354,
title = {Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning},
author = {Haiming Wang and Mert Unsal and Xiaohan Lin and Mantas Baksys and Junqi Liu and Marco Dos Santos and Flood Sung and Marina Vinyes and Zhenzhe Ying and Zekai Zhu and Jianqiao Lu and Hugues de Saxcé and Bolton Bailey and Chendong Song and Chenjun Xiao and Dehao Zhang and Ebony Zhang and Frederick Pu and Han Zhu and Jiawei Liu and Jonas Bayer and Julien Michel and Longhui Yu and Léo Dreyfus-Schmidt and Lewis Tunstall and Luigi Pagani and Moreira Machado and Pauline Bourigault and Ran Wang and Stanislas Polu and Thibaut Barroyer and Wen-Ding Li and Yazhe Niu and Yann Fleureau and Yangyang Hu and Zhouliang Yu and Zihan Wang and Zhilin Yang and Zhengying Liu and Jia Li},
journal= {arXiv preprint arXiv:2504.11354},
year = {2025}
}
备注
22 pages