美团推出超大规模数学推理模型LongCat-Flash-Prover
3月21日，美团旗下LongCat团队正式开源其最新研发的大型语言模型LongCat-Flash-Prover，该模型具备5600亿参数规模，专为处理形式化数学推理任务而设计，核心聚焦于Lean4语言环境下的定理证明能力。
三阶段推理架构实现端到端形式化建模
模型将复杂数学证明过程分解为三大模块：自然语言到形式语句的自动转换、引理级证明结构的草图生成，以及完整可验证的定理推导。每一步均通过集成Agent工具链与Lean4编译器进行实时交互校验，确保逻辑一致性与语法正确性。
创新训练框架保障长程任务稳定性
在训练策略上，团队提出Hybrid-Experts Iteration Framework用于生成初始冷启动数据集，并在强化学习阶段引入HisPO算法以增强模型在长期任务中的表现稳定性。同时，系统内置定理一致性与语法合法性双重检测机制，有效遏制奖励欺骗现象，提升训练可靠性。
多项基准测试刷新开源模型性能上限
在多个权威评测中，LongCat-Flash-Prover展现出卓越能力：于MiniF2F-Test任务中仅需72次推理即达成97.1%的通过率；在ProverBench与PutnamBench测试集上分别取得70.8%与41.5%的准确率，且单题推理次数控制在220次以内，显著优于现有同类开源模型。
