大規模モデルが垂直専門分野に進出する道のりにおいて、メイクドンはついに学術界と産業界を驚かせる結果を提示しました。

3月21日、メイクドンは、超大規模な数学証明モデルであるLongCat-Flash-Proverを正式にオープンソース化しました。この5677億パラメータを持つ巨大なモデルは、高度なMoE（混合エキスパートモデル）構造を採用しており、非常に複雑な数学形式的証明問題に対して深く最適化されています。

image.png

論理推論能力を測定する上位のベンチマークテストにおいて、LongCat-Flash-Proverは圧倒的な実力を示しました:

記録更新: MiniF2F-Testテストで97.1%という驚異的な成績を達成し、わずか72回の推論試行で可能です。

難題の解決: PutnamBenchタスクで41.5%の問題を成功裏に解決し、この二つのデータはともに世界最高水準（SOTA）を更新しました。

大規模モデルが「数学者」のように厳密になるために、メイクドンは技術的なアプローチでいくつかの重要な突破を遂げました:

幻覚の排除: AST（抽象構文木）に基づいた多段階の厳格な検証プロセスを導入し、Lean4形式言語を統合することで、AIが論理推論で「無意味なことを言うこと」を根本的に防ぎました。

トレーニングアルゴリズムの進化: MoEモデルにおける長期的なタスクトレーニングの不安定さという問題に対し、メイクドンは独自開発したHisPOアルゴリズムを導入し、定理の一貫性検出メカニズムと併せて、強化学習の段階で「短期的な利益を得る」ような報酬ハッキング行為を効果的に防止しました。

効率的なアーキテクチャ: 5600億の総パラメータ量により、モデルの深い知識の蓄積が保証され、MoEアーキテクチャにより、推論時の柔軟性と効率性が確保されています。

現在、メイクドンはこのモデルおよびコードをGitHubとHugging Faceプラットフォームで全面的にオープンソース化しています。

LongCat-Flash-Prover