美团开源 LongCat-Flash-Prover 大模型：5600 亿参数，刷新两项 SOTA 水平

美团开源 LongCat-Flash-Prover：参数规模5600亿的数学定理证明专家

美团近期正式开源了LongCat-Flash-Prover，这是一个专门针对形式化数学证明任务设计的大型语言模型。它基于MoE架构构建，总参数量达到5677亿，旨在自动解决并验证复杂的数学定理证明问题。

技术架构：确保形式化推理的严格性

为了保障生成推理的严谨可靠，该模型的核心在于其混合专家迭代框架。该框架被设计用于产出高质量、可验证的形式化证明轨迹，其本质是引导模型生成结构化的、符合逻辑规则的推理步骤。

模型深度整合了Lean4定理证明器，并应用了一套基于抽象语法树的多阶段严格验证流程。这一技术组合对推理的中间和最终输出施加了严格的语法与逻辑约束，从而系统性抑制了模型在演绎过程中产生的“幻觉”输出。

训练策略：数据生成、算法稳定与奖励对齐

模型的训练始于一个数据自生成过程：其混合专家迭代框架本身被用于创建初始的“冷启动”训练数据，缓解了高质量形式化证明数据稀缺的核心瓶颈。

在随后的强化学习精调阶段，研究团队引入了HisPO算法以稳定MoE模型在长序列、高复杂度任务上的优化过程。关键性的创新在于集成了定理一致性与合法性检测机制。该机制作为奖励模型的一部分，主动识别并惩罚模型的“奖励黑客”行为，即那些形式上符合奖励信号但逻辑或语义上无效的推导，确保了训练目标与真实证明能力的一致性。

基准测试：在两项权威证明任务上确立新标杆

在MiniF2F-Test数学证明基准上，该模型取得了97.1%的通过率，且平均仅需72次推理尝试，展现了高精度与高效率。

在更具挑战性的PutnamBench基准上（该基准改编自普特南数学竞赛试题），LongCat-Flash-Prover成功解决了41.5%的问题，平均消耗118次推理尝试。这两项成绩均超越了现有公开模型，确立了该领域新的性能标杆。

获取资源

项目代码、模型权重及相关技术文档已开放，可通过以下渠道获取：

GitHub：https://github.com/meituan-longcat/LongCat-Flash-Prover

Hugging Face：https://huggingface.co/meituan-longcat/LongCat-Flash-Prover

来源：互联网