LongCat-Flash-Prover – 美团开源的数学定理证明模型

LongCat-Flash-Prover是什么

LongCat-Flash-Prover 是美团开源的5600亿参数MoE模型，专注Lean4形式化数学推理。模型通过Agentic工具集成推理（TIR），将任务分解为自动形式化、草图生成和定理证明三大能力。LongCat-Flash-Prover采用混合专家迭代框架和HisPO强化学习算法稳定训练，引入防作弊机制确保推理严谨性。在MiniF2F-Test等基准测试中达到SOTA水平，Pass@32准确率93.9%，PutnamBench难题解决率28.9%，显著超越现有开源模型。

LongCat-Flash-Prover的主要功能

• 自动形式化：支持将自然语言数学问题转化为经过验证的Lean4形式化陈述。