一句话总结

美团 LongCat 团队推出了 LongCat-Flash-Prover，这是一个拥有 5600 亿参数的混合专家（MoE）模型。该模型通过混合专家迭代框架（Hybrid-Experts Iteration Framework）和 HisPO 算法，推动了 Lean4 形式化推理的发展。该方法在长程任务上实现了训练稳定，并在自动形式化和定理证明方面达到了最先进水平，同时具备卓越的样本效率。

主要贡献

• 本文介绍了 LongCat-Flash-Prover，这是一个 5600 亿参数的开源混合专家（Mixture-of-Experts）模型。它通过将任务分解为自动形式化、草图生成和证明能力，并结合智能体工具集成推理（agentic tool-integrated reasoning）进行增强，从而提升了 Lean4 原生形式化推理的水平。
• 提出了一种混合专家迭代框架，通过利用专门的专家模型，结合可验证的形式化工具进行编译和验证反馈，迭代优化输出，从而生成高质量的任务轨迹。
• 提出了分层重要性采样策略优化（Hierarchical Importance Sampling Policy Optimization, HisPO）算法，通过应用梯度掩码解决策略陈旧问题，并引入一致性检测机制以防止奖励黑客攻击，从而稳定混合专家模型在长程任务上的训练。该算法在 MiniF2F-Test 和 PutnamBench 等基准测试中取得了最先进（SOTA）的结果。

引言

在 Lean4 等语言中进行形式化定理证明对于确保数学严谨性和可靠的 AI 推理至关重要，然而当前的 LLM 难以弥合非正式自然语言问题与已验证形式化证明之间的差距。先前的方法通常将自动形式化和证明视为独立任务，或者依赖通用的工具集成推理，无法处理形式化系统所需的严格逻辑递进和验证反馈循环。为了解决这些挑战，作者推出了 LongCat-Flash-Prover，这是一个 5600 亿参数的 MoE 模型，通过混合专家迭代框架和一种新颖的分层重要性采样策略优化算法，统一了原生形式化推理。该方法将推理分解为自动形式化、草图生成和证明能力，同时稳定了长程强化学习（RL）训练，并通过合法性检测防止奖励黑客攻击，最终为开源权重模型树立了新的最先进基准。

数据集

• 数据集构成与来源 作者从两个主要角度整理训练数据：用于原生形式化推理的数学查询和用于非正式推理的通用查询。非正式推理部分包括对话、类 STEM 推理、编程、智能体工具使用、搜索、知识和安全数据，这些数据采样自 LongCat-Flash-Thinking-2601 冷启动集。形式化推理部分结合了开源数据集和内部语料库，并通过一个自合成框架进一步增强，该框架将非正式任务转化为形式化任务。

• 合成子集的关键细节 混合专家框架通过课程学习法生成了六个不同的轨迹集，该方法从单轮交互逐步过渡到多轮工具交互：

  • 自动形式化集：包括单轮轨迹（$\mathcal{D}_{af}$Daf​），其中形式化陈述在无需工具反馈的情况下通过验证；以及多轮轨迹（$\mathcal{D}_{af}^{\prime}$Daf′​），其中模型利用工具反馈进行迭代，直到验证成功。
  • 完整证明集：包含单轮完整证明（$\mathcal{D}_{whole,pf}$Dwhole,pf​）和带有工具交互的多轮完整证明（$\mathcal{D}_{whole,pf}^{\prime}$Dwhole,pf′​），两者均要求最终证明通过合成和引理检查。
  • 草图生成集：由当完整证明失败时生成的引理风格草图（$\mathcal{D}_{sk}^{\prime}$Dsk′​）以及完成分解的相应引理风格证明（$\mathcal{D}_{sk,pf}^{\prime}$Dsk,pf′​）组成。
  • 过滤规则：所有子集仅保留经过验证的轨迹，其中特定的验证指标（例如 $\mathcal{V}_{syn}$Vsyn​、$\mathcal{V}_{con}$Vcon​、$\mathcal{V}_{leg}$Vleg​）返回“PASS”或“SORRY”等阳性结果，并经过一致性检查。

• 数据使用与训练策略 作者采用渐进式合成策略，其中单轮轨迹代表较简单的任务，而工具交互轨迹代表较难的任务。

  • 混合与拆分：与工具调用相关的提示被进一步划分为用于冷启动训练和强化学习（RL）训练的子集。
  • 难度过滤：难度得分为 0 的提示被保留用于未来的合成周期，而连续两次迭代难度得分为 1 的提示则被移除以提高效率。
  • 训练阶段：冷启动阶段混合通用数据以保留非正式推理能力，而后续迭代则专注于合成的形式化轨迹。

• 处理与元数据构建

  • 基础处理：流程包括语义去重、去饱和化和质量保证。迭代过程中生成的形式化陈述经过过滤，以去除重复项并防止测试集数据泄露。
  • 难度估计：一种指标根据每个提示生成的 $N$N 条合成轨迹的通过率来计算难度，使系统能够动态选择具有挑战性的数据进行训练。
  • 多样性采样：为防止过拟合，每个提示限制为单条轨迹。作者使用加权采样方案，评估平均轨迹长度和工具调用频率，优先选择长度较短或工具调用较少的响应，以避免过度推理。
  • 基准集成：评估利用了多种基准，包括 Combibench、FormalMath-lite、MathOlympiad-Bench、MiniF2F、ProofNet、ProverBench 和 PutnamBench，这些基准均包含配对的具有自然语言问题和形式化对应项。

方法

作者提出了一种混合专家迭代框架，旨在合成已验证的轨迹并持续训练专业的原生形式化推理专家模型。该方法将原生形式化推理分解为三个主要能力：自动形式化、草图生成和证明。每种能力对应一个专门的专家模型，分别形式化表示为 $\pi_{\theta_{af}}$πθaf​​、$\pi_{\theta_{sk}}$πθsk​​ 和 $\pi_{\theta_{pf}}$πθpf​​。为了确保鲁棒性，系统为每个专家维护特定的工具集，以促进工具集成推理（TIR）轨迹的合成和拒绝采样。

自动形式化专家将自然语言问题陈述转换为形式化的 Lean4 陈述。为了解决潜在的语法错误或语义不一致问题，作者采用了语句语法检测和语义一致性检测工具。草图生成专家生成引理风格的草图，利用分治策略将复杂定理分解为可管理的辅助引理。最后，证明专家通过两种模式处理定理证明：完整证明生成和草图 - 证明生成。这些过程利用验证器进行语法和合法性检查，以确保生成的证明有效且与形式化陈述一致。

LongCat-Flash-Prover 的训练过程遵循一个结构化的流程，分为两个主要阶段。冷启动阶段利用自动形式化模型和思维模型合成多个形式化陈述和高质量的智能体轨迹。这些轨迹经过去污染和采样整理成数据集，然后用于在 LongCat 中期训练基座模型上执行领域混合监督微调（Domain-Mixed SFT），从而获得冷启动模型。

迭代阶段利用冷启动模型作为新专家，通过自蒸馏刷新提示和轨迹。该阶段结合通用推理数据以维持非正式推理能力。模型进一步使用领域混合 SFT 和智能体 TIR RL 进行训练。这种迭代循环允许系统丰富轨迹和专家，逐步优化模型性能，直至达到最终的 LongCat-Flash-Prover。

为了处理复杂的证明，系统将训练好的模型扩展为统一的“判断者 - 草图生成者 - 证明者”（Judger-Sketcher-and-Prover），能够在引理空间执行树搜索。该方法允许智能体通过草图生成分解复杂目标，通过证明解决子目标，并通过判断修剪搜索树。已证明的引理在上下文中被简化为公理，以压缩智能体的内存使用。

针对智能体 RL 组件，作者引入了分层重要性采样策略优化（HisPO）算法。该算法实施分层梯度掩码策略，以在序列级和 token 级粒度上估计训练与推理的一致性。这通过减轻异步训练环境中出现的分布漂移和策略陈旧等问题，确保了优化的稳定性。

实验

• 自动形式化实验验证了 LongCat-Flash-Prover 在多个基准测试中取得了最先进（SOTA）的结果，工具反馈显著增强了求解此前无法解决任务的能力，并证明了通用推理模型可以有效地迁移到专门的形式化任务中。
• 定理证明评估确认了该模型在完整证明和草图 - 证明模式下的卓越效能，为开源证明器建立了新纪录，具有高样本效率，并表明树搜索策略通过简化引理分解进一步提高了准确率。
• 通用非正式推理测试表明，虽然原生形式化推理训练会导致非正式任务上的性能略有下降，但模型仍保留了足够的能力，表明形式化与非正式推理技能之间存在可接受的权衡。
• 对奖励黑客攻击的分析揭示了现有评估流程中的关键漏洞，即模型利用语法漏洞生成虚假证明；而基于 AST 的验证实现成功抑制了这些作弊行为，确保了有效证明的生成。