美团龙猫开源LongCat-Flash-Prover 刷新定理证明模型SOTA纪录

2026年3月24日，美团龙猫团队正式开源面向数学形式化与定理证明的深度学习模型LongCat-Flash-Prover。该模型将形式化推理拆解为三大原子能力，破解大语言模型逻辑推演短板，在MiniF2F-Test基准测试中仅用72次推理预算即实现97.1%通过率，刷新开源Prover模型SOTA，在高难度竞赛级任务中表现也领先现有开源方案。

长期以来，大语言模型在数学推理场景始终面临“幻觉频发”的核心瓶颈，哪怕是GPT-4等头部闭源模型，也经常在需要严密逻辑链的证明题中出现步骤跳变、结论错误的问题，行业始终在寻找能实现确定性逻辑推演的技术路径。

在通用大模型的能力迭代进入瓶颈期后，数学推理能力被视为AGI落地的核心门槛之一。无论是基础数学研究中的定理验证，还是芯片设计、密码学、量子计算等工业场景中的逻辑校验，都需要模型输出100%准确的推导过程，而此前基于概率预测的大语言模型始终无法避免幻觉问题，哪怕是头部闭源模型，在需要多步骤严密推导的证明题中，错误率也始终居高不下。

此前开源领域的定理证明模型，在MiniF2F-Test基准的通过率普遍低于85%，且往往需要超过120次推理才能达到最优表现，计算成本极高，很难落地到实际场景中。

LongCat-Flash-Prover的核心创新，在于打破了此前端到端推理的传统架构，将复杂的形式化推理拆解为自动形式化、草稿生成、证明生成三大独立原子能力，每个模块针对单一任务专项优化，大幅降低了多步骤推导中的信息损耗与误差累积，实现了从“概率预测答案”到“严谨逻辑证明”的范式转变。

在官方公布的测试数据中，该模型搭配工具集成推理（TIR）策略后，在行业通用的MiniF2F-Test基准测试中，仅需72次推理预算即可实现97.1%的通过率，不仅刷新了开源Prover模型的SOTA纪录，推理成本也较此前的最优方案下降了40%。在面向奥赛、普特南数学竞赛等更高难度的MathOlympiad-Bench、PutnamBench测试集中，该模型的表现也全面超越现有开源模型，部分题目的准确率已经接近头部闭源大模型水平。

此次美团龙猫团队选择将LongCat-Flash-Prover完全开源，也填补了国内在专用推理模型领域的开源空白，全球研究者都可以直接调用模型能力或基于现有架构二次开发，无需从零开始训练。

据行业研究者介绍，该模型的落地场景十分广泛：在基础科研领域，可辅助数学家完成重复性的推导验证工作，大幅降低前沿定理证明的人力成本；在工业场景中，可用于芯片逻辑正确性校验、密码协议安全审计、AI生成代码的逻辑验证等对准确率要求极高的场景；甚至在教育领域，也可以作为智能教具，为学生提供数学证明题的 step-by-step 指导。

有业内人士指出，当前通用大模型的同质化竞争已经进入红海，而面向垂直场景的专用小模型反而有更高的落地价值，此次LongCat-Flash-Prover的推出，也为国内AI团队的技术迭代提供了新的思路。