LongCat-Flash-Prover: Vooruitgang in Native Formeel Redeneren via Agent-gestuurde, Gereedschap-geïntegreerde Versterkend Leren
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
Samenvatting
Wij introduceren LongCat-Flash-Prover, een vlaggenschip open-source Mixture-of-Experts (MoE)-model met 560 miljard parameters, dat Native Formeel Redeneren in Lean4 bevordert via agent-gedreven, tool-geïntegreerd redeneren (TIR). Wij ontleden de taak van native formeel redeneren in drie onafhankelijke formele capaciteiten, namelijk auto-formalisering, schetsen en bewijzen. Om deze capaciteiten te faciliteren, stellen wij een Hybride-Experts Iteratieraamwerk voor om hoogwaardige taaktrajecten uit te breiden, inclusief het genereren van een formele bewering op basis van een gegeven informeel probleem, het produceren van een volledig bewijs direct vanuit de bewering, of een lemma-stijl schets. Tijdens agent-gericht RL presenteren wij een Hiërarchisch Belangsteekproef Beleidsoptimalisatie (HisPO) algoritme, dat tot doel heeft de training van het MoE-model op dergelijke langetermijntaken te stabiliseren. Het hanteert een gradiëntmaskeringsstrategie die rekening houdt met de veroudering van het beleid en de inherente discrepanties tussen train- en inference-engine op zowel sequentie- als tokenniveau. Daarnaast incorporeren wij ook mechanismen voor consistentie van stellingen en legaliteitsdetectie om reward hacking-problemen te elimineren. Uitgebreide evaluaties tonen aan dat onze LongCat-Flash-Prover een nieuwe state-of-the-art vestigt voor open-gewicht modellen in zowel auto-formalisering als stellingenbewijzen. Het demonstreert een opmerkelijke steekproefefficiëntie door een slaagpercentage van 97,1% te behalen op MiniF2F-Test met slechts 72 inference-budget per probleem. Op meer uitdagende benchmarks lost het 70,8% van ProverBench en 41,5% van PutnamBench op met niet meer dan 220 pogingen per probleem, waarmee het bestaande open-gewicht baseline-modellen significant overtreft.
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.