1M AI Newsの監視によると、Meituan LongCatチームは、形式化定理証明言語Lean4の数学的推論タスクに特化した5600億パラメータのMoEモデル「LongCat-Flash-Prover」をオープンソース化しました。モデルの重みはMITライセンスで公開され、GitHub、Hugging Face、ModelScopeにアップロードされています。
モデルは形式的推論を三つの独立した能力に分解します：自動形式化（自然言語の数学的問題をLean4形式の文に変換）、スケッチ生成（補題スタイルの証明フレームワークを生成）、および完全な証明生成。これらの能力はすべて、Agentツールによる統合推論（TIR）とLean4コンパイラとのリアルタイムインタラクションによって検証されます。
トレーニング面では、チームがHybrid-Experts Iteration Frameworkを用いてコールドスタートデータを生成し、強化学習段階でHisPOアルゴリズムを導入してMoEモデルの長期タスクトレーニングを安定化させるとともに、リワードハッキングを防ぐために定理の一貫性と合法性検出メカニズムを追加しました。
ベンチマーク結果によると、LongCat-Flash-Prover はオープンソースの重みモデルにおいて、自動形式化と定理証明の両方で SOTA を更新しました。MiniF2F-Test ではわずか 72 回の推論で 97.1% の通過率を達成し、ProverBench と PutnamBench ではそれぞれ 70.8% と 41.5% を記録し、各問題あたりの推論回数は最大 220 回以内です。