论文

LongCat-Flash-Prover：通过智能体工具集成强化学习推进原生形式推理

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

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来源日期：2026.03.22

模型训练模型架构MoE强化学习Agentic RL

摘要

我们提出LongCat-Flash-Prover，一个旗舰级5600亿参数开源混合专家（MoE）模型，通过智能体工具集成推理（TIR）推进Lean4中的原生形式推理。我们将原生形式推理任务分解为三种独立的形式化能力，即自动形式化、草拟和证明。为促进这些能力，我们提出混合专家迭代框架（Hybrid-Experts Iteration Framework）来扩充高质量任务轨迹，包括基于给定非形式问题生成形式化命题、直接从命题产出完整证明，或生成引理式草稿。在智能体强化学习阶段，我们提出分层重要性采样策略优化（HisPO）算法，旨在稳定MoE模型在此类长程任务上的训练。该算法采用梯度掩蔽策略，在序列与token两个层面考虑策略陈旧性以及训练与推理引擎之间固有的差异。此外，我们还引入定理一致性与合法性检测机制，以消除奖励作弊问题。大量评估显示，LongCat-Flash-Prover在自动形式化和定理证明两项任务上均刷新了开放权重模型的最新纪录。该模型展现出卓越的样本效率，在MiniF2F-Test上以每题仅72次推理预算取得97.1%的通过率。在更具挑战性的基准上，它以每题不超过220次尝试解决ProverBench的70.8%和PutnamBench的41.5%，显著超越现有开放权重基线。

LongCat-Flash-Prover：通过智能体工具集成强化学习推进原生形式推理：论文配图 — 图 2：我们的混合专家工具集成综合管道的概述。在此管道中，我们迭代优化三个不同的专家（即自动形式化器、引理式草图器和证明器），并使用这些专家根据预定义的形式推理功能来合成轨迹。给定一个自然语言问题，我们首先通过与 Lean4 编译器交互将其转换为 Lean4 中的正式语句。然后，正式的陈述将用于生成完整的证明和引理式草图。如果在有限数量的工具反馈轮内，整体证明仍然无法通过验证，则将使用从引理式草图生成的证明来进行验证。在拒绝采样阶段，我们将保留允许我们充分利用工具来执行自动形式化、草图绘制和证明的轨迹。