大模型向垂直专业领域进军的征程中，数学定理证明正成为检验AI逻辑推理能力的试金石。2026年3月24日，美团龙猫（LongCat）团队正式开源专门用于数学形式化与定理证明的深度学习模型——LongCat-Flash-Prover，以5600亿参数的MoE架构，在多个权威基准测试中刷新开源Prover模型SOTA纪录。

三大原子能力：从“概率预测”到“严谨证明”

当前大语言模型在严密逻辑推演中普遍存在短板——它们擅长“猜答案”，却难以输出可验证的严谨证明。LongCat-Flash-Prover的核心突破在于，将形式化推理拆解为三大原子能力，实现了推理范式的根本转变：

自动形式化：将自然语言描述的数学问题转化为Lean4形式化语言

草稿生成：构建证明的初步框架与推理思路

证明生成：输出完整、可被计算机验证的证明过程

这一设计使得模型不再依赖“概率预测”，而是能够输出严格符合逻辑的形式化证明。

基准测试刷新纪录：97.1%通过率仅需72次推理

在衡量模型逻辑推理能力的顶级基准测试中，LongCat-Flash-Prover交出了一份亮眼的成绩单：

MiniF2F-Test：在仅需72次推理尝试的条件下，通过率达到97.1%，刷新开源Prover模型SOTA纪录

PutnamBench：成功解决了41.5% 的问题，使用118次推理尝试，同样创下新纪录

ProverBench：达到70.8% 的通过率

这一表现展现了模型出色的样本效率——用更少的推理尝试实现更高的通过率，在大规模推理场景中意味着显著的成本优势。

技术架构：混合专家迭代框架与HisPO算法

为了从根本上解决逻辑漏洞与代码欺骗问题，LongCat-Flash-Prover采用了一套严谨的技术方案：

基于TIR的混合专家迭代框架：通过集成Lean4Server进行实时校验，确保证明过程的语法正确性；引入语义及定理一致性检测，排除逻辑矛盾；建立针对9种作弊行为的合法性验证机制，有效防止模型在强化学习阶段出现“投机取巧”的奖励黑客行为。

HisPO算法：针对MoE（混合专家）模型长程任务训练不稳定的顽疾，团队引入了分层重要性采样策略优化算法（Hierarchical Importance Sampling Policy Optimization）。该算法在序列和Token层面同时进行梯度掩码控制，显著提升了MoE架构下强化学习的稳定性。

分层Masking与Staleness控制：在训练阶段引入分层Masking策略与Token层面Staleness控制机制，进一步保障了模型训练的收敛效果。

从“语言模型”到“推理引擎”

随着AI推理能力从自然语言模糊处理转向计算机可验证的形式化语言，Prover模型正逐渐超越算法跑分范式，转化为基础科学研究的“底座设施”。

LongCat-Flash-Prover的突破预示着AI深度参与前沿数学探索与文献自动化验证的时代正在加速到来。这类模型可在数学猜想验证、自动化定理证明、代码形式化验证等场景中发挥关键作用，为数学研究、软件安全验证等领域提供新的工具支撑。

展望：AI深度参与数学探索的时代

LongCat-Flash-Prover的发布，标志着开源社区在形式化推理领域迈出了关键一步。在美团龙猫团队此前的LongCat-Flash-Thinking模型中，已展现出同时具备“深度思考+工具调用”与“非形式化+形式化”推理能力的潜力。此次发布的Prover版本进一步聚焦形式化数学证明，将AI的严谨推理能力提升到了新的高度。

随着大模型推理能力从“能说会道”向“严谨推导”演进，AI参与前沿数学研究、文献自动化验证、高可靠性代码验证的场景正在从设想走向现实。这场由开源社区驱动的“严谨推理革命”，才刚刚拉开序幕