先說(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)入了新階段。這類工作通常有幾個(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)證工作壓縮到幾天。適合閱讀這篇文章的主要是三類人一是做數(shù)學(xué)或數(shù)學(xué)物理研究的人想了解AI工具現(xiàn)在能頂?shù)侥囊徊蕉亲鲂问交?yàn)證、定理證明輔助工具的工程師想知道LLM怎么接入Lean、Isabelle這類流程三是對(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)是“它能解微積分、能寫證明那是不是也能推動(dòng)數(shù)學(xué)研究”這種判斷容易踩坑。普通問(wèn)答里的數(shù)學(xué)題大多有明確答案、固定解法、短邏輯鏈模型只要見(jiàn)過(guò)類似例題就能模仿出一篇看起來(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)證明用是這類工作流里最大的失敗原因。所以我的建議是一開(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)前模型到底適合哪類任務(wù)。比如“證明根號(hào)2是無(wú)理數(shù)”“證明素?cái)?shù)有無(wú)窮多個(gè)”這類基礎(chǔ)但完整的證明。別覺(jué)得這些題目太簡(jiǎn)單它們的價(jià)值在于證明結(jié)構(gòu)完整、邏輯鏈清晰、錯(cuò)誤容易發(fā)現(xiàn)你能快速判斷模型是在“真正推理”還是在“回憶相似文本”。實(shí)測(cè)時(shí)你很快會(huì)發(fā)現(xiàn)幾種典型現(xiàn)象模型能寫出歐幾里得素?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)你拿到一段證明第一件事不是看它寫得順不順而是把它拆成步驟逐條對(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ā)展并生成一份帶公式的筆記。候選命題與反例搜索從已知定理做類比擴(kuò)展生成“如果滿足這些條件會(huì)不會(huì)有類似結(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)造先不要一步到位部署大模型。做這類實(shí)驗(yàn)入門階段用API或者在線Demo就夠了重點(diǎn)是“怎么把數(shù)學(xué)問(wèn)題寫成模型能吃透的提示詞”。我在實(shí)際測(cè)試時(shí)發(fā)現(xiàn)很多人不是模型選錯(cuò)而是問(wèn)題描述太含糊。數(shù)學(xué)證明任務(wù)必須把三樣?xùn)|西寫清楚目標(biāo)命題用標(biāo)準(zhǔn)數(shù)學(xué)符號(hào)寫清楚要證明什么。可用工具允許使用哪些已證明的定理、定義、公理。輸出格式要求模型給出定義、證明思路、關(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. 給出證明的主思路不要一步一步寫滿但要讓讀者知道整體走向。 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)有任何定義、引理、條件分類那基本不能用于研究場(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)很專業(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è)坑寫了一個(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把模型名稱、提示詞版本、輸入命題、輸出結(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)的三類落地點(diǎn)3.1 猜想形成階段讓模型生成候選命題和特例重大數(shù)學(xué)發(fā)展很少是憑空冒出來(lái)的很多時(shí)候是先有大量數(shù)值實(shí)驗(yàn)和類比再被凝練成猜想。LLM在這個(gè)階段能做兩件事一是生成“類比命題”二是生成“可能讓命題失敗的特例”。舉個(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)。所以它能給出的類比通常很直接不太可能產(chǎn)生那種需要跨領(lǐng)域抽象才能發(fā)現(xiàn)的深刻猜想。把它當(dāng)成“靈感收集器”比當(dāng)成“新時(shí)代拉馬努金”更實(shí)際。3.2 交互式定理證明用LLM輔助Lean等證明腳本這是目前我覺(jué)得最接近“工程可落地”的方向之一。Lean、Isabelle、Coq這些交互式定理證明器要求每一個(gè)證明步驟都能被機(jī)器檢查。以往寫這類形式化證明非常耗時(shí)尤其是從自然語(yǔ)言草稿翻譯成形式化策略。LLM擅長(zhǎng)的是“看到當(dāng)前證明狀態(tài)生成下一步要執(zhí)行的策略”這個(gè)模式非常適合接入證明器。流程大致是在Lean里把定理陳述寫成標(biāo)準(zhǔn)形式例如一個(gè)目標(biāo)命題。把當(dāng)前“證明狀態(tài)”goal和已有的上下文喂給LLM。讓模型生成一系列策略或中間斷言。把模型輸出交給Lean執(zhí)行查看是否通過(guò)。這里有個(gè)關(guān)鍵認(rèn)知模型不需要一次寫完整份證明它只需要生成“下一步”或者“下一步的一小段”然后通過(guò)證明器反饋來(lái)修正。這種交互模式利用了證明器的確定性彌補(bǔ)了模型的概率性。換句話說(shuō)模型負(fù)責(zé)“出招”證明器負(fù)責(zé)“驗(yàn)證”二者配合得好的時(shí)候會(huì)比我憑空讓模型寫完整證明穩(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)證”。這類任務(wù)不一定要求模型理解全部數(shù)學(xué)內(nèi)容它只需要對(duì)文本做結(jié)構(gòu)化掃描因此成功率較高。我用下來(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ù)分類的參考任務(wù)類型是否適合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ò)去最容易翻車的數(shù)學(xué)任務(wù)通常是那些“模型見(jiàn)過(guò)很多類似文本”的任務(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)但如果只是讀一遍很容易被它的“專業(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è)引理名稱、某個(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 入門階段的最低配置如果你只是想試一下這個(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)方便回溯模型名稱包括版本號(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ì)接的代碼可能寫死了地址。上下文長(zhǎng)度限制數(shù)學(xué)證明往往需要把前面的定義和引理塞進(jìn)上下文很多模型默認(rèn)的context window不夠用。生成到一半突然丟失前文輸出后半段就會(huì)跑偏。max_tokens限制一次生成的最大長(zhǎng)度設(shè)置太小模型還沒(méi)寫完整就被截?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)的三類失敗用LLM做數(shù)學(xué)研究失敗是常態(tài)關(guān)鍵是要識(shí)別它們。我遇到最多的三類失敗是這樣的幻覺(jué)引理模型引用一個(gè)聽(tīng)起來(lái)很標(biāo)準(zhǔn)的定理但實(shí)際并不存在或者條件與當(dāng)前命題不匹配。比如明明是在實(shí)變函數(shù)問(wèn)題的證明里突然搬出一個(gè)“據(jù)復(fù)分析里的某某定理”之類的說(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)單不用寫”。這三種失敗都不是偶發(fā)問(wèn)題而是概率生成模型的結(jié)構(gòu)性特征。我們需要接受這個(gè)現(xiàn)實(shí)然后用流程去兜底。6.2 數(shù)學(xué)場(chǎng)景下的排查鏈路如果模型輸出出了問(wèn)題先不要急著換模型、調(diào)溫度、改并發(fā)。我建議按下面的順序排查先看輸入提示詞是否完整。目標(biāo)命題、可用工具、輸出格式是否寫清楚如果連“需要定義的符號(hào)”都沒(méi)讓模型寫它當(dāng)然容易亂造。再看模型輸出中的變量、定理引用和邏輯步驟。把每一步單獨(dú)拆出來(lái)和原始定義、已知條件對(duì)照。重點(diǎn)不是“這句話通不通”而是“這個(gè)變量的類型對(duì)不對(duì)”“這個(gè)引理的適用條件滿不滿足”。如果輸出是形式化證明腳本運(yùn)行證明器看具體報(bào)錯(cuò)。比如Lean的“unsolved goals”“type mismatch”會(huì)準(zhǔn)確告訴你問(wèn)題在哪一步。此時(shí)不要因?yàn)槟Ｐ蛯懥?0行策略就忽略最后一行錯(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í)就明確寫出什么樣的情況算“值得繼續(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)、證明器、人工重寫。把每一次實(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)”。