美团又开源！专攻数学定理证明，能模拟人类解题，刷新多项开源SOTA
LongCat-Flash-Prover 是美团最新发布并开源的一款专攻数学定理证明的大语言模型。该模型拥有5677亿参数，采用了混合专家（MoE）架构，旨在通过模拟人类的方式解决复杂几何、代数等数学证明问题。
核心架构与技术原理
该模型的核心在于其独特的训练与验证机制，主要通过以下三点实现高效且准确的定理证明：
- 混合专家迭代框架（Hybrid-experts Iteration Framework）：这是模型生成高质量训练数据的关键。该框架能够生成大规模的形式化推理轨迹，为后续的模型训练提供了坚实的基础。
- 严格的多阶段验证：为了消除大模型常见的“幻觉”现象（即生成看似合理但实际错误的内容），LongCat-Flash-Prover 引入了基于抽象语法树（AST）的多阶段严格验证流程，并深度整合了形式化证明语言 Lean4。
- 稳定且防作弊的训练策略：
- 在冷启动阶段，利用混合专家迭代框架生成数据。
- 在强化学习阶段，引入了 HisPO 算法，有效稳定了 MoE 模型在长程任务中的训练过程。
- 同时加入定理一致性和合法性检测机制，专门用于防止模型利用规则漏洞换取高分的“Reward Hacking”（奖励黑客）行为。
刷新多项开源SOTA成绩
在公认的数学定理证明基准测试中，LongCat-Flash-Prover 展现了超越现有开源模型的强大性能：
- MiniF2F-Test：这是一个广泛使用的数学竞赛级测试集。该模型取得了 97.1% 的惊人成绩，且仅需平均 72次 推理尝试。
- PutnamBench：这是一个更具挑战性的基准，包含高难度的大学数学竞赛题目。该模型解决了其中 41.5% 的问题，使用平均 118次 推理尝试。
上述两项成绩均在开源模型中刷新了目前的最好水平（SOTA），甚至在某些指标上超越了参数量更大的模型（如DeepSeek 671B），证明了其在深度推理能力上的高效性。
行业背景与开源意义
数学定理证明被视为人工智能推理能力的“试金石”，一直是前沿AI研究的重点方向。此前，普林斯顿等团队发布的模型虽已取得突破，但美团此次开源的 LongCat-Flash-Prover 进一步降低了高质量数学AI模型的使用门槛。
通过开源模型权重、代码及相关的 GitHub 和 Hugging Face 资源，美团不仅展示了其在大模型底层技术上的积累，也为学术界和工业界提供了一个强有力的工具，有助于推动形式化验证与人工智能结合的进一步发展。