先說(shuō)明白這篇文章聊的不是“AI能不能替代數(shù)學(xué)家”而是更具體的“AI尤其是大語(yǔ)言模型LLM在重大數(shù)學(xué)發(fā)展里到底有哪些已經(jīng)成熟、正在嘗試或者至少值得一試的應(yīng)用示例”。所謂重大數(shù)學(xué)發(fā)展可以粗略理解成一個(gè)新猜想被提出一個(gè)懸置多年的老猜想出現(xiàn)關(guān)鍵證明或者某個(gè)大型研究計(jì)劃進(jìn)入了新階段。這類(lèi)工作通常有幾個(gè)共同特征文獻(xiàn)量大、推理鏈長(zhǎng)、符號(hào)體系復(fù)雜、需要反復(fù)驗(yàn)證。LLM進(jìn)入這個(gè)場(chǎng)景的價(jià)值不是直接給你一個(gè)已完成、可發(fā)表的證明而是把原本需要幾周甚至幾個(gè)月才能做完的整理、枚舉、轉(zhuǎn)譯和初步驗(yàn)證工作壓縮到幾天。適合閱讀這篇文章的主要是三類(lèi)人一是做數(shù)學(xué)或數(shù)學(xué)物理研究的人想了解AI工具現(xiàn)在能頂?shù)侥囊徊蕉亲鲂问交?yàn)證、定理證明輔助工具的工程師想知道LLM怎么接入Lean、Isabelle這類(lèi)流程三是對(duì)AI for Math感興趣的開(kāi)發(fā)者。我的基本判斷是現(xiàn)在的LLM還遠(yuǎn)遠(yuǎn)沒(méi)有到“自動(dòng)解決重大數(shù)學(xué)難題”的階段但它足夠做一套“先產(chǎn)生候選結(jié)果再由人來(lái)驗(yàn)證”的科研協(xié)作流水線。下面我會(huì)按實(shí)際落地順序講清楚能做什么、不能做什么、用什么判斷標(biāo)準(zhǔn)以及踩了哪些坑。1. 先想清楚LLM在數(shù)學(xué)發(fā)展里做的是“參考系”而不是“答案機(jī)”1.1 數(shù)學(xué)任務(wù)和通用文本任務(wù)的區(qū)別很多人第一次用LLM做數(shù)學(xué)題第一反應(yīng)是“它能解微積分、能寫(xiě)證明那是不是也能推動(dòng)數(shù)學(xué)研究”這種判斷容易踩坑。普通問(wèn)答里的數(shù)學(xué)題大多有明確答案、固定解法、短邏輯鏈模型只要見(jiàn)過(guò)類(lèi)似例題就能模仿出一篇看起來(lái)合理的解答。但重大數(shù)學(xué)發(fā)展里的問(wèn)題通常不是“計(jì)算一道題”而是“在一堆已知結(jié)論和未驗(yàn)證假設(shè)之間搭建新的邏輯路徑”。后者對(duì)邏輯自洽性、符號(hào)一致性、引用可靠性的要求極高而這些恰恰是概率生成模型的天然弱點(diǎn)。更準(zhǔn)確地說(shuō)LLM給的是“有可能成立的參考系”不是“已經(jīng)證明的真理”。它可以幫你快速找到可能的思路、可能遺漏的引理、可能存在反例的方向但它給出的每一步都需要重新驗(yàn)證。把模型輸出直接當(dāng)證明用是這類(lèi)工作流里最大的失敗原因。所以我的建議是一開(kāi)始就要給LLM設(shè)定正確的角色。它不是“證明機(jī)”而是“科研助手里的第一階段篩選器”。你在前面做問(wèn)題拆解它負(fù)責(zé)生成候選假設(shè)、整理文獻(xiàn)線索、翻譯證明草稿最后由你或者形式化工具負(fù)責(zé)驗(yàn)證。這樣既能發(fā)揮它的廣度和速度又不至于被它的“流暢表達(dá)”帶偏。1.2 先用一個(gè)經(jīng)典小定理建立判斷直覺(jué)我一般會(huì)建議用幾道經(jīng)典小定理來(lái)測(cè)試當(dāng)前模型到底適合哪類(lèi)任務(wù)。比如“證明根號(hào)2是無(wú)理數(shù)”“證明素?cái)?shù)有無(wú)窮多個(gè)”這類(lèi)基礎(chǔ)但完整的證明。別覺(jué)得這些題目太簡(jiǎn)單它們的價(jià)值在于證明結(jié)構(gòu)完整、邏輯鏈清晰、錯(cuò)誤容易發(fā)現(xiàn)你能快速判斷模型是在“真正推理”還是在“回憶相似文本”。實(shí)測(cè)時(shí)你很快會(huì)發(fā)現(xiàn)幾種典型現(xiàn)象模型能寫(xiě)出歐幾里得素?cái)?shù)無(wú)限證明的大體框架但在“為什么若p1...pn的乘積加1的質(zhì)因子不在列表中”這一步偶爾會(huì)出現(xiàn)含糊表述。有些模型會(huì)把“反證法”和“構(gòu)造法”混在一起讀起來(lái)像證明但實(shí)際存在循環(huán)論證。有些模型會(huì)引用一個(gè)“顯然成立”的引理但這個(gè)引理本身就是目標(biāo)命題。這些現(xiàn)象不是模型太笨而是它的訓(xùn)練目標(biāo)決定了它更擅長(zhǎng)“生成概率上合理的詞序列”而不是“維護(hù)一個(gè)貫穿全文的邏輯狀態(tài)”。所以當(dāng)你拿到一段證明第一件事不是看它寫(xiě)得順不順而是把它拆成步驟逐條對(duì)照定義和前提看有沒(méi)有跳步。用經(jīng)典小定理建立基線之后再拿它測(cè)試你研究領(lǐng)域里的中等難度問(wèn)題。這樣能形成一張“模型能力地圖”哪些任務(wù)它能穩(wěn)定輸出半成品哪些任務(wù)它基本在胡說(shuō)。有了這張地圖后續(xù)在大問(wèn)題上才不會(huì)被一次漂亮輸出誤導(dǎo)。1.3 重大數(shù)學(xué)發(fā)展中LLM真正能插入的環(huán)節(jié)如果只是一句“LLM能做數(shù)學(xué)”太泛了。放到重大數(shù)學(xué)發(fā)展這個(gè)具體場(chǎng)景里我覺(jué)得有三個(gè)環(huán)節(jié)最值得關(guān)注文獻(xiàn)線索整理大型研究計(jì)劃往往有幾百篇相關(guān)論文LLM可以快速提取某條思路的相似定義、證明技巧、后續(xù)發(fā)展并生成一份帶公式的筆記。候選命題與反例搜索從已知定理做類(lèi)比擴(kuò)展生成“如果滿足這些條件會(huì)不會(huì)有類(lèi)似結(jié)論”的候選命題同時(shí)提出可能讓結(jié)論失效的邊界例子。證明草稿補(bǔ)全研究人員有整體思路但中間缺少某個(gè)引理LLM可以補(bǔ)一個(gè)版本再由人判斷或交給形式化工具檢查。這三個(gè)環(huán)節(jié)的共同點(diǎn)模型只負(fù)責(zé)“產(chǎn)出可能性”真正做最終裁決的是人、數(shù)值實(shí)驗(yàn)或定理證明器。我不知道未來(lái)LLM會(huì)不會(huì)直接證明黎曼猜想但我知道至少在當(dāng)下把它當(dāng)“會(huì)讀很多論文、檢索速度快、但容易一本正經(jīng)胡說(shuō)”的實(shí)習(xí)生來(lái)用更合適。2. 一個(gè)可復(fù)現(xiàn)的最小案例讓LLM幫忙整理證明思路2.1 準(zhǔn)備環(huán)境和輸入構(gòu)造先不要一步到位部署大模型。做這類(lèi)實(shí)驗(yàn)入門(mén)階段用API或者在線Demo就夠了重點(diǎn)是“怎么把數(shù)學(xué)問(wèn)題寫(xiě)成模型能吃透的提示詞”。我在實(shí)際測(cè)試時(shí)發(fā)現(xiàn)很多人不是模型選錯(cuò)而是問(wèn)題描述太含糊。數(shù)學(xué)證明任務(wù)必須把三樣?xùn)|西寫(xiě)清楚目標(biāo)命題用標(biāo)準(zhǔn)數(shù)學(xué)符號(hào)寫(xiě)清楚要證明什么?？捎霉ぞ咴试S使用哪些已證明的定理、定義、公理。輸出格式要求模型給出定義、證明思路、關(guān)鍵步驟、待驗(yàn)證風(fēng)險(xiǎn)點(diǎn)而不是一段“散文式證明”。下面是我常用的一種提示詞框架你可以根據(jù)自己的任務(wù)調(diào)整【任務(wù)】 請(qǐng)幫我拆解下面這個(gè)命題的證明思路。 【目標(biāo)命題】 對(duì)任意滿足條件 H 的對(duì)象 X證明性質(zhì) P(X) 成立。 【已知工具】 1. 已有定理 A說(shuō)明 ... 2. 基本不等式或性質(zhì) B說(shuō)明 ... 3. 可以使用反證法、歸納法、構(gòu)造法等標(biāo)準(zhǔn)證明方法。 【輸出要求】 1. 先列出題目中需要明確的所有符號(hào)、定義和假設(shè)。 2. 給出證明的主思路不要一步一步寫(xiě)滿但要讓讀者知道整體走向。 3. 對(duì)每個(gè)關(guān)鍵步驟標(biāo)注“優(yōu)先級(jí)必須驗(yàn)證”。 4. 額外指出這個(gè)思路可能失敗的地方或者可能存在的反例。 【注意】 如果某個(gè)步驟引用了未說(shuō)明的引理請(qǐng)單獨(dú)列出并說(shuō)明為什么需要它。這個(gè)模板的核心作用不是讓模型直接輸出“完美證明”而是讓它在可控范圍內(nèi)給出結(jié)構(gòu)化的半成品。我在實(shí)際使用時(shí)會(huì)發(fā)現(xiàn)一旦要求模型“標(biāo)出必須驗(yàn)證的步驟”它的生成質(zhì)量會(huì)明顯好很多因?yàn)樘崾驹~迫使它把隱含假設(shè)暴露出來(lái)。2.2 判斷一個(gè)輸出是否值得繼續(xù)投入模型輸出了一段內(nèi)容接下來(lái)不是直接信也不是直接丟。要快速做一輪“可投入度”判斷我的標(biāo)準(zhǔn)很簡(jiǎn)單能不能把輸出翻譯成一系列可檢查的步驟。如果輸出只是一大段流暢的自然語(yǔ)言沒(méi)有任何定義、引理、條件分類(lèi)那基本不能用于研究場(chǎng)景。下面這張表可以幫你快速區(qū)分可用輸出和垃圾輸出維度可用輸出垃圾輸出符號(hào)定義對(duì)每個(gè)變量、集合、映射都有說(shuō)明使用未定義的符號(hào)或同一符號(hào)在不同位置含義不同邏輯關(guān)系步驟之間明顯是從前提到結(jié)論的推進(jìn)前面講A后面突然跳到結(jié)論C缺少B引理引用明確說(shuō)“引用定理X條件是...”并且條件確實(shí)滿足提到一個(gè)聽(tīng)起來(lái)很專(zhuān)業(yè)但不存在的定理名風(fēng)險(xiǎn)標(biāo)注會(huì)指出哪一步需要驗(yàn)證、哪里可能有反例每一步都像“顯然成立”可驗(yàn)證性能提取出具體條件放到數(shù)值實(shí)驗(yàn)或證明器里試都是空泛的邏輯連接詞沒(méi)有可執(zhí)行內(nèi)容在收到第一次輸出后我會(huì)先把“待驗(yàn)證風(fēng)險(xiǎn)點(diǎn)”提取出來(lái)作為下一步驗(yàn)證清單。比如模型說(shuō)“這里需要使用柯西-施瓦茨不等式但需要先確認(rèn)函數(shù)在區(qū)間上平方可積”那我接下來(lái)就去檢查這個(gè)平方可積條件是否滿足。如果不滿足這條路線可能要先修正而不是繼續(xù)往下走。2.3 從單條測(cè)試到批量評(píng)估一旦單條任務(wù)跑通了你會(huì)想同時(shí)測(cè)試多個(gè)問(wèn)題、多個(gè)模型或者多個(gè)提示詞版本。這里一定要控制節(jié)奏。我一開(kāi)始踩過(guò)一個(gè)坑寫(xiě)了一個(gè)循環(huán)一口氣提交了50個(gè)證明任務(wù)結(jié)果很快觸發(fā)了接口限流而且有一大半輸出因?yàn)檩斎敫袷藉e(cuò)誤被截?cái)嘧詈笾荒苤匦屡堋８€(wěn)妥的方式是分三步批次規(guī)模先壓到5到10條。跑通之后檢查每條輸出是否進(jìn)入預(yù)期目錄、是否占用太多資源、是否有異常報(bào)錯(cuò)。給每條任務(wù)設(shè)置唯一ID把模型名稱(chēng)、提示詞版本、輸入命題、輸出結(jié)果、人工評(píng)級(jí)都記錄到一張表里。這樣才能回溯是哪一輪改動(dòng)導(dǎo)致質(zhì)量下降。開(kāi)一個(gè)小型隊(duì)列不要一次性并發(fā)太多。如果使用API可以限制每秒或每分鐘的請(qǐng)求數(shù)如果本地部署則需要觀察顯存和GPU利用率避免多個(gè)任務(wù)相互爭(zhēng)搶。這樣做的好處是后續(xù)你可以對(duì)每次實(shí)驗(yàn)做清晰的對(duì)比。畢竟在數(shù)學(xué)研究里很多東西沒(méi)法用“感覺(jué)更好”來(lái)評(píng)判把結(jié)果結(jié)構(gòu)化之后才能用數(shù)據(jù)說(shuō)話。3. 在重大數(shù)學(xué)發(fā)展里更常見(jiàn)的三類(lèi)落地點(diǎn)3.1 猜想形成階段讓模型生成候選命題和特例重大數(shù)學(xué)發(fā)展很少是憑空冒出來(lái)的很多時(shí)候是先有大量數(shù)值實(shí)驗(yàn)和類(lèi)比再被凝練成猜想。LLM在這個(gè)階段能做兩件事一是生成“類(lèi)比命題”二是生成“可能讓命題失敗的特例”。舉個(gè)例子你已知某個(gè)定理在“有限生成群”條件下成立那你自然想問(wèn)在“可數(shù)生成群”或者“有限表示群”條件下結(jié)論還能不能成立這種問(wèn)題對(duì)數(shù)學(xué)家來(lái)說(shuō)需要翻閱很多文獻(xiàn)因?yàn)椤笆欠裼腥搜芯窟^(guò)”本身就是信息。LLM可以幫你在大量論文摘要、綜述、知識(shí)庫(kù)中做初步匹配并生成“從已知結(jié)果看條件變化后最可能失效的是哪一步”的判斷。同時(shí)它會(huì)根據(jù)已有定理的證明結(jié)構(gòu)列出可能破壞結(jié)論的邊界例子。比如“如果換成分裂域”“如果去掉緊致性條件”“如果不要求光滑只是連續(xù)”等等。這些候補(bǔ)特例不一定對(duì)但它們能幫助你快速縮小搜索空間。我自己的習(xí)慣是把模型生成的特例拿到數(shù)值計(jì)算軟件里快速驗(yàn)證能篩掉一大批明顯錯(cuò)誤剩下那些不容易驗(yàn)證的再人工攻。當(dāng)然這條路的局限也很明顯模型沒(méi)有真正的“數(shù)學(xué)直覺(jué)”它靠的是訓(xùn)練語(yǔ)料里的統(tǒng)計(jì)關(guān)聯(lián)。所以它能給出的類(lèi)比通常很直接不太可能產(chǎn)生那種需要跨領(lǐng)域抽象才能發(fā)現(xiàn)的深刻猜想。把它當(dāng)成“靈感收集器”比當(dāng)成“新時(shí)代拉馬努金”更實(shí)際。3.2 交互式定理證明用LLM輔助Lean等證明腳本這是目前我覺(jué)得最接近“工程可落地”的方向之一。Lean、Isabelle、Coq這些交互式定理證明器要求每一個(gè)證明步驟都能被機(jī)器檢查。以往寫(xiě)這類(lèi)形式化證明非常耗時(shí)尤其是從自然語(yǔ)言草稿翻譯成形式化策略。LLM擅長(zhǎng)的是“看到當(dāng)前證明狀態(tài)生成下一步要執(zhí)行的策略”這個(gè)模式非常適合接入證明器。流程大致是在Lean里把定理陳述寫(xiě)成標(biāo)準(zhǔn)形式例如一個(gè)目標(biāo)命題。把當(dāng)前“證明狀態(tài)”goal和已有的上下文喂給LLM。讓模型生成一系列策略或中間斷言。把模型輸出交給Lean執(zhí)行查看是否通過(guò)。這里有個(gè)關(guān)鍵認(rèn)知模型不需要一次寫(xiě)完整份證明它只需要生成“下一步”或者“下一步的一小段”然后通過(guò)證明器反饋來(lái)修正。這種交互模式利用了證明器的確定性彌補(bǔ)了模型的概率性。換句話說(shuō)模型負(fù)責(zé)“出招”證明器負(fù)責(zé)“驗(yàn)證”二者配合得好的時(shí)候會(huì)比我憑空讓模型寫(xiě)完整證明穩(wěn)定很多。但也要注意坑形式化證明的語(yǔ)法、庫(kù)函數(shù)命名、策略選擇都和具體版本強(qiáng)相關(guān)。同一個(gè)模型在Lean4和Lean3上的表現(xiàn)可能差異巨大。所以不要直接拿網(wǎng)上老的示例代碼跑先確認(rèn)你的Lean版本、Mathlib版本和運(yùn)行環(huán)境都正確。報(bào)錯(cuò)信息里的“unknown identifier”經(jīng)常不是模型思路錯(cuò)而是庫(kù)里的函數(shù)名變了。3.3 長(zhǎng)篇數(shù)學(xué)論述的梳理和交叉檢查一份重大證明草稿可能長(zhǎng)達(dá)幾百頁(yè)里面會(huì)反復(fù)引用前面已經(jīng)證明過(guò)的引理、定義和記號(hào)。人工做全文一致性檢查既辛苦又容易漏。LLM雖然不能替你證明但在“文本層面的結(jié)構(gòu)梳理”上可以幫上大忙。比如你可以把文檔按章節(jié)切塊喂給模型讓它輸出每章使用了哪些定義、引理、定理和假設(shè)。然后把這些輸出匯總成一張依賴表交叉檢查某個(gè)引理到底有沒(méi)有被證明、有沒(méi)有循環(huán)引用。這種做法本質(zhì)上是在做“文檔工程”但它能把人的注意力集中在真正需要數(shù)學(xué)判斷的地方而不是耗在翻頁(yè)和檢索上。再比如你可以讓模型檢查“同一個(gè)符號(hào)在不同章節(jié)是否保持一致”或者“某個(gè)定理的假設(shè)條件在使用時(shí)是否被再次驗(yàn)證”。這類(lèi)任務(wù)不一定要求模型理解全部數(shù)學(xué)內(nèi)容它只需要對(duì)文本做結(jié)構(gòu)化掃描因此成功率較高。我用下來(lái)后最明顯的感受是這類(lèi)輔助工作占用時(shí)間從原來(lái)的整個(gè)半天縮短到半小時(shí)而且因?yàn)檩敵鼋Y(jié)構(gòu)統(tǒng)一我還能繼續(xù)用腳本做二次檢查。4. 判斷模型能力的關(guān)鍵指標(biāo)以及怎么設(shè)置“及格線”4.1 適合用LLM處理的數(shù)學(xué)任務(wù)特征不是所有數(shù)學(xué)問(wèn)題都適合交給LLM。結(jié)合我自己的測(cè)試適合的任務(wù)通常有這幾個(gè)特征允許啟發(fā)式輸出目標(biāo)是尋找思路、生成候選命題、整理文獻(xiàn)而不是一步到位證明。有清晰驗(yàn)證手段輸出可以被數(shù)值實(shí)驗(yàn)、已有文獻(xiàn)或形式化驗(yàn)證器檢查哪怕檢查本身也要花時(shí)間。邏輯鏈不超過(guò)一定長(zhǎng)度如果問(wèn)題本身需要連續(xù)推理20步以上當(dāng)前模型很容易在中間某個(gè)位置出現(xiàn)斷裂。上下文相對(duì)完整模型能看到足夠多的定義、條件和樣例不需要“猜測(cè)”你腦中的隱含信息。下面這張表是我給任務(wù)分類(lèi)的參考任務(wù)類(lèi)型是否適合LLM說(shuō)明生成若干候選引理適合輸出后需人工或計(jì)算驗(yàn)證搜索反例的思路比較適合可以提供數(shù)值嘗試方向但需運(yùn)行實(shí)驗(yàn)自然語(yǔ)言證明翻譯為形式化策略中等配合證明器反饋可以逐步修正數(shù)百頁(yè)手稿的一致性檢查適合屬于文本結(jié)構(gòu)任務(wù)不是數(shù)學(xué)推理任務(wù)直接證明未解大猜想不適合輸出無(wú)法成為可驗(yàn)證的“證明”除非后續(xù)流程極嚴(yán)格要特別注意即使任務(wù)“適合”也只是一開(kāi)始適合。真正落地時(shí)模型的回答質(zhì)量和你的提示詞、驗(yàn)證機(jī)制、容錯(cuò)設(shè)計(jì)強(qiáng)相關(guān)。4.2 哪些任務(wù)容易被模型的“流暢表達(dá)”騙過(guò)去最容易翻車(chē)的數(shù)學(xué)任務(wù)通常是那些“模型見(jiàn)過(guò)很多類(lèi)似文本”的任務(wù)。比如常見(jiàn)的數(shù)論定理、經(jīng)典不等式、基礎(chǔ)群論結(jié)論模型很容易在開(kāi)頭引用正確中間開(kāi)始堆砌已知結(jié)論最后用一句“因此”收尾。表面上很完整實(shí)際上并沒(méi)有構(gòu)造出有效的證明鏈。更隱蔽的是“存在性證明”和“構(gòu)造性證明”混合的任務(wù)。模型可能會(huì)說(shuō)“定義映射f為該集合到另一集合的映射”但完全沒(méi)說(shuō)明映射的存在性、良定義性或者是否依賴于選擇公理。對(duì)受過(guò)訓(xùn)練的人來(lái)說(shuō)這種跳步可以被發(fā)現(xiàn)但如果只是讀一遍很容易被它的“專(zhuān)業(yè)感”迷惑。因此在大型數(shù)學(xué)發(fā)展里用LLM時(shí)我建議對(duì)所有模型輸出設(shè)置一個(gè)共同原則任何沒(méi)有被獨(dú)立驗(yàn)證的聲明都只當(dāng)作候選材料處理。哪怕它引用了某個(gè)定理也要去查原文獻(xiàn)確認(rèn)定理?xiàng)l件確實(shí)適用于當(dāng)前情境。這不是不信任模型而是概率模型本身的邊界決定了它無(wú)法保證邏輯確定性。4.3 怎么給模型輸出設(shè)置“及格線”“及格線”不是“模型回答得對(duì)不對(duì)”而是“這份回答能不能進(jìn)入下一步驗(yàn)證流程”。我一般用四個(gè)層次L0無(wú)法使用。輸出混亂、符號(hào)未定義、邏輯跳躍直接丟棄。L1可以摘取片段。整體不可靠但里面某幾個(gè)例子、某個(gè)引理名稱(chēng)、某個(gè)數(shù)值方向有價(jià)值可以提取出來(lái)。L2可以進(jìn)入半自動(dòng)驗(yàn)證。輸出結(jié)構(gòu)完整可分離出關(guān)鍵斷言我可以用計(jì)算腳本或證明器逐一檢驗(yàn)。L3可以作為草稿繼續(xù)推進(jìn)。大部分步驟都合理需要補(bǔ)充的只是具體計(jì)算和細(xì)節(jié)整理。用這個(gè)分級(jí)標(biāo)準(zhǔn)每次模型輸出后都有明確的去向而不是籠統(tǒng)地“覺(jué)得還行”。在研究了幾個(gè)真實(shí)案例之后你會(huì)發(fā)現(xiàn)L2和L3的比例通常不高但這并不代表LLM沒(méi)用因?yàn)長(zhǎng)1里經(jīng)常藏著有價(jià)值的線索。真正重要的是你不能把L1當(dāng)成L3來(lái)用。5. 資源環(huán)境與批量化本地、API和集群怎么選5.1 入門(mén)階段的最低配置如果你只是想試一下這個(gè)主題先不需要急著部署本地大模型。用常見(jiàn)API、開(kāi)源模型的在線Demo或者跑一個(gè)量化過(guò)的中小型模型都可以完成大部分實(shí)驗(yàn)。這個(gè)階段需要的不是滿血的推理能力而是低成本、快速迭代。本地部署的低配參考大概是16GB內(nèi)存加一張8GB顯存的GPU能跑7B參數(shù)級(jí)別的量化模型處理單條數(shù)學(xué)證明思路沒(méi)問(wèn)題但速度不快。如果是13B、14B模型最好有16GB以上顯存如果沒(méi)有獨(dú)顯只靠CPU也能跑但你要有等待的心理準(zhǔn)備一個(gè)長(zhǎng)文本生成任務(wù)可能要幾分鐘甚至更久。比較穩(wěn)妥的順序是先用API或在線環(huán)境驗(yàn)證提示詞和流程等確認(rèn)這套流程有穩(wěn)定價(jià)值后再考慮本地部署。千萬(wàn)不要一開(kāi)始就花大量時(shí)間配置服務(wù)結(jié)果發(fā)現(xiàn)你的問(wèn)題根本不適合LLM處理。5.2 批量任務(wù)的資源管理和日志結(jié)構(gòu)當(dāng)你開(kāi)始批量測(cè)試最重要的事情就不是單個(gè)模型有多強(qiáng)而是任務(wù)管理有多規(guī)范。我建議至少記錄以下信息字段說(shuō)明任務(wù)ID每個(gè)輸入的唯一編號(hào)方便回溯模型名稱(chēng)包括版本號(hào)例如“某個(gè)開(kāi)源模型的7B量化版”提示詞版本因?yàn)槟阋欢〞?huì)多次修改提示詞輸入命題原始目標(biāo)命題輸出文本模型生成的完整結(jié)果人工評(píng)級(jí)L0/L1/L2/L3驗(yàn)證結(jié)果是否通過(guò)了數(shù)值驗(yàn)證、證明器或人工檢查錯(cuò)誤信息如果有超時(shí)、截?cái)唷⒏袷藉e(cuò)誤記錄原始異常批量任務(wù)不要一上來(lái)就開(kāi)最大并發(fā)。如果你的接口有限速并發(fā)太大會(huì)直接觸發(fā)429或者被斷開(kāi)如果你本地部署多個(gè)請(qǐng)求同時(shí)跑會(huì)導(dǎo)致顯存溢出或響應(yīng)時(shí)間急劇上升。我一般會(huì)從“1個(gè)并發(fā)”開(kāi)始跑通后再逐步增加到2、4、8同時(shí)觀察成功率和延遲的變化。5.3 本地部署時(shí)我自己踩過(guò)的幾個(gè)坑本地部署數(shù)學(xué)任務(wù)時(shí)最常遇到的問(wèn)題不是模型不會(huì)推理而是環(huán)境配置把你的時(shí)間吃掉了。列幾個(gè)高頻坑端口被占用啟動(dòng)服務(wù)時(shí)提示“端口已被使用”先查進(jìn)程不要直接換端口因?yàn)槟愫竺鎸?duì)接的代碼可能寫(xiě)死了地址。上下文長(zhǎng)度限制數(shù)學(xué)證明往往需要把前面的定義和引理塞進(jìn)上下文很多模型默認(rèn)的context window不夠用。生成到一半突然丟失前文輸出后半段就會(huì)跑偏。max_tokens限制一次生成的最大長(zhǎng)度設(shè)置太小模型還沒(méi)寫(xiě)完整就被截?cái)?。這個(gè)問(wèn)題會(huì)把一個(gè)有潛力的證明思路切成殘稿。顯存溢出批量任務(wù)或長(zhǎng)文本生成時(shí)最容易出現(xiàn)。解決辦法一般是降低批量數(shù)、降低推理精度、或者切斷超長(zhǎng)輸入。我建議的排查順序是先用最短的輸入做一次生成確認(rèn)服務(wù)能啟動(dòng)、輸出不是空然后逐步增加輸入長(zhǎng)度觀察顯存和內(nèi)存占用最后再跑批量。這樣你才能確定一個(gè)“最大安全輸入長(zhǎng)度”避免后續(xù)任務(wù)集體失敗。6. 失敗模式和排查順序?yàn)槭裁础澳Ｐ驼f(shuō)得對(duì)”不等于“證明是對(duì)的”6.1 最常見(jiàn)的三類(lèi)失敗用LLM做數(shù)學(xué)研究失敗是常態(tài)關(guān)鍵是要識(shí)別它們。我遇到最多的三類(lèi)失敗是這樣的幻覺(jué)引理模型引用一個(gè)聽(tīng)起來(lái)很標(biāo)準(zhǔn)的定理但實(shí)際并不存在或者條件與當(dāng)前命題不匹配。比如明明是在實(shí)變函數(shù)問(wèn)題的證明里突然搬出一個(gè)“據(jù)復(fù)分析里的某某定理”之類(lèi)的說(shuō)法。符號(hào)漂移同一個(gè)變量在文章前半段表示集合后半段變成映射或者“n”在第一個(gè)引理表示正整數(shù)在第二個(gè)引理里變成某個(gè)生成元的個(gè)數(shù)。這種錯(cuò)誤在長(zhǎng)篇生成里幾乎無(wú)法避免。邏輯跳步模型知道開(kāi)頭和結(jié)論但中間省略了關(guān)鍵的構(gòu)造或驗(yàn)證步驟。省略的原因可能是上下文被截?cái)嘁部赡芫褪悄Ｐ陀X(jué)得“太簡(jiǎn)單不用寫(xiě)”。這三種失敗都不是偶發(fā)問(wèn)題而是概率生成模型的結(jié)構(gòu)性特征。我們需要接受這個(gè)現(xiàn)實(shí)然后用流程去兜底。6.2 數(shù)學(xué)場(chǎng)景下的排查鏈路如果模型輸出出了問(wèn)題先不要急著換模型、調(diào)溫度、改并發(fā)。我建議按下面的順序排查先看輸入提示詞是否完整。目標(biāo)命題、可用工具、輸出格式是否寫(xiě)清楚如果連“需要定義的符號(hào)”都沒(méi)讓模型寫(xiě)它當(dāng)然容易亂造。再看模型輸出中的變量、定理引用和邏輯步驟。把每一步單獨(dú)拆出來(lái)和原始定義、已知條件對(duì)照。重點(diǎn)不是“這句話通不通”而是“這個(gè)變量的類(lèi)型對(duì)不對(duì)”“這個(gè)引理的適用條件滿不滿足”。如果輸出是形式化證明腳本運(yùn)行證明器看具體報(bào)錯(cuò)。比如Lean的“unsolved goals”“type mismatch”會(huì)準(zhǔn)確告訴你問(wèn)題在哪一步。此時(shí)不要因?yàn)槟Ｐ蛯?xiě)了10行策略就忽略最后一行錯(cuò)誤。最后才調(diào)整模型或參數(shù)。溫度、top_p這些參數(shù)主要影響隨機(jī)性不能解決邏輯斷裂。如果同樣的輸入反復(fù)失敗問(wèn)題多半不在參數(shù)而在任務(wù)分解或驗(yàn)證機(jī)制。我把這個(gè)順序?qū)懗闪艘粋€(gè)清單每次實(shí)驗(yàn)前都過(guò)一遍。你會(huì)發(fā)現(xiàn)很多時(shí)候“模型不行”其實(shí)是輸入材料或驗(yàn)證過(guò)程沒(méi)跟上。6.3 降低風(fēng)險(xiǎn)的具體策略與其期待模型變得更強(qiáng)不如在流程設(shè)計(jì)上降低風(fēng)險(xiǎn)。我常用的幾招強(qiáng)制分步輸出在提示詞里要求“先列出需要的引理再給出證明思路”。這樣即便最終證明失敗你也能拿到一份引理清單繼續(xù)排查。要求標(biāo)注待驗(yàn)證聲明讓模型對(duì)每個(gè)關(guān)鍵步驟標(biāo)出“這里需要獨(dú)立驗(yàn)證”。這可以逼它把隱含假設(shè)暴露出來(lái)。自動(dòng)抽查關(guān)鍵信息把輸出中的定理名、公式、變量提取出來(lái)和已有論文或符號(hào)庫(kù)做匹配。雖然不能驗(yàn)證邏輯但能很快發(fā)現(xiàn)“引用一個(gè)不存在的定理”這種問(wèn)題。重要結(jié)論必須過(guò)證明器或人工復(fù)核只要一條路線可能進(jìn)入正式論文就不能停留在“模型說(shuō)可以”。這些策略不會(huì)讓模型變聰明但它們能把“模型產(chǎn)生的噪音”控制在可管理的范圍內(nèi)。7. 我的經(jīng)驗(yàn)先把“小定理跑通”再談“重大發(fā)展”7.1 從經(jīng)典問(wèn)題開(kāi)始建立基線如果你想在這個(gè)方向認(rèn)真投入我特別建議先花一兩周時(shí)間做“小定理跑通”訓(xùn)練。選一個(gè)你熟悉的數(shù)學(xué)分支找三到五個(gè)經(jīng)典引理讓LLM給你生成證明思路再逐條驗(yàn)證。不要選太容易的也不要選世界難題選那種“你完全知道標(biāo)準(zhǔn)證明但過(guò)程有幾步需要仔細(xì)檢查”的問(wèn)題。記錄下三個(gè)指標(biāo)結(jié)構(gòu)完整率輸出中是否有完整的定義、條件和結(jié)論?？沈?yàn)證步驟比例輸出的步驟有多少能直接進(jìn)入計(jì)算或證明器驗(yàn)證。有效修正次數(shù)在人工介入后你需要修正多少次才能得到可靠證明。這些數(shù)據(jù)會(huì)告訴你這個(gè)模型在你這個(gè)領(lǐng)域里到底處于什么水平。我測(cè)試下來(lái)不同模型在不同數(shù)學(xué)分支上的表現(xiàn)差異很大不能簡(jiǎn)單說(shuō)“某模型擅長(zhǎng)數(shù)學(xué)”。7.2 把LLM當(dāng)作科研流水線上的“第一階段篩子”在真正涉及重大數(shù)學(xué)發(fā)展的工作中我更愿意把LLM看成“第一階段篩子”。它的作用不是做最終判斷而是快速擴(kuò)大搜索范圍。比如一個(gè)研究方向有100種可能的路徑人的精力只能認(rèn)真看5種LLM可以幫你從100種里挑出15種“至少在文本層面沒(méi)有明顯矛盾”的路徑然后你再重點(diǎn)投入。這個(gè)篩選過(guò)程不是“用模型代替判斷”而是“用模型降低試錯(cuò)成本”。一條路徑會(huì)被淘汰往往不是因?yàn)樗跀?shù)學(xué)上真的不可行而是因?yàn)橘Y料查找和初步嘗試的成本太高。LLM把這一步成本壓下來(lái)之后整個(gè)科研流程的推進(jìn)速度會(huì)明顯更快。當(dāng)然這也意味著你需要有一套嚴(yán)格的“淘汰標(biāo)準(zhǔn)”。我習(xí)慣在篩選時(shí)就明確寫(xiě)出什么樣的情況算“值得繼續(xù)”什么樣的情況算“直接放棄”。比如說(shuō)如果模型給出的證明思路在第一步就需要一個(gè)未被證明且看起來(lái)很難證的引理那我可能立刻降低優(yōu)先級(jí)如果模型給出的主要困難恰好是當(dāng)前研究計(jì)劃里已經(jīng)準(zhǔn)備處理的步驟那就可以繼續(xù)。7.3 給想入坑的人三條建議最后給想在這個(gè)方向投入的人三條建議都是我自己踩過(guò)坑以后才總結(jié)出來(lái)的從可驗(yàn)證的小問(wèn)題入手不要直接挑戰(zhàn)大猜想。大猜想如果失敗你分不清是模型能力問(wèn)題、提示詞問(wèn)題還是這個(gè)猜想本身太難小問(wèn)題可以幫你把變量控制住。給模型的輸出預(yù)設(shè)驗(yàn)證機(jī)制不留“可能對(duì)”的模糊地帶。每一步輸出都應(yīng)該能映射到某個(gè)可執(zhí)行檢查數(shù)值計(jì)算、已有文獻(xiàn)、證明器、人工重寫(xiě)。把每一次實(shí)驗(yàn)記錄成可復(fù)現(xiàn)材料。包括提示詞、模型版本、輸入命題、輸出結(jié)果、驗(yàn)證結(jié)論。沒(méi)有記錄就無(wú)法判斷自己是在進(jìn)步還是在原地打轉(zhuǎn)。我更傾向于把LLM看成“數(shù)學(xué)工作的協(xié)處理器”而不是“證明機(jī)”。它真正能幫上忙的地方是讓那些大量重復(fù)、文獻(xiàn)密集、結(jié)構(gòu)繁瑣的前期工作變得不那么消耗人。至于最終證明是否成立還是要靠形式化工具、同行評(píng)審和你自己的數(shù)學(xué)判斷。如果你能把這兩者結(jié)合起來(lái)現(xiàn)在就能把很多“不可能完成”的初期調(diào)研任務(wù)變成“只要花一個(gè)下午就能跑完的實(shí)驗(yàn)”。