ゲートニュースによると、3月21日に美団LongCatチームがLongCat-Flash-Proverをオープンソース化しました。これは5600億パラメータのMoEモデルで、形式化定理証明言語Lean4を用いた数学的推論タスクに特化しています。モデルの重みは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回を超えません。
