LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , , , , , , , , , , , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910062800273408 |
|---|---|
| author | Wang, Jianing Zhang, Jianfei Guo, Qi Guo, Linsen Li, Rumei Zhang, Chao Peng, Chong Wang, Cunguang Zhao, Dengchang Shi, Jiarong Wang, Jingang Feng, Liulin Shen, Mengxia Li, Qi An, Shengnan Wang, Shun Shi, Wei Xi, Xiangyu Li, Xiaoyu Cao, Xuezhi Lu, Yi Zhao, Yunke Chen, Zhengyu Lin, Zhimin Wang, Wei Pei, Peng Cai, Xunliang |
| author_facet | Wang, Jianing Zhang, Jianfei Guo, Qi Guo, Linsen Li, Rumei Zhang, Chao Peng, Chong Wang, Cunguang Zhao, Dengchang Shi, Jiarong Wang, Jingang Feng, Liulin Shen, Mengxia Li, Qi An, Shengnan Wang, Shun Shi, Wei Xi, Xiangyu Li, Xiaoyu Cao, Xuezhi Lu, Yi Zhao, Yunke Chen, Zhengyu Lin, Zhimin Wang, Wei Pei, Peng Cai, Xunliang |
| contents | We introduce LongCat-Flash-Prover, a flagship 560-billion-parameter open-source Mixture-of- Experts (MoE) model that advances Native Formal Reasoning in Lean4 through agentic tool-integrated reasoning (TIR). We decompose the native formal reasoning task into three independent formal capabilities, i.e., auto-formalization, sketching, and proving. To facilitate these capabilities, we propose a Hybrid-Experts Iteration Framework to expand high-quality task trajectories, including generating a formal statement based on a given informal problem, producing a whole-proof directly from the statement, or a lemma-style sketch. During agentic RL, we present a Hierarchical Importance Sampling Policy Optimization (HisPO) algorithm, which aims to stabilize the MoE model training on such long-horizon tasks. It employs a gradient masking strategy that accounts for the policy staleness and the inherent train-inference engine discrepancies at both sequence and token levels. Additionally, we also incorporate theorem consistency and legality detection mechanisms to eliminate reward hacking issues. Extensive evaluations show that our LongCat-Flash-Prover sets a new state-of-the-art for open-weights models in both auto-formalization and theorem proving. Demonstrating remarkable sample efficiency, it achieves a 97.1% pass rate on MiniF2F-Test using only 72 inference budget per problem. On more challenging benchmarks, it solves 70.8% of ProverBench and 41.5% of PutnamBench with no more than 220 attempts per problem, significantly outperforming existing open-weights baselines. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_21065 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning Wang, Jianing Zhang, Jianfei Guo, Qi Guo, Linsen Li, Rumei Zhang, Chao Peng, Chong Wang, Cunguang Zhao, Dengchang Shi, Jiarong Wang, Jingang Feng, Liulin Shen, Mengxia Li, Qi An, Shengnan Wang, Shun Shi, Wei Xi, Xiangyu Li, Xiaoyu Cao, Xuezhi Lu, Yi Zhao, Yunke Chen, Zhengyu Lin, Zhimin Wang, Wei Pei, Peng Cai, Xunliang Artificial Intelligence Computation and Language We introduce LongCat-Flash-Prover, a flagship 560-billion-parameter open-source Mixture-of- Experts (MoE) model that advances Native Formal Reasoning in Lean4 through agentic tool-integrated reasoning (TIR). We decompose the native formal reasoning task into three independent formal capabilities, i.e., auto-formalization, sketching, and proving. To facilitate these capabilities, we propose a Hybrid-Experts Iteration Framework to expand high-quality task trajectories, including generating a formal statement based on a given informal problem, producing a whole-proof directly from the statement, or a lemma-style sketch. During agentic RL, we present a Hierarchical Importance Sampling Policy Optimization (HisPO) algorithm, which aims to stabilize the MoE model training on such long-horizon tasks. It employs a gradient masking strategy that accounts for the policy staleness and the inherent train-inference engine discrepancies at both sequence and token levels. Additionally, we also incorporate theorem consistency and legality detection mechanisms to eliminate reward hacking issues. Extensive evaluations show that our LongCat-Flash-Prover sets a new state-of-the-art for open-weights models in both auto-formalization and theorem proving. Demonstrating remarkable sample efficiency, it achieves a 97.1% pass rate on MiniF2F-Test using only 72 inference budget per problem. On more challenging benchmarks, it solves 70.8% of ProverBench and 41.5% of PutnamBench with no more than 220 attempts per problem, significantly outperforming existing open-weights baselines. |
| title | LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning |
| topic | Artificial Intelligence Computation and Language |
| url | https://arxiv.org/abs/2603.21065 |