longcat-flash-prover 是什么
longcat-flash-prover 是美团推出的开源大型语言模型，参数规模达5600亿，采用moe（mixture of experts）架构，专为lean4形式化数学推理任务设计。该模型融合了“基于智能体的工具集成推理”（tir）范式，将复杂推理流程拆解为三大核心能力：自动形式化、草图生成与定理证明。其训练依托混合专家迭代框架与hispo强化学习算法，兼顾稳定性与收敛性，并内建防作弊机制以保障推理过程的逻辑严谨性。在minif2f-test等权威评测中刷新开源模型纪录，pass@32准确率达93.9%，putnambench难题求解率达28.9%，显著领先当前主流开源竞品。
☞☞☞AI 智能聊天, 问答助手, AI 智能搜索, 多模态理解力帮你轻松跨越从0到1的创作门槛☜☜☜
One API key for 70+ AI models. Route to GPT, Claude, Gemini, Qwen, Deepseek, Grok and more
下载
统一LLM网关 - 一个API对接70+AI模型，使用单一API密钥即可调用GPT、Claude、Gemini、Qwen、Deepseek、Grok等主流模型。
LongCat-Flash-Prover 的主要功能
- 自动形式化：可将自然语言描述的数学命题精准转化为经验证无误的Lean4形式化表达式。
- 草图生成：依据原始题目及对应形式化陈述，自动生成结构清晰、含关键引理提示的证明草图框架。
- 定理证明：支持端到端输出完整可验证证明，亦可动态引入辅助引理，逐步推导目标定理。
- 工具集成推理（TIR）：模型原生支持调用Lean4编译器，在线执行语法检查、类型推断与证明验证，并基于反馈实时优化推理路径。
LongCat-Flash-Prover 的技术原理
- 混合专家迭代框架：部署多个领域特化专家子模型，分别聚焦于自动形式化、草图构建与证明生成。各专家在Lean4工具链支撑下协同生成高质量推理轨迹，并通过多轮迭代修正与反思，模拟人类数学家的学习机制，有效扩充冷启动阶段的高质量训练数据。
- 分层重要性采样策略优化（HisPO）：针对MoE模型在长程推理任务中梯度不稳定的问题，HisPO提出双层级重要性评估——在序列级与token级分别估算采样权重，主动抑制训练与推理引擎差异过大所导致的异常梯度信号，从而提升强化学习训练鲁棒性。
- 防奖励作弊机制：系统内置双重校验模块——定理一致性检测（确保证明结论与形式化目标语义一致）与合法性检测（识别未声明假设、非法公理引用或条件缺失等违规行为），从源头拦截虚假奖励驱动下的错误证明输出。
LongCat-Flash-Prover 的关键信息和使用要求
- 模型规模：5600亿参数MoE结构，是当前开源领域参数量最大的形式化推理模型之一
- 核心定位：深度适配Lean4原生生态，无需修改底层架构即可实现与形式化证明环境的无缝对接
- 性能表现：MiniF2F-Test Pass@32达93.9%，PutnamBench达28.9%，均为开源模型最高水平
- 推理效率：仅需72次尝试即可在MiniF2F-Test上达成97.1%通过率，样本利用效率远超同类方案
- 训练数据：依托混合专家迭代框架合成覆盖自动形式化、草图生成与定理证明三类任务的高质量推理轨迹
- 硬件需求：560B MoE模型推理需大规模GPU集群支持，推荐配置高显存多卡环境（如A100/H100×8+）
- 软件依赖：必须安装Lean4 v4.8+及配套工具链（包括leanproject、mathlib4等），模型通过Lean4服务器进行实时交互验证
- 部署模式：支持Whole-Proof（一次性输出完整证明）与Sketch-Proof（先生成草图再细化补全）两种方式，后者结合TIR效果更优
LongCat-Flash-Prover 的核心优势
- 原生集成能力：将形式化推理作为模型基础能力而非附加插件，天然兼容Lean4工具链，实现LLM与形式化系统的深度耦合。
- 全面SOTA表现：在MathOlympiad-Bench、MiniF2F-Test、ProofNet、ProverBench、PutnamBench五大主流评测集上均居开源模型首位，部分指标已逼近甚至超越闭源商业模型。
- 超高样本效率：MiniF2F-Test仅需72次推理即达97.1%通过率，大幅降低计算资源消耗与推理延迟。
- 可信推理保障：通过定理一致性与合法性双重检测机制，杜绝模型绕过逻辑约束获取虚假奖励的行为，确保输出结果真实可靠。
如何使用 LongCat-Flash-Prover
- 环境搭建：安装Lean4最新稳定版及其完整工具链；配置具备充足显存的GPU运行环境（建议≥8×A100 80GB），完成模型加载与服务启动。
- 模型获取：从HuggingFace平台下载预训练权重，或克隆GitHub仓库，直接复用官方提供的推理脚本与示例代码。
- 模式选择：面对简单命题可启用Whole-Proof模式快速获得终稿；对复杂问题推荐选用Sketch-Proof模式，先产出结构化草图再逐层填充细节。
- 问题输入：向模型提交自然语言数学题或待证定理，模型将自动触发Lean4编译器进行实时验证，并根据报错信息反向优化后续推理步骤。
- 结果获取：最终输出经Lean4严格验证通过的形式化证明代码，可直接导入Lean项目用于进一步研究、教学或工程验证。
LongCat-Flash-Prover 的项目地址
- GitHub仓库：https://www.php.cn/link/c4539e880b908ad22a401caf9046d152
- HuggingFace模型库：https://www.php.cn/link/3e767120d0d3139f058bf36295fc4a18
- 技术论文：https://www.php.cn/link/c4539e880b908ad22a401caf9046d152/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 | 671B | 13.9% | 82.4% | 3.3% | 此前开源SOTA，无草图生成机制 |
| Kimina-Prover-72B | 72B | 13.1% | 84.0% | 3.9% | 早期开源方案，推理效率较低 |
LongCat-Flash-Prover 的应用场景
- 学术数学研究：协助研究人员将非形式化猜想快速转译为Lean4可验证表述，并自动化探索证明路径，尤其适用于代数几何、解析数论等高度依赖形式逻辑的前沿方向。
- 数学竞赛辅导：面向IMO、Putnam等高难度赛事，提供标准化解题思路建模与形式化验证服务，帮助参赛者深入理解命题结构与证明策略。
- 形式化验证工程实践：应用于操作系统内核、密码协议、芯片指令集等关键基础设施的形式化正确性验证，提升系统安全性与可靠性保障能力。
- 智能教育辅助系统：作为交互式数学助教，为学习者提供从问题解析、引理构思、步骤展开到漏洞诊断的全流程引导，增强逻辑思维训练效果。
