美团龙猫开源 LongCat-Flash-Prover：面向数学形式化的定理证明模型

2026年3月24日，美团龙猫（LongCat）团队宣布开源一款面向数学形式化与定理证明的深度学习模型——LongCat-Flash-Prover。该模型针对大语言模型在严密逻辑推演方面的不足，将形式化推理拆分为自动形式化（Auto-Formalization）、草稿生成（Sketching）与证明生成（Proving）三项基础能力，推动从“概率性给答案”到“可核验逻辑证明”的范式转变。

在结合工具集成式推理（TIR）策略的条件下，该模型在 MiniF2F-Test 基准上仅用 72 次推理预算就拿到 97.1% 的通过率，创下开源 Prover 模型新的 SOTA 记录。此外，在 MathOlympiad-Bench 与 PutnamBench 等高难度竞赛级任务上，其表现也全面领先当前开源模型。

技术层面，LongCat-Flash-Prover 采用了基于 TIR 的“混合专家迭代”框架。模型内置 Lean4Server 校验、语义与定理一致性检测，并对 9 类作弊行为进行合法性审查，有效遏制逻辑漏洞与代码作假。在训练阶段，引入分层 Masking 策略与 Token 级 Staleness 控制，显著提升了 MoE 架构中的强化学习稳定性。

随着 AI 推理从自然语言的模糊表达转向可被计算机验证的形式化语言，此类 Prover 模型正从单纯的“跑分工具”逐步升级为支撑基础科学研究的底层设施。这一进展预示着 AI 深度参与前沿数学探索与文献自动化校验的时代正在加速到来。

• GitHub:

  https://github.com/meituan-longcat/LongCat-Flash-Prover

• Hugging Face: https://huggingface.co/meituan-longcat/LongCat-Flash-Prover

• Report:

  https://github.com/meituan-longcat/LongCat-Flash-Prover/blob/main/LongCat_Flash_Prover_Technical_Report.pdf