陶哲軒親測點贊o3-mini：專家級證明，我收到了一個完美的答案

2025年03月11日14:40:15 遊戲 7363

金磊發自凹非寺
量子位 | 公眾號 qbitai

剛剛，陶哲軒親測了一下o3-mini，然後他給出了這樣的結論：

重建圖論中一個標準（專家級）結果的證明，o3-mini是完全可以hold住的。

陶哲軒要重建的這個證明，叫做三角形移除引理（triangle removal lemma），由ruzsa和szemeredi於1978年提出，是極值圖論中的重要結果:

對於任意的η＞0，都存在c>0，使得對於任意一個足夠大的有n個頂點的圖，如果該圖中最多包含cn3個三角形，那麼可以通過移除最多ηn2條邊，使這個圖變為無三角形的圖。

用另一種表述方式就是，如果一個有n個頂點的圖包含o(n3)個三角形，那麼可以通過移除o(n2)條邊來刪除所有的三角形。

然後陶哲軒看罷o3-mini的作答後表示：

在幾秒鐘後，我收到了一個完美的答案，（o3-mini）正確地解釋了這種蘊含關係。

o3-mini是如何作答的？

首先，我們來看下陶哲軒的prompt：

ruzsa和szemeredi的三角形移除引理斷言，如果一個具有n個頂點的圖（n很大）包含o(n3)個三角形，那麼可以通過移除o(n2)條邊使其變為無三角形圖。顯然，這一引理蘊含了以下結論：如果一個具有n個頂點的圖是n個誘導匹配的並集，那麼它只包含o(n2)條邊。你知道後者是如何從前者的結論中推導出來的嗎？

對於這個問題，o3-mini的回答是這樣的：

（註：為完整體現內容，o3-mini的作答將以英文呈現）

可以看到，o3-mini回答的邏輯還是比較清晰的。

一步一步展開論證，從起始條件（誘導匹配的並集），到構建輔助圖，再到建立邊與三角形數量的聯繫、應用引理，最後得出結論。

緊接著，陶哲軒開始追問了：

謝謝！三角形移除引理的另一個標準推論是(6,3)定理：如果一個具有n個頂點的3-一致超圖不包含(6,3)-配置，即不存在六個頂點確定至少三個超邊的情況，那麼該超圖只包含o(n2)條超邊。你能解釋一下為什麼這也是三角形移除引理的一個推論嗎？

o3-mini在思考了片刻後，開始作答：

o3-mini對這個問題的總結是：

在一個不包含任何「(6,3)-configuration」（即任意六個頂點不生成三條或更多超邊）的3-uniform 超圖中，由於將超邊編碼為輔助圖中的三角形後，輔助圖的三角形結構受超圖條件限制呈現「稀疏」狀態，根據三角形移除引理可以推斷出，該超圖中的超邊總數為o(n2)，也就是說這樣的超圖不會過於稠密。

在此之後，陶哲軒便開始加大難度：

感謝你的大致概述！我有興趣將其擴展成一個更詳細的證明。我聽說首先考慮超圖是線性的情況會很有幫助——即任意兩條超邊不會共享兩個頂點。你能將你的概述擴展成一個更精確的論證，專門針對線性情況嗎？

這一次，o3-mini思考的時間足足是上個問題的四倍：

這次o3-mini的推理過程，是通過構造一個輔助圖g，將超圖中的每個超邊對應到輔助圖中的一個三角形。利用線性性質保證這些三角形邊不相交，再通過假設m=Ω(n2)推出與三角形移除引理相矛盾的結果，從而證明原假設錯誤，得出超邊數量的漸近上界。

陶哲軒再追問：

如何確保圖g不會產生任何額外的三角形，除了那些直接由超邊生成的三角形之外？

至此，陶哲軒評價道：

好的，我認為這給出了(6,3)定理在線性情況下的完整證明。

然後繼續追問o3-mini：

你有什麼建議，如何建立一般情況下使用這個線性的情況？

o3-mini給出了一種「清理」的路數：

清理超圖：通過刪除少量超邊使得到的子超圖h』線性化，「(6,3) 條件」保證不會移除過多超邊。
應用線性情況結論：為線性超圖h』構建輔助圖，每個超邊對應一個邊不相交三角形。
利用三角形移除引理：過多的邊不相交三角形會導致與引理矛盾，所以h』有o(n2)個超邊。
推導原始超圖的邊界：因為h』保留了h』的幾乎所有超邊，所以原始超圖h』也有o(n2)個超邊。

陶哲軒認為這是一個不錯的策略，並最後提出了一個問題：

你能不能試著給出一個更精確的清理步驟的描述，這個步驟可能會把一個一般的(6,3)超圖轉換成一個線性的(6,3)超圖，並對邊緣進行一些控制？

但也有局限性

在陶哲軒六連問之後，除了剛才提到的「完美答案」之外，他還給出了更加客觀中立的評價：

我的總體感覺是，至少對於研究級的數學任務，當前的模型在「僅需用戶提供大致指導即可真正有用」和「只有在用戶提供大量詳細指導後才有用」之間波動，而最強大的模型在前者中的回答比例更高。
它們似乎特別適合那些非常標準的問題，這些問題的答案基本上可以在現有資源（如維基百科或stackoverflow）中找到。
但隨著問題變得越來越冷門，成功率逐漸下降（儘管下降的方式較為平緩），並且需要更多的用戶指導（或更高的計算資源）才能使llm的輸出達到可用的形式。