LongCat-Flash-Prover: Avanzare nel Ragionamento Formale Nativo tramite Apprendimento per Rinforzo Agente-Integrato con Strumenti
LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning
March 22, 2026
Autori: 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
Abstract
Introduciamo LongCat-Flash-Prover, un modello open-source flagship da 560 miliardi di parametri basato su Mixture-of-Experts (MoE) che avanza il Ragionamento Formale Nativo in Lean4 attraverso un ragionamento agentivo integrato con strumenti (TIR). Scomponiamo il compito del ragionamento formale nativo in tre capacità formali indipendenti: auto-formalizzazione, abbozzo (sketching) e dimostrazione. Per facilitare queste capacità, proponiamo un Hybrid-Experts Iteration Framework per espandere traiettorie di compito di alta qualità, inclusa la generazione di un enunciato formale basato su un dato problema informale, la produzione di un'intera dimostrazione direttamente dall'enunciato, o di uno schema in stile lemma. Durante l'RL agentivo, presentiamo un algoritmo di Hierarchical Importance Sampling Policy Optimization (HisPO), che mira a stabilizzare l'addestramento del modello MoE su tali compiti a lungo orizzonte. Esso impiega una strategia di mascheramento del gradiente che tiene conto dell'obsolescenza della policy e delle intrinseche discrepanze tra il motore di addestramento e quello di inferenza, sia a livello di sequenza che di token. Inoltre, incorporiamo meccanismi di rilevamento della consistenza dei teoremi e della legalità per eliminare problemi di reward hacking. Valutazioni estensive mostrano che il nostro LongCat-Flash-Prover stabilisce un nuovo stato dell'arte per i modelli open-weights sia nell'auto-formalizzazione che nella dimostrazione di teoremi. Dimostrando un'efficienza campionaria notevole, raggiunge un tasso di successo del 97.1% su MiniF2F-Test utilizzando solo un budget di inferenza di 72 per problema. Su benchmark più impegnativi, risolve il 70.8% di ProverBench e il 41.5% di PutnamBench con non più di 220 tentativi per problema, superando significativamente le baseline open-weights esistenti.
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.