10月6日、OpenAIは未公開の内部モデルが生成した数学論文719本をGitHubに公開した。この公開は、同社自身の諮問機関がAI研究機関に対し専有モデルでの高度な数学問題のテスト停止を呼びかけたわずか1週間後に行われた。この1週間の経緯は、AI駆動の数学研究を巡る緊張関係を浮き彫りにしている。研究機関はモデルの進捗を測るために公開問題を利用する一方、数学コミュニティの一部は、AI生成の結果が拡散される前に情報開示と従来型の査読を求めている。

600件超の調査回答がIAS諮問パネルの9月29日ガイダンスを形成

ニュージャージー州プリンストンの高等研究所に拠点を置く「数学と人工知能に関する諮問グループ」は、600件を超える調査回答に基づく勧告を9月29日に発表した。「冒頭で明確に申し上げたい。我々はこの慣行を承認するものではなく、専有モデルでの高度な数学問題のテストを停止するよう要請する」と同グループはそのガイダンスの中で記している。

同じ文書は、非公開の内部モデルが、一部の研究機関が他の分野を引き離す二層構造を生むリスクがあると警告している。

リポジトリによれば、OpenAIはモデル開発の一環として公開研究問題でモデルをテストしており、既存の数学ベンチマークが飽和状態——モデルが現在のテストで満点に近いスコアを取る段階——に達した後、テストを拡大した。同社は諮問グループと協議し、その勧告を今回の公開に反映させたと述べている。10月6日付の声明で同グループは、その諮問役割は「OpenAIがこれらの結果を得たプロセスの承認」を意味しないとし、コンプライアンスの判断をより広い数学コミュニに委ねた。

ナビエ-ストークスのLeanコードは論文の記述よりも弱い主張しか証明していない

OpenAIは719本の論文を372の数学ファミリーに整理し、それぞれ主要な結果とその関連証明を中心に構成している。専有モデルには約4,000件の問題が与えられ、各結果には平均して約3時間のChatGPT Pro思考計算を要した。

諮問グループはAI研究機関に対し、各結果についてモデル名、使用したプロンプト、要約された思考連鎖、所要時間、計算コストを公開するよう要請している。OpenAIは10件の推論要約を公開し、主要結果の約42%にLean形式化が付いている。今回の公開がこの結果ごとのチェックリストにどこまで適合しているかは、数学コミュニティが判断すべき問題の一つとして残されている。

Leanはコンピュータが証明を検証できるプログラミング言語である。コードがコンパイルしても、それはコードと記述された論証が同一であることを意味しない。形式的な命題が真であることを確認するに過ぎない。このように記述された論証を機械検証可能なコードに変換することを、研究者は自動形式化と呼んでいる。

この乖離は、10月6日に公開された論文でAlexander Bastounis、Fabian Circelli、Anders C. Hansenの3氏が検証した。彼らは、OpenAIの記述形式によるナビエ-ストークス論文がLeanコードで証明される範囲を超える主張を含み、ある推定では入力微分の順序が変わっていることを発見した。著者らはOpenAIのオイラーの証明にも同様の誤訳を検出し、OpenAIの記述形式の証明やその他の自動形式化されたLean証明は「他の証明に課されるのと同じ査読プロセスと精査なしには、 prima facie(一見したところ)信頼すべきではない」と記している。

OpenAIは9月8日にナビエ-ストークスの結果を発表した。この方程式はクレイ数学研究所のミレニアム懸賞問題の一つであり、各問題には100万ドルの賞金が設定されている。その後、NYUの数学者Tristan Buckmasterは、この研究に係る人間の関与が最小限であるとする同社の説明に異議を唱えた(Cryptopolitanの報道)。同社は主要なAI結果に関するワークショップ、会議、特別プログラムへの資金提供を約束している。10月6日、数学者のTerence Taoは、AIシステムにプロンプトを与える人々はしばしば問題を解いた後にその分野への関心を失い、多くは結果に関する質問に答えたり講演したりできないと記した。同投稿でOpenAIの名前には触れていない。

同社は諮問機関に研究のペースを左右する発言権はないと述べている(9月のCryptopolitanの報道)。コンプライアンスの判断が数学コミュニティの手に委ねられた今、注目すべきは、査読が記述からLeanへの変換を支持するか否か、そして今後の公開において、モデル名、プロンプト、要約された思考連鎖、所要時間、計算コストといった諮問グループが各結果に求めている情報開示が明示されるか否かである。