LongCat-Flash-Prover: 에이전트 도구 통합 강화학습을 통한 네이티브 형식적 추론 기술 발전

LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning

March 22, 2026

저자: 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

초록

본 논문에서는 에이전트 도구 통합 추론(TIR)을 통해 Lean4의 네이티브 형식적 추론 능력을 발전시키는 5600억 개의 매개변수를 가진 오픈소스 MoE(전문가 혼합) 플래그십 모델인 LongCat-Flash-Prover를 소개한다. 우리는 네이티브 형식적 추론 과제를 세 가지 독립적인 형식적 능력, 즉 자동 형식화, 스케치 작성, 증명으로 분해한다. 이러한 능력을 지원하기 위해 고품질 작업 궤적을 확장하는 하이브리드 전문가 반복 프레임워크를 제안하며, 여기에는 주어진 비형식 문제를 바탕으로 형식 명제 생성, 명제로부터 직접 전체 증명 생성, 또는 보조정리 스타일 스케치 생성이 포함된다. 에이전트 강화학습 과정에서는 이러한 장기 과제에서 MoE 모델 학습을 안정화하기 위한 계층적 중요도 샘플링 정책 최적화(HisPO) 알고리즘을 제시한다. 이 알고리즘은 시퀀스 및 토큰 수준에서의 정책 노후화와 내재된 학습-추론 엔진 간 차이를 고려하는 그래디언트 마스킹 전략을 사용한다. 또한, 보상 해킹 문제를 방지하기 위해 정리 일관성 및 합법성 검출 메커니즘을 통합하였다. 광범위한 평가 결과, 우리의 LongCat-Flash-Prover는 자동 형식화 및 정리 증명 분야에서 오픈 가중치 모델의 새로운 최첨단 기술을 수립하였다. 놀라운 샘플 효율성을 보여주며, 문제당 72회의 추론 예산만으로 MiniF2F-Test에서 97.1%의 통과율을 달성했다. 더 어려운 벤치마크에서는 문제당 최대 220회의 시도로 ProverBench의 70.8%, PutnamBench의 41.5%를 해결하여 기존 오픈 가중치 기준선을 크게 능가하는 성능을 보였다.

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.