LongCat-Flash-Prover : Faire progresser le raisonnement formel natif via l'apprentissage par renforcement agentique intégrant des outils

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

March 22, 2026

Auteurs: 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

Résumé

Nous présentons LongCat-Flash-Prover, un modèle phare open-source à 560 milliards de paramètres de type Mixture-of-Experts (MoE), qui fait progresser le raisonnement formel natif dans Lean4 grâce à un raisonnement agentique intégrant des outils (TIR). Nous décomposons la tâche de raisonnement formel natif en trois capacités formelles indépendantes : l'auto-formalisation, l'esquisse de preuve (sketching) et la démonstration. Pour faciliter ces capacités, nous proposons un cadre d'itération à experts hybrides (Hybrid-Experts Iteration Framework) pour développer des trajectoires de tâches de haute qualité, incluant la génération d'un énoncé formel à partir d'un problème informel donné, la production d'une preuve complète directement à partir de l'énoncé, ou une esquisse de type lemme. Durant l'apprentissage par renforcement agentique (RL), nous présentons un algorithme d'optimisation de politique par échantillonnage d'importance hiérarchique (Hierarchical Importance Sampling Policy Optimization, HisPO), qui vise à stabiliser l'entraînement du modèle MoE sur ces tâches à long horizon. Il utilise une stratégie de masquage des gradients qui prend en compte la vétusté de la politique (policy staleness) et les écarts inhérents entre les moteurs d'entraînement et d'inférence, aux niveaux de la séquence et du token. De plus, nous intégrons également des mécanismes de détection de la cohérence et de la légalité des théorèmes pour éliminer les problèmes de détournement de récompense (reward hacking). Des évaluations approfondies montrent que notre LongCat-Flash-Prover établit un nouvel état de l'art pour les modèles à poids ouverts (open-weights) à la fois en auto-formalisation et en démonstration de théorèmes. Faisant preuve d'une remarquable efficacité en termes d'échantillons, il atteint un taux de réussite de 97,1 % sur MiniF2F-Test en utilisant seulement un budget de 72 inférences par problème. Sur des benchmarks plus difficiles, il résout 70,8 % de ProverBench et 41,5 % de PutnamBench avec pas plus de 220 tentatives par problème, surpassant significativement les modèles de référence à poids ouverts existants.

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.