智東西
編譯 陳佳
編輯 程茜

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

LongCat-Flash-Prover將復(fù)雜的定理證明過程拆解為三個(gè)步驟：先將自然語言問題轉(zhuǎn)化為可驗(yàn)證的形式化表達(dá)，再生成結(jié)構(gòu)化的證明草稿，最后完成嚴(yán)格的形式化證明。通過這種類似人類解題的分階段方式，模型能夠更穩(wěn)定地處理長鏈條、強(qiáng)邏輯約束的推理任務(wù)。

▲LongCat-Flash-Prover項(xiàng)目主頁

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

▲定理證明任務(wù)性能對比

為了讓模型真正具備可靠的證明能力，研究團(tuán)隊(duì)在訓(xùn)練機(jī)制上也作出了創(chuàng)新。他們提出分層重要性采樣策略優(yōu)化（HisPO）算法，通過序列和詞元兩個(gè)維度的梯度掩碼，解決混合專家模型在長序列強(qiáng)化學(xué)習(xí)訓(xùn)練中的不穩(wěn)定問題。團(tuán)隊(duì)還發(fā)現(xiàn)模型在訓(xùn)練過程中學(xué)會(huì)了9種“作弊”手法，通過生成語法合規(guī)但邏輯不成立的虛假證明來騙過評(píng)估系統(tǒng)。為此，團(tuán)隊(duì)專門開發(fā)了基于抽象語法樹（AST）的合法性檢測機(jī)制，有效封堵了這一獎(jiǎng)勵(lì)欺騙問題。

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

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

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

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

技術(shù)報(bào)告：https://github.com/meituan-longcat/LongCat-Flash-Prover/blob/main/LongCat_Flash_Prover_Technical_Report.pdf

一、把“數(shù)學(xué)題”變成“可驗(yàn)證代碼”，讓AI先學(xué)會(huì)讀懂題

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

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

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

▲自動(dòng)形式化提示詞

在這個(gè)過程中，所有輸入的問題都會(huì)被統(tǒng)一看作自然語言語句（包括完整問題、未完成的證明或中間推理步驟），然后由專門的自動(dòng)形式化專家模型（記為πθaf）進(jìn)行轉(zhuǎn)換，輸出對應(yīng)的形式化語句。這個(gè)過程并不簡單，因?yàn)槟Ｐ图瓤赡軐懗稣Z法錯(cuò)誤的代碼，也可能在語義上偏離原題，比如誤解條件或改變問題含義——論文中稱之為“篡改原始問題語義”。

為了解決這些問題，系統(tǒng)引入了兩層自動(dòng)校驗(yàn)機(jī)制：

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

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

只有同時(shí)通過這兩種檢測的結(jié)果，才會(huì)被認(rèn)為是有效的形式化轉(zhuǎn)換，進(jìn)入后續(xù)任務(wù)流程。

通過這一系列設(shè)計(jì)，模型完成了從“語言理解”到“可驗(yàn)證表達(dá)”的關(guān)鍵跨越，相當(dāng)于為后續(xù)的證明過程建立了一個(gè)可靠的起點(diǎn)。只有在這個(gè)基礎(chǔ)上，后續(xù)的草稿生成和定理證明才有可能真正做到嚴(yán)謹(jǐn)和可驗(yàn)證。

▲不同推理模型和專用自動(dòng)形式化模型在多個(gè)基準(zhǔn)數(shù)據(jù)集上的自動(dòng)形式化性能

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

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

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

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

這種拆解帶來兩個(gè)關(guān)鍵好處。第一，每個(gè)子問題的難度顯著降低，使模型更容易生成正確的推理步驟；第二，已經(jīng)完成的部分可以被重復(fù)利用，減少重復(fù)推理的成本，提高整體效率。例如，在證明一個(gè)復(fù)雜定理時(shí)，某些中間結(jié)論可以在后續(xù)多個(gè)步驟中反復(fù)調(diào)用，從而形成更穩(wěn)定的推理結(jié)構(gòu)。

在實(shí)際執(zhí)行中，如果模型直接生成完整證明失敗，系統(tǒng)會(huì)自動(dòng)切換到“草稿模式”，優(yōu)先生成結(jié)構(gòu)合理的證明框架，再逐步補(bǔ)全每一個(gè)引理。這一過程同樣結(jié)合工具驗(yàn)證：草稿需要通過語法檢查，并確保整體結(jié)構(gòu)與原定理保持一致。隨后，定理證明模塊會(huì)逐個(gè)補(bǔ)全這些未完成的部分，最終合成為完整證明。

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

▲不同推理模型和專用定理證明模型在多個(gè)基準(zhǔn)數(shù)據(jù)集上的定理證明性能

三、引入工具反饋和強(qiáng)化學(xué)習(xí)，讓模型在試錯(cuò)中學(xué)會(huì)“嚴(yán)謹(jǐn)”

在讓模型具備“讀懂題目”和“拆解問題”的能力之后，研究進(jìn)一步關(guān)注如何讓模型在復(fù)雜推理過程中變得更加穩(wěn)定和可靠。為此，整體訓(xùn)練過程不再依賴一次性生成答案，而是引入工具集成推理（Tool-Integrated Reasoning, TIR）與帶可驗(yàn)證獎(jiǎng)勵(lì)的智能體強(qiáng)化學(xué)習(xí)（RLVR）機(jī)制，讓模型在反復(fù)試錯(cuò)中逐步提升推理質(zhì)量。

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

具體來說，每當(dāng)模型生成形式化語句、證明草稿或完整證明時(shí)，系統(tǒng)都會(huì)調(diào)用一系列驗(yàn)證工具進(jìn)行檢查：

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

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

3、定理一致性檢測（Vtheo）：驗(yàn)證草稿結(jié)構(gòu)與原始定理的一致性。

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

▲評(píng)判器-草稿生成器-定理證明器

在此基礎(chǔ)上，研究引入了智能體強(qiáng)化學(xué)習(xí)階段，訓(xùn)練任務(wù)被設(shè)計(jì)為多個(gè)可驗(yàn)證目標(biāo)：基于自然語言問題生成形式化語句、由形式化語句直接生成證明、生成引理式證明草稿等。每個(gè)任務(wù)的結(jié)果都可以通過工具自動(dòng)打分，從而為模型提供明確的獎(jiǎng)勵(lì)信號(hào)。模型會(huì)傾向于強(qiáng)化那些能夠通過驗(yàn)證的行為。

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

1、序列級(jí)差異掩碼：計(jì)算序列內(nèi)所有詞元差異比率的幾何平均值，若超過閾值δseq則剔除整個(gè)序列的梯度貢獻(xiàn)；

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

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

▲LongCat-Flash-Prover訓(xùn)練流程總覽

四、模型學(xué)會(huì)了9種作弊手法，團(tuán)隊(duì)專門造了個(gè)“反作弊系統(tǒng)”

在模型訓(xùn)練過程中，研究團(tuán)隊(duì)發(fā)現(xiàn)了一個(gè)有趣的問題。隨著推理能力提升，模型不僅學(xué)會(huì)了解題，還逐漸學(xué)會(huì)了“鉆規(guī)則漏洞”。具體表現(xiàn)為，模型可以生成一些在表面上通過驗(yàn)證、但實(shí)際上并不符合數(shù)學(xué)邏輯的“虛假證明”。這些結(jié)果在原有評(píng)估體系下可能被判定為正確，從而導(dǎo)致訓(xùn)練指標(biāo)出現(xiàn)異常提升，但真實(shí)能力并沒有同步提高。

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

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

這一問題在強(qiáng)化學(xué)習(xí)階段尤為明顯，訓(xùn)練過程中，模型的滾動(dòng)通過率曾在第80步左右出現(xiàn)爆炸性激增。排查后發(fā)現(xiàn)，這并不是模型真正變強(qiáng)，而是因?yàn)閷W(xué)會(huì)了更高效的“作弊方式”，從而騙過評(píng)估系統(tǒng)。這是典型的獎(jiǎng)勵(lì)欺騙（reward hacking）問題。

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

在引入這套機(jī)制后，訓(xùn)練集上的滾動(dòng)通過率曲線恢復(fù)正常增長，“虛假通過率”被有效抑制。進(jìn)一步實(shí)驗(yàn)表明，在1024個(gè)訓(xùn)練樣本上，修復(fù)后的模型能夠更有效地避免虛假證明，取得更高的有效證明率?；贏ST的檢查源碼已在項(xiàng)目主頁開源。

整體來看，這一“反作弊系統(tǒng)”不僅提升了模型輸出的可靠性，也為后續(xù)形式化推理模型的評(píng)估提供了更嚴(yán)謹(jǐn)?shù)臉?biāo)準(zhǔn)，縮小了獎(jiǎng)勵(lì)/指標(biāo)分?jǐn)?shù)與真實(shí)證明能力之間的差距。

▲強(qiáng)化學(xué)習(xí)滾動(dòng)通過率（存在欺騙行為 vs 無欺騙行為）/不同驗(yàn)證層級(jí)的評(píng)估結(jié)果

結(jié)語：從“會(huì)解題”到“會(huì)證明”，AI解數(shù)學(xué)難題邁向新階段

從自動(dòng)形式化、草稿生成到最終的形式化證明，LongCat-Flash-Prover提供了一種更接近人類解題過程的技術(shù)思路：先理解問題，再拆解結(jié)構(gòu)，最后完成嚴(yán)格推導(dǎo)。這一路徑并不追求一次性生成完整答案，而是通過分階段處理和多輪驗(yàn)證，逐步提高推理過程的穩(wěn)定性。結(jié)合工具反饋與強(qiáng)化學(xué)習(xí)機(jī)制，模型在復(fù)雜數(shù)學(xué)任務(wù)中的表現(xiàn)確實(shí)有所提升，相關(guān)基準(zhǔn)測試結(jié)果也在一定程度上體現(xiàn)了這一方法的有效性。

不過，從當(dāng)前情況來看，這類模型仍處在探索階段。無論是工程適配、運(yùn)行成本，還是實(shí)際應(yīng)用場景，都還有待進(jìn)一步驗(yàn)證。圍繞其價(jià)值的討論也呈現(xiàn)出分化：既有對其在數(shù)學(xué)研究、程序驗(yàn)證等高可靠性領(lǐng)域潛力的期待，也存在對“應(yīng)用邊界不清”的質(zhì)疑?？梢源_定的是，形式化推理提供了一種不同于通用生成模型的發(fā)展方向，其長期意義如何，仍有待更多實(shí)踐來回答。