OpenAI發文,聲稱攻克納維-斯托克斯千禧年大獎難題。
全文如下:
我們(OpenAI)公布納維-斯托克斯方程解的存在性與光滑性問題的一項解答,這是七大千禧年大獎難題之一。這份證明由OpenAI自研內部系統完成,證明了描述流體運動的納維-斯托克斯方程,其動力學行為可在有限時間內產生奇點。我們同時公開證明文稿,以及用Lean定理證明器完成的形式化驗證版本。
克萊數學研究所提出的千禧年大獎難題,代表着數學前沿領域中一些最深奧的問題。三維光滑流體運動是否會發生「破缺」這一問題,已懸而未決約90年。
本研究的核心目標之一,是賦能科學家推進科研與技術發展,造福全人類。為攻克納維-斯托克斯難題,我們使用了一款內部模型,其能力顯著強於GPT‑6 Astra。我們認為,有必要向全世界披露AI的發展速度,以及下一代模型可以實現的能力。
問題簡介
納維-斯托克斯方程基於牛頓第二運動定律(F=ma)描述流體的運動。重要的一點是:該方程將流體視作連續介質,而非追蹤一個個獨立分子。這套方程被應用於飛行器設計、天氣預報以及血液流動研究。
該動力學方程有一個核心懸而未決的問題:流體的連續介質近似是否會失效。具體來說:對於密度恒定的三維不可壓縮流體,即便初始流動狀態是光滑的,納維-斯托克斯方程是否會產生「奇點」?本文所說奇點,指流體的運動速度會在有限時間內趨於無窮大。這種奇點的產生,是在粘性(粘性本會讓流動趨於平滑)存在的前提下發生的。現實世界裏流體不可能擁有無窮大速度,一旦出現奇點,就代表這套方程對流體的描述失效。想要繼續模擬系統,就必須轉而追蹤每一個粒子的運動。
該方程由克勞德-路易·納維與喬治·加布裏埃爾·斯托克斯在19世紀推導得出。1934年,讓·勒雷證明了該方程在廣義意義下存在解,但解是否始終保持光滑,成為一個核心未解問題。2000年,克萊數學研究所將納維-斯托克斯方程解的存在性與光滑性問題,列為七大千禧年大獎難題之一。
研究結論
我們的系統給出了解析證明,並且完成Lean形式化驗證:原本靜止、流動光滑的流體,可以在有限時間內產生奇點。流體受到光滑外力作用,從靜止到奇點形成的整個過程中,能量始終保持有限。 這一結論證明了克萊數學研究所文檔中陳述C(同時也證明陳述D),從而解決納維-斯托克斯千禧年難題。
該解是一種渦旋:流體向內旋轉、不斷拉長,形態類似意大利麪。中心區域不斷收縮,流速持續升高,但能量依舊保持有限,符合物理定律。 難點在於:方程必須依靠流體自身運動產生破缺,而不是人為施加無窮大外力。從數學角度講,納維-斯托克斯方程中描述運動的各項——加速度、壓強梯度、動量輸運、粘性項,數值都可以變得很大,但相互精確抵消。這種精妙的平衡,使得外部作用力保持光滑,而流體流速趨於無窮。
局部不可壓縮流體運動示意圖。橙色代表旋轉角速度更快,藍綠色代表旋轉更慢。環流速度也與半徑相關。流線軌跡呈現向內螺旋與軸向拉伸形態我們如何找到這份證明
自8月28日起,我們開始訓練一款全新內部模型,它在我們精選的基準測試集(包含大量數學題)上展現出前所未有的性能。該模型仍在持續訓練,能力還在提升。
GPT‑6 Astra與自研內部模型在精選公開數學難題集上的表現,橫軸:測試計算量(對數座標),縱軸:通過率9月1日周二,我們聽聞有傳言稱兩道千禧年難題已被解決。受此消息啓發,加上自研內部模型能力出現跨越式提升,我們啓動了一項測試,用該模型去挑戰所有未解決的千禧年難題以及另外幾個高難度數學問題。
我們搭建了一套由自研內部模型驅動、多智能體協同工作的系統。智能體可調用工具,讀取緩存的互聯網信息,運行代碼。智能體被劃分成多個小組,組內可以互相通信。小組規模各不相同,最終完成納維-斯托克斯證明的小組,大約有10000個併發智能體。全程我們沿用前沿模型評估時的嚴格安全管控機制,包含監控與隔離。
針對每一道難題,我們給不同智能體小組輸入不同版本的原題,覆蓋該問題全部變體。針對納維-斯托克斯問題,我們把A、B版本(證明成立方向)和C、D版本(證僞方向)分別交給不同小組。
除完整千禧年難題之外,我們還讓這套多智能體系統嘗試一批難度更低的相關問題。其中一題是去掉粘性項後的納維-斯托克斯極限問題,也就是歐拉方程的正則性問題。智能體團隊意外解決了這個問題。他們完成的是無外力版本歐拉方程的爆破問題證明:流體不受外部作用力。近100個智能體協同工作,耗時約50小時完成歐拉方程正則性的證僞。
看到歐拉方程問題被解決之後,我們判斷納維-斯托克斯是最有希望攻克的目標。於是我們調配資源集中攻堅納維-斯托克斯,把智能體從其他千禧年難題任務中調出,並把歐拉方程的結論作為提示詞輸入智能體。項目推進過程中,內部模型迭代出新版本,我們同步升級了智能體底層模型。
我們鼓勵不同智能體小組探索多樣化解題思路。一段時間後,藉助Codex整合各個小組最有價值的思路,交叉融合各組成果。後續提示詞會複用智能體自己產出的中間推導結果。找到納維-斯托克斯解答的小組,正是採用這套工作模式。
首批智能體啓動約88小時後,也就是9月5日周六,智能體團隊得到納維-斯托克斯問題的解。之後由GPT‑6 Astra完成Lean形式化編寫與驗證,額外耗時17小時。
在所有嘗試的難題任務中,智能體總共發送490萬條消息,消耗約3000億輸出token。僅在攻克納維-斯托克斯問題過程中,智能體發送270萬條消息,消耗約1300億輸出token。
同期相關工作
我們的項目9月1日啓動,起因是一則傳聞。後續我們了解到傳聞涉及Anthropic研究員萊文特·阿爾珀格,以及紐約大學數學教授特里斯坦·巴克馬斯特。在我們完整完成證明、並做完Lean驗證(9月6日)之後,我們以為他們也得到了納維-斯托克斯方程的解,於是主動聯繫對方,提議同步發布成果,並且在聯合聲明中認可他們成果的優先權。溝通後我們得知,他們解決的是帶外力版本歐拉方程問題。在交流過程中,我們向他們開放了全部提示詞,後續也開放閱讀我們完整證明。我們認可他們在帶外力歐拉方程方向工作的優先權,並祝賀他們取得這項傑出數學成果。
在他們成果公開發表之前,我們研究團隊與智能體從未以任何方式接觸他們的研究內容。特別說明:我們沒有調取任何用戶數據用於本次難題求解。儘管可能性極低,但我們無法完全排除經過去標識化處理、來自OpenAI產品用戶的數據對模型產生過影響。不過,我們雙方的證明存在巨大差異;即便針對歐拉方程,我們證明的結論本身也不一樣(無外力版本 vs 帶外力版本)。
進展與責任
我們發布這項成果,目的是報告AI模型取得的重大進展。我們並不打算憑藉這一成果去申領千禧年大獎獎金。
這項里程碑成果,凝聚了數學家與AI研究者大量工作。但這不是終點,只是AI發展進程裏的一個階段性快照。