OpenAI 正在分享納維-史托克斯存在性與平滑性問題的解決方案,這是七大千禧年大獎難題之一。這項證明由 OpenAI 內部系統產生,顯示流體運動的納維-史托克斯方程式可能在有限時間內產生奇異點。我們同時公開了證明文件和 Lean 形式化版本。
千禧年大獎難題代表著數學前沿最深奧的一些問題。關於平滑三維流體運動是否會崩潰的問題,已經懸而未決大約 90 年。
我們工作的一個主要目標是賦能科學家,推動造福全人類的研究和技術發展。為了解決納維-史托克斯問題,我們使用了一個內部模型,其能力遠超 GPT-6 Astra。
我們認為,讓世界了解 AI 進步的速度以及未來模型的能力至關重要。
納維-史托克斯方程式利用牛頓第二運動定律(「F=ma」)來描述流體如何運動。重要的是,它們將流體視為連續介質,而非追蹤單個分子。
這些方程式被應用於飛機設計、天氣預報以及血液流動的研究。
這些動力學方程式的一個基本未解問題是,流體的連續介質近似是否會失效。具體來說,即使運動開始時是平滑的,具有恆定密度的三維不可壓縮流體的納維-史托克斯方程式是否會產生「奇異點」?
在這裡,奇異點意味著流體中的速度在有限時間內無限增長。奇異點的產生必須發生在儘管有黏度(黏度傾向於平滑運動)存在的情況下。由於真實流體不可能無限快地運動,這將標誌著方程式對流體建模方式的失效。要繼續對系統建模,就必須單獨追蹤每個粒子的行為。
這些方程式可追溯到十九世紀 Claude-Louis Navier 和 George Gabriel Stokes 的研究。1934 年,Jean Leray 證明了廣義解的存在,但它們是否始終保持平滑成為一個核心未解問題。
2000 年,克雷數學研究所將納維-史托克斯存在性與平滑性問題列為七大千禧年大獎難題之一。
我們的系統產生了一個分析證明和 Lean 形式化,證明了最初靜止的平滑流體可以在有限時間內產生奇異點。流體受到平滑力的作用,其能量在整個動力學過程中(從靜止到奇異點形成)保持有限。
這透過確立官方千禧年大獎表述中的「C」聲明(以及「D」聲明),解決了納維-史托克斯千禧年大獎難題。
該解決方案是一個渦旋,即一種旋轉的流體漩渦,它向內螺旋並變得越來越細長,就像義大利麵一樣。這個中心區域在縮小的同時加速,但其能量仍保持有限,符合物理定律。
技術挑戰在於方程式必須透過流體自身的運動來產生崩潰,而不是例如我們手動施加無限大的力。更數學地說,納維-史托克斯方程式中描述運動的項——加速度、壓力梯度、動量傳遞、黏度——必須同時變大,但又以精確的方式相互抵消。這種精細的平衡使得即使流體速度無限增長,外部力仍然是平滑的。
我們如何找到證明 自 8 月 28 日以來,我們一直在訓練一個新的內部模型,該模型在我們的基準測試中(包括數學領域)展現出前所未有的性能。
這個模型的訓練仍在進行中,其性能持續提升。
9 月 1 日星期二,我們聽說有兩個千禧年大獎難題已獲解決的傳聞。受這些傳聞以及我們內部模型性能顯著提升的啟發,我們啟動了一項工作,評估它在所有未解的千禧年大獎難題以及其他一些高影響力問題上的表現。
我們使用了一個由內部模型驅動的協調代理系統。這些代理可以存取工具,例如從網際網路快取版本讀取資料以及執行程式碼。代理被細分為小組,小組內部可以互相溝通。
小組規模各異,解決納維-史托克斯問題的小組涉及大約 10,000 個並行代理。我們始終維持與所有前沿模型評估相同的嚴格安全措施,包括監控和隔離。
對於每個問題,我們向不同的代理小組提供了問題陳述的不同變體,涵蓋了問題的所有可能性。對於納維-史托克斯問題,我們向不同的代理小組建議了「A」和「B」版本(納維-史托克斯問題的特定形式,會產生證明)以及「C」和「D」版本(會產生反證)。
除了完整的千禧年大獎難題,我們還要求我們的多代理系統嘗試一系列「較簡單」的問題。其中一個問題是納維-史托克斯問題在移除黏度項後的極限情況,類似的「爆破」問題。
這被稱為歐拉方程式的規律性問題,我們的代理令我們驚訝地解決了這個問題。他們解決的具體問題變體是無外力版本,即沒有外部力施加於流體。近 100 個代理協同工作約 50 小時,產生了我們的歐拉規律性反證。
一旦我們看到歐拉方程式的解,我們認為納維-史托克斯問題是最有希望解決的。因此,我們決定將資源投入到納維-史托克斯問題上。
為此,我們將代理從其他千禧年難題轉移過來,並以歐拉方程式的解來提示這些代理。在整個工作中,當我們內部模型的進一步訓練版本可用時,我們就將代理更新到該模型。
我們鼓勵不同的代理小組探索多樣化的方法。一段時間後,我們透過使用 Codex 整合各代理小組最有用的見解,進行了小組間的「交叉授粉」。
這些後續提示詞借鑒了代理自身的階段性成果。找到納維-史托克斯問題解決方案的小組就是以這種方式引導的。
代理們在 9 月 5 日星期六達成了他們的解決方案,距離首批代理啟動約 88 小時。透過 GPT-6 Astra 進行 Lean 形式化和驗證又花了額外 17 小時。
同步工作 我們的努力始於 9 月 1 日,當時我們聽到一個傳聞,後來才意識到這與 Anthropic 員工 Levent Alpöge 和紐約大學數學教授 Tristan Buckmaster 有關。在我們完成整個專案和 Lean 驗證(9 月 6 日)後,我們根據傳聞認為他們也解決了納維-史托克斯問題,於是聯繫他們,提議同時發布我們的結果並在聯合聲明中承認他們的優先權。
那時我們才發現他們解決的是受力歐拉問題。在這些討論中,我們向他們提供了我們使用的所有提示詞,並隨後讓他們查看證明。我們承認他們在受力歐拉問題上的工作優先權,並祝賀他們取得了卓越的數學成就。
我們(研究人員和代理)在他們公開發布之前,沒有透過任何方式看到他們的任何工作——特別是,沒有為了解決這個問題而存取任何特定的使用者資料。雖然可能性不大,但我們不能排除從他們使用我們產品中獲得的去識別化資料有助於改進我們的模型。
然而,我們的證明顯著不同,即使在歐拉方程式的情況下(受力與無外力),所證明的精確結果也不同。
進步與責任 我們發布此結果的目標是報告我們 AI 模型的實質性進展。我們不打算為此結果聲稱千禧年大獎。
這個里程碑代表了數學家和 AI 研究人員的實質性工作。然而,這並非終點,而只是 AI 發展進程中的一個時間點。
我們相信我們現在正處於 AI 進步的下一個階段,今天的結果提供了進一步的證據。我們正專注於理解這個模型,並利用所學來指導和調整我們如何追求能力的進一步提升。
我們的一個關鍵目標是建立可控、負責任並與人類連結的 AI 系統,這可能需要更審慎地選擇進步的速度,因為我們將繼續我們的使命,確保通用人工智慧 (AGI) 造福全人類。
