新聞 
幣種資訊 
關於我們 
OpenAI執行長山姆·奧特曼（Sam Altman）估計，證明納維–斯托克斯方程式的工作成本約為1,000萬美元（約134億韓元）。若按他提出的成本降至百分之一估算，重做同一證明約需10萬美元（約1億3,400萬韓元），但這不是確定報價。
奧特曼在29日公開的 Cheeky Pint 訪談中表示，以「更聰明的模型和更好的方法」，從當時完成這項工作起算一年後，便可能以百分之一的成本重做同一證明。他形容當時的成本「約1,000萬美元，可能還要多一些」。
10萬美元是把奧特曼的概略估算除以100所得。OpenAI於9月8日公開的證明資料並未列出美元成本。
OpenAI表示，約1萬個以內部AI模型為基礎的代理參與解題，約花88小時找到結果。
將結果轉成Lean格式並完成驗證，又花了17小時。過程中，代理約傳送270萬則訊息，並使用約1,300億個輸出詞元。OpenAI在公告中說明了這些數據。
Lean是一種將數學論證表示為可由電腦檢查形式的工具。驗證以Lean形式化的論證，與確認該論證是否和人類可讀的論文內容一致，是兩件不同的事。
納維–斯托克斯方程式用來描述水、空氣等流體的運動。這項問題探討的是，在平滑外力作用下，三維不可壓縮流體是否會在有限時間內出現奇異點。
OpenAI表示已提出一項證明，顯示奇異點可能出現。此處的奇異點，是指方程式所描述的流體速度在有限時間內無界增大的情況。
OpenAI先前曾公開一項反駁埃爾德什猜想的通用AI證明；這次公告處理的是另一道數學問題。
曾為這項問題懸賞100萬美元（約13億4,000萬韓元）的克雷數學研究所，9月11日評估這項成果「看來已獲解決」，同時表示不會倉促完成成果評估與功勞認定程序。
OpenAI表示不會申領獎金。是否申領獎金，與數學界對證明的審查是兩回事。
倫敦國王學院與劍橋大學研究人員在10月6日公開的預印本中指出，人類可讀的證明與Lean形式化內容，在部分段落未必提出強度相同的主張。
研究人員表示，這項質疑並不等於判定OpenAI原始證明有誤；但僅通過Lean驗證，還不足以確認人類可讀的論文也已獲得驗證。
奧特曼的說法是，未來或能以更低成本完成相同工作。證明內容是否與形式化結果一致，仍須另由數學界審查。
留言 0