美团开源560B参数MoE定理证明模型
美团LongCat团队开源了LongCat-Flash-Prover模型。这是一个拥有5600亿参数的混合专家模型，专门用于形式化定理证明语言Lean4的数学推理任务。模型权重已按MIT协议在GitHub、Hugging Face和ModelScope发布。
核心能力与验证机制
模型将形式化推理分解为三项独立能力：
- 自动形式化：将自然语言数学问题转化为Lean4形式语句。
- 草图生成：产出引理风格的证明框架。
- 完整证明生成：生成最终证明。
所有能力均通过Agent工具集成推理与Lean4编译器进行实时交互验证。
训练方法与性能表现
团队采用Hybrid-Experts Iteration Framework生成训练数据，并在强化学习阶段引入HisPO算法以稳定MoE模型的长程任务训练，同时加入防作弊检测机制。
在基准测试中，该模型刷新了开源模型在自动形式化和定理证明两项任务上的SOTA记录：
- MiniF2F-Test：仅用72次推理即达到97.1%的通过率。
- ProverBench：通过率达70.8%。
- PutnamBench：通过率达41.5%。
各项测试中，每道题的推理次数均不超过220次。
