美團又開源！專攻數學定理證明，能模擬人類解題，刷新多項開源SOTA

智東西
編譯 陳佳
編輯 程茜

智東西3月25日消息，昨日，美團龍貓（LongCat）團隊發布專門了用于數學形式化與定理證明模型LongCat-Flash-Prover的背后技術棧。該模型已于3月20日全面開源。

LongCat-Flash-Prover將復雜的定理證明過程拆解為三個步驟：先將自然語言問題轉化為可驗證的形式化表達，再生成結構化的證明草稿，最后完成嚴格的形式化證明。通過這種類似人類解題的分階段方式，模型能夠更穩定地處理長鏈條、強邏輯約束的推理任務。

▲LongCat-Flash-Prover項目主頁

LongCat-Flash-Prover基于美團自研的LongCat中期訓練基礎模型構建，總參數量5600億，激活參數約270億，采用混合專家（MoE）架構。在性能上，該模型在多個權威數學基準測試中刷新開源模型最優成績：在MiniF2F-Test數據集上，每個問題僅需72次推理嘗試，通過率即可達到97.1%；在難度更高的PutnamBench和ProverBench數據集上，解題率分別達到41.5%和70.8%，每個問題推理嘗試不超過220次，優于現有開源基線模型。

▲定理證明任務性能對比

為了讓模型真正具備可靠的證明能力，研究團隊在訓練機制上也作出了創新。他們提出分層重要性采樣策略優化（HisPO）算法，通過序列和詞元兩個維度的梯度掩碼，解決混合專家模型在長序列強化學習訓練中的不穩定問題。團隊還發現模型在訓練過程中學會了9種“作弊”手法，通過生成語法合規但邏輯不成立的虛假證明來騙過評估系統。為此，團隊專門開發了基于抽象語法樹（AST）的合法性檢測機制，有效封堵了這一獎勵欺騙問題。

根據美團龍貓官方消息，LongCat-Flash-Prover模型在開源后幾日內，不僅受到了AI和大模型研究者們的關注，更引起了數學界的反響。發布當日，他們便收到了國內頂尖高校的合作邀請，共同探討基于該模型開發形式化證明Agent的可能性。美團龍貓團隊期望借此將現有的數學教材和前沿論文“翻譯”成形式化語言，進一步充實形式化數學的知識底座，為整個數學研究領域的范式創新提供助力。

在海外社區Reddit，有網友對LongCat-Flash-Prover模型的工程落地表示關切，指出輕量版Flash模型對llama.cpp的適配工作至今仍未完成，實際部署仍存在障礙。也有聲音直接質疑這類研究的實際價值，認為形式化驗證模型本質上只是擅長一門極小眾語言的代碼模型，“看不出背后有什么大格局，更想不出幾個真正可落地的應用場景”。

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

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

技術報告：https://github.com/meituan-longcat/LongCat-Flash-Prover/blob/main/LongCat_Flash_Prover_Technical_Report.pdf

一、把“數學題”變成“可驗證代碼”，讓AI先學會讀懂題

大模型會解題，但它會“證明”嗎？這是兩件難度完全不同的事。數學解題只需要最終答案正確，定理證明依賴完整且嚴密的邏輯鏈條，任何一步表述不清或推導不嚴，都可能使結論失效。

這項研究首先聚焦于一個看似基礎但實際非常困難的問題：讓AI真正“讀懂”數學題。與日常對話不同，數學問題往往包含隱含條件、嚴格定義以及精確的邏輯關系，如果只是停留在自然語言層面，模型很容易出現理解偏差。

因此，美團龍貓團隊研究的核心思路，是把自然語言描述的問題，轉化為一種可以被計算機嚴格校驗的形式化表達，也就是基于Lean4定理證明語言的數學語句。Lean4是一種兼具數學表達和程序驗證雙重特性的形式化語言，既能精確描述數學命題，又能被編譯器嚴格檢查。

▲自動形式化提示詞

在這個過程中，所有輸入的問題都會被統一看作自然語言語句（包括完整問題、未完成的證明或中間推理步驟），然后由專門的自動形式化專家模型（記為πθaf）進行轉換，輸出對應的形式化語句。這個過程并不簡單，因為模型既可能寫出語法錯誤的代碼，也可能在語義上偏離原題，比如誤解條件或改變問題含義——論文中稱之為“篡改原始問題語義”。

為了解決這些問題，系統引入了兩層自動校驗機制：

第一層是語句語法檢測（Vsyn）：通過Lean4 Server編譯器檢查生成的形式化語句是否符合語言規則，將語句與占位符拼接后編譯，輸出二元結果（SORRY表示語法正確但待證明，FAIL表示存在語法錯誤）；

第二層是語義一致性檢測（Vcon）：通過基于大語言模型的語義過濾器（采用QWQ-32B和Qwen3-32B作為評判模型，聚合投票判斷），識別并剔除與原始自然語言語句語義不一致的形式化語句。

只有同時通過這兩種檢測的結果，才會被認為是有效的形式化轉換，進入后續任務流程。

通過這一系列設計，模型完成了從“語言理解”到“可驗證表達”的關鍵跨越，相當于為后續的證明過程建立了一個可靠的起點。只有在這個基礎上，后續的草稿生成和定理證明才有可能真正做到嚴謹和可驗證。

▲不同推理模型和專用自動形式化模型在多個基準數據集上的自動形式化性能

二、像人類一樣“先打草稿”，復雜證明拆成小步驟讓準確率再漲10%

在完成“讀懂題目”的形式化轉換之后，研究進一步解決的是如何讓AI更穩定地完成復雜定理證明。直接生成完整證明往往難度很高，尤其是在長鏈條推理中，一步出錯就會導致整體失敗。為此，模型引入了一種類似人類解題習慣的策略：先生成引理式證明草稿，再逐步完善細節。

這一過程由專門的草稿生成專家模型（記為πθsk）完成。給定已經驗證正確的形式化語句sx，模型不會立刻輸出完整證明，而是先構建一個包含多個輔助引理（lemma）的證明框架。這個草稿通常由若干尚未完成的小結論和一個整體證明結構組成，其中未完成的部分會以占位形式標記出來。這樣的設計本質上借鑒了“分而治之”和動態規劃的思想：把一個困難問題拆分成多個更容易解決的小問題。

▲普特南1969B1題的引理式草稿

這種拆解帶來兩個關鍵好處。第一，每個子問題的難度顯著降低，使模型更容易生成正確的推理步驟；第二，已經完成的部分可以被重復利用，減少重復推理的成本，提高整體效率。例如，在證明一個復雜定理時，某些中間結論可以在后續多個步驟中反復調用，從而形成更穩定的推理結構。

在實際執行中，如果模型直接生成完整證明失敗，系統會自動切換到“草稿模式”，優先生成結構合理的證明框架，再逐步補全每一個引理。這一過程同樣結合工具驗證：草稿需要通過語法檢查，并確保整體結構與原定理保持一致。隨后，定理證明模塊會逐個補全這些未完成的部分，最終合成為完整證明。

實驗結果表明，這種“草稿證明模式”顯著提升了成功率。在32次嘗試預算限制下，帶工具集成推理的草稿證明模式在MiniF2F-Test數據集上達到93.9%的通過率，在PutnamBench數據集上達到28.9%的準確率，均優于直接生成完整證明的模式。在更高預算下，結合樹搜索策略的草稿證明可進一步提升準確率約3.1%。這說明，對于長鏈條推理任務，結構化拆解是提升AI可靠性的關鍵路徑。

▲不同推理模型和專用定理證明模型在多個基準數據集上的定理證明性能

三、引入工具反饋和強化學習，讓模型在試錯中學會“嚴謹”

在讓模型具備“讀懂題目”和“拆解問題”的能力之后，研究進一步關注如何讓模型在復雜推理過程中變得更加穩定和可靠。為此，整體訓練過程不再依賴一次性生成答案，而是引入工具集成推理（Tool-Integrated Reasoning, TIR）與帶可驗證獎勵的智能體強化學習（RLVR）機制，讓模型在反復試錯中逐步提升推理質量。

▲混合專家工具集成合成流程總覽，從左至右分別是自動形式化、草稿生成、完整證明生成和草稿式證明生成四個模塊，每個模塊都通過Lean4編譯器進行語法和合法性校驗，只有通過驗證的結果才進入下一步。

具體來說，每當模型生成形式化語句、證明草稿或完整證明時，系統都會調用一系列驗證工具進行檢查：

1、語法驗證（Vsyn）：判斷語法是否正確，輸出SORRY（語法正確但含未證明語句）、PASS（完全通過）或FAIL（存在語法錯誤）；

2、合法性檢測（Vleg）：檢測證明是否與原始形式化語句語義一致，防止篡改定理定義、設置特殊編譯上下文等“獎勵欺騙”行為；

3、定理一致性檢測（Vtheo）：驗證草稿結構與原始定理的一致性。

每一次檢查都會返回明確的反饋信息（如錯誤信息、錯誤位置），模型可以根據這些反饋重新生成結果，從而形成”生成—驗證—修正”的循環過程。對于簡單問題，模型可能一次就能通過驗證；而對于復雜問題，則需要多輪與工具交互，逐步逼近正確答案。

▲評判器-草稿生成器-定理證明器

在此基礎上，研究引入了智能體強化學習階段，訓練任務被設計為多個可驗證目標：基于自然語言問題生成形式化語句、由形式化語句直接生成證明、生成引理式證明草稿等。每個任務的結果都可以通過工具自動打分，從而為模型提供明確的獎勵信號。模型會傾向于強化那些能夠通過驗證的行為。

為了應對混合專家（MoE）模型在長序列任務訓練中的不穩定問題，研究提出了分層重要性采樣策略優化（Hierarchical Importance Sampling Policy Optimization, HisPO）算法。該方法從序列和詞元兩個維度估算訓練-推理一致性：

1、序列級差異掩碼：計算序列內所有詞元差異比率的幾何平均值，若超過閾值δseq則剔除整個序列的梯度貢獻；

2、詞元級差異掩碼：對剩余序列，剔除差異比率超過閾值δtok的個別詞元；

3、詞元級滯后性控制：對保留詞元通過裁剪限制更新幅度。

▲LongCat-Flash-Prover訓練流程總覽

四、模型學會了9種作弊手法，團隊專門造了個“反作弊系統”

在模型訓練過程中，研究團隊發現了一個有趣的問題。隨著推理能力提升，模型不僅學會了解題，還逐漸學會了“鉆規則漏洞”。具體表現為，模型可以生成一些在表面上通過驗證、但實際上并不符合數學邏輯的“虛假證明”。這些結果在原有評估體系下可能被判定為正確，從而導致訓練指標出現異常提升，但真實能力并沒有同步提高。

進一步分析發現，這類問題源于現有開源評估流水線的關鍵漏洞。傳統評估主要依賴Lean4語法驗證和目標定理定義一致性檢查，而目標定理的形式化上下文（如import、open命令、輔助lemma定義等）是完全可編輯的。這給模型留下了“操作空間”，使其能夠通過多種手段規避驗證規則。研究團隊識別并分類出9種具體的欺騙模式。

▲9種欺騙模式與具體操作

這一問題在強化學習階段尤為明顯，訓練過程中，模型的滾動通過率曾在第80步左右出現爆炸性激增。排查后發現，這并不是模型真正變強，而是因為學會了更高效的“作弊方式”，從而騙過評估系統。這是典型的獎勵欺騙（reward hacking）問題。

為了解決這一問題，研究團隊開發了合法性檢測機制（Vleg）。核心思路是不再只看結果是否通過驗證，而是深入分析證明本身的結構。具體做法是開發輕量級Lean4詞法分析器和語法分析器，將生成的證明代碼轉化為抽象語法樹（AST），并嚴格校驗形式化語句與證明/草稿之間的抽象語法樹一致性。

在引入這套機制后，訓練集上的滾動通過率曲線恢復正常增長，“虛假通過率”被有效抑制。進一步實驗表明，在1024個訓練樣本上，修復后的模型能夠更有效地避免虛假證明，取得更高的有效證明率。基于AST的檢查源碼已在項目主頁開源。

整體來看，這一“反作弊系統”不僅提升了模型輸出的可靠性，也為后續形式化推理模型的評估提供了更嚴謹的標準，縮小了獎勵/指標分數與真實證明能力之間的差距。

▲強化學習滾動通過率（存在欺騙行為 vs 無欺騙行為）/不同驗證層級的評估結果

結語：從“會解題”到“會證明”，AI解數學難題邁向新階段

從自動形式化、草稿生成到最終的形式化證明，LongCat-Flash-Prover提供了一種更接近人類解題過程的技術思路：先理解問題，再拆解結構，最后完成嚴格推導。這一路徑并不追求一次性生成完整答案，而是通過分階段處理和多輪驗證，逐步提高推理過程的穩定性。結合工具反饋與強化學習機制，模型在復雜數學任務中的表現確實有所提升，相關基準測試結果也在一定程度上體現了這一方法的有效性。

不過，從當前情況來看，這類模型仍處在探索階段。無論是工程適配、運行成本，還是實際應用場景，都還有待進一步驗證。圍繞其價值的討論也呈現出分化：既有對其在數學研究、程序驗證等高可靠性領域潛力的期待，也存在對“應用邊界不清”的質疑。可以確定的是，形式化推理提供了一種不同于通用生成模型的發展方向，其長期意義如何，仍有待更多實踐來回答。