OpenAI、モデルが局所平滑化予想を証明し、指数時間仮説を反証、Yang–Mills理論の存在を証明したと発表

OpenAIは、同社のモデルが数学、計算機科学、物理学で3つの成果を生み出したと発表した。以下はすべてOpenAI自身の主張であり、まだ独立した検証は行われていない。OpenAIによれば、成果はLeanで検証済みだという。

• 数学（調和解析）。 OpenAIによると、モデルはあらゆる次元で局所平滑化予想を証明した。OpenAIは、これにより新しい補助偏微分方程式を用いて、すべての次元におけるKakeya予想とSteinの制限予想も解決したとしている。モデルが作成した自然言語による解説とLean証明を、10月6日の公開と同様の方針で、公開GitHubリポジトリ openai/math で公開した。
• 計算機科学。 OpenAIによると、同社のシステムはブール式充足可能性の計算量に関する予想、指数時間仮説（ETH）を反証し、その反証はLeanで検証されたという。Ryan WilliamsがRussell ImpagliazzoおよびRamamohan Paturi（Francis ZaneとともにETHを提唱）とグループを率い、反証を検証して説明する。グループの要請を受け、OpenAIは自然言語による証明とLean形式化を公開した。
• 物理学。 OpenAIによると、モデルはゲージ場とフェルミオンを含む、相互作用する特定の4次元量子場理論の数学的に厳密な存在証明を作成した。これにはQCDと標準模型の統一的な完成形が含まれ、部分問題として、クレイ数学研究所のミレニアム懸賞問題の一つである純粋Yang–Mills理論の存在証明も含まれる。証明はLeanで形式的に検証済みだという。David Grossが率い、Michael Douglas、Arthur Jaffe、Igor Klebanov、Nikita Nekrasovが参加するグループが研究を導き、資料の公開についてはOpenAIが同グループの判断に委ねる。

OpenAIは原稿を「生の研究データ」と表現し、外部専門家に研究を導く役割を依頼したところ、成果ごとに異なる公開方針を提案されたと述べている。発表によると、局所平滑化の成果は10月18日（翌日にLeanで形式化）、ETHの反証は10月16日（10月17日に形式化）、Yang–Millsの存在証明は9月9日（QCDは9月18日、Yang–MillsのLean形式化は10月16日に完了）に得られた。物理学のグループは、連絡を専用メールアドレス宛てにするよう求めており、自ら研究をまとめる間、AIが生成した成果物の公開を見送ることを決めた。

OpenAIによると、共同研究は4つの原則に従っている。透明性（秘密保持契約を結ばない）、OpenAIは学術的評価を求めないこと、グループへの評価、独立性（参加は任意かつ無報酬で、メンバーは各自の立場でのみ発言すること）だ。OpenAIはETHの成果に関する会議への資金提供を表明し、AIが生み出した成果に関するワークショップやプログラム向けにSimons Foundationへ最近500万ドルを寄付したことにも言及している。また、GitHubリポジトリに小規模な変更を加え、その内容を履歴ファイルに記載した。Xでの発表スレッドは、10月26日夜の時点で405ポイント、コメント30件だった。