OpenAIは10月6日、内部の最先端モデルが生成した数学研究の成果をGitHub上で公開した。リポジトリ名は「openai/math」で、Apache 2.0ライセンスのもとで提供されている。中には722本の論文が収められており、372の研究「ファミリー」に分類されている。同じ問題に対する異なる証明や一般化、改訂版がまとめて置かれている形だ。
OpenAIの発表によると、この研究過程でモデルに課された問題は合計で約4000問に上る。採用された結果1件あたり、平均してChatGPT Proの拡張思考モードを3時間動かした分に相当する計算リソースを消費したという。
対象となった分野
論文は数論、計算複雑性理論、数理物理学、幾何学、理論計算機科学にまたがる。報道で挙げられた例には、円周率πの無理数測度に関する問題、いくつかのNP困難問題、マーラー予想、等差数列、自由群の因子、さらには量子ハイゼンベルク強磁性体や相対論的Vlasov-Maxwell方程式などが含まれる。
証明の多くにはLeanによる形式化版が添付されている。Leanは、証明の論理をコンピュータが一段ずつ検証できるプログラミング言語で、形式化に通れば推論の筋道に穴がないことが保証される。ただしすべての論文にLeanファイルが対応しているわけではなく、OpenAIは説明の中で率直にこう述べている。
"some of the unformalized results could have issues"
つまり、形式化されていない結果には問題が残っている可能性があるということだ。同社は今後発見された誤りを修正し、形式化された証明を段階的に増やしていくとしている。リポジトリには論文の改訂プロセスと引用規則も付属しており、研究者はある結果が何回改訂されたか、引用時にどのバージョンを参照すべきかを追跡できる。
これまでの流れをつなぐ
今回の発表は、OpenAIが数学分野で前回大きな動きを見せてから4カ月以上が経っている。今年5月、OpenAIのモデルは約80年間未解決だったエルデシュの問題を解決した。当時は一点突破型で、1問ずつ報告される形だった。それが10月には、数百本の論文を一括でリポジトリに収める形に変わり、公開の仕方自体がニュースの一部になっている。
形式にも変化があった。今回の公開に先立ち、OpenAIはプリンストン高等研究所(IAS)が招集した独立の「数学とAIに関する諮問グループ」に意見を求めた。同グループは9月29日、数学界から600件以上のフィードバックを受けて提言をまとめ、AIが生成した数学的成果についてモデル名、使用したプロンプト、推論の要約、計算コスト、そして同種の問題におけるモデルの失敗率を公開するよう求めていた。
このリストと照らし合わせると、OpenAIは今回、計算コストの基準(平均してPro思考モード3時間分)、問題の総数(約4000問)、そして大量のLean証明を提示した。モデル自体は依然非公開で、発表では「内部モデル」とだけ呼ばれ、責任を持って公開を進めていると説明されている。約4000問のうちどれだけが未解決で、途中で放棄されたものがどれかは、公開された資料からは分からない。
数学界はこうした生産量について以前から懸念を示していた。テレンス・タオは今年8月と9月の2回、この問題について公に発言しており、AIによって証明の生産量が人間のレビュー能力を大きく上回り、良質な難問も急速に「採掘」され尽くしてしまう恐れがあると指摘している。722本の論文が一度に公開された今、レビューの負担が最終的に誰にのしかかるのか、答えを示した人はまだいない。
今後の予定
OpenAIは、数学界がAIが生成した結果を理解し受け止める助けとなるよう、関連するワークショップや専門プログラムに資金を提供するとしている。これらの論文が正式な学術誌に掲載され得るか、著者表示をどう扱うかについて、同社は具体的な方針を示していない。外部の数学者による1本ごとの検証結果も、まだ公表されていない。
参考資料：OpenAI公式ブログ、Interesting Engineering、CocoLoop、Unite.AI。論文数、問題総数、計算コストの基準はOpenAIの公開情報に基づき、諮問グループの提言内容はIASグループの公開文書に基づく。