OpenAI、内部フロンティアモデルの数学成果をLean形式化付きでGitHub公開

OpenAIは、内部のフロンティアモデルが生み出した数学の未解決問題に関する幅広い新成果を、Leanによる証明の形式化や研究の詳細とともにGitHubリポジトリで公開しました。平均的な結果1件あたりの計算量は、ChatGPT Proでおよそ3時間考え続けた場合に相当するとしています。

何が新しいか

OpenAIは今回、成果の公開方法をInstitute for Advanced Studyの独立諮問グループ「Advisory Group on Mathematics and Artificial Intelligence」と協議し、その助言と公開勧告を取り入れました。成果はGitHubリポジトリで公開し、論文の改訂・引用に関するプロトコルも掲載しています。OpenAIは、諮問グループのガイドラインを満たすコミュニティ運営の別の公開先も引き続き検討するとしています。

リポジトリで確認できる内容

項目	内容
数学の成果	内部フロンティアモデルが生成した新たな結果
Lean形式化	多くの証明を形式化済み。追加の形式化が得られ次第更新
モデルの推論要約	10件
計算量の推定	ChatGPTのPro利用量換算。平均的な結果で約3時間分のChatGPT Pro thinking
試行問題数	試行した問題数の統計
論文関連	改訂・引用のプロトコル

Leanは、数学的証明をコンピューターで検証できるプログラミング言語です。

背景と今後

OpenAIは、科学的な透明性と開放性を高める目的で、結果の取得方法に関する追加情報を公開したと説明しています。今後の公開では引用、数学的な説明、結果の提示を改善し、コミュニティのフィードバックを基に重要な科学的成果の開示基準を更新するとしています。

またOpenAIは、AIが生み出した主要な成果の理解を目的とするワークショップ、会議、特別プログラムに資金を提供する予定で、詳細は近く発表するとしています。今回の成果を生み出したモデルについても、責任ある形での公開に取り組んでいると述べています。