AI 摘要
- OpenAI 內部模型嘗試約 4,000 道開放數學問題並於 GitHub 公開 722 篇研究手稿。
- 研究透過 Lean 形式化驗證邏輯，但部分未驗證的手稿仍可能存在推論錯誤。
- 學術諮詢小組警告以專有模型研究前沿數學可能導致學術圈出現不平等的兩級制度。
人工智慧研究機構 OpenAI 於 10 月 6 日公布大量由其內部前沿模型推導出的數學研究成果，並在開源平台 GitHub 上公開發布 722 篇研究手稿。OpenAI 指出，隨著現有標準化數學基準測試逐漸無法有效區分高階模型的能力差距，團隊已將測試範疇推進至尚未解決的真實開放數學難題。目前，產生這批研究成果的底層前沿模型尚未對外公開，OpenAI 表示正評估以負責任的方式釋出該技術。
涵蓋372個研究家族，每項平均耗費3小時推論運算
根據 OpenAI 釋出的技術說明，該內部模型總共嘗試了解答約 4,000 道數學問題。經過系統性整理與重要性篩選後，這些成果被歸納為 372 個研究家族，最終編纂成 722 篇手稿。在架構上，同一個家族可能涵蓋核心成果、輔助證明、延伸推論或相異的證明路徑。OpenAI 估算，產生每項研究結果的平均運算資源，相當於 ChatGPT Pro thinking 模式持續運算約 3 小時。
研究課題跨足多個高度專業的數學分支，OpenAI 同步公開了其中 10 項成果的模型推理摘要，涵蓋主題包括：
- π 的無理性指數（Irrationality measure of π）
- Mahler 猜想（Mahler’s conjecture）
- Kaplansky 直接有限性猜想（Kaplansky’s direct finiteness conjecture）
- Mézard–Parisi 公式（Mézard–Parisi formula）
- 自由群因子同構（Free group factor isomorphism）
- 三維相對論 Vlasov–Maxwell 系統
此外，部分具備特殊性質的研究未完全遵循標準化評測流程，例如黎曼 ζ 函數零點自由區域的研究，以及 CM 阿貝爾簇的 Hodge 猜想證明；其中涉及黎曼 ζ 函數的論文曾由人類專家進行編輯以提高文本可讀性。
導入 Lean 形式化驗證，未經驗證內容仍存潛在錯誤
為了解決大型語言模型在嚴謹邏輯推導中的可驗證性問題，OpenAI 為部分研究成果建立了 Lean 形式化證明。Lean 語言可讓電腦程式根據嚴格的定義與推導規則逐行校驗論證是否成立。然而，OpenAI 坦承目前公布的 722 篇手稿並未全部完成 Lean 形式化，部分未經形式化驗證的推論仍可能包含瑕疵，團隊後續將補齊形式化程式碼並修正錯誤。
除了研究手稿本身，OpenAI 也揭露了部分實驗脈絡，包含嘗試問題總數、算力估算與推理摘要，並為手稿建立了修訂版本控制及引用機制。該機構未來計畫探索由數學社群主導的研究發布平台，並提供資金贊助相關研討會與專案計畫，以協助學術界審視與延伸這些成果。
學術諮詢小組提出警訊：防範研究領域出現「兩級制度」
針對本次資料發布，獨立組織「數學與人工智慧諮詢小組」（Advisory Group on Mathematics and Artificial Intelligence，AGMAI）發布觀點，將此事件定調為「數學領域的一項重要事件」，但也表明其諮詢身分並不代表替成果的學術影響背書，亦非贊同 OpenAI 取得結果的方法。
AGMAI 提出反思，指出前沿 AI 模型產生的複雜論證，有時可能超出提示者本人理解與驗證的能力範圍。該組織認為，數學的發展不能單純看重正確結論的數量，更核心的價值在於人類如何理解、推演與延伸這些思想。此外，AGMAI 反對研究機構使用外界無法取得的閉源專有模型來探索前沿問題，憂心此舉將導致資源龐大的 AI 實驗室大幅領先其他學者，形成不平等的「兩級制度」，甚至可能削弱數學家獨立提出問題與發展理論框架的主導權。
Reference Link : ithome.com.tw
