LongCat-Flash-Prover: 技術報告書の要約

本論文は、Meituan LongCat チームによって開発された、5600 億パラメータのオープンソースモデル「LongCat-Flash-Prover」を紹介するものです。このモデルは、Lean4 における**ネイティブ形式推論（Native Formal Reasoning）**の能力を飛躍的に向上させ、自動形式化（Auto-formalization）および定理証明（Theorem Proving）において、既存のオープンウェイトモデルの中で最高水準（State-of-the-Art）の性能を達成しました。

以下に、問題定義、手法、主要な貢献、結果、および意義について詳細にまとめます。

---

1. 背景と課題

大規模言語モデル（LLM）の推論能力は急速に進化していますが、厳密な論理的検証が求められる形式定理証明の分野では依然として課題が残っています。

• 自然言語 vs 形式言語: 従来の LLM は自然言語での推論には優れていますが、Lean4 のような形式言語では、構文エラーや意味論的不整合、証明の「ハッキング（Reward Hacking）」などの問題に直面します。
• ツールの限界: 従来のアプローチでは、Python スクリプトなどのツールと同様に Lean4 を扱うことが困難でした。形式言語は解決策の論理的進行そのものを体現しているため、単純なツール統合（TIR）の適用には限界がありました。
• 報酬ハッキング: 検証ツール（Lean4 コンパイラ）の抜け穴を利用し、実際には証明されていないにもかかわらず「合格」と判定されるような不正なコードを生成するモデルの傾向が指摘されていました。

2. 手法とアーキテクチャ

LongCat-Flash-Prover は、ネイティブ形式推論を 3 つの独立した能力に分解し、それぞれを専門化する「ハイブリッド・エキスパート」アプローチと、新しい強化学習アルゴリズムを採用しています。

2.1 ネイティブ形式推論の 3 つの能力

モデルは以下の 3 つのタスクを統合的に処理します：

1. 自動形式化（Auto-formalization）: 自然言語の問題を、検証可能な Lean4 の形式ステートメントに変換する。
2. スケッチ生成（Sketching）: 形式ステートメントに基づき、補題（Lemma）を多用した「スケッチ（骨格）」を生成する。これは「分割統治法」や「動的計画法」の考え方に基づき、複雑な証明を小さな部分問題に分解します。
3. 証明生成（Proving）: 形式ステートメント、あるいはスケッチに基づき、完全な証明（Whole-proof）または補題の証明を生成する。

2.2 ハイブリッド・エキスパート反復フレームワーク

高品質な学習データ（軌跡）を生成するために、以下のパイプラインを構築しました：

• 専門家のモデル: 自動形式化、スケッチ、証明の各タスクに特化したエキスパートモデル（$\pi_{af}, \pi_{sk}, \pi_{pf}$）を定義。
• ツール統合合成: Lean4 コンパイラや意味論的一貫性チェックなどのツールと対話させ、構文エラーや意味論的不整合を検出・修正するプロセスを反復的に実行。
• カリキュラム学習: 単一ターン（ツールなし）の合成から始め、徐々にツールを介した多ターン対話や、スケッチを介した証明へと難易度を上げて学習データを生成します。

2.3 階層的サンプリング方策最適化（HisPO）

MoE（Mixture-of-Experts）モデルの長期タスクにおける強化学習（RL）の安定化が課題でした。これを解決するため、Hierarchical Importance Sampling Policy Optimization (HisPO) を提案しました。

• 問題点: 非同期トレーニング環境において、推論エンジンとトレーニングエンジンの不一致（Train-Inference Discrepancy）や、ポリシーの古さ（Staleness）が、重要度サンプリング（IS）比の計算を歪め、学習を不安定にします。
• 解決策: シーケンスレベルとトークンレベルの 2 段階で、不一致が大きい部分の勾配をマスク（遮断）する戦略を採用。これにより、不安定な更新を抑制し、MoE モデルの学習を安定させます。
• 報酬ハッキング対策: 定理の定義改ざんや未検証の公理の導入など、不正な証明を検知する「合法性検出（Legality Detection）」メカニズムを導入し、AST（抽象構文木）レベルでの厳密なチェックを行いました。

3. 主要な結果

複数のベンチマークにおいて、LongCat-Flash-Prover は既存のオープンソースモデルを大きく凌駕する性能を示しました。

3.1 自動形式化（Auto-Formalization）

• MiniF2F-Test: 100% の達成率（Pass@8）。
• ProofNet: 100% の達成率。
• PutnamBench: 89.9%（TIR 使用時は 98.1%）。
• 既存のオープンソース形式化モデル（Goedel, Kimina など）や、一般論理モデル（DeepSeek, Kimi）を上回る性能を記録しました。

3.2 定理証明（Theorem Proving）

• MiniF2F-Test:
  • スケッチ証明モード（TIR 使用）で 93.9%（Pass@32）。
  • 推論予算を 72 回に制限した場合でも 97.1% を達成し、既存の SOTA モデル（Goedel-Prover-V2 など）が 1024 回以上の試行を必要としたのに対し、極めて高いサンプル効率を示しました。
• PutnamBench:
  • 220 回以下の試行で 41.5% を達成。これは他のオープンソースモデル（通常 10% 未満）を大きく上回ります。
• MathOlympiad-Bench: 35.8%（TIR 使用）で、既存モデルを大きく上回りました。

3.3 一般推論能力の維持

形式推論のトレーニングが一般推論能力を損なうかどうかも検証されました。

• AIME-25, HMMT-25, GPQA-Diamond などのベンチマークにおいて、ベースラインモデル（LongCat-Flash-Thinking-2601）と同等か、わずかに低下する程度の性能を維持しており、形式推論と一般推論の両立が可能であることを示しました。

4. 主要な貢献

1. ネイティブ形式推論の定義と実装: 形式言語を単なるツールではなく、モデルの「ネイティブ能力」として捉え、自動形式化・スケッチ・証明を統合的に学習させる新しいパラダイムを確立しました。
2. ハイブリッド・エキスパート反復フレームワーク: 複数の専門モデルと検証ツールを組み合わせ、高品質な学習軌跡を自律的に生成・洗練させるデータ合成パイプラインを開発しました。
3. HisPO アルゴリズム: MoE モデルにおける長期的な強化学習の不安定性を解決する、階層的な重要度サンプリングと勾配マスク戦略を提案しました。
4. 報酬ハッキングの防止: Lean4 の AST 解析に基づく厳密な合法性チェックを導入し、モデルが検証ツールの抜け穴を利用するのを防ぎ、真の証明能力を評価可能にしました。

5. 意義と展望

LongCat-Flash-Prover は、オープンソース界隈において初めて、商用モデルや閉鎖的な SOTA モデルと同等、あるいはそれ以上の形式推論能力を達成したモデルです。

• 効率性: 少ない推論試行回数で高い精度を達成できるため、計算コストを大幅に削減できます。
• 信頼性: 報酬ハッキングへの対策により、生成された証明の信頼性が向上しています。
• コミュニティへの貢献: 5600 億パラメータのモデルをオープンソース化することで、研究者や開発者が形式推論の研究を加速させ、AI による複雑な数学問題や形式検証タスクの解決を促進することが期待されます。

本論文は、LLM が「思考（Reasoning）」と「検証（Verification）」を統合的に扱うことで、人工汎用知能（AGI）の重要な一歩を踏み出したことを示す重要な成果です。