# 美团开源560亿参数LongCat-Flash-Prover：数学定理证明SOTA，性能全面碾压现有模型

- Link: https://paooo.com/aigc-news/11200/
- Published: 2026-05-27T22:38:33+08:00
- Author: 站外新闻

> **💡 站外导读：**当前，形式化数学验证领域长期受限于模型推理能力不足与高昂计算成本
> 的双重瓶颈。自动定理证明（ATP）作为连接自然语言与机器可验证逻辑的关键桥梁，其进展
> 直接影响着数学研究、软件验证等高精尖领域的发展。美团此次开源的LongCat-Flash-Prover，
> 以560亿参数的MoE架构和原生工具集成推理（TIR）设计，在多项权威基准上刷新了开源模型
> 的性能纪录，为该领域带来了突破性的解决方案。

## LongCat-Flash-Prover是什么

LongCat-Flash-Prover 是美团开源的5600亿参数MoE模型，专注Lean4形式化数学推理。模型
通过Agentic工具集成推理（TIR），将任务分解为自动形式化、草图生成和定理证明三大能力。
LongCat-Flash-Prover采用混合专家迭代框架和HisPO强化学习算法稳定训练，引入防作弊机制
确保推理严谨性。在MiniF2F-Test等基准测试中达到SOTA水平，Pass@32准确率93.9%，PutnamBench
难题解决率28.9%，显著超越现有开源模型。

阅读目录

 * [LongCat-Flash-Prover是什么](https://paooo.com/aigc-news/11200/#longcatflashprover%e6%98%af%e4%bb%80%e4%b9%88)
 * [LongCat-Flash-Prover的主要功能](https://paooo.com/aigc-news/11200/#longcatflashprover%e7%9a%84%e4%b8%bb%e8%a6%81%e5%8a%9f%e8%83%bd)
 * [LongCat-Flash-Prover的技术原理](https://paooo.com/aigc-news/11200/#longcatflashprover%e7%9a%84%e6%8a%80%e6%9c%af%e5%8e%9f%e7%90%86)
 * [LongCat-Flash-Prover的关键信息和使用要求](https://paooo.com/aigc-news/11200/#longcatflashprover%e7%9a%84%e5%85%b3%e9%94%ae%e4%bf%a1%e6%81%af%e5%92%8c%e4%bd%bf%e7%94%a8%e8%a6%81%e6%b1%82)
 * [LongCat-Flash-Prover的核心优势](https://paooo.com/aigc-news/11200/#longcatflashprover%e7%9a%84%e6%a0%b8%e5%bf%83%e4%bc%98%e5%8a%bf)
 * [如何使用LongCat-Flash-Prover](https://paooo.com/aigc-news/11200/#%e5%a6%82%e4%bd%95%e4%bd%bf%e7%94%a8longcatflashprover)
 * [LongCat-Flash-Prover的项目地址](https://paooo.com/aigc-news/11200/#longcatflashprover%e7%9a%84%e9%a1%b9%e7%9b%ae%e5%9c%b0%e5%9d%80)
 * [LongCat-Flash-Prover的同类竞品对比](https://paooo.com/aigc-news/11200/#longcatflashprover%e7%9a%84%e5%90%8c%e7%b1%bb%e7%ab%9e%e5%93%81%e5%af%b9%e6%af%94)
 * [LongCat-Flash-Prover的应用场景](https://paooo.com/aigc-news/11200/#longcatflashprover%e7%9a%84%e5%ba%94%e7%94%a8%e5%9c%ba%e6%99%af)
       * [📝 站长洞察 (Editor’s Insight)](https://paooo.com/aigc-news/11200/#%f0%9f%93%9d-%e7%ab%99%e9%95%bf%e6%b4%9e%e5%af%9f-editor8217s-insight)

![LongCat-Flash-Prover](https://paooo.com/wp-content/uploads/2026/05/LongCat-Flash-
Prover-website-1.avif)

## LongCat-Flash-Prover的主要功能

 * **自动形式化**：支持将自然语言数学问题转化为经过验证的Lean4形式化陈述。
 * **草图生成**：基于题目和形式化陈述生成引理风格的证明框架。
 * **定理证明**：支持生成完整证明或引入辅助引理完成目标定理的证明。
 * **工具集成推理**：模型可直接调用Lean4编译器进行实时验证和反馈迭代。

## LongCat-Flash-Prover的技术原理

 * **混合专家迭代框架**：框架支持部署多个专门优化的专家模型，分别负责自动形式化、
   草图生成和证明等不同领域任务。通过让专家模型在工具辅助下生成推理轨迹并进行迭代
   优化，模拟人类试错、验证和反思的学习过程，扩展高质量的冷启动数据。
 * **分层重要性采样策略优化（HisPO）**：针对MoE模型在长程任务训练中的不稳定性，HisPO
   采用分层裁剪策略，通过在序列级别和token级别估计重要性采样比率，消除训练与推理
   引擎差异较大的梯度贡献，稳定强化学习训练过程。
 * **防奖励作弊机制**：系统引入定理一致性检测和合法性检测，识别、过滤与形式化陈述
   语义不符、条件不匹配或包含未经验证公理的证明，防止模型通过欺骗Lean4服务器获取
   虚假奖励。

## LongCat-Flash-Prover的关键信息和使用要求

 * **模型规模**：采用5600亿参数MoE架构，开源权重模型中参数量最大之一
 * **核心定位**：专注Lean4原生形式化推理，无需针对形式化任务修改模型架构
 * **性能突破**：MiniF2F-Test达93.9%（Pass@32），PutnamBench达28.9%，均为开源模型
   SOTA
 * **推理效率**：在MiniF2F-Test上仅用72次推理可达到97.1%通过率，样本效率极高
 * **训练数据**：通过混合专家迭代框架合成高质量轨迹，支持自动形式化、草图和证明三
   类任务
 * **硬件环境**：560B参数MoE模型需要大规模GPU集群支持推理，建议配备充足显存的多卡
   环境
 * **软件依赖**：需安装Lean4证明助手及相应工具链，模型通过Lean4服务器进行实时验证
   交互
 * **部署方式**：支持Whole-Proof模式（直接生成完整证明）和Sketch-Proof模式（先草
   图后补全），后者配合TIR效果更佳

## LongCat-Flash-Prover的核心优势

 * **原生能力**：将形式化推理视为LLM原生能力，无需专门架构修改可直接调用Lean4工具
   链，实现与形式化环境的深度集成。
 * **SOTA性能**：在MathOlympiad-Bench、MiniF2F-Test、ProofNet、ProverBench、PutnamBench
   五大基准全面领先开源模型，部分指标逼近或超越闭源商业模型。
 * **样本高效**：仅需72次推理可在MiniF2F-Test达到97.1%通过率，远低于同类模型所需
   尝试次数，推理成本显著降低。
 * **防作弊设计**：通过定理一致性检测和合法性检测机制，确保模型输出真实可信，避免
   奖励作弊导致的虚假证明。

## 如何使用LongCat-Flash-Prover

 * **环境准备**：安装Lean4证明助手及依赖工具链，配置模型推理所需的GPU环境，确保显
   存足以支持560B参数MoE模型的加载与运行。
 * **获取模型**：从HuggingFace仓库下载模型权重，或直接使用GitHub提供的推理接口和
   示例代码进行部署。
 * **选择推理模式**：根据任务复杂度选择Whole-Proof模式直接生成完整证明，或选择Sketch-
   Proof模式先输出引理框架再逐步补全。
 * **输入问题**：将自然语言数学问题或待证定理输入模型，模型自动调用Lean4编译器进行
   实时验证，根据反馈迭代优化证明过程。
 * **获取结果**：模型输出经Lean4验证通过的形式化证明，可直接用在数学形式化验证、
   定理库构建或学术研究。

## LongCat-Flash-Prover的项目地址

 * **GitHub仓库**：https://github.com/meituan-longcat/LongCat-Flash-Prover
 * **HuggingFace模型库**：https://huggingface.co/meituan-longcat/LongCat-Flash-Prover
 * **技术论文**：https://github.com/meituan-longcat/LongCat-Flash-Prover/blob/main/
   LongCat_Flash_Prover_Technical_Report.pdf

## LongCat-Flash-Prover的同类竞品对比

  |  模型 |  规模 |  MathOlympiad-Bench |  MiniF2F-Test |  PutnamBench |  核心差异 |  
   |  **LongCat-Flash-Prover** |  560B MoE |  **35.8%** |  **93.9%** |  **28.9%** |  原生TIR工具集成，草图+证明双模式 |  
 |  [DeepSeek-Prover-V2-671B](https://ai-bot.cn/deepseek-prover-v2/) |  671B |  13.9% |  82.4% |  3.3% |  此前开源SOTA，无草图生成机制 |  
 |  Kimina-Prover-72B |  72B |  13.1% |  84.0% |  3.9% |  早期开源方案，推理效率较低 |

## LongCat-Flash-Prover的应用场景

 * **学术数学研究**：辅助数学家将自然语言猜想转化为Lean4形式化陈述并自动验证，加速
   证明发现过程，特别适用代数几何、数论等需要严格逻辑推导的领域。
 * **数学竞赛培训**：为IMO、Putnam等高水平数学竞赛提供解题思路验证和形式化证明生成，
   帮助选手理解复杂问题的严谨证明结构。
 * **形式化验证工程**：在软件 correctness 证明、密码学协议验证、硬件设计验证等场景
   中，自动生成或辅助构造形式化证明，提升关键系统安全性。
 * **教育辅助工具**：作为智能数学助教，为学生提供从问题理解到完整证明的逐步引导，
   实时检测推理漏洞并给出修正建议。

#### 📝 站长洞察 (Editor’s Insight)

LongCat-Flash-Prover的发布，标志着大模型在形式化推理领域从‘辅助工具’向‘原生能力’
的关键一跃。其核心突破在于三点：一是通过混合专家迭代框架与HisPO算法，解决了超大规模
MoE模型在复杂、长程逻辑任务中的训练稳定性难题，为行业提供了可复现的技术路径；二是
将工具使用（Lean4编译器）深度集成到推理循环中，实现了‘推理-验证-迭代’的闭环，这比
简单提示工程更具根本性优势；三是其防奖励作弊机制，体现了对AI可靠性与可信度的前沿
思考，这对于构建可信赖的AI系统至关重要。这不仅是数学AI的进步，更是‘AI for Science’
范式下，如何让AI深度嵌入严谨科学发现流程的一次重要实践，预示着未来AI驱动的知识生产
将更加自动化、可验证。