LongCat-Flash-Prover: Fortschritte im nativen formalen Beweisen durch agentenbasiertes, werkzeugintegriertes bestärkendes Lernen
LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning
March 22, 2026
Autoren: 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
Zusammenfassung
Wir stellen LongCat-Flash-Prover vor, ein bahnbrechendes Open-Source-Mixture-of-Experts (MoE)-Modell mit 560 Milliarden Parametern, das das native formale Schließen in Lean4 durch agentenbasiertes, werkzeugintegriertes Reasoning (TIR) voranbringt. Wir zerlegen die Aufgabe des nativen formalen Schließens in drei unabhängige formale Fähigkeiten: Autoformalisierung, Skizzierung und Beweisführung. Um diese Fähigkeiten zu ermöglichen, schlagen wir ein Hybrid-Experts-Iterationsframework vor, um hochwertige Aufgabenverläufe zu erweitern, einschließlich der Generierung einer formalen Aussage basierend auf einem gegebenen informellen Problem, der direkten Erzeugung eines vollständigen Beweises aus der Aussage oder einer lemmenartigen Skizze. Während des agentenbasierten Reinforcement Learnings präsentieren wir einen Hierarchical Importance Sampling Policy Optimization (HisPO)-Algorithmus, der darauf abzielt, das Training des MoE-Modells für solche langfristigen Aufgaben zu stabilisieren. Er verwendet eine Gradient-Masking-Strategie, die die Veralterung der Policy sowie die inhärenten Diskrepanzen zwischen Trainings- und Inferenz-Engine auf Sequenz- und Token-Ebene berücksichtigt. Zusätzlich integrieren wir Mechanismen zur Überprüfung der Theoremkonsistenz und -legalität, um Reward-Hacking-Probleme zu beseitigen. Umfangreiche Evaluationen zeigen, dass unser LongCat-Flash-Prover einen neuen State-of-the-Art für Open-Weights-Modelle sowohl in der Autoformalisierung als auch in der Theorembeweisführung setzt. Es zeigt eine bemerkenswerte Probeneffizienz und erreicht eine Bestehensrate von 97,1 % auf MiniF2F-Test mit nur 72 Inferenzversuchen pro Problem. Auf anspruchsvolleren Benchmarks löst es 70,8 % von ProverBench und 41,5 % von PutnamBench mit nicht mehr als 220 Versuchen pro Problem und übertrifft damit existierende Open-Weights-Baselines deutlich.
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.