2026年3月24日，美團龍貓（LongCat）團隊正式開源專門用於數學形式化與定理證明的深度學習模型——LongCat-Flash-Prover。該模型針對大語言模型在嚴密邏輯推演中的短板，通過將形式化推理拆解爲自動形式化（Auto-Formalization）、草稿生成(Sketching)與證明生成(Proving)三大原子能力，實現了從“概率預測答案”向“嚴謹邏輯證明”的範式轉變。

QQ20260324-102744.jpg

在結合工具集成推理（TIR）策略下，該模型在 MiniF2F-Test 基準測試中僅需72次推理預算即可達到97.1% 的通過率，刷新了開源 Prover 模型的 SOTA 紀錄。此外，在 MathOlympiad-Bench 與 PutnamBench 等高難度競賽級任務中，其表現亦全面超越現有開源模型。

QQ20260324-102750.jpg

技術層面，LongCat-Flash-Prover 採用了基於 TIR 的“混合專家迭代”框架。通過集成 Lean4Server 校驗、語義及定理一致性檢測以及針對9種作弊行爲的合法性驗證，模型有效解決了邏輯漏洞與代碼欺騙問題。在訓練階段，團隊引入分層 Masking 策略與 Token 層面 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