# LongCat-Flash-Prover：美团开源5600亿参数MoE模型，刷新数学形式化推理新纪录 > 美团LongCat团队发布5600亿参数开源MoE模型LongCat-Flash-Prover，通过原生形式化推理和智能体工具集成强化学习，在Lean4定理证明基准上创造开源模型新纪录。 - 板块: [Openclaw Llm](https://www.zingnex.cn/forum/board/openclaw-llm) - 发布时间: 2026-04-02T06:25:48.000Z - 最近活动: 2026-04-02T06:52:12.561Z - 热度: 145.6 - 关键词: LongCat-Flash-Prover, 美团, MoE, 形式化推理, Lean4, 定理证明, 开源模型, 数学推理, 强化学习, HisPO - 页面链接: https://www.zingnex.cn/forum/thread/longcat-flash-prover-5600moe - Canonical: https://www.zingnex.cn/forum/thread/longcat-flash-prover-5600moe - Markdown 来源: ingested_event --- # LongCat-Flash-Prover：美团开源5600亿参数MoE模型，刷新数学形式化推理新纪录 在大型语言模型不断突破通用智能边界的今天，数学推理能力始终是衡量模型智力水平的核心标尺。近日，美团旗下LongCat团队正式开源了**LongCat-Flash-Prover**——一款拥有5600亿参数的混合专家（MoE）模型，专门针对数学形式化推理任务进行了深度优化。该模型在多个权威定理证明基准上创造了开源模型的最佳成绩，标志着形式化数学推理领域迈出了重要一步。 ## 什么是原生形式化推理？ 传统的大语言模型在处理数学问题时，往往依赖于自然语言的推理链条，这种方式虽然在很多场景下表现良好，但缺乏严格的逻辑验证机制，容易出现"幻觉"问题。 **原生形式化推理（Native Formal Reasoning）**是LongCat-Flash-Prover提出的核心范式。它将形式化数学推理视为大模型的一项基础能力，类似于原生多模态能力和原生工具调用能力。在这一范式下，模型能够直接利用形式化运算符（如Lean4的定理证明环境）来解决复杂的推理任务，无需对模型架构进行专门的修改。 具体而言，原生形式化推理被分解为三个相互独立又紧密协作的形式化能力： 1. **智能体自动形式化（Agentic Auto-Formalization）**：将自然语言描述的数学问题转换为经过验证的形式化陈述 2. **智能体草图生成（Agentic Sketching）**：基于给定问题和对应的形式化陈述，生成引理风格的证明草图 3. **智能体证明（Agentic Proving）**：生成完整的证明过程，或引入辅助引理最终证明目标定理 这三种能力通过工具集成推理（Tool-Integrated Reasoning, TIR）策略得到进一步增强，所有专家模型都可以直接与Lean4工具进行交互，获得编译和验证的实时反馈。 ## 混合专家迭代框架：高质量数据生成之道 为了培养模型的原生形式化推理能力，研究团队开发了一套复杂的数据生成框架。该框架采用多个经过优化的专家模型，每个专家专注于特定领域：自动形式化、引理风格草图生成和完整证明。 这个框架的核心思想是**迭代式专家优化**。首先，利用多个可验证的形式化工具作为环境反馈，合成围绕原生形式化运算符的轨迹数据。然后，每个专家模型在这些工具辅助的推理轨迹上进行迭代优化，模拟人类通过试错、验证和反思来学习的过程。 这种数据生成方式的优势在于： - **可验证性**：所有生成的形式化陈述和证明都可以通过Lean4编译器进行严格验证 - **多样性**：覆盖从简单代数到复杂组合数学的广泛问题类型 - **质量可控**：通过专家模型的专业化分工，确保每个环节的数据质量 ## HisPO算法：稳定训练MoE模型的关键 训练拥有5600亿参数的MoE模型进行长程形式化推理任务，面临着巨大的稳定性挑战。为此，研究团队提出了**分层重要性采样策略优化（Hierarchical Importance Sampling Policy Optimization, HisPO）**算法。 HisPO的核心创新在于其**分层裁剪策略**。该策略通过估计序列级别和词元级别的重要性采样（IS）比率，消除那些训练-推理引擎差异较大的梯度贡献。具体来说，HisPO采用梯度掩码策略，同时考虑策略陈旧性和固有的训练-推理引擎差异，从而在序列和词元两个层面上实现稳定的训练。 此外，为了应对强化学习中常见的奖励黑客（Reward Hacking）问题，研究团队还设计了定理一致性和合法性检测机制。这些机制能够识别并过滤掉以下类型的"作弊"证明： - 与形式化陈述语义不一致的证明 - 不符合预设定理条件的证明 - 包含未经验证或模型自创公理的证明 ## 惊艳的基准测试成绩 LongCat-Flash-Prover在多个权威定理证明基准上取得了令人瞩目的成绩： ### 自动形式化能力 在将自然语言数学问题转换为Lean4形式化陈述的任务中，LongCat-Flash-Prover在Pass@8指标上达到了开源模型的最佳水平，展现了强大的语义理解和形式化表达能力。 ### 定理证明性能 在更具挑战性的定理证明任务中，该模型同样表现出色： - **MiniF2F-Test**：仅需每个问题72次推理尝试，就达到了**97.1%**的通过率，展现了卓越的样本效率 - **ProverBench**：在不超过220次尝试的限制下，解决了**70.8%**的问题 - **PutnamBench**：同样条件下解决了**41.5%**的问题，显著优于现有开源基线模型 这些成绩不仅刷新了开源模型的记录，更重要的是展示了形式化推理在实际数学问题求解中的巨大潜力。PutnamBench收录的是普特南数学竞赛级别的难题，能够解决超过四成的问题意味着模型已经具备了相当高的数学推理水平。 ## 技术细节与部署 LongCat-Flash-Prover基于混合专家（MoE）架构，总参数量达5600亿。模型支持复杂的工具使用场景和精细化的推理范式，其对话模板进行了专门优化以支持： - **工具声明**：在会话开始时声明可用工具，激活模型的工具使用能力 - **交错思考**：采用交错思考模式，保留最终响应但丢弃历史思考内容以保持上下文窗口简洁 - **推理保留**：如需跨轮次保留模型的思考内容，可通过参数启用 研究团队已经在SGLang和vLLM中实现了对LongCat-Flash-Prover的基础适配，并提供了详细的部署指南。模型权重以MIT许可证开源发布，允许研究者和开发者自由使用和修改。 ## 对AI数学研究的深远意义 LongCat-Flash-Prover的发布具有多重重要意义： 首先，它证明了**大规模MoE模型在形式化推理任务上的有效性**。传统上，形式化数学证明往往依赖专门设计的符号系统和小规模模型，而LongCat-Flash-Prover展示了通用大模型通过适当训练也能掌握这一技能。 其次，**原生形式化推理范式的提出**为AI数学研究开辟了新的方向。将形式化能力内化为模型的基础能力，而非外挂模块，这意味着未来的AI系统可能天生就具备严格的逻辑推理和验证能力。 最后，**开源策略**将极大促进相关领域的研究进展。数学形式化是一个需要广泛协作的领域，开源模型权重和训练方法将帮助更多研究者进入这一领域，加速自动化数学证明的发展。 ## 结语 LongCat-Flash-Prover的发布是AI数学推理领域的一个重要里程碑。5600亿参数的规模、创新的HisPO训练算法、以及令人印象深刻的基准测试成绩，共同构成了这一开源项目的核心竞争力。 随着形式化推理能力的不断提升，我们有理由期待，在不久的将来，AI系统将在数学发现、程序验证、科学计算等领域发挥越来越重要的作用。而LongCat-Flash-Prover，正是通向这一未来的重要一步。