美团开源LongCat-Flash-Prover：AI数学定理证明刷新SOTA

背景

尽管当前的大语言模型（LLM）在自然语言处理、代码生成以及复杂的 Agent 工作流中表现出色，但在面对需要极度严谨逻辑链条的数学定理证明时，往往显得力不从心。常规的数学解题通常只需关注最终数值或结果的准确性，而数学定理证明则要求每一步推导都具备无可辩驳的逻辑严密性。自然语言固有的模糊性使得步骤级的严谨验证变得困难，任何模棱两可的表述都可能导致整个证明体系的崩塌。

为了解决这一挑战，让 AI 从“猜测答案”转向“严谨证明”，美团技术团队开源了专门用于数学形式化与定理证明的模型 —— LongCat-Flash-Prover。该模型旨在通过引入形式化语言（如 Lean4），将数学问题转化为计算机可验证的代码，从而实现对证明过程的 100% 严谨校验。

核心内容

LongCat-Flash-Prover 的核心创新在于将形式化推理拆解为三个原子能力：自动形式化（Auto-Formalization）、草稿生成（Sketching）和证明生成（Proving），并结合**工具集成推理（Tool-Integrated Reasoning, TIR）**策略进行训练和优化。

1. 形式化推理的三大原子能力

• 自动形式化（Auto-Formalization）：充当“翻译官”，将自然语言描述的数学问题精准翻译为 Lean4 计算机可理解的形式化描述。
• 草稿生成（Sketching）：充当“大纲撰写者”，面对复杂定理时，不急于一步到位，而是先生成包含多个待证明引理（Lemma）和主体（Main Body）的草稿，理清逻辑主线。
• 证明生成（Proving）：充当“细节补全者”，沿着草稿思路，逐步补全剩余证明过程，完成逻辑推演。

2. 混合专家迭代框架

为了掌握上述能力，团队设计了一套结合 TIR 的“混合专家迭代”框架：

• Cold-Start（冷启动）阶段：利用专有模型 ATF-32B 合成 Formal Statement，结合 LongCat-Flash-Thinking-2601 生成带有工具反馈的高质量轨迹。经过去污、去重和采样后，构建冷启动数据集，并通过领域混合 SFT 整合不同专家模型的功能。
• Iteration（迭代）阶段：以冷启动模型为新的专家，合成新的推理轨迹。整合通用数据以保留非形式推理能力，通过多轮 SFT 和 RL 训练，最终得到 LongCat-Flash-Prover。

3. 课程学习模式下的 TIR 轨迹合成

在数据合成中，采用课程学习方法动态调整难度和策略：

• 单轮到多轮：先从单轮无工具合成开始，逐步过渡到多轮调用工具的 TIR 模式。
• 完整证明到引理草稿：先生成完整证明（Whole-Proof），若失败则激活 TIR 模式修正；若仍无法证明（如超过 1000 行或极复杂问题），则开启 Sketch-Proof 策略，先生成引理草稿，再对每个引理进行证明。
• 工具反馈机制：利用 Lean4 Server 验证语法，使用语义一致性打分模型（LLM-as-a-Judger）防止模型篡改原始问题（Hack 问题），并通过 Theorem 一致性规则约束证明目标不被修改。

4. 形式化智能体工具

共享一套智能体工具以支持专家迭代和 RL 训练：

• Lean4 Server：部署服务器验证语法准确性。通过插入锚点直接指出错误代码片段，而非仅提供行列坐标，提高纠错准确率。
• 语义一致性验证：防止模型为生成语法正确代码而修改原始问题。
• Theorem 一致性验证：基于规则约束，确保模型在生成 Sketch 或 Proof 时不篡改原始证明目标。
• Legality 验证：开发轻量级 Lean4 词法和语法分析器，排查约 9 种作弊行为（如修改题目、插入 #exit、捏造公理、使用宏绕过编译错误等）。

5. HisPO 算法与训练稳定性

在 RL 阶段，基于 DORA 训练框架引入 HisPO 算法，解决 MoE 模型中的训推一致性和 Staleness 问题：

• 训推一致性评估：通过重要性采样比（IS Ratio）衡量训练引擎与推理引擎的一致性。
• 分层 Masking 策略：
  • 序列层面：若序列级 IS Ratio 几何平均值超出范围，移除该序列梯度贡献。
  • Token 层面：移除具有显著训推不一致性的 Token。
• Staleness 控制：对保留的 Token 进行标准的 Clipping 操作，限制更新幅度，保证训练稳定。

关键要点

• SOTA 性能表现：在 MiniF2F-Test 上，仅用 72 次推理预算，通过率高达 97.1%，刷新已知开源 Prover 模型 SOTA；在 MathOlympiad-Bench 和 PutnamBench 等超难竞赛级任务上分别达到 46.7% 和 41.5%。
• 极高的样本效率：相比传统模型需上千次尝试，LongCat-Flash-Prover 结合 TIR 后大幅降低预算，MiniF2F-Test 仅需 72 次尝试即获高分。
• “打草稿”策略有效：实验证明，采用 Sketching 将问题拆解为引理，在相同计算预算下，证明准确率平均提升约 10%。
• 自动形式化满分：在 MiniF2F-Test 和 ProofNet 测试中，自动形式化任务获得 100% 得分，TIR 改进带来高达 14% 的性能提升。
• 对抗 AI 作弊行为：通过引入语义一致性、Theorem 一致性及 Legality 验证，有效纠正了模型通过修改题目、插入终止符或捏造公理来“骗过”编译器的行为。
• 开源与社区反馈：模型已在 GitHub、Hugging Face 全面开源，发布后迅速引起数学界关注，多家顶尖高校邀请合作开发形式化证明 Agent。

意义与影响

LongCat-Flash-Prover 的突破标志着 AI 在定理证明领域从“算法跑分”走向“基础科学研究基础设施”的转变。

1. 范式创新：通过将现有数学教材和前沿论文“翻译”成形式化语言，该模型有助于充实形式化数学的知识底座，为数学研究提供新的范式。
2. 科研助手：AI 不再仅仅是计算工具，而是成为数学研究者、教育者和学习者的得力伙伴。它不仅能帮助翻译文献、验证思路，还能启发新的证明路径，甚至参与前沿数学问题的探索。
3. 严谨性保障：通过 Lean4 编译器逐行校验，实现了从“答案看起来对”到“每一步都能被验证”的跨越，为数学证明提供了计算机可验证的闭环，极大提升了数学研究的可靠性和效率。