オリンピック級の幾何学AIシステム AlphaGeometry
(deepmind.google)- 国際数学オリンピックがAIの数学的推論の試金石となるなか、AlphaGeometry は幾何問題30問中25問を制限時間内に解き、人間の金メダリスト平均25.9問に迫った
- 中核は ニューラルネットワーク言語モデル とルールベースの 記号推論エンジン の結合で、直感的な構成提案と形式論理による検証を1つのループ内で処理する
- 人間の実演なしに作成した 1億件のユニークな合成例 が学習のボトルネックを減らし、このうち900万件は証明に必要な補助構成を含む
- すべてのオリンピック解答はコンピュータで検証されており、Evan Chen は出力が機械検証可能でありながら人間にも読みやすく、生徒たちが使う古典幾何の規則に従っていると評価した
- IMOの1回分では通常6問中2問だけが幾何であるため適用範囲は限定されるが、幾何の性能だけで2000年と2015年のIMO銅メダル基準を超えられる初のAIモデルとなった
IMO幾何ベンチマークでの成果
- Nature で公開された AlphaGeometry は、複雑な幾何問題を人間のオリンピック金メダリストに近い水準で解く
- ベンチマークは2000年から2022年までのオリンピックから選ばれた IMO-AG-30 幾何問題30問で構成される
- AlphaGeometry: 制限時間内に25問を解決
- 既存の最高手法である Wu’s method: 10問を解決
- 人間の金メダリスト平均: 25.9問を解決
- Google DeepMind は AlphaGeometry のコードとモデル をオープンソースで公開した
ニューラル・シンボリックシステムの構造
- AlphaGeometry は ニューラル・シンボリックシステム であり、ニューラルネットワーク言語モデルと記号推論エンジンが協調して複雑な幾何定理の証明を見つける
- 言語モデルはデータから一般的なパターンと関係を素早く識別し、有用である可能性の高い構成を予測する
- ただし厳密な推論や判断理由の説明能力は不足することがある
- 記号推論エンジンは形式論理と明確な規則に従って結論へ到達する
- 説明可能で合理的だが、大きな問題を単独で扱う場合は遅く柔軟性が低いことがある
- 2つの構成要素を組み合わせることで、言語モデルが新しい点・線・円といった 補助構成要素 を提案し、推論エンジンがそれを基に図形についての追加の結論を導く
補助構成を見つける解法ループ
- オリンピック幾何問題は、与えられた図形だけではそのまま解けず、解法に必要な新しい幾何構成要素を追加しなければならない場合がある
- AlphaGeometry の解法過程は、記号推論と言語モデルの提案が交互に働く方式である
- 与えられた図形と定理の前提から、記号推論エンジンが新しい命題を導出する
- 解答が見つからない、またはこれ以上新しい命題を作れなくなると、言語モデルが有用である可能性の高い補助構成要素を1つ追加する
- 追加された構成要素が推論エンジンに新たな経路を開き、解答が見つかるまでこの過程が繰り返される
- 2015年国際数学オリンピック第3問で、AlphaGeometry の解答は 109の論理ステップ で構成された
1億件の合成データ生成
- 幾何学は空間・距離・形・相対位置の理解に基づき、芸術、建築、工学など多くの分野の基礎となる
- AlphaGeometry の合成データ生成方式は、人が図形を見ながら既存知識を用いて新しい幾何学的性質や関係を見つける過程を大規模に模倣する
- システムは高度に並列化された計算によって 10億個のランダムな図形 を生成する
- 各図形で点と線のあらゆる関係を徹底的に導出する
- 各図形に含まれるすべての証明を見つける
- その証明に到達するためにどの追加構成要素が必要かを逆向きに追跡する
- この過程は symbolic deduction and traceback と呼ばれる
- 膨大なデータプールは類似例を除外するようフィルタリングされ、最終的に難易度の異なる 1億件のユニークな学習例 となる
- このうち900万件は補助構成要素が追加されたケースである
- 言語モデルは、補助構成が証明につながる例を大量に学習することで、オリンピック問題でも新しい構成を提案できる
検証可能性と適用の限界
- AlphaGeometry が提供したすべてのオリンピック問題の解答は コンピュータで確認・検証 されている
- 結果は以前のAI手法およびオリンピックにおける人間の成績と比較された
- 数学コーチであり元オリンピック金メダリストでもある Evan Chen が一部の解答を評価した
- AlphaGeometry の出力は検証可能で整っている
- 過去の証明ベース競技問題に対するAIの解答は、正しいこともあれば誤っていることもあり、人による確認が必要な場合があった
- AlphaGeometry の解答は機械検証可能な構造を持ちながら、人間にも読める
- 座標系で膨大な代数計算を力押しするのではなく、角度や相似三角形のような 古典幾何の規則 を生徒のように使う
- IMOの1回分は6問で構成され、通常そのうち2問だけが幾何に集中している
- したがって AlphaGeometry は1回分の問題のおよそ3分の1にしか適用できない
- それでも幾何能力だけで2000年と2015年のIMO銅メダル基準を通過できる初のAIモデルとなった
数学推論AIへの拡張
- AlphaGeometry は、AIが 論理的に推論 し、新しい知識を発見・検証する能力を高めつつあることを示している
- オリンピック級の幾何問題を解くことは、より深い数学的推論と、より高度な汎用AIシステムへ向かう重要なマイルストーンである
- 大規模な合成データでAIをゼロから学習させるアプローチは、数学を超えて科学やAIにおける新しい知識発見の方法に影響を与える可能性がある
- AlphaGeometry は Google DeepMind と Google Research の数学推論AIの取り組みの流れの上にある
- 純粋数学の美しさを新しい方法で探る
- Minerva で言語モデルを活用して数学・科学問題を解く
- FunSearch は大規模言語モデルを使って数理科学の公開問題で初の発見を実現した
- 長期目標は、複数の数学分野にまたがって一般化し、汎用AIシステムに必要な洗練された問題解決と推論を発展させ、人類の知識の境界を広げるAIシステムを作ることである
1件のコメント
Hacker Newsの意見
IMOのような大会の問題作成者だった立場から、この論文は非常に興味深く読んだ。同時に、AI、つまり賢い知識インデックスと推論方式インデックスに最初に崩される分野は幾何に違いなかったと思う
数学オリンピックの分野の中で、幾何の問題は概して最も「機械的」だ。問題を座標、たとえばXY座標や複素平面で表現できれば、コンピュータが解を見つけるために使える有限のステップの集合が生まれる。もちろんIMOの現場では、時間制限と人間のミスが実用性を阻む。以前はこうした方法で、自分が作った幾何問題や予想の証明をWolframAlphaで検証していた
代数、特に不等式も似ていて、強力な計算を押し通せば答えが出ることが多い
知的システムが本当に発展する様子を見たい分野は、整数論と組合せ論だ。探索空間がはるかに複雑で、何かが不可能であることの証明を求める場合が多い。こうした問題は総当たり計算では解きにくい
幾何が最初だろうという点には同意する。ここで見た限りでは、代数幾何、ベクトル、複素数による解法に依存するという意味での「総当たり」ではないが、「興味深い」補助作図を片っ端から探すという意味では総当たり探索に近い
幾何はずっと自分の最悪の科目だったが、正しい作図が与えられると問題がずっと簡単になると感じていた。ただ、その作図を素早く思いつく直感は身につかなかった。このAIにもそうした直感があるようには見えないが、はるかに速く大量に出せる。垂線、平行線、二等分線のように作れる候補は結局限られており、角度と比をすべて展開してみたり、点のべき乗を試したりする形で、かなり機械的に評価できる
非常に印象的だが、「エンジン対AI」という意味では、DeepMind:Kasparov::AlphaGeo:Terry Taoのように見える
代数が次である可能性が高いという点にも同意する。幾何と同じく、たいていは賢い置換を1つ、2つ、3つ見つければよく、選択肢は限られている
一部の組合せ論の問題も、この探索戦略に合うかもしれない。たとえば、同じ対象を2通りの方法で数えるような問題だ。ただしそれはさらに遠い橋であり、全体の問題の一部しか捉えられない
整数論が、満点42点に到達する前の最後のフロンティアになりそうだ
解けることを検証した後、最終的な問題セットに入れる特定の問題をどう選ぶのかも気になる。投票なのか、別の評価方法なのか？
誰かが合成幾何をアドベンチャーゲームにすべきだ。Leanより単純な証明記述言語を使えるし、視覚的にも見栄えよく作れる
論文をきちんと読めているなら、これは本物の仕事に見える。先月DeepMindが未解決の数学研究問題を解いたと誤って宣伝していたAI数学論文より、はるかに正当性がある。それでも、その構造が一般に考えられている自動推論/知能とどれほど違うかはかなり目立つ
Transformerを数百万個の初等幾何の定理で学習させ、証明を総当たり探索するのに使う、と理解した。初等幾何という文脈のため、構造は必然的に初等的で、真/偽を記号的に容易に判定できる。総当たり探索が失敗すると、中点の追加のような補助的な幾何作図をランダムに加え、その追加材料で探索できるかを見る方式だと思った
編集: Imnimoの訂正の通り、私は逆に理解していた。総当たり探索は純粋な総当たり探索で、Transformerはどの補助作図を追加するかを予測するのに使われる
また、ブログ記事にはないが、実際の問題文も修正/脚色される必要があった。たとえば原文の「三角形ABCの高さをAH1、BH2、CH3とする…」のような文は、「ABCを三角形とする。AIが角BACの二等分線であり、CIが角ACBの二等分線となるように点Iを定義するとする…」のように、はるかに明示的な定義の列挙に変わり、最後は「T1I=IZを証明せよ」という形になる
説明された過程は人間が使う過程とまったく同じだ。役に立ちそうなものを推測し、細部を機械的に解いてみる。行き詰まったら別の推測をする。結局は木を探索するのに似ている
人々はすでに1955年にこの過程を見いだし、定理を証明できる動作プロトタイプも作っていた: https://en.wikipedia.org/wiki/Logic_Theorist 重要なのは良いヒューリスティックを使うことにかかっている。ニューラルネットワークはデータからヒューリスティックを引き出せるので、ここで意味がある
「自動推論」の一般的な考え方を何だと見ているのか気になる。どんな問題でも一回の線形パスで解く魔法の装置なのか？
大学の数学科に入ってから、ようやく正しいやり方を学び、楽しめるようになった
この分野はまだ初期段階で、未完の仕事が多く見える。探索部分は小さなニューラルネットに置き換えるべきで、推論部分は難しくなく、大きく改善する必要もなさそうだ
いまは自己対局で性能を上げる時点だ。平面幾何の問題で、証明すべき結論を図形の一つの点、条件を別の点と見なし、2人のプレイヤーが互いに向かってできるだけ移動しながらデータを共有させることができる。この過程で各プレイヤーの寄与を囲碁の勝敗計算になぞらえて、性能改善に使える
この特定のモデルが一般化可能に見えるわけではないが、ニューラル・シンボリックアプローチは非常に有望に見える
現在の機械学習の大半である、ますます強力になる「システム1」ツールを、論理的な証明生成のような構造化された「システム2」ツールと接続する方式だ。システム2は計画を立て、出力の真実性や価値を確認できる
システム2が行き詰まるまで進め、行き詰まったらシステム1が状態空間のどの部分を次に確認するかについて直感的な推測を提供する
ここでは、コンピュータで証明を生成できる点を活用して1億個の証明データセットを作り、スケーラブルな自己教師あり学習を可能にした。記号領域はこのようなデータ生成をよく許容する形に見える。個々のインスタンスの価値は低くても、集まれば有用な事前学習が可能かもしれない
こうした要素を組み合わせると、かなり遠くまで行けるアプローチだ
重要なマイルストーンは、特定の形式/記号領域に依存しなければならない必要から脱し、その領域で学んだ技術を一般化できる事前学習システムを作ることだ
また、適用可能な領域内では、現在のAIの流れで「幻覚」と呼ばれる根本問題の一つを完全に解決する。ただし、その解決は正確性を証明する非AIシステムがあるから可能になる
大枠ではこのアプローチはそれほど新しくない。生化学ではAIで候補分子を見つけ、物理実験で検証する方式が使われてきた
組合せゲームAIも、AIを昔ながらのモンテカルロ探索への入力として使ってきた
論文とともにコードと重みを公開してくれた点がありがたい。私の記憶する限り、実行可能な推論コードとチェックポイントを公開した有名なDeepMind論文は今回が初めてだ。もっと早い事例があるなら訂正してほしい
まだ公開された学習セットや学習コード例は見当たらないが、それでも他の研究者がその上に積み上げられる何かを提供したという点で良い前進だ。結局、それが学術論文の目的でもある
私が間違っていなければt5モデルを使っているのか？ 少なくともSentencePiece t5語彙を使っているようだ
このモデルの学習にGPU時間をどれだけ使ったのか、どの学習パラメータを使ったのかも気になる
誤解しないでほしい。このシステムは魅力的で、応用工学がどのようなものであるべきかを示している。ただ、学習の詳細、初期データ、合成データの生成方法をもっと知りたい
言語モデルが有用な作図をどれくらい頻繁に生み出すのか、とても気になる。明らかにランダムよりはましだろうが、良いものを見つけるまで何千個もの作図を投げているのか、それとも人間の専門家に近い割合で有用な提案を出しているのかは分からない
論文では「言語モデルのデコーディング過程は、k 個の代替補助作図を記述する k 個の異なるシーケンスを返すため、各ビームのスコアを価値関数として用い、この k 個の選択肢に対してビーム探索を行う。この設定はビーム間の並列化が非常に容易で、並列計算リソースがある場合に大きく高速化される。実験ではビームサイズ k=512、最大反復回数 16、各ノードの分岐係数、すなわちデコーディングのバッチサイズ 32 を使用する」としている
ただ、512 と 16 が提案された総作図数にどう換算されるのか、完全には理解できていない。ビームサイズと最大反復を取り除いても性能はある程度しか低下しないとも述べている。これは、モデルが実際に有用な作図を上位にかなりうまく持ってきていて、最も難しい問題でだけ何千個も必要になる、という意味なのだろうか？
それでも試しにまとめるなら 262,144 だが、文字どおりに受け取るべきではない
デコーディング関数の出力はトークンで、おおよそ単語の 3/4 程度だが、ここでは 1 単語としておこう
出力トークン 1 つあたりに考慮されるトークン数は
beam_size * branching_factor * max_iterations = 512 * 32 * 16 = 262,144になるサンプル解法の単語数を数えればよい: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
解法の総トークン数は 2289 個で、考慮された総トークン数は
262,144 * 2289 = 600,047,616個になる無理やりな計算として、「考慮した解法数」を総考慮トークン数 / 解法の総トークン数と置くと 262,144 になる。各反復ステップで見たトークン数と同じ値なので、一応つじつまは合う
使われた Transformer が小さい点が興味深い。論文によると Meliad ライブラリのデフォルト設定で学習しており、12 層、埋め込み次元 1,024、アテンションヘッド 8 個、ReLU 活性化を使う次元 4,096 のアテンション間の密結合層を持つ
入力と出力ヘッドの埋め込み層を除くと、Transformer 全体は1億5,100万個のパラメータを持つ。カスタムトークナイザーは SentencePiece の ‘word’ モードで学習し、語彙サイズは 757。最大コンテキスト長は 1,024 トークンに制限し、T5 式の相対位置埋め込みを使用している。シーケンスの 90% 以上が長さ 200 未満なので、シーケンスパッキングも使用している
私にとって本当に新しく知った点は、以前の最高水準システムでもこうした問題を10問も解けていたということだ。平面幾何の問題に対する決定アルゴリズムがあるとは聞いていたが、実用的なアルゴリズムだとは知らなかった。探してみると参考資料として http://www.mmrc.iss.ac.cn/~xgao/paper/book-area.pdf が出てくる
この手の成果物はたいてい「人間の証明らしくない」という感じなので疑う用意をしていたが、Evan Chen が実際にすっきりしていて人間が読める証明だと言っているのを見て考えを改めた
Evan Chen はオリンピアード数学コミュニティの有名人で、有名なオリンピアード幾何の本の著者でもあるので[1]、今回は機械が IMO 問題の一部を実際に攻略したことを認めるべきだろう
[1]: https://web.evanchen.cc/geombook.html
それでも O2 が九点円上にあるというアイデアは正しい
編集: 前言を撤回する。有向角[2]を使っているようで、それならその文は正しい
[1]: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
[2]: https://web.evanchen.cc/handouts/Directed-Angles/Directed-An...
関連して https://www.nytimes.com/2024/01/17/science/ai-computers-math... も読む価値があります
https://news.ycombinator.com/item?id=39030186 経由で来たもので、そのスレッドはこちらにマージされる予定です
関連: https://aimoprize.com/
IMOで優れた成果を出すモデルに与えられる1,000万ドルの賞金です