新聞 
幣種資訊 
關於我們 
OpenAI公開的722篇數學手稿中，目前存檔剩下719篇。頂尖結果約42%已用Lean形式化，但數學界仍在評估整體成果。
OpenAI在10月6日的公告中表示，已公開內部前沿模型產出的數學研究成果。公開存檔將722篇手稿整理為372組結果，並稱曾向模型提出約4000道題目。存檔異動紀錄顯示，3篇手稿撤回、14篇修訂。
手稿涵蓋數論、代數幾何、分析學與理論計算機科學等領域。OpenAI也公開部分證明的Lean形式化內容、10份推理摘要，以及運算量估算。公司表示，取得單一結果平均使用的運算量，相當於ChatGPT Pro「思考」功能約3小時。模型名稱及模型本身並未公開。
Lean是一種將數學命題轉成形式語言，並由電腦檢查證明步驟是否符合邏輯規則的工具。OpenAI存檔目前標示，頂尖結果約42%已形式化；截至10月7日的異動紀錄則顯示，719篇中有300篇完成形式化。
形式化比例不代表所有手稿都正確。Lean能檢查輸入的形式命題及其證明過程，但不會自動判斷該命題是否符合論文聲稱的結果，也不會確認假設與適用範圍是否恰當。OpenAI也在存檔中表示，尚未形式化的結果可能存在問題。
除了驗證，研究過程公開到什麼程度也受到關注。OpenAI在公告中表示，已參考獨立顧問小組的建議，並將手稿修訂與引用流程，以及部分方法資訊放入存檔。不過，公司未公開模型及完整提示詞，外部研究者難以在相同條件下重現結果。
數學與人工智慧顧問小組（AGMAI）於10月6日表示，此次公開是理解成果並將其納入數學知識的起點。該小組也指出，與OpenAI進行討論，不代表其認可成果的影響力或為公開流程背書。小組並強調，數學家不應只負責檢視AI公司挑選題目的結果，也應能自行發展問題與研究方法。
僅憑手稿數量與形式化比例，難以確定個別結果的重要性或學術意義。OpenAI公布722篇手稿時，當時也只有部分證明以Lean形式化，整體成果尚未完成驗證。此次確認的變化，是公開後有手稿撤回與修訂，並有部分證明完成形式化。
留言 0