まるで頭の上にピアノを落としておいて、その楽譜をレビューしろと言わんばかりの、学術界におけるまさにそれ。OpenAIは今週、700以上の原稿にまたがる約400件のAI生成数学的成果を公開した。数学界の反応は「驚愕」から「純粋な狂気」まで様々だった――そしてそれらはまだ丁寧な方だった。

そのコレクションは組み合わせ論、幾何学のいくつかの分野、数論、理論計算機科学、代数学、トポロジー、確率論と統計力学、数理物理学に及ぶ。あまりに膨大なので、OpenAIは広大なGitHubリポジトリのナビゲート方法に関するガイダンスを公開せざるを得なかった。これは、今火をつけたばかりの建物の地図を渡すようなものだ。

「要約のリスト全体をざっと見るだけで圧倒される」とコネチカット大学の数学教授アルバロ・ロザノ＝ロブレドは語った。何人かの数学者はThe Vergeに対し、約40ページの目次と要約を単に読み通すだけで1時間近くかかったと話した。自宅でスコアを付けている人のために言えば、メニューを読むだけで1時間である。

何百もの原稿の中には、Leanによる形式化が散りばめられている。Leanは計算による検証を可能にするプログラミング言語兼証明支援系だ。これらの形式化は、OpenAIの以前の数学的主張のいくつかを評価する上で極めて重要な役割を果たしており、研究者たちは、たとえその背後にある議論を完全に理解していなくても、主張が論理的に正しいという自信を得ることができる――これは、割り算が何かを知らずに電卓を信頼するようなものだ。

しかし、各結果がどの程度検証されているかは大きく異なっていた。GitHub上でOpenAIは、結果は「検証の異なる段階にあり」、「多くのかなりの数の原稿が形式化されているが、すべてではない」と認めた。執筆時点で、コレクション内の原稿の半数未満しか正式に記述されていないようだ。OpenAIは719件の原稿のうちトップラインの結果は300件のみが形式化されたと述べ――約42パーセント――、「入手次第、より多くの形式化でリポジトリを更新する」とした。つまり、数学的黙示録のおよそ58パーセントは未検証のままである。ぐっすりお休みください。

何人かの数学者はThe Vergeに対し、特に結果の数が膨大であることを考えると、形式化の欠如について不満を述べた。Leanコードが結果に付随している場合でも、評価は即座には行えない。研究者は、形式化が実際に結果の主張を証明しているかどうかを確認しなければならない――これもまた時間のかかるプロセスだ。論文を掘り下げた何人かは、計算機で検証可能な証明が提供されている場合でも、その品質は一貫性がなく、検証されたステートメントが付随する原稿の主張に必ずしもきちんと対応しているようには見えないと述べた。

インペリアル・カレッジ・ロンドンの数学教授ケビン・バザードは、自身の専門分野である代数的整数論において多数の定理を特定したが、そのうちすぐに「目立った」のは約6つだけだったと述べた。それらのうちLeanで正式に検証されたものはほとんど、あるいは全くないようだ。「したがって、私はおそらく正しくないスロップを読むか、他の誰かが同じことをするのを待つか、誰かがそれらを形式化して結果が正しいと断言できるようになるまで待つしかない。」バザードの懸念は他の多くの研究者にも共有されており、彼らはおそらく今週他にやるべきことがあったのだろう。

バザードはAIの「スロップ」――低品質で頻繁に誤りを含むAI生成素材の略称で、オンラインや現実世界、学術論文にまで増え続けている――を心配する唯一の人物ではなかった。他の分野と同様に、数学者たちはThe Vergeに対し、近年ChatGPTやClaudeのようなツールで生成されたそのような素材が急増しているのを目にしていると語った。その多くは混乱を招き、読みにくく、主題への理解をほとんど示していない。特に他の研究者へのクレジットに関してはお粗末である。OpenAIの以前の数学的記述は専門家から広く批判された。