LongCat-Flash-Prover：美团开源5600亿参数MoE模型，刷新数学形式化推理新纪录

美团LongCat团队正式开源5600亿参数混合专家（MoE）模型LongCat-Flash-Prover，针对数学形式化推理任务深度优化。该模型通过原生形式化推理范式与智能体工具集成强化学习，结合创新的HisPO训练算法，在Lean4定理证明基准上创造开源模型新纪录，标志着形式化数学推理领域的重要突破。

数学推理能力是衡量大模型智力水平的核心标尺。传统大语言模型处理数学问题依赖自然语言推理链条，缺乏严格逻辑验证机制，易出现"幻觉"问题。为此，LongCat团队提出原生形式化推理范式，将形式化推理作为模型基础能力，直接利用Lean4等形式化运算符解决任务，无需修改架构。

原生形式化推理分解为三个智能体能力：自动形式化（自然语言转验证过的形式化陈述）、草图生成（引理风格证明草图）、证明（完整证明或辅助引理），通过工具集成推理增强。训练框架采用混合专家迭代优化，合成可验证轨迹数据。针对5600亿参数MoE训练稳定性，提出HisPO算法，通过分层裁剪策略消除梯度差异，并设计定理一致性检测防止奖励黑客。

LongCat-Flash-Prover在权威基准表现优异：自动形式化Pass@8指标达开源最佳；定理证明方面，MiniF2F-Test仅72次尝试通过率97.1%，ProverBench解决70.8%问题，PutnamBench（普特南竞赛级难题）解决41.5%，显著优于现有开源基线。

模型基于MoE架构（5600亿参数），对话模板优化支持工具声明、交错思考、推理保留。已适配SGLang和vLLM，提供部署指南，模型权重以MIT许可证开源，允许自由使用修改。

该模型证明大规模MoE在形式化推理的有效性，原生形式化范式为AI数学研究开辟新方向，开源策略促进领域协作。未来AI系统有望在数学发现、程序验证、科学计算等领域发挥更重要作用，LongCat-Flash-Prover是关键一步。