美团开源560B参数推理模型LongCat：融合Agent工具调用，登顶Lean4定理证明SOTA

美团正式开源代号为LongCat-Flash-Prover的5600亿参数MoE模型。该模型将形式化推理拆解为自动形式化、草图生成及完整证明生成三大核心能力，并创新性地通过Agent工具集成推理与Lean4编译器进行实时交互验证。在训练上，团队采用Hybrid-Experts框架生成冷启动数据，并引入HisPO算法优化MoE长程任务训练。测试显示，该模型在MiniF2F-Test上以72次推理达到97.1%的通过率，刷新了开源模型在自动形式化和定理证明领域的SOTA记录。