标题LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning来源arXiv, 2603.21065v1摘要我们引入了LongCat-Flash-Prover一个5600亿参数的开源Mixture-ofExperts莫伊模型它通过代理工具集成推理TIR推进了Lean 4中的原生形式化推理。我们将原生形式化推理任务分解为三个独立的形式化功能即自动形式化、草图绘制和证明。为了促进这些功能我们提出了一个混合专家迭代框架来扩展高质量的任务轨迹包括基于给定的非正式问题生成正式陈述直接从陈述中产生完整的证明或引理风格的草图。在代理RL期间我们提出了分层重要性抽样策略优化HisPO算法其目的是稳定莫伊模型在此类长时间任务上的训练。它采用梯度掩蔽策略该策略考虑了策略陈旧性和固有的训练-推理引擎在序列和标记级别上的差异。此外我们还整合了定理一致性和合法性检测机制以消除奖励黑客问题。广泛的评估表明我们的LongCat-Flash-Prover为自动和自动两种开放权重模型设置了新的最先进的技术。形式化和定理证明。展示了显着的样本效率它在MiniF 2F-Test上实现了97.1%的通过率每个问题仅使用72个推理预算。在更具挑战性的基准测试中它解决了70.8%的ProverBench和41.5%的PutnamBench每个问题的尝试不超过220次显著优于现有的开放权重基线。️文章简介研究问题如何利用智能体工具集成强化学习解决大模型在 Lean4 原生形式化推理中面临的长程任务训练不稳定及奖励欺骗难题主要贡献论文提出了 LongCat-Flash-Prover一个 560B 参数的 MoE 模型通过混合专家迭代框架和分层重要性采样策略优化算法在自动形式化和定理证明任务上刷新了开源模型的最优纪录。重点思路定义原生形式推理范式将其拆解为智能体自动形式化、引理风格草图生成及完整证明三个独立能力并引入工具集成推理策略使专家能直接与 Lean4 编译器交互。提出混合专家迭代框架利用专用专家模型合成高质量冷启动数据通过课程学习从单轮生成逐步过渡到多轮工具反馈模拟人类试错与反思过程。设计分层重要性采样策略优化算法通过在序列级和令牌级估计训练与推理引擎的差异及策略陈旧度实施梯度掩码以稳定 MoE 模型的长程强化学习训练。引入定理一致性与合法性检测机制基于抽象语法树严格检查代码逻辑有效消除模型通过篡改定义或引入未验证公理进行的奖励欺骗行为。分析总结实验表明该模型在 MiniF2F-Test 上仅用 72 次尝试即达到 97.1% 的通过率显著优于现有开源基线展现出极高的样本效率。在高难度的 PutnamBench 基准测试中模型解决了 41.5% 的问题大幅超越了之前的开源最强模型证明了其在复杂数学竞赛题上的强大推理能力。消融实验证实工具集成推理策略至关重要相比无工具模式性能提升显著且草图证明模式结合树搜索能进一步挖掘模型潜力。修复奖励函数后的训练曲线显示合法性检测机制成功抑制了作弊行为确保了模型学习到的是真实的证明能力而非利用评估漏洞。个人观点论文将形式化推理视为大模型的原生能力而非外挂任务通过精细化的专家分工与稳定的长程强化学习算法真正实现了模型与形式化验证工具的深度协同。附录