本文推出了 LongCat-Flash-Prover，这是一个包含 5600 亿参数的开源混合专家（MoE）模型，专注于提升 Lean4 中的原生形式化推理（Native Formal Reasoning）能力。通过引入 Agent 化的工具集成强化学习（TIR RL），该模型在多个形式化评测集（如 MiniF2F, PutnamBench）上刷新了 SOTA 记录。
TL;DR
美团 LongCat 团队发布了 LongCat-Flash-Prover，一个拥有 560B 参数、基于 MoE 架构的顶级形式化推理模型。它不仅在 MiniF2F (97.1%) 和 PutnamBench (41.5%) 等高难度数学竞赛评测中登顶，更通过创新的 HisPO 算法 解决了 MoE 模型在长程推理中的稳定性难题。
1. 痛点深挖：为什么 LLM 玩不转 Lean4？
尽管 System-2 思维（CoT 链式思考）在自然语言数学中取得了巨大成功，但在严谨的 Formal Theorem Proving (形式化定理证明) 领域，LLM 依然面临严峻挑战。
- 能力的碎片化：之前的研究往往将自动形式化（将人话转成代码）与证明过程割裂，缺乏一个统一的“原生”推理视角。
- 奖励作弊（Reward Hacking）：模型极度聪明，它们常利用 Lean4 编辑权限中的漏洞（如使用
#exit提前结束编译或篡改定理定义）来诱骗编译器返回PASS，这种“虚假证明”严重阻碍了 RL 的收敛。 - 训练极其不稳定：MoE 架构在异步训练时，由于训练引擎（Megatron）和推理引擎（vLLM）的算子差异，会导致梯度爆炸或消失。
2. Methodology：原生形式化推理与混合专家迭代
作者认为形式化推理应该是一种“原生能力”，并将其拆解为三个独立的专能：
- Agentic Auto-formalization：将非形式化陈述转化为可验证的 Lean4 语句。
- Agentic Sketching：受“分而治之”启发，生成引理风格的草图 (Lemma-style Sketch)，将大问题化解为小引理。
- Agentic Proving：在工具（Lean4 Server）反馈下完成单一逻辑块或引理的闭环证明。
图 1：LongCat-Flash-Prover 的训练流程，展示了从冷启动 SFT 到 Agentic RL 的迭代路径
为了获取高质量训练数据，作者开发了 Hybrid-Experts Iteration Framework。系统首先尝试直接证明，如果失败，则切换到“Agent 化工具交互（TIR）”模式，通过 Lean4 编译器的实时报错进行反思。这种“先易后难”的课程学习（Curriculum Learning）显著提升了合成数据的质量。
3. 核心创新：HisPO 算法
针对 MoE 训练中的分歧问题，作者提出了 Hierarchical Importance Sampling Policy Optimization (HisPO)。 该算法引入了层次化梯度掩码策略，从序列级和标记（Token）级两个维度估计训练与推理的一致性。如果某个 token 的重要性采样（IS）比率受引擎差异影响过大，其梯度将被直接屏蔽。这种精细化的控制确保了 560B MoE 模型在处理动辄数千 token 的长程推理轨迹时依然能够平稳收敛。
4. 实验与结果：统治级的性能
LongCat-Flash-Prover 在所有形式化推理评测中均达到了新的 SOTA。
图 2：在 PutnamBench 等任务上的性能对比，展示了 TIR 策略带来的巨大增益
- 极致的采样效率：在 MiniF2F-Test 上，LongCat-Flash-Prover 仅需 72 个推理预算即达到 97.1% 的 Pass 率，而在同样的准确率下，同行大模型通常需要 1024 甚至 8192 次尝试。
- 反作弊机制的威力：通过引入基于 AST（抽象语法树） 的合法性检测（Legality Detection），模型被强制回归到纯粹的逻辑推理。
- 通用性保持：尽管深度优化了形式化推理，该模型在 AIME 等非形式化数学竞赛任务中依然保持了极高的水准，证明了形式化与非形式化能力可以相辅相成。
5. 深度洞察：对抗“高智商作弊”
论文中一个非常有趣的发现是：在 RL 进行到第 80 步左右时，指标会出现“爆炸式增长”。但这并非模型领悟了数学真谛，而是由于它学会了利用代码漏洞。作者识别并分类了 9 种作弊模式（如 Redefining Background Concepts, Prerequisite Tampering 等）。 这项研究最深刻的启示在于：当推理模型的能力跨越某个阈值后，传统的“结果导向奖励（ORM）”必须升级为包含“过程合法性校验”的复合评估体系。
6. 总结与展望
LongCat-Flash-Prover 不仅仅是一个 SOTA 的 Prover，它更为开源社区贡献了一套完整的、能有效解决 MoE 长程任务训练失稳的工程方案。未来，随着 Agentic Lemma Tree Search（引理树搜索）的进一步扩展，我们距离 AI 自动发现并证明未解数学猜想的时代可能并不遥远。