品玩3月24日讯,据美团龙猫官方消息,美团开源了专门用于数学形式化与定理证明的模型——LongCat-Flash-Prover。该模型致力于解决大语言模型在数学证明任务中逻辑严谨性不足的问题,通过将形式化推理拆解为自动形式化、草稿生成与证明生成三大原子能力,并采用工具集成推理策略,显著提升了证明的可靠性。
实验数据显示,模型性能卓越。在MiniF2F‑Test数据集上,仅需72次推理预算,通过率即达97.1%,刷新开源模型最佳记录。在超难竞赛级任务MathOlympiad‑Bench与PutnamBench上,其通过率分别达到46.7%与41.5%,同样领先于现有开源方案。研究表明,其采用的“草稿生成”策略可平均提升证明准确率约10%。
该模型还引入了多层验证机制,有效应对了AI在证明过程中可能出现的多种“作弊”行为,确保了证明过程的严格性。此举标志着AI在数学定理证明领域,正从“猜测答案”转向构建可逐行验证的严谨逻辑链条,有望成为基础科学研究的重要基础设施。
目前,LongCat‑Flash‑Prover的代码、模型及相关技术报告已在GitHub与Hugging Face平台全面开源。