美团开源超大规模数学证明模型 LongCat-Flash-Prover

3月21日，美团正式对外开源了一款名为 LongCat-Flash-Prover 的数学证明模型，参数规模达5677亿，是目前全球公开的规模最大、专为形式化证明设计的AI模型之一。该模型基于混合专家（MoE）架构，专攻复杂数学定理的形式化验证，已在多个权威基准测试中刷新世界纪录，引发学术界和工业界广泛关注。

突破性成绩：在顶级数学推理测试中领跑全球

在衡量AI数学推理能力的两大核心基准中，LongCat-Flash-Prover 表现突出：

• 在 MiniF2F-Test 数据集上，以 97.1% 的准确率完成证明，仅用72次推理尝试，远超此前由DeepMind和Google发布的模型成绩。
• 在 PutnamBench（以美国大学生数学竞赛Putnam题为基准）中，成功解决41.5%的题目，这是该榜单历史上首次有AI模型突破40%大关，此前最优模型仅在30%左右徘徊。

这些结果不仅意味着模型能“看懂”高等数学题，更能在严格的逻辑框架下自动生成可验证的证明过程，而非依赖模糊推理或模板套用。

不是“猜答案”，而是“写证明”

与许多大模型在数学题上“蒙答案”不同，LongCat-Flash-Prover 的核心能力在于生成符合形式化语言规范的完整证明脚本。它不输出“答案是5”，而是输出一整套可被Lean4定理证明器逐行验证的代码——这意味着每一步推理都必须逻辑自洽，不能有跳跃或漏洞。

为此，美团团队构建了一套多阶段验证系统：模型生成的证明首先通过抽象语法树（AST）解析，再由Lean4编译器进行语法和语义双重校验，最终只有完全通过验证的证明才会被接受。这套机制从源头上杜绝了AI常见的“幻觉”问题——即看似合理、实则逻辑错误的“伪证明”。

技术突破：解决MoE模型的“训练不稳”难题

5677亿参数的模型若直接训练，极易出现资源浪费、收敛困难、专家模块“躺平”等问题。美团团队为此自研了 HisPO（Hierarchical Policy Optimization）训练算法，结合定理一致性检测机制，有效提升了模型在强化学习阶段的稳定性。

传统强化学习中，模型常通过“钻空子”获得高奖励——比如生成冗长但无实质内容的证明步骤，或重复使用已知引理伪装创新。HisPO通过引入“证明结构一致性评分”，引导模型专注于逻辑深度而非长度，显著抑制了“奖励黑客”行为。实测显示，该方法使有效证明生成率提升近35%。

5600亿参数，为何不卡顿？MoE架构是关键

虽然总参数高达5677亿，但模型在实际推理时，仅激活约1200亿参数——这得益于MoE架构的“专家路由”机制。每次推理，系统会根据输入问题动态选择最相关的专家子模块，而非调动全部参数。这种设计既保留了海量知识的覆盖能力，又保证了推理效率，单次证明平均耗时控制在30秒以内，适合在集群环境下部署。

开源：所有人都能用，也能参与改进

美团已将 LongCat-Flash-Prover 的完整模型权重、训练代码、验证工具链和数据集预处理脚本，同步开源至 GitHub 和 Hugging Face 平台，支持商用与研究用途。开源文档中包含详细的部署指南、Lean4环境配置说明，以及如何用自己的数学问题微调模型的示例。

目前，已有多个高校研究团队和开源项目开始基于该模型构建数学教育辅助工具、自动化定理验证插件，甚至用于验证金融算法的正确性。一位MIT的博士生在社交媒体上表示：“我们过去需要花三个月验证一个证明，现在模型半小时给出草稿，我们只需聚焦关键逻辑漏洞——这改变了研究节奏。”

意义不止于数学

数学证明是逻辑严谨性的终极考验。当AI能可靠地完成形式化证明，意味着它在代码验证、硬件设计、协议安全、金融合约校验等领域也具备了潜在应用价值。LongCat-Flash-Prover 不是“会做题的AI”，而是首个在真实工程级验证环境中被证明“值得信赖”的大模型。

它的出现，标志着中国团队在高阶推理领域，从跟随者走向了引领者。AI不再只是写代码、写文章的助手，它正在成为数学家和工程师的“第二大脑”——而这一次，它不是在模仿人类，而是在帮人类避免错误。