2024年5月，OpenAI的一個內部模型找到了Erdős單位距離猜想的一個反例。這個猜想自1946年提出以來一直懸而未決，許多專家都試圖證明它，而OpenAI找到的卻是一個反例。一個月後，OpenAI發表了對迴圈雙覆蓋（Cycle Double Cover，CDC）問題的證明，到7月又給出了另外十個開放問題的解答；9月，它又發表了對納維-斯托克斯（Navier-Stokes）方程的證明。與此同時，Anthropic發表了費馬大定理的形式化工作，並給出了黎曼猜想上的改進界。這些模型突然變得擅長數學了。
我感興趣的問題是：我們能否預測這類模型會解決哪類問題？是什麼讓一個問題對LLM而言變得可處理，這些解答又有哪些共同點？如果AI解決問題的路徑與人類不同，找出這種差異應當能幫助我們決定把AI朝哪個方向引導。關於單位距離反例的評論最為豐富，所以我們從這裡開始。
問題複雜度
這裡有一個簡單的心智模型。要解決任何給定問題，你都需要一串提示或洞見，以及它們之間的工作。這個模型出人意料地貼合日常的簡單問題，也貼合廣義相對論這樣的複雜思想。序列大致是這樣的：洞見 → 時間／工作 → 洞見 → 時間／工作 → 解答。
專家需要的提示比新手少，因為他們有更多背景知識。在關於單位距離證明的評論中，WT Gowers使用了類似的想法：證明的難度，就是讓專家能夠重建該證明的最短提示序列。他稱之為“模去專家的柯爾莫哥洛夫複雜度”。對單位距離問題，他的提示序列包含三部分：第一，尋找反例；第二，取已知最好的構造並將其推廣；第三，嘗試一系列次數遞增的數域，但使用有界範數的素理想。
Gowers提出的複雜度公式是2^k + t，其中k是最短提示序列的長度，t是展開它所需的工作量。這是一個看起來很嚴格、直到你試圖代入具體數字的公式，而這差不多正是重點所在。複雜度隨著解決問題所需洞見數量的增加而呈指數增長。
大部分解題過程都是這些洞見之間的工作。你有一個頓悟時刻，然後花幾個月把這條提示發展下去，直到下一次概念跳躍成為可能。對專家而言，花費的時間是這類工作的有用代理指標，這就是t。把第一條單位距離提示交給某人，他們仍然要做足夠多的工作才能到達那個推廣構造。
這個模型很有用，但它是事後性的。你無法看著一個問題就預測它需要x條提示。因此，問題的年齡、嘗試次數以及附帶的獎金，常被用來作為難度的代理指標。
給定提示的特徵
典型的洞見會改變問題的表述方式，也就是問題被表示和理解的方式發生變化。有兩點決定一條提示有多大價值：其一，它在被給出之前看起來有多不可能，而在給出之後看起來又有多顯然——這比人們意識到的更難。在單位距離問題中，許多專家並不認為反例是可能的。其二，它在序列中的位置：提示是有序的。只有在對前兩條提示的工作已經取得足夠進展、使第三條提示變得可操作之後，第三條提示才有用。這也就否定了那種樸素的暴力思路：列出一千種數學技巧並嘗試所有組合。提示序列遍歷的是一棵樹：最初的洞見改變問題，並揭示後續的選擇。
人類以廣度優先的方式解題
把k和t結合起來，你就得到了人類的搜尋模式：生成候選方向，淺層探索，放棄大部分，再投入到少數幾個上。如果一個有前景的方向沒有儘早給出足夠的鼓勵，它就會被放棄。這是人類的一個約束：發展一個想法可能需要數月。在投入之前，研究者需要相信它會通向某處的理由：概念上的前景、早期結果，或在類似問題上的經驗。發現這一點所需的時間越長，嘗試這個想法的門檻就越高。
大多數研究軟體的存在，就是為了透過自動化那些乏味、機械、可重複的工作來縮短這段時間。AI把這段時間縮短到了足以讓搜尋模式本身發生翻轉的程度，而下游的一切都由此而來。
AI與複雜度
首先是t。模型相當於“努力”的東西是算力和token，它們花在單條軌跡上（測試時計算），或分散到並行智慧體上（並行測試時計算）。預訓練還提供了人類研究者必須自行查詢或重建的知識。沒有哪個專家知道此前每一項進展，所以偶爾會重複已經做過的事情。
更大的差異在於模型如何搜尋：LLM是深度優先的。
給模型一個提示，它就會給出一個解答，可能正確，也可能不正確。要求它給出證明，它就會給出某種接近好證明的東西。這些模型的思維鏈也以貪心的深度優先方式執行，而且這個過程可以擴充套件。給並行智慧體十種方法，你就會得到十個朝結論推進的嘗試，它們也許彼此不同，也許有所重疊。每一個要麼撞上路障，要麼產出一個看起來正確的論證。放任不管，你就會得到漂亮的假證明。
這看起來像是在浪費算力和資源，直到你加入一個自動驗證器，它可以剪除已完成的軌跡並識別出正確的那些。有了這個檢查器，把鉅額算力花在不確定的想法上就變得理性了：你幾分鐘內就能知道某個想法是否行得通。問題在於，驗證器只能判斷已完成的論證，它無法告訴你一個只發展了一半的想法是否有前途。
對比
如果你能在五分鐘內知道一條提示是否有效，那麼這條提示需要有多好？對人類來說，質量門檻很高，因為追求一條提示可能要花數月。對模型來說，這個門檻幾乎消失了。提示可以是普通的、不太可信的，甚至是幾乎不成形的。沿著它走下去，就能確定它是否通向某處。LLM讓我們得以用時間換算力，並幫助我們在更短的時間內攻克更多問題。
失敗的嘗試對LLM而言也是提示
模型不需要一個確定的方向才能開始。預訓練已經給了它關於問題歷史和既往嘗試的先驗。每一個錯誤的解答都可以作為負向提示回傳給模型，供下一輪迭代使用。系統會積累關於哪些做法已經失敗、以及為何失敗的指令。粗略地說，一個執行框架是這樣的：起草器負責寫出給求解模型的提示，這些提示基於模型先驗、用於緩解此前執行的錯誤，並考慮到所有走進死衚衕的有希望路徑（這些是負向提示）；求解器接收提示，給出一個或多個候選解答，它可以執行多個子智慧體，用並行測試時計算走不同路徑；驗證器／檢查器則檢查論證是否有效，是否確立了所要求的結果。
以CDC的提示為例：它先假設本任務存在一個完整的肯定性證明，從而防止模型把預訓練中學到的該問題尚未解決這一狀況當作停下來的理由。接著它列出若干不足以解決問題的替代品：特殊圖類的證明、某些邊被覆蓋次數不是兩次的迴圈覆蓋構造、有界長度或指定迴圈的變體、歸約到另一個未證明的猜想、對任何固定圖規模的計算機驗證，以及沒有完整不存在性證書的候選反例。它還要求全程使用對抗性智慧體：每個候選證明都必須檢查是否恰好兩次重數、是否有偽裝成迴圈的重複邊閉跡、平行邊2-迴圈、不連通圖、割點、歸約引入的橋，以及是否迴圈使用了等價的CDC陳述。此外還有一句針對習得性懶惰的話：“不要僅僅因為當前方法失敗或智慧體報告了定理級別的缺口就返回。”
OpenAI很可能進行了多輪嘗試，起草器收集錯誤和失敗的想法，引導下一輪迭代避開它們。這裡的每一行都是一條失敗路徑，被寫成了指令。
重建單位距離證明與Tsimerman的工作
讓我們透過這個執行框架的視角重讀Gowers的三條提示。第一條，尋找反例：這真的很難，因為學界和模型的預訓練先驗都認為該猜想為真。起草器最可能是由於求解器在追求證明時不斷失敗才得出了這條提示。這個框架阻止模型把公認觀點當作它必須追求的方向。每一次失敗嘗試都讓反例顯得不那麼不可能。第二條，取已知最好的構造並將其推廣：這最接近學界先驗，是標準動作。實質性的工作是把推廣發展到足以發現它允許什麼，這是t很大的那一步。但請注意，這是一個反例的推廣，而幾乎沒人在找反例。第三條，嘗試次數遞增的數域：一旦前兩條提示建立了它適用的空間，這就是標準工具。
順序很重要。從第三條開始，你甚至不知道這項練習是要做反證。跳過推廣構造，第三條就沒有作用物件。而即便三條提示齊全，工作量依然巨大。反例這條提示事後看來很明顯，這讓人不禁要問為什麼沒人試過。事實上，有人試過。
最近被OpenAI聘用的Jacob Tsimerman研究過這個反例。他懂數論，甚至考慮過提高次數，然後他停下了。尋找反例是第一個洞見，但那只是開始。阻止他的不是缺乏技能，而是一種恰如其分的清醒感受：一個人已經在沼澤裡走了好幾周，卻沒有任何證據表明另一邊還有岸。用他自己的話說：“這是一種非常可怕的動態，很難想清楚解析區域並保持引導性直覺，耗費大量時間，而且經常不成功。”
心理學早在幾十年前就發現了問題解決的這一人類側面：Metcalfe和Wiebe每隔十五秒詢問解題者覺得自己離解答有多近，在普通問題上，他們報告出的進展感會上升；在頓悟型問題上，這種感覺一直平緩，直到他們找到答案。他們報告不出任何能支撐搜尋的進展感。頓悟型問題沒有梯度。在解決之前，你不知道自己離答案有多近。
因此，專家面臨的問題有兩重：是否有人真的進入這個分支（即提示），以及進入之後，他們是否停留足夠久，讓普通的勝任能力完成工作。停留的代價是工作記憶、士氣和職業生涯。而在一條所有已知專家都認為錯誤的路線上停留，會把這三者疊加放大。對LLM來說，這是一個巨大優勢。用Arul Shankar的話說：“模型很快過了一遍各種想法，但當它到達那個關鍵想法時（在以‘樂觀地假設……’開頭的那段裡），它相當有條不紊地鎖定到了證明上。”
這可以壓縮成兩個問題：一個問題需要多少洞見，以及在你能判斷一個方向是否值得之前，這些洞見之間有多少工作。Tsimerman這樣描述AI這一側：“這也許指出了AI系統擁有優勢的一種方式：不僅僅是它們能嘗試所有已知方法，還在於它們能比數學家玩得更久、在更險惡的水域中前行而不被壓垮。當然，這一點目前還不穩健地成立，但這也許是一個預示性事件。”
其他證明
OpenAI對納維-斯托克斯方程的證明展示了同樣的過程。根據粗略閱讀，它把已完成的工作推進到了完成……（原文在此處截斷）。這一點值得作為警示保留：關於這些模型在數學上能力的敘述仍在展開，其中一些說法來自近期、尚未經過完整同行評審的材料，因此應當審慎對待，而不是當作定論。不過，那種逐漸顯現的模式——深度優先的搜尋、廉價的驗證、由失敗嘗試構成的負向提示，以及把時間換成算力——確實有助於解釋為什麼某些開放問題如今對AI而言變得可處理，以及接下來應當把AI指向哪裡。