LongCat-Flash-Prover: エージェント的ツール統合型強化学習によるネイティブ形式推論の進展

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

March 22, 2026

著者: Jianing Wang, Jianfei Zhang, Qi Guo, Linsen Guo, Rumei Li, Chao Zhang, Chong Peng, Cunguang Wang, Dengchang Zhao, Jiarong Shi, Jingang Wang, Liulin Feng, Mengxia Shen, Qi Li, Shengnan An, Shun Wang, Wei Shi, Xiangyu Xi, Xiaoyu Li, Xuezhi Cao, Yi Lu, Yunke Zhao, Zhengyu Chen, Zhimin Lin, Wei Wang, Peng Pei, Xunliang Cai

cs.AI

要旨

我々は、エージェント的ツール統合推論（TIR）を通じてLean4におけるネイティブ形式推論を推進する、5600億パラメータのフラッグシップオープンソースMixture-of-Experts（MoE）モデル「LongCat-Flash-Prover」を紹介する。ネイティブ形式推論タスクを、自動形式化、スケッチング、証明の3つの独立した形式的能力に分解する。これらの能力を促進するため、高品質なタスク軌道を拡張するハイブリッドエキスパート反復フレームワークを提案し、与えられた非形式的問題に基づく形式ステートメントの生成、ステートメントからの完全証明の直接生成、または補題スタイルのスケッチの生成を含む。エージェント的強化学習では、階層的重要度サンプリング方策最適化（HisPO）アルゴリズムを提示し、このような長期タスクにおけるMoEモデル学習の安定化を図る。これは、方策の陳腐化とシーケンスレベル・トークンレベル双方における訓練-推論エンジンの本質的差異を考慮した勾配マスキング戦略を採用する。加えて、定理の一貫性と合法性検出メカニズムを組み込み、報酬ハッキング問題を排除する。大規模評価により、当モデルが自動形式化と定理証明の両方においてオープンウェイトモデルの新たなstate-of-the-artを確立することを示す。顕著なサンプル効率を実証し、問題あたり72回の推論予算のみでMiniF2F-Testにおいて97.1%の合格率を達成する。より困難なベンチマークでは、問題あたり最大220試行でProverBenchの70.8%、PutnamBenchの41.5%を解決し、既存のオープンウェイトベースラインを大幅に上回る。

English

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.