OpenAIは10月6日、社内のフロンティアモデルが生み出した数学の研究成果をまとめて公開した。成果物はGitHubリポジトリ「openai/math」に置かれ、論文のPDFとソース、定理証明支援系Leanによる形式証明、モデルの推論過程の要約が含まれる。公開の経緯と方針はOpenAIの発表「Sharing AI progress in mathematics」で説明されている。
リポジトリに収められた論文は722本で、関連する論文を束ねた「ファミリー」単位では372件になる。ファミリーは主結果とその系、補助的な議論、別証明などをまとめたもので、数学の分野ごとに分類されている。評価の過程でモデルに与えた問題はおよそ4,000問あり、そこから成果をファミリーと論文に集約し、一定の重要度を満たすものだけを残した。1件あたりの計算量は、ChatGPT Proの思考時間に換算して平均約3時間だという。
形式証明はすべての論文に付いているわけではない。リポジトリの形式化カタログに主結果のLean証明が登録されている論文は、10月7日時点で162本と全体の2割強にとどまる。形式化された結果には、第三者が手元で検証をやり直すための「Comparator」用の設定と手順も添えられており、Leanの環境があれば主定理の宣言と証明の対応を自分で確かめられる。OpenAI自身も、形式化されていない結果には問題が含まれうると明記し、見つかれば速やかに修正するとしている。修正は新しいバージョンとして記録し、以前の版も閲覧できる状態で残す。ライセンスはApache 2.0。
推論過程の要約が公開されたのは10ファミリーで、円周率πの無理数度、Mahler予想、算術級数に関する準多項式の上界、標数2におけるKaplanskyの直接有限性予想、希釈スピングラスのMézard–Parisi公式、量子ハイゼンベルク強磁性体の自発磁化、自由群因子の同型問題、3次元相対論的Vlasov–Maxwell系などを扱う。大半の結果は同じ手順で得られたが、リーマンゼータ関数の零点を含まない領域（Re(s) > 11/12）と、CMアーベル多様体に対するホッジ予想の証明は例外扱いとされ、前者は読みやすさのために人間が文章を編集したと注記されている。
9月の「100件超」が722本の論文として出てきた
OpenAIは9月21日、米プリンストン高等研究所（IAS）を拠点とする独立諮問委員会「Advisory Group on Mathematics and Artificial Intelligence」の設立を発表した際、社内モデルが100件以上の未解決問題を解いたと述べていた。ただしその時点で詳細を示したのはナビエ–ストークス方程式の1件だけで、残りは分野も証明の有無も明かされていなかった。今回の公開は、その中身を論文単位で外に出したもので、規模は372ファミリー・722本まで膨らんでいる。
8月1日に「Astra」の内部版による10件の成果を発表したときと比べると、量だけでなく計算量の示し方も変わった。8月は10問の解決に使ったトークン量をSol APIの料金換算で約2,000ドルと説明していたが、今回は1件あたりChatGPT Proで約3時間という、一般のユーザーが体感しやすい単位で示している。発表文の「社内フロンティアモデル」という語は9月8日のナビエ–ストークス解決の発表ページにリンクされており、8月28日から学習が続く未公開モデルの系統を指す。OpenAIはこのモデルについて、科学者が直接使えるよう責任ある形での公開を進めているとしている。
諮問委員会の提言に沿った公開手順
公開の方法は、諮問委員会の助言と、同委員会が9月29日に出した公開に関する提言をもとに決めたという。論文ごとにBibTeXの引用情報を用意し、改訂履歴を保存する運用はその反映だ。9月11日にフィールズ賞受賞者25人が連名で出した声明は、検証が追いつかない速度でのAI生成数学の公表や、帰属表示の曖昧さを問題にしていた。今回の形式は、少なくとも引用と版管理の面ではその指摘に応えている。GitHubは暫定的な置き場という位置づけで、OpenAIは委員会の指針を満たすコミュニティ運営の公開先を引き続き検討している。
あわせてOpenAIは、AIが出した主要な結果を数学者が理解するためのワークショップや会議、特別プログラムに資金を出す方針も示した。722本という量は、人間の査読者が1本ずつ確認する通常の流れでは短期間に消化できない。Leanで機械的に検証できる162本と、それ以外の560本では信頼性の担保の仕方が異なり、後者については外部の数学者による検証がどこまで進むかが、今回の成果の評価を左右する。
