
微新创想: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 深度参与前沿数学探索与文献自动化验证的时代正在加速到来。
