The Year in AI Papers
The year/Independent research

Paper 2603.21065

LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning

Jianing Wang, Jianfei Zhang, Qi Guo, Linsen Guo, Rumei Li, Chao Zhang, Chong Peng, Cunguang Wang, Dengchang Zhao, Jiarong Shi, Jingang Wang, Liulin Feng, et al.

Published
Mar 2026
Research lab
Independent
Citations
5
GitHub
93 stars

01 In brief

Summary

LongCat-Flash-Prover is a 560-billion-parameter open-source Mixture-of-Experts (MoE) model for native formal reasoning in Lean4, developed by Meituan LongCat Team.

It decomposes formal reasoning into auto-formalization, sketching, and proving, and uses a Hybrid-Experts Iteration Framework to synthesize high-quality trajectories with tool feedback.

The model is trained with Hierarchical Importance Sampling Policy Optimization (HisPO), which stabilizes MoE training by masking gradients based on sequence- and token-level train-inference discrepancies and policy staleness.

Legality detection via AST checks prevents reward hacking.

On benchmarks, it achieves 97.1% pass rate on MiniF2F-Test with 72 attempts, 70.8% on ProverBench, and 41.5% on PutnamBench with up to 220 attempts, outperforming open-weights baselines.

It also sets state-of-the-art results in auto-formalization across multiple benchmarks, with TIR boosting performance by up to 14%.

General reasoning performance is slightly lower than LongCat-Flash-Thinking-2601 but remains competitive.

02 From the paper

Abstract

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.