2026年3月24日、メイドゥンロンカット（LongCat）チームは、数学の形式化と定理証明に特化した深層学習モデル「LongCat-Flash-Prover」を正式にオープンソース化しました。このモデルは、大規模言語モデルが厳密な論理的推論において持つ欠点に対処するため、形式的な推論を自動形式化（Auto-Formalization）、下書き生成（Sketching）、証明生成（Proving）の3つの基本的な能力に分解し、確率的な答えの予測から厳密な論理的証明へのパラダイムの変化を実現しています。

QQ20260324-102744.jpg

ツール統合推論（TIR）戦略を組み合わせた場合、このモデルはMiniF2F-Testベンチマークテストでわずか72回の推論予算で97.1％の通過率を達成し、オープンソースProverモデルにおけるSOTA記録を更新しました。さらに、MathOlympiad-BenchやPutnamBenchなどの高難度コンペティションレベルのタスクにおいても、既存のオープンソースモデルをすべて上回る性能を示しています。

QQ20260324-102750.jpg

技術的には、LongCat-Flash-ProverはTIRに基づく「混合エキスパートイテレーション」フレームワークを採用しています。Lean4Serverの検証、意味と定理の一貫性検出、および9種類の不正行為に対する合法性検証を統合することで、論理的な穴やコードの詐欺問題を効果的に解決しました。トレーニング段階では、階層的なマスキング戦略とトークンレベルでのStaleness制御を導入し、MoEアーキテクチャでの強化学習の安定性を大幅に向上させました。

AIの推論能力が自然言語の曖昧な処理からコンピュータで検証可能な形式言語へと移行する中、このようなProverモデルは、アルゴリズムスコアの枠を超えて、基礎科学の「インフラストラクチャー」として進化しています。この革新は、AIが先端数学の探求と文献の自動検証に深く関与する時代が急速に訪れていることを示しています。

  • GitHub:

    https://github.com/meituan-longcat/LongCat-Flash-Prover

  • Hugging Face: https://huggingface.co/meituan-longcat/LongCat-Flash-Prover

  • Report:

    https://github.com/meituan-longcat/LongCat-Flash-Prover/blob/main/LongCat_Flash_Prover_Technical_Report.pdf