數(shù)學(xué)界無視「30年漏洞」，GPT-5一眼看穿！陶哲軒：AI科研革命開始了

新智元報道

編輯：KingHZ

【新智元導(dǎo)讀】星星之火，可以燎原！證明的尊嚴(yán)在于可驗(yàn)證；這一次，GPT-5讓數(shù)學(xué)證據(jù)落在了代碼里。

一雪前恥，ChatGPT為OpenAI「正名」！

被Hassabis吐槽太尷尬之后，GPT-5真啟發(fā)了新的數(shù)學(xué)結(jié)論。

OpenAI的科學(xué)家Sebastien Bubeck高調(diào)宣揚(yáng)GPT-5破解了十道Erd?s難題。

但被指出GPT并非解決了Erd?s問題，而是找到了已經(jīng)解決這些問題的文獻(xiàn)。

之后，他刪除了推文并表示自己并非有意誤導(dǎo)。

Yann LeCun斥之為「自食其果」：OpenAI被他們自己的GPTards所害。

之后，他在LinkedIn上的發(fā)帖，明顯低調(diào)多了：

現(xiàn)在，事情來了反轉(zhuǎn)——

Sebastien Bubeck被「冤枉」了，AI的確在加速科學(xué)進(jìn)步。

反轉(zhuǎn)

ChatGPT為OpenAI「正名」

昨天，這個故事來了一個反轉(zhuǎn)——

普林斯頓大學(xué)數(shù)學(xué)博士Boris Alexeev（下圖左）和俄亥俄州立大學(xué)副教授Dustin G. Mixon（下圖右）發(fā)現(xiàn)，懸賞1000美元的707號Erd?s問題，在被提出前30年，就已經(jīng)被解決了。

論文地址：https://borisalexeev.com/pdf/erdos707.pdf

事情有些離譜，堪稱數(shù)學(xué)家的「虛空索敵」——

答案比問題早30年，但直到前不久，外界還普遍以為問題沒有被解決！

目前，707號Erd?s問題已被標(biāo)注為「Disproved」（被證偽）。

傳送門：https://www.erdosproblems.com/go_to/707

這次，Sebastien Bubeck扳回一局，發(fā)推表示：

看來文獻(xiàn)檢索，終究不是件簡單的事。

潛臺詞是說，GPT-5過去找到的10個已有解答，并非易事。

但后面的更精彩。

ChatGPT輔助數(shù)學(xué)證明，陶哲軒點(diǎn)贊

兩位數(shù)學(xué)家也懷疑結(jié)果，于是決定用GPT5在Lean中生成形式化證明。最后，居然成功了！

注意??：ChatGPT和Lean被列入了合作者，但論文內(nèi)容中還是作者「手搓」。

不過，人類在這個過程中可沒少花功夫，需要不斷給GPT5提供反饋，完善形式化論證。

在「Erd?s的難題」網(wǎng)站上，近期涌現(xiàn)了不少成功案例，研究者利用大語言模型在現(xiàn)有文獻(xiàn)中找到了埃爾德什問題的解法。

值得一提的是，用AI找到Erd?s問題的「已有答案」，

陶哲軒也注意到了這次新證明，認(rèn)為這是計算機(jī)輔助證明的有趣例子。

在研究過程中，兩位數(shù)學(xué)家確信Lean能幫助驗(yàn)證已有論文的真?zhèn)危?dāng)時既不熟悉Lean，又覺得其操作界面不夠友好。

然而由于ChatGPT能編寫Lean代碼，他們決定通過氛圍編程（vibe coding）方式形式化整個證明。

這個過程耗時約一周，體驗(yàn)頗為煎熬，但最終意外成功了——

形式系統(tǒng)中，ChatGPT嚴(yán)格證明了Erd?s猜想的否命題。

最終生成的證明超過6000行代碼，包含26個定義、169個引理和4個定理（最終的反例驗(yàn)證部分）。在普通筆記本電腦上，代碼驗(yàn)證耗時不足半分鐘。

經(jīng)過數(shù)輪往復(fù)的互動后，Boris和Dustin認(rèn)為，如果大語言模型的接口能與Lean深度整合，并針對這種交互方式進(jìn)行適當(dāng)微調(diào)，許多問題都會大大緩解。

即使是少量的針對性優(yōu)化，也足以讓這種「人機(jī)協(xié)作證明」的體驗(yàn)更加流暢、自然。

陶哲軒高度認(rèn)可這次AI輔助證明。他表示，這是在研究論文中負(fù)責(zé)任地使用LLM輸出的罕見用例之一：

重要的是，沒有任何LLM生成的輸出被直接放入正文（除了為了說明目的引用LLM生成的 Lean 代碼片段外）；

相反，這種輸出僅用于完全可驗(yàn)證的上下文中（在本例中，用于生成可由 Lean進(jìn)行類型檢查的代碼）。

不過，陶哲軒強(qiáng)調(diào)：「Lean形式化只是對人類證明的補(bǔ)充，并不能取而代之?！?/p>

此外，他幾乎可以預(yù)見會有一些夸張的報道——「這回LLM真解決了一個Erd?s問題！」

—— 但事實(shí)遠(yuǎn)比這復(fù)雜微妙。要得出任何結(jié)論，都需要先把來龍去脈仔細(xì)梳理清楚。

GPT-5推動研究，端倪初現(xiàn)

加州大學(xué)歐文分校數(shù)學(xué)教授Paata Ivanisvili，也把ChatGPT列為論文合作者。

新論文由數(shù)學(xué)教授Paata Ivanisvili、2022屆中科大本科校友Xinyuan Xie (謝新元)合作，ChatGPT是第一作者。

這一探索起源于兩人請GPT-5 Pro在公開的未解問題（下文）中尋找反例。

鏈接：https://simons.berkeley.edu/sites/default/files/openprobsmerged.pdf

標(biāo)題：Real Analysis in Computer Science：A collection of Open Problems

經(jīng)過若干數(shù)值實(shí)驗(yàn)后，它提出了一個關(guān)于帶擦除的非交互相關(guān)蒸餾問題（Non-Interactive Correlation Distillation, NICD with erasures）的反例：

一個定義在5比特上的布爾函數(shù)，在擦除參數(shù)p=0.40時，其 E∣f(z)∣值 嚴(yán)格大于 5比特多數(shù)函數(shù)（majority function）的對應(yīng)值。

他們記錄了這一發(fā)現(xiàn)并驗(yàn)證全部計算過程。

這一結(jié)果與線性閾值函數(shù)中關(guān)于「Majority is Least Stable」的經(jīng)典反例，形成了呼應(yīng)：即便AI只是將已知的反例模式應(yīng)用于新場景并加以驗(yàn)證，其貢獻(xiàn)依然值得肯定。

傳送門：https://arxiv.org/abs/1703.07657

這是理論計算機(jī)科學(xué)中AI的「星星之火」：以往大語言模型（LLMs）多用于文獻(xiàn)檢索或數(shù)值輔助，而此次則真正生成了一個具體、有限且可驗(yàn)證的反例。

此外，UCLA的數(shù)學(xué)教授Ernest Ryu，借助GPT-5 Pro解決了一個凸優(yōu)化領(lǐng)域的開放問題。

盡管模型約有80%的證明嘗試是錯誤的，卻提出了多條新穎思路。

GPT-5 Pro的具體貢獻(xiàn)：

• 給出了最終可行的證明思路與論證框架

• 通過快速排除無效路線，大幅加速了探索進(jìn)程

這項(xiàng)工作耗時約12小時，分3天完成。事后，Ernest Ryu回想起來，這個證明其實(shí)非常簡單。

ChatGPT生成的證明的關(guān)鍵步驟：

可以上下滾動的圖片

Ernest Ryu總結(jié)了他自己的貢獻(xiàn)：

• 篩選出不正確的論點(diǎn)，并積累一系列正確的事實(shí)。

• 識別有前景的新推理思路，并引導(dǎo) ChatGPT 進(jìn)一步探索這些思路

• 認(rèn)識到何時某個策略已被充分探索，并決定何時轉(zhuǎn)向其他方向。

他還將繼續(xù)開發(fā)這個項(xiàng)目，并將結(jié)果發(fā)表在專業(yè)的優(yōu)化理論期刊上，并分享更新和未來的部分。

被吐槽的OpenAI科學(xué)家Sebastien Bubeck，也復(fù)現(xiàn)了類似的場景——

GPT-5可以證明有趣的數(shù)學(xué)結(jié)論。

不過，人類實(shí)際上搶先了gpt-5 一步:-)。另一位作者完全填補(bǔ)了差距，證明了新的界限。

GPT-5提出的證明：

GPT-5已經(jīng)提出了多個具有研究價值的新想法。不僅如此，它實(shí)際上自己想出了大部分提示詞：

傳送門：https://github.com/Dicklesworthstone/model_guided_research

AI輔助研究大門，正在打開。

或許，歷史銘記的不是那句「太尷尬了」，而是那行悄無聲息通過編譯的qed。

參考資料：

https://x.com/SebastienBubeck/status/1980804267524116569

https://x.com/PI010101/status/1981014478969033156

https://borisalexeev.com/pdf/erdos707.pdf

https://mathstodon.xyz/@tao/115416211466664814

https://x.com/slow_developer/status/1980990021248160009