![]()
本文的共同第一作者包括北京大學信息科學技術學院圖靈班本科生柯繹思、疏彥凱、數學科學學院本科生黃天域;共同通訊作者為北京大學王立威老師、卡內基梅隆大學博士生蓋景初;其他作者還包括北京大學賀笛老師。
近期,LLM 已經在 IMO 上取得了很好的成績,在一些研究級數學上(如短程證明、組合構造)也有所進展。但如果真正讓 LLM 去處理提出數十年的數學猜想,結果會是如何?在本工作中,北大王立威教授團隊構建了一套基于 LLM 的框架,聚焦Gilbert-Pollak 猜想(斯坦納比猜想),成功將二維平面的斯坦納比從 1985 年證明的 0.824 改進到了,距離猜想目標僅差 0.01,一步之遙!
該進展已被陶哲軒 Terence Tao收錄組合數學優化中的常數列表中!問題編號 43。
- 倉庫鏈接:https://github.com/teorth/optimizationproblems
這個問題有多大影響力?在上個世紀,該問題由貝爾實驗室科學家 Gilbert 和 Pollak 提出。著名數學家、美國數學學會(AMS)前主席 Ronald Graham(葛立恒)、美國國家科學院院士 Fan Chung(金芳蓉)都對該問題進行過系統深入的研究。1990 年,堵丁柱教授和 Frank Hwang(黃光明)研究員進行了一系列相關研究,曾被譽為 1989 年 - 1990 年度美國離散數學界和理論計算機科學界重大成果。圍繞該問題的研究論文眾多,是一個飽受數學家關注的猜想。
目前該工作已被 ICML 2026 接收,相關代碼和數學證明均已開源。
![]()
- 論文標題:Towards Solving the Gilbert-Pollak Conjecture via Large Language Models
- 論文地址:https://arxiv.org/abs/2601.22365
- 項目倉庫:https://github.com/keyisi2006/Steiner-Ratio
困擾人類 60 年的 Gilbert-Pollak 猜想
![]()
![]()
形象點說:給定平面上 n 個城市,最小生成樹(MST)就是修建 n - 1 條鐵路將它們連起來。最小斯坦納樹(SMT)就是可以額外修建若干個中轉站,再修建鐵路將它們連起來。可以看出,合適地建立中轉站會讓路程變短,但猜想指出:并不會短太多。
![]()
![]()
問題 1:直接寫成 prompt 問 LLM,行不行?
之前一系列 AI4Math 的工作,要么是數學證明的長度較短(如 IMO 問題),要么是針對構造性的、非嚴謹證明性的組合構造問題。
![]()
讓 LLM 直接去寫幾十頁的嚴謹數學證明,還要有創新性,對于目前 LLM 能力來說為時過早。為了解決斯坦納比猜想,必須減少證明長度,或者向構造性的方向轉換。
步驟 1.1:看看人類數學家怎么做?
回顧人類數學家的工作,發現大家都是采取了歸納法:對于一棵很大的斯坦納樹,只去考慮一個局部,從中摘除(prune)掉一小部分的點,并將剩下的點重連成斯坦納樹。
![]()
那么,只要剩下的部分滿足比例(歸納假設)+ 摘除過程的變化量滿足比例,就可以合并得到原問題滿足比例!寫成一行公式就是:
![]()
從而,問題的關鍵就是找到更好的摘除 / 分割樹的方式。
步驟 1.2:整理一下?這就是 Max-Min 問題!
本工作中提出了一個叫做驗證函數(verification functions)的數學工具,一個驗證函數就代表了一種分割樹的方式。歸納法就是要求:任意的樹形態,存在一種分割,使得比例成立。其實這就是一個max-min 問題:最大的樹形態 w ——最小的驗證函數 F。
![]()
人類數學家嘗試了 10 種不同的 F,可以得到 0.824 的下界。如果 LLM 能幫助人類嘗試 1000 種不同的 F,就有機會得到更好的下界!
本工作設計了一個Reward Model,自動化了這一 max-min 問題的求解過程,通過證明單調性,并配合分治法,為所有樹形態 w 找到一個驗證函數 F 進行覆蓋。以前人類數學家需要手動進行啟發式的參數空間劃分,現在一個代碼自動搞定。下圖是假設參數空間是 2 維的一個例子:
![]()
至此,LLM 不再需要證明完整的猜想,它只需要找到更多的驗證函數 F,再與 reward model 交互就可以了!
問題 2:找來的這么多 F,正確性怎么保證?
想要生成 1000+ 個 F,只需要反復調用 LLM 即可。但基于自然語言推理的 LLM,你能相信它的嚴謹性嗎?如果讓人類一個一個檢查,時間開銷不可估量,難以 scale up。
![]()
因此,我們必須讓 LLM 在正確性可驗證的框架中運行。
步驟 2.1:給 LLM 一個引理模板
本工作通過數學變換,證明了一個事實:找更多的 F 函數,可以通過找兩類引理的方式實現:一類是 Trapped Regular Point Lemma,另一類是 4-Point Steiner Tree Lemma。
![]()
LLM 只需要負責填入結構化的參數,通過代碼片段進行表達,系統就可以通過翻譯(嵌入代碼片段)的方式產生一系列合法的 F。以第 1 類為例,這個翻譯過程可以是構造分段函數:
![]()
步驟 2.2:光有模板還不夠,讓 LLM 徹底「搭積木」
生成結構化的代碼片段仍然可能會出錯。必須要讓 LLM 像「搭積木」一樣,拼湊人類提供的規則(rules),讓數學軟件 Mathematica「合成」保對的引理,才能從根本上保證正確性。
以第 1 類引理為例,本工作提出了 A、B 兩類規則,分別代表斯坦納樹必須滿足的性質,和確保點存在性的條件。LLM 要做的,就是去選擇 2 - 3 個規則,調用 Mathematica 去化簡「什么條件下,若干個 A 能推出一個 B」。
![]()
通過這種方法,LLM 能在多輪的 tools 調用中,充分探索這個推理空間。而且這是保對的——任何的創意搭建,都不會產生邏輯的錯誤。
問題 3:正確的 F 就能提升下界嗎,有沒有「渾水摸魚」?
目前為止,系統看似很完美,實則還有一個隱藏的大問題:只是重復運行,生成 1000+ 個 F,很可能其中很多是平凡的甚至重復的,根本對斯坦納比沒有提升!
![]()
如何讓 LLM 真正生成有效的 F?必須給它針對性的迭代引導信號
步驟 3:針對問題的瓶頸反省機制
本工作提出了瓶頸(bottleneck)的概念:在 reward model 運行完成后,把得到的提升一個小量 δ(比如 0.0001),再讓 reward model 運行——此時必然反饋失敗,未被 F 覆蓋的部分的 bounding box,就是瓶頸區域。
![]()
換言之,瓶頸就是讓 ρ += δ 必須克服的參數區域。在下一輪生成 F 時,LLM 必須確保能夠覆蓋瓶頸區域。從而為每一輪的高效提升提供了保障。
迭代系統框架和成果
通過「重復生成 Reward → 確定瓶頸 → LLM Agent 提出引理 → 翻譯并開始下一輪」這個迭代范式,系統成功在 ~10 輪迭代中,將斯坦納比改進到了 0.8559。最終的成果通過了人類的檢查。
![]()
本文基于 GPT-5 系列構建了系統,并驗證了模型魯棒性:其余模型如 Gemini 3 和 Claude 4.6 均可得到類似的結果。下圖展示了迭代輪次和斯坦納比的關系。
![]()
結語
本工作證明了 LLM 有能力為研究級數學提供幫助,但要設計合適的運作框架。
在這個過程中,人類的 insight 仍然是必要的。同時,人類檢查也是必不可少的部分。
如果要用 LLM 去處理其他數學問題,可以參考的內容包括,設計一個「搭積木」式的結構化推理空間,以及設計瓶頸反省機制。
特別聲明:以上內容(如有圖片或視頻亦包括在內)為自媒體平臺“網易號”用戶上傳并發布,本平臺僅提供信息存儲服務。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.