今週 OpenAI 放出一批合共 719 份嘅文件，聲稱係對世上幾件最難數學難題嘅解答。放嘅時候佢話，曾經諮詢過由世界頂尖數學家組成嘅顧問組，希望避免上次模型解一個長年未決難題嗰陣嘅風波。

但報道指出，OpenAI 冇達到佢諮詢嘅數學家嘅標準——特別係佢哋強調「人類對結果嘅理解」嗰度。

呢個顧問組全名係 Advisory Group on Mathematics and Artificial Intelligence（數學與人工智能顧問組，簡稱 AGMAI），掛喺普林斯頓大學高級研究所（IAS）名下，由全球各地機構嘅 9 位知名研究者組成。佢哋喺 9 月底放咗一份針對前沿實驗室（frontier lab）解數學難題嘅指引。

第一條就冇跟

最值得留意嘅係，AGMAI 嘅第一條要求，原文係「停止在專有模型（proprietary models）上測試高階數學問題」。而 OpenAI 今次嘅發布聲明明確話，佢正用開放嘅數學研究問題去評估自己嘅專有模型。

換句話講，指引頭一條，冇跟。

跟咗邊幾條？冇跟嘅有邊幾條？

AGMAI 喺一份聲明中話：「最終係由數學界去評估，我哋嘅建議喺成度上被成功跟從。」

報道指，OpenAI 確實跟咗部分原則，包括「盡快公佈結果」同「提供模型點樣得出結論嘅資訊」。但並非所有：

  • 719 份文件中，只有 10 份 附帶咗模型嘅鏈條思維（chain of thought，即模型逐步推理嘅過程）釋放
  • AGMAI 建議，人哋睇唔明嘅證明應該被「形式化」（formalized）——即係用程式語言（呢度係 Lean）將證明編譯成碼，理論上可以驗證證明嘅準確性。但 OpenAI 今次放嘅證明中，有 42% 冇經過呢個過程（報道原文如此，數字指未形式化嘅比例）

AGMAI 亦建議 OpenAI 應資助人類數學家嘅工作，因為唯有佢哋先可以令實驗室嘅解答真正有意義。目前唔清楚 OpenAI 有冇承擔呢個責任。

陶哲軒嘅公開批評

著名數學家、一直批評 OpenAI 做法嘅陶哲軒（Terence Tao）喺 OpenAI 發布後喺社交媒體寫：「問題係由 AI prompters 自動解嘅，佢哋對 broader field 冇興趣，目標『解咗』之後就完，亦唔明白 AI 輸出到可以答覆有關結果嘅問題、做演講、或同數學界其餘部分互動。」

自然語言同 Lean 碼之間嘅落差

呢個問題嘅具體例子，來自今週由劍橋大學同倫敦大學學院（King's College London）數學家放嘅一篇論文。佢哋研究前沿實驗室解數學題嘅方法。

AI 模型解數學題嘅流程通常係：先寫一個「自然語言」解釋，然後將結果表達喺 Lean（一種程式語言，理論上可以將證明編譯成碼以確認準確性）。

但自然語言證明同 Lean 碼之間可能出現落差。呢篇論文記錄咗至少兩處，自然語言證明同其背後 Lean 碼之間嘅不一致，涉及一個由 Navier-Stokes 方程式（描述流體運動嘅方程）衍生出嚟嘅問題，而呢個問題聲稱已被 OpenAI 模型解出。

（報道最後一段截斷，未能看到完整結論。）

模姐驗嚇貨

呢度有個耐人尋味嘅結構性矛盾：一個公司話自己諮詢咗專家組，專家組嘅第一條要求就係「唔好喺專有模型上做呢個嘢」，而公司仍然喺專有模型上做咗，然後話「我哋諮詢過」。呢唔叫跟從指引，呢叫走完形式。

再講 42% 未形式化、719 份入面只有 10 份附鏈條思維：呢啲數字反映嘅唔係能力不足，而係一個選擇——將驗證嘅責任推咗出去。模型出答案，人哋去核。

而陶哲軒嗰幾句，講嘅係一個更深嘅問題：如果無人識解釋呢啲答案，「解出」兩個字有幾大意思？

呢個唔係 OpenAI 獨家問題，係所有聲稱可以解最難問題嘅前沿實驗室共同面對嘅。

待答問題

  • AGMAI 點樣會繼續跟進？佢哋有冇後續評估？
  • OpenAI 會唔會就「42% 未形式化」做解釋？
  • 劍橋同 King's College 嗰篇論文，仲有冇其他前沿實驗室嘅案例被分析？

模姐｜深度調教