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

Аннотация

Мы представляем LongCat-Flash-Prover — флагманскую открытую модель Mixture-of-Experts (MoE) с 560 миллиардами параметров, которая развивает нативное формальное рассуждение в Lean4 за счёт агентного рассуждения с интеграцией инструментов (Tool-Integrated Reasoning, TIR). Мы декомпозируем задачу нативного формального рассуждения на три независимые формальные способности: автоформализацию, создание эскизов (скетчинг) и доказательство. Для поддержки этих способностей мы предлагаем Гибридный экспертный итерационный фреймворк (Hybrid-Experts Iteration Framework) для расширения высококачественных траекторий задач, включая генерацию формального утверждения по заданной неформальной проблеме, создание полного доказательства непосредственно из утверждения или леммо-подобного эскиза. В ходе агентного обучения с подкреплением (RL) мы представляем алгоритм Иерархической оптимизации стратегии с важностным взвешиванием (Hierarchical Importance Sampling Policy Optimization, HisPO), направленный на стабилизацию обучения MoE-модели на таких задачах с длинным горизонтом. Он использует стратегию маскирования градиентов, учитывающую устаревание стратегии и присущие расхождения между механизмами обучения и вывода на уровне как последовательности, так и отдельных токенов. Кроме того, мы также внедряем механизмы проверки согласованности теорем и корректности для устранения проблем взлома функции вознаграждения (reward hacking). Обширные оценки показывают, что наша модель LongCat-Flash-Prover устанавливает новое state-of-the-art значение для моделей с открытыми весами как в автоформализации, так и в доказательстве теорем. Продемонстрировав выдающуюся эффективность по выборке, она достигает 97.1% успешных решений на MiniF2F-Test, используя всего 72 шага вывода на задачу. На более сложных бенчмарках модель решает 70.8% задач ProverBench и 41.5% задач PutnamBench, делая не более 220 попыток на задачу, что значительно превосходит существующие открытые базовые модели.

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.