OpenAIがAIモデル生成の数学研究カタログを公開—719件の成果を検証中

OpenAI、AI生成の数学研究カタログをGitHubで公開

OpenAIは、未発表の社内AIモデルが生成した数学研究論文と、それを裏付ける証明成果をまとめたカタログを、2024年5月28日にGitHubで公開しました (OpenAI math research catalogue)。このカタログは、AIが複雑な数学的問題解決にどの程度貢献できるかを示すものとして、大きな注目を集めています。

OpenAIのAIモデルが生成した719件の数学論文が公開され、AIの学術研究への応用可能性が示されました。

このコレクションには、719の論文が372の関連する「ファミリー」として整理されています。ファミリーは、主要な結果、補足的な議論、結果、または代替の証明を含む複数の関連論文をまとめたものです。各ファミリーは数学の分野別に分類されており、研究者は概要や原稿マップを通じて個々の論文や関連資料を閲覧できます。

カタログの成果と検証状況

公開された成果の約42%は、Leanを用いた形式的な証明を伴っています。Leanは、数学的証明をコンピュータで検証するためのツールチェーンです。OpenAIは、今後も形式化された証明を随時追加していくとしています。

OpenAIは、これらの結果の大部分が、未発表の社内モデルを用いて同じ手順で得られたと述べています。平均して、各結果には「ChatGPT Pro」の3時間分の計算リソースが使用されたとのことです。評価期間中、モデルには約4,000の問題が提示され、その中から適切な有意性を持つ出力が集約されて、今回のカタログが作成されました。

既に撤回された一部の成果と今後の更新

今回の発表以前に、OpenAIは既にいくつかの数学的結果を撤回していることが明らかになっています。例えば、3つの論文（「Algebraicity of Weil classes on split abelian eightfolds」「Algebraicity of Kuga–Satake Correspondences for K3 Surfaces」「The rati」）は、研究レポジトリの更新に伴い撤回されました（Dan Roberts on X）。

一部の非形式化結果には問題がある可能性があり、OpenAIは速やかな修正に努めるとしています。

これは、AIが生成した成果であっても、人間による厳密な検証と修正が不可欠であることを示唆しています。OpenAIは、非形式化された結果に問題が見つかった場合は速やかに修正し、過去の公開履歴を維持しつつ、新しいバージョンとして修正版を公開する方針を示しています。また、これらの資料をコミュニティがホストするリポジトリでの公開も検討しているとのことです。

エンジニア目線で見ると：AIの創造性と検証のバランスが重要

今回のOpenAIの発表は、AIが単なるツールとしてではなく、新しい知識や概念を生み出す「共同研究者」となり得る可能性を示唆していると感じます。特に、約42%の成果が形式化された証明を伴っている点は、AIが生成する結果の信頼性を高める上で非常に重要ではないでしょうか。

私自身、普段のコーディングでClaude Codeを使ってバイブコーディングを実践している身としては、AIが単に既存のパターンを組み合わせるだけでなく、真に新しいアイデアや証明の道筋を見つけ出す能力を持っていることに驚きを感じます。数学的証明は、その厳密さからAIにとって非常にハードルの高い領域だと考えられてきました。このカタログの公開は、LLMの推論能力が、これまで考えられていた以上に高度なレベルに達していることを示しているように感じます。

一方で、非形式化された結果に問題が含まれる可能性や、既に一部の論文が撤回されている事実は、AIが生成した成果に対する人間の検証が不可欠であることを明確に示しています。これは、AIが生成したコードをそのまま本番環境にデプロイするのではなく、人間によるレビューやテストを徹底するのと同じ感覚です。数学のような厳密な分野では、一層の確認が求められるでしょう。

今後、コミュニティを巻き込んだ検証体制がどのように構築されていくのか、その動向に注目したいと思います。もしかすると、AIが生成した証明を別のAIが検証するような、「AIペアプログラミング」ならぬ「AIペアプルーフ」のような仕組みが生まれる可能性もあるかもしれません。