数学界で、OpenAIによるAI生成の数学論文719本をどこまで信用できるのかをめぐり、疑問の声が強まっている。きっかけは、同社が先に公表したナビエ–ストークス方程式の証明について、新たな論文が「論文本文と形式検証用のLeanコードが一致していない」と指摘したことだ。
重要ポイント
- OpenAIは当初722本としていたAI生成数学論文カタログから、符号ミスが見つかった3本を撤回し、現在は719本となっている。
- 英国拠点の数学者3人が、ナビエ–ストークス証明について、論文本文とLeanコードが食い違う箇所を2カ所特定した。
- 著者たちは証明そのものが「誤り」とは断じていないが、「機械による形式検証は査読の代わりにはならない」と警鐘を鳴らしている。
OpenAIの数学論文公開
OpenAIは10月6日にこのコレクションを公開した。木曜に公表された調査レポートは、同社の取り組みが、独立した数学者パネルがAI研究機関向けにまとめたガイドラインから逸脱していると指摘した。カタログは当初722本でスタートしたが、OpenAIはその翌日に3本を撤回。1本の論文で符号の誤りにより議論が破綻し、その議論に依拠していた2本も連鎖的に成り立たなくなったためだ。
これらのガイドラインは、9人で構成されるMathematics and Artificial Intelligence諮問グループが9月29日に公表したもので、冒頭で「高度な数学問題をプロプライエタリな（非公開の）モデルでテストすることを控えるように」とAI研究機関に要請している。OpenAIのリポジトリによると、今回の論文群は、未公開の社内モデルを未解決問題に適用して得られた結果をまとめたものだという。
モデルの思考過程をまとめた説明が付いているのは全体のうち10件にとどまり、トップレベルの結果の約42%のみがLeanで形式化されている。Leanは、証明をコードとして記述し、コンピュータが論理的整合性を検証できるようにするプログラミング言語だ。
関連記事: AnthropicのCEO年収はいくらか──IPO目論見書が示す報酬実態
ナビエ–ストークス証明の齟齬
キングス・カレッジ・ロンドンのアレクサンダー・バストゥーニス、ケンブリッジ大学のファビアン・チルチェッリとアンデルス・ハンセンの3氏は、OpenAIが9月に成果として公表したナビエ–ストークス方程式の証明を精査した。その結果、論文本文の議論とLeanコードの間で2カ所に食い違いがあると報告している。うち1カ所では、コードが証明している評価は、論文中で主張されているものよりも弱い内容にとどまっていた。
著者らは、書かれた証明が正しいかどうか自体については判断を差し控えている。問題提起の焦点はもっと限定的だ。彼らによれば、Leanは「最終的な定理が成り立つかどうか」は確認できる一方、読者が目にする中間の議論ステップまで健全かどうかを保証するものではない。そのため、この種の証明であっても、人間による査読プロセスは依然として不可欠だと主張する。
フィールズ賞受賞者であるテレンス・タオは、10月6日付の投稿で、問題が「AIプロンプター」によって解かれていることへの懸念を記した。彼の言う「AIプロンプター」とは、モデルからの出力を十分に理解できておらず、質問に答えたり、自ら講演で説明したりできない人々を指す。諮問グループのメンバーでハーバード大学教授のメラニー・マチェット・ウッドも、こうした成果は公開された時点では「誰もきちんと理解していない」と述べ、「ここからが本当の仕事の始まりだ」とコメントしている。
OpenAI証明をめぐる論争
同諮問グループは、OpenAIがどの程度ガイドラインに沿って行動したかを最終的に評価できるのは、広範な数学コミュニティしかないとの立場だ。今回の精査は、すでに緊張が高まっていた中で行われている。OpenAIがナビエ–ストークス方程式の結果を発表したのは9月8日で、これがニューヨーク大学の数学者トリスタン・バックマスターとの貢献度をめぐる対立を引き起こした。そのわずか3日後には、25人のフィールズ賞受賞者が連名で声明を発表し、大量生産されるAI生成の数学結果が分野に悪影響を与えかねないと警鐘を鳴らした。
