一雪前恥，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)。

GPT-5破解世紀(jì)難題，竟是上網(wǎng)抄來(lái)的！哈薩比斯：太尷尬了。

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

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

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

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

反轉(zhuǎn)

ChatGPT為OpenAI「正名」

昨天，這個(gè)故事來(lái)了一個(gè)反轉(zhuǎn)——

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

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

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

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

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

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

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

看來(lái)文獻(xiàn)檢索，終究不是件簡(jiǎn)單的事??。

潛臺(tái)詞是說，GPT-5過去找到的10個(gè)已有解答，并非易事。

但后面的更精彩。

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

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

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

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

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

值得一提的是，用AI找到Erd?s問題的「已有答案」，陶哲軒之前已經(jīng)成功展示過概念驗(yàn)證。

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

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

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

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

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

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

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

即使是少量的針對(duì)性優(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形式化只是對(duì)人類證明的補(bǔ)充，并不能取而代之。」

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

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

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

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

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

這一探索起源于兩人請(qǐng)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)后，它提出了一個(gè)關(guān)于帶擦除的非交互相關(guān)蒸餾問題（Non-Interactive Correlation Distillation, NICD with erasures）的反例：

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

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

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

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

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

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

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

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

• 給出了最終可行的證明思路與論證框架
• 通過快速排除無(wú)效路線，大幅加速了探索進(jìn)程

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

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

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

• 篩選出不正確的論點(diǎn)，并積累一系列正確的事實(shí)。
• 識(shí)別有前景的新推理思路，并引導(dǎo) ChatGPT 進(jìn)一步探索這些思路。
• 認(rèn)識(shí)到何時(shí)某個(gè)策略已被充分探索，并決定何時(shí)轉(zhuǎn)向其他方向。

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

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

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

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

GPT-5提出的證明：

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

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

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

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