美团开源 5677 亿参数 LongCat-Flash-Prover：专攻数学证明，MiniF2F 通过率高达 97.1%

在 AI 大模型普遍存在“逻辑幻觉”的今天，如何讓 AI 像数学家一样严谨地思考？

美团正式开源 LongCat-Flash-Prover，这是一款拥有 5677 亿参数 的混合专家模型（MoE）。它并非通用的聊天机器人，而是专为解决复杂数学证明和形式化推理而打造的旗舰级模型。

• GitHub：https://github.com/meituan-longcat/LongCat-Flash-Prover
• 模型：https://huggingface.co/meituan-longcat/LongCat-Flash-Prover

凭借独特的架构设计，该模型在权威基准测试 MiniF2F-Test 上取得了 97.1% 的惊人通过率，每个问题仅需 72 次推理尝试，树立了开放权重模型的新标杆。

核心突破：原生形式化推理 (Native Formal Reasoning)

LongCat-Flash-Prover 提出了“原生形式化推理”的新范式，将复杂的推理任务拆解为三种核心能力，并直接与 Lean4 证明助手集成：

1. 智能体自动形式化：
   • 能将自然语言描述的非正式数学问题，自动转换为 Lean4 可验证的形式化陈述。
2. 智能体草图构建：
   • 根据问题和形式化陈述，生成引理风格的证明草图，规划解题路径。
3. 智能体证明：
   • 生成完整的证明代码，或引入辅助引理最终完成定理证明。

关键特性：所有专家模型都能直接与 Lean4 工具 交互，进行实时编译和验证。这意味着模型不再是“闭门造车”，而是在一个可验证的环境中不断修正自己的逻辑。

技术架构：如何消除“幻觉”？

为了克服传统大模型在长程推理中容易产生的“幻觉”和“奖励黑客（Reward Hacking）”问题，美团团队引入了多项创新技术：

1. 混合专家迭代框架 (Hybrid-Experts Iteration Framework)

• 冷启动数据生成：利用多个专用专家模型（分别擅长形式化、草图、证明），合成高质量的任务轨迹。
• 迭代优化：模拟人类“试错 - 验证 - 反思”的学习过程，利用 Lean4 的反馈不断修正模型输出，确保每一步都逻辑严密。

2. 分层重要性采样策略优化 (HisPO)

• 稳定训练：针对 MoE 模型在长周期任务中难以收敛的问题，提出 HisPO 算法。
• 梯度掩蔽：通过估计序列级或 Token 级的重要性采样比率，消除因训练与推理引擎差异导致的梯度噪声，大幅提升训练稳定性。

3. 防作弊机制 (Anti-Cheating)

• 合法性检测：内置严格的检测机制，识别并惩罚“奖励黑客”行为。
• 拦截手段：自动过滤那些语义不一致、条件不匹配、或试图通过未经验证公理欺骗 Lean4 服务器的“伪证明”。

性能实测：刷新多项世界纪录

评估结果显示，LongCat-Flash-Prover 在数学证明领域达到了前所未有的高度：

此外，该模型在保持超强数学能力的同时，并未牺牲通用推理能力，在多个通用基准测试中依然保持领先。

战略意义：从“概率预测”到“逻辑确证”

LongCat-Flash-Prover 的开源，标志着 AI 推理能力从“基于概率的猜测”向“基于逻辑的确证”迈出了关键一步。

• 科研加速：能够辅助数学家验证复杂猜想，缩短证明周期。
• 代码安全：形式化验证技术可迁移至软件领域，用于生成无 Bug 的高可靠代码。
• 教育赋能：为学生提供严谨的数学解题思路和步骤验证。