本文へスキップ
IFAI

研究

OpenAI、未公開モデルによる数学論文722本を公開 検証支援に500万ドル拠出

公開 拡散指数 36

OpenAIは未公開のフロンティアモデルが作成した722本の数学論文を公開した。Lean言語による形式化証明も含み、1成果あたり平均約3時間のChatGPT Pro思考演算を消費したという。10月15日にはサイモンズ財団へ500万ドルを助成し、数学者による検証を支援する方針を示した。

OpenAI、未公開モデルによる数学論文722本を公開 検証支援に500万ドル拠出
画像:openai.com

トップクラスの数学者が生涯をかけて挑むような難問を、AI がわずか数時間で、しかも大量に片付けてしまう時代が現実になりつつあります。

OpenAI は 10 月 6 日、未公開の社内フロンティアモデルが作成した 722 本の数学論文を GitHub 上で一挙に公開しました。これらは 372 の成果グループに分類されており、数論や幾何学、理論計算機科学における重要な未解決問題を解決、あるいは大きく進展させたと同社は説明しています。

驚くべきはその計算効率です。OpenAI は約 4,000 件の問題をモデルに提示しましたが、そのほとんどがわずか 1 回のプロンプトで生成されました。1 つの成果にかかった計算リソースは、平均して ChatGPT Pro の推論時間およそ 3 時間分にすぎません。

リーマン予想への接近と Lean による厳密検証

今回最も注目を集めているのが、「準リーマン予想」の証明です。素数の分布則に関する有名な 100 万ドルの未解決難問「リーマン予想」の派生版にあたる問題です。

モデルは完全な解決には至らなかったものの、例外的なゼロ点が領域の外側 12.5% には存在し得ないことを証明し、可能性のある範囲を 25% 狭めることに成功しました。また、有理数解を認めた場合のヒルベルトの第 10 問題に関しても、一般的な判定アルゴリズムが存在しないことを示す証明が含まれています。

ハルシネーション(もっともらしい嘘)への懸念に対して、OpenAI は計算機科学のアプローチで対抗しました。公開された成果のうち 162 本については、コンピュータで論理ステップを機械検証できるプログラミング言語「Lean」を用いて形式化されています。

称賛の声と、学会からの強い反発

今回の大量公開に対し、研究者の反応は大きく二分しています。

競合企業 Anthropic の数学者である Levent Alpöge 氏は「数学の歴史上、明らかに最も重大な瞬間だ」と惜しみない賛辞を送りました。

一方で、現場の数学者たちからは困惑と怒りの声が上がっています。WIRED の報道によると、人間側が査読・消化できるよう「発表時期を分散させる」と OpenAI が約束していたと信じる研究者も少なくありませんでした。これに対し OpenAI の広報担当者は、そうした約束は把握していないと回答しています。

学会との摩擦を緩和するため、OpenAI は 10 月 15 日、サイモンズ財団(Simons Foundation)の新たな取り組みへ 500 万ドルを寄付すると発表しました。人間が AI の生成結果を検証・理解するためのワークショップ開催を支援し、モデルや計算環境へのアクセスを提供する方針です。

なぜ重要か

私たちは、この発表が科学的発見のスケール則を不可逆的に変えてしまったと考えています。これまで人間のひらめきに依存していた数学の進歩が、投じたチップと電力の量に比例して進む段階へ移行しつつあります。

研究者にとっての価値は極めて具体的です。すでに 162 本が Lean で検証済みであるため、単なる宣伝文句ではなく、実際の研究の土台として今すぐ参照できます。今後は「自力で地道に証明を書く」ことよりも、「どの未解決問題に計算資源を割り振るか」「AI の証明からどんな概念的洞察を引き出すか」という目利きが問われることになります。

OpenAI の手法で巧みだったのは、機械検証可能な Lean コードをセットにした点です。これにより、単なる AI のホラ話として片付けられるのを防ぎました。

しかし、手放しでは喜べません。残る 4 分の 3 近くの手稿は未検証のままであり、大量の未消化な論文を一方的に押し付けられた学術界の査読負担は限界を超えつつあります。AI による成果の生成速度に、人間の検証能力が追いつかなくなる構造的リスクが浮き彫りになっています。

情報源 (1)

  1. [1]
    openai.com(新しいタブで開きます)原文openai.com

毎日のAIピックアップ