Saved in:
| Main Authors: | , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2504.11354 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915244095307776 |
|---|---|
| author | Wang, Haiming Unsal, Mert Lin, Xiaohan Baksys, Mantas Liu, Junqi Santos, Marco Dos Sung, Flood Vinyes, Marina Ying, Zhenzhe Zhu, Zekai Lu, Jianqiao de Saxcé, Hugues Bailey, Bolton Song, Chendong Xiao, Chenjun Zhang, Dehao Zhang, Ebony Pu, Frederick Zhu, Han Liu, Jiawei Bayer, Jonas Michel, Julien Yu, Longhui Dreyfus-Schmidt, Léo Tunstall, Lewis Pagani, Luigi Machado, Moreira Bourigault, Pauline Wang, Ran Polu, Stanislas Barroyer, Thibaut Li, Wen-Ding Niu, Yazhe Fleureau, Yann Hu, Yangyang Yu, Zhouliang Wang, Zihan Yang, Zhilin Liu, Zhengying Li, Jia |
| author_facet | Wang, Haiming Unsal, Mert Lin, Xiaohan Baksys, Mantas Liu, Junqi Santos, Marco Dos Sung, Flood Vinyes, Marina Ying, Zhenzhe Zhu, Zekai Lu, Jianqiao de Saxcé, Hugues Bailey, Bolton Song, Chendong Xiao, Chenjun Zhang, Dehao Zhang, Ebony Pu, Frederick Zhu, Han Liu, Jiawei Bayer, Jonas Michel, Julien Yu, Longhui Dreyfus-Schmidt, Léo Tunstall, Lewis Pagani, Luigi Machado, Moreira Bourigault, Pauline Wang, Ran Polu, Stanislas Barroyer, Thibaut Li, Wen-Ding Niu, Yazhe Fleureau, Yann Hu, Yangyang Yu, Zhouliang Wang, Zihan Yang, Zhilin Liu, Zhengying Li, Jia |
| contents | We introduce Kimina-Prover Preview, a large language model that pioneers a novel reasoning-driven exploration paradigm for formal theorem proving, as showcased in this preview release. Trained with a large-scale reinforcement learning pipeline from Qwen2.5-72B, Kimina-Prover demonstrates strong performance in Lean 4 proof generation by employing a structured reasoning pattern we term \textit{formal reasoning pattern}. This approach allows the model to emulate human problem-solving strategies in Lean, iteratively generating and refining proof steps. Kimina-Prover sets a new state-of-the-art on the miniF2F benchmark, reaching 80.7% with pass@8192. Beyond improved benchmark performance, our work yields several key insights: (1) Kimina-Prover exhibits high sample efficiency, delivering strong results even with minimal sampling (pass@1) and scaling effectively with computational budget, stemming from its unique reasoning pattern and RL training; (2) we demonstrate clear performance scaling with model size, a trend previously unobserved for neural theorem provers in formal mathematics; (3) the learned reasoning style, distinct from traditional search algorithms, shows potential to bridge the gap between formal verification and informal mathematical intuition. We open source distilled versions with 1.5B and 7B parameters of Kimina-Prover |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_11354 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning Wang, Haiming Unsal, Mert Lin, Xiaohan Baksys, Mantas Liu, Junqi Santos, Marco Dos Sung, Flood Vinyes, Marina Ying, Zhenzhe Zhu, Zekai Lu, Jianqiao de Saxcé, Hugues Bailey, Bolton Song, Chendong Xiao, Chenjun Zhang, Dehao Zhang, Ebony Pu, Frederick Zhu, Han Liu, Jiawei Bayer, Jonas Michel, Julien Yu, Longhui Dreyfus-Schmidt, Léo Tunstall, Lewis Pagani, Luigi Machado, Moreira Bourigault, Pauline Wang, Ran Polu, Stanislas Barroyer, Thibaut Li, Wen-Ding Niu, Yazhe Fleureau, Yann Hu, Yangyang Yu, Zhouliang Wang, Zihan Yang, Zhilin Liu, Zhengying Li, Jia Artificial Intelligence We introduce Kimina-Prover Preview, a large language model that pioneers a novel reasoning-driven exploration paradigm for formal theorem proving, as showcased in this preview release. Trained with a large-scale reinforcement learning pipeline from Qwen2.5-72B, Kimina-Prover demonstrates strong performance in Lean 4 proof generation by employing a structured reasoning pattern we term \textit{formal reasoning pattern}. This approach allows the model to emulate human problem-solving strategies in Lean, iteratively generating and refining proof steps. Kimina-Prover sets a new state-of-the-art on the miniF2F benchmark, reaching 80.7% with pass@8192. Beyond improved benchmark performance, our work yields several key insights: (1) Kimina-Prover exhibits high sample efficiency, delivering strong results even with minimal sampling (pass@1) and scaling effectively with computational budget, stemming from its unique reasoning pattern and RL training; (2) we demonstrate clear performance scaling with model size, a trend previously unobserved for neural theorem provers in formal mathematics; (3) the learned reasoning style, distinct from traditional search algorithms, shows potential to bridge the gap between formal verification and informal mathematical intuition. We open source distilled versions with 1.5B and 7B parameters of Kimina-Prover |
| title | Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning |
| topic | Artificial Intelligence |
| url | https://arxiv.org/abs/2504.11354 |