LongCat-Flash-Prover – 美团开源的数学定理证明模型

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的主要功能

• 自动形式化：支持将自然语言数学问题转化为经过验证的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的应用场景

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