OpenAI は日本時間 10 月 7 日朝、まだ公開していない社内のモデルが書いた数学の論文 722 本を、GitHub の公開リポジトリ openai/math にまとめて出した。論文は 372 のファミリー (関連する論文のまとまり) に分けられ、数学の分野ごとに整理されている。
数学の新しい結果を、人ではなくモデルが大量に生み出し、それを誰でも読める場所に置いた。発見が AI の側から届くようになると、人が学ぶことと、確かめる仕事の中身が変わり始める。
4,000 問から 722 本へ
リポジトリの説明によると、OpenAI はモデル開発の一環として、未解決の研究問題でモデルを試してきた。既存の数学の評価では成績が頭打ちになったため、評価の範囲を広げたという。
- 評価の中でモデルに出した問題は、およそ 4,000 問
- 結果の大半は同じ手順で得たもので、1 件あたり平均 3 時間、ChatGPT Pro の推論時間を使った
- 出力をまとめ、一定の重要度を求めた結果が、722 本・372 ファミリーという目録になった
例外も明記されている。リーマンのゼータ関数の零点が現れない領域についての仕事と、CM アーベル多様体に対するホッジ予想の証明は、この固定の手順の外で得た。ゼータ関数の一件は、読みやすくするために人が文章を手直ししたという。
モデルの推論の要約も 10 件ついている。円周率 π の無理数度、マーラー予想、標数 2 におけるカプランスキーの直有限性予想への反例などだ。
形式証明がついたのは 162 本
OpenAI 自身が、結果の検証の段階はまちまちだと書いている。すべての論文に Lean (証明を機械で一行ずつ検査できる言語) の形式証明がついているわけではない。主結果の形式証明がついた論文は、目録の上で 162 本だ。
形式証明がない結果について、リポジトリは「問題を含む可能性がある」と認め、見つかれば速やかに直すとしている。修正は新しい版として記録し、前の版も残す。ライセンスは Apache 2.0 で、読むことも検証し直すことも開かれている。
OpenAI の X 投稿によれば、公開にあたっては高等研究所 (IAS) の「数学と AI に関する独立諮問グループ」と協議してきたという。
だから、この公開を「AI が未解決問題を大量に解いた」と一言でまとめるのは早い。正確には、モデルが書いた主張が大量に机に載り、そのうち一部は機械で検査済み、残りは人と機械の検証を待っている、という状態だ。
発見が届く側の仕事は、確かめることに寄っていく
新しい結果を生む速さが上がるほど、価値が増すのは、それを確かめる力のほうだ。Lean で書かれた証明を検査にかける、論文の主張が先行研究とどう重なるかを読む、どの結果が本当に重要かを見分ける。どれもいま人の手が要る作業で、今回のリポジトリはまさにその作業を外に向けて開いた。
数学を専門にしない人にとっても、似た変化はやって来る。AI が答えを先に出す場面が増えると、学ぶことの重心は、自分で答えを出すことから、出てきた答えを検査して使いどころを決めることへ寄っていく。
ただし、確かめる側に回るのは簡単ではない。リポジトリの Lean ライブラリは一つの大きな塊で、全体をまとめてコンパイルすると環境によっては失敗するため、少しずつ扱うよう案内されている。論文を読むにも、分野ごとの専門知識が要る。検証が開かれていることと、誰でも検証できることは別の話だ。
次に見ておくこと
確認できる次の一点は、openai/math の Lean 形式証明の目録 (formalization.yaml) の本数だ。OpenAI は形式証明が得られ次第リポジトリを更新するとしている。次の版で 162 本からどこまで増えるか、そして訂正の版が出るかどうかが、この 722 本の重みを決めていく。
ことば
- Lean — 数学の証明を一行ずつ機械に検査させるための言語と道具。人が読み落とす飛躍もコンピューターが止めるため、AI が書いた証明を信頼してよいかを確かめる手段として注目が集まっている。
- 形式証明 — 自然言語ではなく、機械が検査できる厳密な形で書かれた証明。書き起こすのに手間がかかる分、検査を通れば論理の誤りがないと言える。今回の 722 本のうち、主結果にこれがついたものは 162 本。
- ファミリー — 今回の目録の単位で、主な結果とその別証明・系・関連する議論をひとまとめにしたもの。1 ファミリーに複数の論文が入るため、論文の本数と結果の数は一致しない。
答えが先に届く時代に、あなたは何を自分で確かめられるようにしておきたいだろうか？
