LongCat-Flash-Prover – 美团5677亿MoE数学推理大模型详解

LongCat-Flash-Prover是美团开源的5677亿参数MoE大模型，专攻复杂数学定理与形式化推理。融合 Lean4 证明器与 AST 校验，严格防幻觉；依托HisPO强化学习稳定长链推导，在MiniF2F、普特南难题刷新 SOTA，适用于科研证明、严谨验证等高阶理性任务。

一、核心定位与参数

• 全称：LongCat-Flash-Prover（美团 LongCat 系列）
• 参数规模：5677 亿，采用 **MoE（混合专家）** 架构
• 核心目标：解决复杂数学定理证明、形式化验证等强推理任务
• 开源地址：
  • GitHub：https://github.com/meituan-longcat/LongCat-Flash-Prover
  • Hugging Face：https://huggingface.co/meituan-longcat/LongCat-Flash-Prover

二、关键技术创新

1. 混合专家迭代框架

   生成高质量形式化推理轨迹，提升长程证明的连贯性与效率。

2. Lean4 + AST 多阶段验证

   内置Lean4定理证明器与 ** 抽象语法树（AST）** 校验，严格消除 AI 幻觉，确保每一步推理合法、可验证。

3. HisPO 强化学习算法

   稳定 MoE 模型在长程数学任务上的训练，加入定理一致性检测，防止 “奖励黑客” 行为。

三、性能表现（SOTA）

• MiniF2F-Test：97.1% 成功率，仅需72 次推理尝试
• PutnamBench（普特南数学竞赛级）：41.5% 问题解决率，118 次尝试

四、适用场景

• 数学定理自动证明
• 形式化验证（软件 / 硬件 / 协议）
• 科研级数学推理与辅助证明
• 教育领域的数学解题与推导