722本の「原稿」が、GitHubに置かれた
10月6日、OpenAIは「Sharing AI progress in mathematics」と題した研究発表とともに、未公開の社内フロンティアモデルが生み出した数学的成果を一挙に公開した。置き場所はGitHubの「openai/math」リポジトリで、ライセンスはApache-2.0。中身は722本の原稿(マニュスクリプト)で、関連するものをまとめた372の「ファミリー」に整理されている。数論、計算複雑性、幾何学、数理物理と分野は幅広い。数学の成果としての大きさもさることながら、研究者として注目したのは、成果の「出し方」のほうだ。AIが作った数学を、数学コミュニティにどう信用してもらうか。その作法を、OpenAIが外部の助言を受けながら模索している様子が見えてくる。
助言したのは高等研究所のグループ
OpenAIは今回の公開方法について、プリンストン高等研究所に置かれた独立の「数学と人工知能に関する諮問グループ」に相談し、その公開済みの提言を参考にしたと説明している。AIが生んだ成果の公開作法を、数学者の側から整理しようとする動きがすでにあり、そこに歩み寄る形で公開を設計したということだ。具体的には、原稿の改訂と引用に関するプロトコルを定め、旧版にも引き続きアクセスできるようにしている。論文の置き場については、GitHub以外に、諮問グループの指針に合う、コミュニティ主体の置き場も探っていくという。
「Leanで検証済み」の意味と限界
信頼性の担保として前面に出ているのが、Leanによる形式化だ。Leanは、数学の証明をコンピューターで機械的に検査できるプログラミング言語で、形式化された証明は、書かれた論理の筋道に飛躍や穴があればはじめから通らない。OpenAIは、多くの証明のLean版を公開しており、今後も得られ次第追加するとしている。ただし、「多くの」であって「すべて」ではない点は押さえておきたい。さらに一般論として、Leanが保証するのは「形式化された命題が証明された」ことであり、その命題が人間の意図した定理と正確に一致しているかどうかは、別に人間が確認する必要がある。形式化の段階での取り違えは、機械検査だけでは見つからない。
透明性の「中身」を数字で見る
OpenAIは、結果に至る過程についても情報を出している。モデルの推論を要約した10件の資料、ChatGPT Proの利用に換算した計算量の見積もり、そして試行した問題の数に関する統計だ。報告によれば、評価には約4,000問が関わっており、1件の成果あたりの平均計算量は、ChatGPT Proで約3時間考えさせた分に相当するという。READMEには、既存の数学評価が飽和したため、未解決の研究問題へ評価を拡張したことも書かれている。ここで冷静に見たいのは、約4,000問と372ファミリーを単純に割って「成功率」にはできない、という点だ。1つの問題が複数の原稿につながる場合も、逆の場合もありうるからだ。試行の分母を公開したこと自体は評価できるが、その読み方には注意がいる。
再現できない、という最大の制約
一方で、検証という観点での最大の制約は明確だ。成果を生んだモデルは未公開のままで、外部の数学者が同じ手順を再現して確かめることはできない。OpenAI自身も、このモデルを責任ある形で公開すべく取り組んでいる、と述べるにとどまる。つまり現時点では、Leanで機械検査された部分は誰でも検証できるが、「どうやってその証明にたどり着いたのか」「同じ条件で別の問題でも同様の成果が出るのか」は、外からは確かめられない。
原稿の品質を、自ら課題として挙げている
もう一点、率直さが表れているのが、今後の改善項目だ。OpenAIは、将来の公開に向けて、引用の質、数学的な説明の仕方、結果の提示の仕方を改善していくと約束している。裏を返せば、現状の原稿にはこれらの点で改善の余地がある、ということだ。研究論文は、証明が正しいだけでは十分でなく、先行研究との位置づけや読み手が理解できる説明を備えて初めて、共同体の知識として使える。722本という量がある分、この質の部分が追いついているかは、数学者による個別の評価を待つほかない。
研究者として見ておきたいこと
成果の価値を最終的に決めるのは、各分野の数学者が個々の原稿をどう評価するかだ。OpenAIは、AIが出した主要な成果の理解をテーマにしたワークショップや会議、特別プログラムに資金を出す計画も示している。今回の公開で重要なのは、結果の大きさそのものより、AIが生んだ数学をコミュニティが検証・引用・批判できる形で出す「型」が作られ始めたことだ。Lean形式化の拡充、モデルの外部提供、そして独立した数学者による検証結果が揃っていくかどうかを、引き続き注視したい。