LongCat-Flash-Prover: Avanzando en el Razonamiento Formal Nativo mediante Aprendizaje por Refuerzo con Integración de Herramientas Agentes
LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning
March 22, 2026
Autores: 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
Resumen
Presentamos LongCat-Flash-Prover, un modelo insignia de código abierto con 560 mil millones de parámetros basado en Mezcla de Expertos (MoE), que avanza en el Razonamiento Formal Nativo en Lean4 mediante un razonamiento agentivo integrado con herramientas (TIR). Descomponemos la tarea de razonamiento formal nativo en tres capacidades formales independientes: auto-formalización, bosquejo y demostración. Para facilitar estas capacidades, proponemos un Marco de Iteración de Expertos Híbridos para expandir trayectorias de tareas de alta calidad, que incluyen generar un enunciado formal a partir de un problema informal dado, producir una demostración completa directamente desde el enunciado o un bosquejo de tipo lema. Durante el RL agentivo, presentamos un algoritmo de Optimización de Políticas con Muestreo de Importancia Jerárquico (HisPO), que tiene como objetivo estabilizar el entrenamiento del modelo MoE en tareas de horizonte tan largo. Emplea una estrategia de enmascaramiento de gradientes que considera el desfase de la política y las discrepancias inherentes entre el motor de entrenamiento y el de inferencia, tanto a nivel de secuencia como de token. Adicionalmente, incorporamos mecanismos de detección de consistencia y legalidad de teoremas para eliminar problemas de hackeo de recompensas. Evaluaciones exhaustivas muestran que nuestro LongCat-Flash-Prover establece un nuevo estado del arte para modelos de pesos abiertos tanto en auto-formalización como en demostración de teoremas. Demostrando una eficiencia muestral notable, alcanza una tasa de aprobación del 97.1% en MiniF2F-Test utilizando solo un presupuesto de 72 inferencias por problema. En benchmarks más desafiantes, resuelve el 70.8% de ProverBench y el 41.5% de PutnamBench con no más de 220 intentos por problema, superando significativamente a las bases de referencia de pesos abiertos existentes.
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.