LongCat-Flash-Prover：美团开源 560B 智能体模型，刷新形式化推理 SOTA

美团开源了 LongCat-Flash-Prover，一个 5600 亿参数的混合专家模型，通过智能体工具集成强化学习推进 Lean4 中的形式化数学推理。该模型在自动形式化和定理证明两个方向上，为开源权重模型设立了新的最优水平。

模型将形式化推理分解为三个独立能力——自动形式化、草图构建和证明——并使用创新的层级重要性采样策略优化（HisPO）算法来稳定 MoE 在长时序任务上的训练。梯度掩蔽策略在序列和 token 两个层面处理策略陈旧和训练-推理引擎差异的问题。

系统采用混合专家迭代框架扩展高质量任务轨迹：从非形式化问题生成形式化陈述、直接生成完整证明，或创建引理风格的草图。定理一致性和合法性检测机制消除了奖励攻击问题。

对于智能体生态，LongCat-Flash-Prover 展示了智能体 RL 训练如何将专项推理能力推到远超标准微调的水平。工具集成方法——模型在 RL 过程中学习使用 Lean4 证明助手作为外部工具——是一个可以泛化到任何需要学习使用外部工具的智能体的范式。

GitHub：https://github.com/meituan-longcat/LongCat-Flash-Prover
论文：https://arxiv.org/abs/2603.21065