美团开源数学定理证明模型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 深度参与前沿数学探索与文献自动化验证的时代正在加速到来。