北京
8月2日消息，OpenAI周六公開十項數學與理論計算機科學成果，同時放出249頁論文、62頁推理說明和一套Lean 4形式化證明。不過生成這些結果的下一代模型Astra仍是內部版本，沒有隨之開放。
據OpenAI介紹，Astra生成數學論證后，人類與模型共同將其整理成論文，再由模型編寫Lean證明。OpenAI把尋找十項解法消耗的token按Sol API價格折算，估計成本約為2000美元。
這種發布方式在AI行業里不太尋常的：外界暫時無法測試Astra，卻可以先檢查它交出的數學結果。
周五The Information曾援引三名知情人士稱，Astra當時仍是暫定名稱。OpenAI向華盛頓的政策制定者和監管人員演示過它處理長時任務和多智能體協作的能力，但沒有給出產品發布時間和最終型號。
十項成果，分屬不同的證明任務
這份名單橫跨高維幾何、編碼理論、群論、算術電路、量子復雜性、格密碼和極值組合數學等多個分支。
具體來看，高維球堆積和編碼理論得到新的上界；Astra構造了非sofic群，并為Connes剛性猜想給出反例；Ehrhart體積猜想得到銳界；多色Ramsey數和極值圖論的研究則解決了三個由保羅·厄多斯提出、長期未解的問題。
有些工作把已知邊界向前推進，有些構造過去不知道是否存在的對象，還有些推翻或完成具體猜想。它們被放在同一次發布里，后續復核和引用則會分別發生在各自領域。
Lean 給外部復核加了一條可運行路徑
OpenAI在GitHub公布了十項結果的Lean文件、統一構建命令和Comparator配置。官方形式化清單顯示，主要證明的sorry_count為0，只使用propext、Classical.choice和Quot.sound三類公理。Comparator目錄里的sorry是留給外部核驗者的題面空缺，不在正式證明文件中。
配置相應版本的Lean、mathlib和Comparator后，研究者可以在本地重跑證明，檢查解答是否證明同一形式化命題、是否引入清單之外的公理、以及推導能否被Lean內核接受。同行審稿通常需要數月乃至數年，形式化文件提供了一條可以定位到具體行的復核路徑。
不過Lean內核只檢查推導本身。猜想到形式化命題的翻譯是否走樣、方法是否新穎、結果在學科內的分量，仍需要人來判斷。
62頁推理說明是事后整理稿。文件注明，模型讀過原始思維鏈與最終論文后，重新敘述成功思路、失敗路線和轉折點。這意味著，讀者看到的是重構后的路線圖，不是模型當時的原始思考。
2000 美元只是 token 成本
尋找解法約2000美元這個數字，只計算token，并按Sol API價格折算。模型訓練、選題、數學家參與、基礎設施和項目中的其他成本沒有列入。官方倉庫另注明，把這些證明寫成Lean形式化文件，前后花了一周時間。
與這次發布同期，《華爾街日報》報道，新晉菲爾茲獎得主雅各布·齊默曼（Jacob Tsimerman）將從多倫多大學休假，加入OpenAI從事AI安全研究。他準備把數學中的形式語言和驗證方法用于理解、評估模型行為。
兩周前，Anthropic研究員萊文特·阿爾珀格（Levent Alp?ge）公布了Jacobian猜想在三維及更高維度的反例，并把尋找反例的功勞歸給Fable 5。提示詞、搜索過程以及人和模型各自完成了多少工作，至今沒有公開。
阿爾珀格的博士導師正是齊默曼。
OpenAI這次用Lean檢查模型給出的數學證明。齊默曼加入后，想把形式化方法繼續用到模型行為上。對OpenAI而言，“驗證”正在同時進入模型的產出和模型本身。（易句）
（本文由AI翻譯，網易編輯負責校對）
本文來源：網易智能
責任編輯：
王鳳枝_NT2541
