LongCat-Flash-Prover: Avançando o Raciocínio Formal Nativo via Aprendizagem por Reforço com Integração de Ferramentas 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
Resumo
Apresentamos o LongCat-Flash-Prover, um modelo de código aberto líder com 560 bilhões de parâmetros baseado em Mistura de Especialistas (MoE), que avança o Raciocínio Formal Nativo no Lean4 por meio de raciocínio agentivo integrado a ferramentas (TIR). Decompomos a tarefa de raciocínio formal nativo em três capacidades formais independentes: autoformalização, esboço e prova. Para facilitar essas capacidades, propomos um Framework de Iteração Híbrida de Especialistas para expandir trajetórias de tarefas de alta qualidade, incluindo a geração de uma afirmação formal com base em um problema informal dado, a produção de uma prova completa diretamente a partir da afirmação ou um esboço no estilo de lema. Durante o RL agentivo, apresentamos um algoritmo de Otimização de Política por Amostragem de Importância Hierárquica (HisPO), que visa estabilizar o treinamento do modelo MoE em tarefas de horizonte longo. Ele emprega uma estratégia de mascaramento de gradiente que leva em conta a obsolescência da política e as discrepâncias inerentes entre o motor de treinamento e inferência, tanto em nível de sequência quanto de token. Adicionalmente, também incorporamos mecanismos de detecção de consistência e legalidade de teoremas para eliminar problemas de manipulação de recompensa. Avaliações extensivas mostram que nosso LongCat-Flash-Prover estabelece um novo estado da arte para modelos de pesos abertos tanto em autoformalização quanto em prova de teoremas. Demonstrando notável eficiência amostral, ele alcança uma taxa de aprovação de 97,1% no MiniF2F-Test usando apenas 72 orçamentos de inferência por problema. Em benchmarks mais desafiadores, ele resolve 70,8% do ProverBench e 41,5% do PutnamBench com não mais que 220 tentativas por problema, superando significativamente as linhas de base de pesos abertos 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.