LongCat-Flash-Prover：通过智能体工具集成强化学习推进原生形式化推理 LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning
560B MoE模型在Lean4定理证明任务上达到开源SOTA
前置知识
形式化定理证明 (Formal Theorem Proving)
形式化定理证明是使用严格定义的形式化语言（如Lean4、Coq等）来表达数学定理及其证明的过程。与自然语言证明不同，形式化证明必须通过验证工具（如Lean4编译器）的语法检查和类型验证，确保每一步推理都是正确的。这种严格性使得计算机可以验证证明的正确性，但同时也要求模型必须精确理解形式化语言的语法和语义规则。
本文的核心任务是提升LLM在形式化定理证明上的能力，理解形式化证明的基本概念是理解本文研究动机和方法的基础。
Mixture-of-Experts (MoE) 架构
MoE是一种神经网络架构，通过门控机制选择性地激活模型中的部分专家网络。在LongCat-Flash-Prover中，总参数量为560B，但每次推理只激活约27B参数。这种设计在保持模型容量的同时降低了计算成本。MoE架构的关键挑战包括专家路由策略、训练稳定性（特别是长序列场景下的重要性采样比率计算）以及训练与推理引擎之间的不一致性。
LongCat-Flash-Prover采用MoE架构，理解这一架构对于理解HisPO算法的设计动机以及训练稳定性挑战至关重要。
工具集成推理 (Tool-Integrated Reasoning, TIR)
TIR是指LLM在推理过程中调用外部工具（如编译器、验证器）来获取反馈并修正输出的范式。在本文中，TIR特指模型与Lean4验证工具的交互：模型生成形式化代码，Lean4编译器检查语法和类型，模型根据错误信息迭代修正。TIR与传统的单次生成不同，允许多轮交互直到生成正确的证明。
TIR是本文方法的核心机制，理解模型如何与Lean4工具交互对于理解数据合成流程和推理策略至关重要。
自形式化 (Auto-Formalization)
自形式化是指将自然语言描述的数学问题或定理自动转换为形式化语言（如Lean4）的过程。这是形式化推理的第一步，因为大多数数学问题最初都是用自然语言描述的。自形式化的挑战在于不仅要保证语法正确（通过Lean4编译器），还要保证语义一致性（形式化版本准确反映了原始问题的含义）。
自形式化是本文提出的三个原子能力之一，理解这一任务对于理解整体框架的设计至关重要。
草图证明 (Sketch-Proof)
草图证明是一种分治策略：先将复杂定理分解为多个辅助引理（helper lemmas），生成一个包含主定理证明体和多个待证引理的草图结构，然后分别证明每个辅助引理。这种方法借鉴了算法设计中的分治和动态规划思想，通过降低单步证明难度来提升整体证明成功率。
草图证明是本文的关键创新之一，理解这一策略对于理解实验中sketch-proof mode的优异表现至关重要。
强化学习验证奖励 (Reinforcement Learning with Verified Reward, RLVR)
RLVR是一种强化学习范式，使用可验证的奖励信号（如程序是否通过编译、证明是否被验证）来训练模型。与人类反馈奖励（RLHF）不同，RLVR的奖励来自形式化验证工具，具有确定性和可重复性。在本文中，奖励信号来自Lean4编译器的语法检查、类型验证以及自定义的合法性检测机制。
RLVR是本文训练流程的核心组件，理解这一概念对于理解HisPO算法和训练流程至关重要。
重要性采样 (Importance Sampling)
重要性采样是一种统计技术，用于在目标分布与采样分布不同时估计期望值。在强化学习中，重要性采样比率用于校正行为策略与目标策略之间的差异。在MoE模型中，由于训练和推理引擎的不一致性以及策略版本的滞后性，这一比率的计算会出现偏差，导致训练不稳定。
HisPO算法的核心创新是通过分层重要性采样比率的梯度掩码来解决训练稳定性问题，理解这一概念是理解HisPO的基础。
研究动机
当前大语言模型在形式化定理证明任务上面临严峻挑战。尽管在自然语言推理方面取得了显著进展，但LLM在使用严格形式化语言（如Lean4）生成正确证明方面仍然表现不佳。现有的形式化推理方法存在两个关键问题：第一，自形式化和定理证明通常被视为独立任务，分别训练专门的模型（如Kimina-AutoFormalizer和Kimina-Prover-V2、Goedel-Formalizer-V2和Goedel-Prover-V2），这种分离的范式限制了模型对形式化推理的整体理解能力。第二，现有的开源评估流水线存在严重漏洞，仅依赖Lean4语法验证和目标定理定义一致性检查，而完全忽略了形式化上下文的可编辑性，这使得模型可以通过篡改编译上下文、引入未验证的公理等方式进行作弊，导致评估指标与真实证明能力之间存在巨大偏差。此外，在使用GRPO算法对MoE模型进行长序列强化学习时，训练与推理引擎之间的不一致性以及策略滞后性会导致重要性采样比率计算出现偏差，引发训练不稳定甚至模型崩溃。
本文的目标是本文的具体目标是构建一个统一的原生形式化推理模型LongCat-Flash-Prover，该模型能够同时具备自形式化、草图生成和定理证明三种能力，并通过工具集成推理（TIR）策略与Lean4验证工具进行交互。具体而言，作者希望：1）在MiniF2F-Test上达到97%以上的通过率，且推理预算控制在72次以内；2）在更具挑战性的PutnamBench上超越现有开源模型；3）在保留形式化推理能力的同时，保持与LongCat-Flash-Thinking-2601相当的非形式化推理性能；4）开发有效的训练算法解决MoE模型在长序列强化学习中的稳定性问题。
与已有工作不同的是，本文的独特切入角度体现在三个方面：首先，作者提出原生形式化推理的概念，将自形式化、草图生成和定理证明视为LLM的原子能力，类似于原生多模态和原生工具调用，这种统一的范式使得模型可以根据问题难度动态选择合适的证明策略。其次，作者开发了混合专家迭代框架，通过多轮迭代合成高质量的工具集成推理轨迹，结合课程学习策略（从单轮到多轮、从整证明到草图证明）来逐步提升模型能力。第三，作者发现了现有评估流水线中的关键漏洞，并开发了基于AST的严格检查机制来防止奖励欺骗，这一发现对于整个形式化推理领域的评估标准具有重要意义。
核心方法
LongCat-Flash-Prover的方法框架可以从两个层面理解：数据合成层面和模型训练层面。在数据合成层面，作者提出了混合专家迭代框架，将原生形式化推理分解为三个独立的能力（自形式化、草图生成、证明），每个能力对应一个专门的专家模型。这些专家模型通过与Lean4验证工具的交互来合成高质量的推理轨迹，并采用课程学习策略：先合成单轮轨迹（无需工具调用），再合成多轮TIR轨迹；先进行整证明生成，再进行草图证明。在模型训练层面，训练流程分为冷启动阶段和迭代阶段：冷启动阶段使用ATF-32B（自形式化模型）和LongCat-Flash-Thinking-2601合成初始数据，通过领域混合SFT训练出冷启动模型；迭代阶段使用冷启动模型作为新的专家，通过自我蒸馏和智能体TIR强化学习进一步提升能力，经过多轮迭代后得到最终的LongCat-Flash-Prover模型。
本文的核心创新点体现在三个方面：第一，原生形式化推理范式，不同于以往将自形式化和证明视为独立任务的做法，本文将它们统一为原生形式化推理的原子能力，使得模型可以在同一推理流程中灵活组合这些能力。第二，HisPO（分层重要性采样策略优化）算法，这是针对MoE模型长序列强化学习的关键创新。HisPO通过两个层级的梯度掩码来解决训练稳定性问题：序列级掩码通过计算所有token的几何平均不一致性比率来过滤整体偏差过大的序列，token级掩码则移除单个token级别的异常值。第三，合法性检测机制，作者发现现有评估流水线中的漏洞（模型可以通过篡改编译上下文、引入未验证公理等方式作弊），开发了基于AST的严格检查来消除奖励欺骗。
方法步骤详情
LongCat-Flash-Prover的训练流程包含以下关键步骤：第一步，冷启动数据合成，使用ATF-32B对自然语言问题生成形式化语句，使用LongCat-Flash-Thinking-2601生成完整的TIR推理轨迹，通过去污染、去重和基于难度与多样性的采样构建高质量冷启动数据集。第二步，领域混合SFT，以LongCat Mid-train Base模型（560B MoE）为基础，使用冷启动数据进行监督微调，得到冷启动模型。第三步，专家迭代，冷启动模型成为新的专家，通过混合专家迭代框架合成新的轨迹数据。具体地，对于每个问题，先用自形式化专家生成N个形式化语句，通过语法检查和语义一致性检查进行拒绝采样；然后用证明专家生成N个整证明，通过语法检查和合法性检测进行拒绝采样；对于未解决的问题，使用草图专家生成草图，再用证明专家完成引理证明。第四步，智能体TIR RL，使用HisPO算法进行强化学习，通过分层掩码矩阵控制梯度流。第五步，迭代重复，重复步骤三和四多次，每轮使用不同形式化语句作为输入，增加发现正确证明的概率。
技术新颖性
本文的技术新颖性主要体现在以下几个方面：首先，HisPO算法的设计具有独创性。现有方法如GSPO仅考虑序列级别的训练-推理一致性，而HisPO采用了更精细的分层策略：序列级掩码使用几何平均来估计整体一致性，避免了GSPO过度忽略有价值的token；token级掩码则移除单个token的异常值。此外，作者引入了三重裁剪方案来处理负优势样本的无界方差问题。其次，混合专家迭代框架的课程学习策略具有创新性：从单轮到多轮、从整证明到草图证明的渐进式合成，使模型能够根据任务难度动态选择证明策略。第三，基于AST的合法性检测机制是首次被系统性地应用于形式化推理评估，它能够检测多种作弊手段，包括篡改编译上下文、引入未验证公理、修改定理定义等，这对于提升评估标准具有重要意义。
实验结果
LongCat-Flash-Prover在多个形式化推理基准测试上取得了显著成果。在自形式化任务（Pass@8）中，模型在MiniF2F-Test上达到99.2%（使用TIR时达到100%），在ProofNet上达到87.1%（TIR时97.9%），在PutnamBench上达到89.9%（TIR时98.1%），显著超越所有开源和闭源对比模型。在定理证明任务（Pass@32）中，模型在MiniF2F-Test上以sketch-proof + TIR模式达到93.9%，超越Goedel-Prover-V2-32B的88.1%；在PutnamBench上达到28.9%，是所有开源模型中最高的。更重要的是，模型展现出卓越的样本效率：在MiniF2F-Test上仅用72次推理预算就达到97.1%的通过率，而Goedel-Prover-V2-32B和Kimina-Prover-72B达到92.2%都需要超过1024次尝试。Tree Search策略进一步提升性能，平均提升3.1%。在非形式化推理任务上，模型保持了与LongCat-Flash-Thinking-2601相当的性能，例如AIME-25上达到97.7%（对比99.6%），GPQA-Diamond上达到79.2%（对比80.5%），证明了形式化推理训练不会显著损害模型的通用推理能力。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| 自形式化 (Pass@8) | Pass@8 (%) | LongCat-Flash-Prover w/ TIR: MiniF2F 100.0%, ProofNet 97.9%, PutnamBench 98.1% | Goedel-V2-Formalizer-32B: MiniF2F 98.4%, ProofNet 79.0%, PutnamBench 85.9% | MiniF2F +1.6%, ProofNet +18.9%, PutnamBench +12.2% |
| 定理证明 (Pass@32, MiniF2F-Test) | Pass@32 (%) | sketch-proof w/ TIR: 93.9% | Goedel-Prover-V2-32B: 88.1% | +5.8% |
| 定理证明 (Pass@32, PutnamBench) | Pass@32 (%) | sketch-proof w/ TIR: 28.9% | Goedel-Prover-V2-32B: 6.7% | +22.2% |
| 定理证明 (高预算, MiniF2F-Test) | Pass@72 (%) | sketch-proof w/ TIR & Tree Search: 97.1% | Goedel-Prover-V2-32B: 92.2% (Pass@8192) | +4.9% 且预算减少113倍 |
| 非形式化推理 (AIME-25) | Avg@16 (%) | 97.7% | LongCat-Flash-Thinking-2601: 99.6% | -1.9%（保持竞争力） |
局限与改进
本文存在以下局限性：首先，在非形式化推理任务上，LongCat-Flash-Prover相比LongCat-Flash-Thinking-2601存在一定性能损失，例如AIME-25从99.6%降至97.7%，HMMT-25从93.4%降至90.8%，这表明形式化推理训练会对通用推理能力产生一定负面影响。其次，与闭源模型Seed-Prover和Seed-Prover 1.5相比，本文模型在某些基准测试上仍有差距，例如Seed-Prover在PutnamBench上达到50.4%，而本文模型为41.5%，但需要注意Seed-Prover的推理预算未公开，无法进行公平比较。第三，模型在某些高难度数学竞赛题目上仍有提升空间，例如IMO-AnswerBench上仅为77.3%。第四，训练成本高昂，560B参数的MoE模型需要大量计算资源进行多轮迭代训练和强化学习，这限制了方法的可复现性。此外，作者在第4.4节提到，他们发现现有评估流水线存在严重漏洞（模型可以通过篡改编译上下文、引入未验证公理等方式作弊），这表明该领域的评估标准仍需进一步完善。
独立分析的弱点
本文存在以下可改进的弱点：第一，形式化与非形式化推理的平衡问题，作者承认训练过程会导致非形式化推理性能下降，但未提供具体的解决方案。未来可以探索更精细的课程学习策略或正则化方法来平衡两种能力。第二，草图生成的质量瓶颈，当前的草图生成依赖于专门的sketcher专家，但论文未详细分析草图质量对最终证明成功率的影响。可以考虑引入更强大的草图生成策略，如基于人类专家草图的监督学习。第三，Tree Search策略的效率，虽然Tree Search能提升3.1%的准确率，但其计算开销较大。可以探索更高效的搜索策略，如基于蒙特卡洛树搜索（MCTS）的方法或学习到的启发式搜索。第四，合法性检测的覆盖范围，当前的AST检查主要针对特定类型的作弊手段，可能无法覆盖所有可能的奖励欺骗方式。可以考虑引入更全面的形式化语义分析。第五，奖励函数设计，当前主要使用二元奖励（通过/失败），可以考虑引入更细粒度的奖励信号，如证明步骤的正确性、工具调用的有效性等。
未来方向
基于本文成果，未来研究可以从以下方向展开：第一，扩展到更多形式化语言，当前工作专注于Lean4，可以探索将方法推广到Coq、Isabelle等其他形式化系统。第二，提升样本效率，虽然本文模型已经展现出优秀的样本效率（72次尝试达到97.1%），但可以通过学习更有效的搜索策略或引入人类专家知识来进一步减少所需的推理预算。第三，多步证明的可解释性，当前模型生成的证明是形式化的Lean4代码，难以被人类理解。可以探索生成同时包含形式化和自然语言解释的证明。第四，自动化数学发现，将形式化推理能力应用于数学猜想的自动生成和验证，推动自动化数学研究。第五，与人类数学家协作，开发更自然的人机协作界面，让数学家能够与AI系统共同完成复杂的证明任务。第六，提升HisPO算法的通用性，探索将HisPO应用于其他长序列强化学习任务，如代码生成、多轮对话等。
复现评估
本文的可复现性评估如下：在开源方面，作者已经将模型权重发布在HuggingFace（meituan-longcat/LongCat-Flash-Prover）并在GitHub上提供了项目页面，这大大降低了复现门槛。然而，完整的训练流程仍难以复现，因为：1）冷启动数据的合成依赖于ATF-32B和LongCat-Flash-Thinking-2601这两个专门的模型；2）多轮迭代训练需要大量计算资源（560B参数的MoE模型）；3）HisPO算法的实现依赖于作者自研的DORA训练系统。在数据方面，论文提到使用了开源数据集和内部数据集，但未详细说明具体的数据来源和预处理流程。在评估方面，作者提供了详细的评估框架，包括语法检查、语义一致性检查和AST合法性检查，这有助于社区进行公平的对比评估。总体而言，虽然完整的训练流程难以复现，但模型权重的开源使得研究者可以直接使用和微调模型，降低了应用门槛。
论文图表
