米オープンAI、数学成果722編を内部モデルから公開　372系統、多くはLeanで検証可能

　米オープンAIは10月6日（米国時間）、社内の最先端モデルが生み出した数学の新たな成果を公開したと発表した。GitHubのリポジトリに、722編の論文原稿を掲載した。関連する成果をまとめた372系統に分けて、数学の分野別に並べている。ライセンスはApache-2.0としている。

　成果の大半は、未公開の社内モデルが出したものだという。評価の過程で投げた問題は約4000問で、1件あたりの計算量は平均してChatGPT Proの約3時間分の思考に相当するとしている。

　数学の証明を計算機で検査できるプログラミング言語「Lean」による形式化も、多くの証明について公開した。ただし、形式化されていない成果の一部には問題が残る可能性があるとし、見つかり次第、速やかに修正すると説明している。モデルの推論過程の要約10件、計算量の見積もり、挑戦した問題数の統計も併せて載せた。形式化は今後も追加する。

　公開にあたっては、米プリンストン高等研究所（IAS）に設けられた「数学と人工知能に関する独立諮問グループ」の助言と公開勧告を参考にしたという。論文の改訂と引用の手順も定めた。あわせて、AIが出した主要な成果の理解を深めるワークショップや会議、特別プログラムに資金を出す方針で、詳細は近く明らかにするとしている。

　オープンAIは9月8日、数学のミレニアム懸賞問題の一つである「ナビエ・ストークス方程式」の証明を発表していた。9月21日には、数学者9人による独立した諮問グループの発足と、社内モデルが100件超の未解決問題を解決したことを明らかにしている。今回の公開は、このモデルによる成果を一挙に示す形となる。