LongCat-Flash-Prover：Meituanの5,600億パラメータエージェント型モデルが形式的推論の新基準を樹立

Meituanが、エージェント型ツール統合強化学習を通じて形式的数学推論を推進する5,600億パラメータのMixture-of-Expertsモデル「LongCat-Flash-Prover」をオープンソースで公開した。このモデルは、Lean4における自動形式化と定理証明の両方でオープンウェイトモデルの新たな最高水準を達成している。

モデルは形式的推論を自動形式化、スケッチ、証明という3つの独立した能力に分解し、MoEの長期ホライズンタスクにおける訓練を安定化させる新しいHierarchical Importance Sampling Policy Optimization（HisPO）アルゴリズムを使用する。グラディエントマスキング戦略により、シーケンスおよびトークンの両レベルでポリシーの陳腐化と訓練・推論エンジンの不一致に対処している。

システムはHybrid-Experts Iteration Frameworkを採用し、高品質なタスク軌跡を拡張する。非形式的な問題から形式的な命題を生成したり、完全な証明を直接生成したり、補題スタイルのスケッチを作成したりする。定理の一貫性チェックと合法性検出メカニズムにより、報酬ハッキングを排除している。

エージェントエコシステムにおいて、LongCat-Flash-Proverは、エージェント型RL訓練が標準的なファインチューニングをはるかに超えて専門的な推論能力を押し上げられることを実証している。RL中にモデルがLean4の証明アシスタントを外部ツールとして使用する方法を学習するツール統合アプローチは、外部ツールを効果的に活用する必要のあるあらゆるエージェントに一般化できるパターンである。

GitHub：https://github.com/meituan-longcat/LongCat-Flash-Prover
論文：https://arxiv.org/abs/2603.21065