美团 LongCat 团队最新开源的 LongCat-Flash-Prover，一款拥有5600亿参数的专家混合（MoE）模型，专门针对形式化定理证明语言 Lean4 的数学推理任务，掀起了行业新的风潮。
【创新特性亮点】
– **强大能力整合**：模型将形式化推理细化为三大核心能力：
– **自动形式化**：自然语言数学问题到 Lean4 形式语句的无缝转化。
– **草图生成**：提供类似引理的证明框架，为后续验证建立基础。
– **完整证明生成**：生成完整、严谨的数学证明，流程高效可靠。
– **实时验证**：三项能力通过智能Agent工具集成推理（TIR），结合Lean4编译器，实现边推理边验证，确保每一步的正确性。
【先进的训练策略】
团队采用**Hybrid-Experts Iteration Framework**，通过生成冷启动数据，推动模型快速适应任务需求。在强化学习阶段，引入创新的HisPO算法，不仅保证长程任务训练的稳定性，还结合定理一致性和合法性检测机制，有效防止奖励黑客（reward hacking）现象，确保模型真正“学有所用”。
【卓越的性能表现】
在多个公开基准测试中，LongCat-Flash-Prover刷新了自动形式化和定理证明的多项SOTA纪录：
– **MiniF2F-Test**：仅用72次推理，即达到97.1%的高通关率。
– **ProverBench**：表现优异，突破70.8%的成功率。
– **PutnamBench**：也取得了41.5%的突出成绩。
所有测试中，每题推理次数均不超过220次，效率极高！
【资源与合作】
模型权重已完全遵循MIT协议开源，现已同步上线GitHub、Hugging Face和ModelScope，为广大研究者和开发者提供宝贵的资源支持。
未来，LongCat-Flash-Prover有望成为数学自动推理、形式化验证领域的核心工具，引领AI在复杂数学证明中的创新前沿。
原创文章，作者：admin，如若转载，请注明出处：https://www.23btc.com/161451/
