米国のシモンズ財団 (Simons Foundation) は10月15日、AI が数学の研究を急速に変えるなかで、数学者がその変化に向き合うための新しい取り組みを発表した。財団と Anthropic、OpenAI の3者で、資金と計算資源をあわせて1500万ドルを出す。
OpenAI はこのうち500万ドルを拠出すると自社のページで明らかにした。目的は、AI が出した数学の結果を数学者が検証し、理解し、その上に研究を積めるようにすることだ。AI の答えを、正しいかどうかに加えて人が分かるかどうかで受け止め直す動きで、数学はその最前線にいる。
速報では OpenAI の拠出の骨子だけを伝えた。ここでは、なぜ AI の会社がこの資金を出すのか、その背景にある数学界からの求めを見ていく。
1500万ドルで何をするか
財団の発表によると、資金は財団が管理し、公募も含めて配分する。支援の対象は、次のようなワークショップや取り組みだ。
- 最近の AI の助けを借りた成果を評価する
- 新しい道具を学び、使う
- それぞれの見方を持ち寄る
- AI の使い方について、共同体としての基準をつくる
OpenAI の説明では、資金はワークショップ、学会、特別プログラムに充てられる。加えて Anthropic と OpenAI は、財団が支援する研究者に AI の道具と計算資源を提供する。その範囲は数学にとどまらず、基礎科学に広がる。
各社の負担の内訳は、財団の発表には書かれていない。公募の時期や応募の条件もまだ出ていない。
10月6日に公開された AI の数学の成果
この資金の手前には、10月6日に OpenAI が公開した数学の成果がある。社内の最先端モデルが出した幅広い新しい結果を、GitHub のリポジトリにまとめて載せた。多くの証明は Lean で形式化して添え、モデルの推論の要約10件や、使った計算量の見積もりも公開した。1つの結果にかかった計算は、平均で ChatGPT Pro の思考およそ3時間分だったという。
OpenAI は今回の500万ドルを、この公開分を含む AI の成果を数学者が理解するためのものだと書いている。
数学界が AI の会社に求めたこと
公開にあたって OpenAI が相談したのが、プリンストン高等研究所 (IAS) の独立した諮問グループ、Advisory Group on Mathematics and Artificial Intelligence だ。このグループは9月29日、AI が生んだ数学の責任ある公開についての提言を出していた。600件を超える数学者からの回答をもとにまとめたものだ。
提言の出発点は、数学の古くからの作法にある。論文の著者は議論を自分で理解し、正しさを確かめ、内容に責任を持つ。ところが AI は、問いを投げた人が理解も検証もできない証明を出せるようになった。そこで提言は、人の理解を伴わない成果を出す AI の研究機関に対し、理解が後から追いつくよう責任を持ち、資金を含めて大きな支援をするよう求めた。同時に、理解を育てる過程は数学の共同体が主導し、AI の研究機関が方向を決めてはならないとした。
財団のデイヴィッド・スパーゲル会長も同じ線に立つ。ツールの評価や導入、使い方の議論を引っ張るべきなのは共同体であって、どこか一つの会社や機関ではない、と発表の中で述べている。お金は AI の会社からも出るが、配分は財団が受け持つ。今回の取り組みはその形をとった。
提言は、最先端の問題を一般に公開されていない社内モデルで試すこと自体を支持しないとも明記している。OpenAI は結果を出したモデルを責任ある形で公開する準備を進めているとしており、そのモデルはまだ外部の研究者が自由に使える状態にない。
数学の外にいる私たちへ
AI の答えを自分で確かめきれない場面は、数学に限らない。契約書の要約、プログラムの修正、家計の試算でも同じことが起きる。数学の世界が選んだのは、正しさを機械で検査する道と、人が理解するまで時間と資金をかける道の両方だった。
ここには実践のコストもはっきり出ている。Lean はオープンソースの道具で誰でも試せるが、証明をその形に書き下すには、数学と道具の両方を学ぶまとまった時間が要る。そして数学者でさえ、AI が出した結果を読み解くには場と資金が必要だと言っている。確かめる側にも費用がかかる。
確認できる次の点
次に見るのは、シモンズ財団のニュースページに出る公募の案内だ。財団は公募を通じて配分するとしているが、時期と応募条件はまだ示していない。OpenAI も、AI の成果を理解するためのワークショップや学会について、近く詳しく知らせるとしている。
ことば
- Lean — 数学の証明を、コンピュータが一行ずつ検査できる形で書くためのプログラミング言語。シモンズ財団が開発を支えてきた。AI が出した証明が正しいかを、人が全部を読まずに機械で確かめる手段として使われ始めている。
- 形式化 — 自然言語で書かれた証明を、Lean のような言語で機械が検査できる形に書き直すこと。正しさの確認には強いが、なぜそれが成り立つのかという理解までは与えてくれない。
答えが正しいことと、自分がそれを分かっていることは別の話だ。AI の答えを受け取るとき、あなたはどこまでを自分で分かっておきたいだろうか？
