DeepMindのAI、国際数学オリンピックの問題を銀メダル水準で解く
(deepmind.google)- 高難度の数学的推論を測る代表的な試金石である IMO 2024 で、Google DeepMindのAlphaProofとAlphaGeometry 2が6問中4問を解き、AIとして初めて銀メダル圏の成績に到達
- 総点42点中 28点 を獲得し、解いた問題はいずれも満点扱い。2024年の金メダル基準である29点に1点届かない水準
- 評価はIMOの採点規則に従って数学者が実施。代数・数論はAlphaProofが、幾何はAlphaGeometry 2が担当し、異なる推論方式を組み合わせた
- 問題はまず 形式数学言語 に手作業で翻訳された。学生の競技時間が4.5時間×2回である一方、システムは1問を数分で、他の問題は最大3日かけて解いた
- 今回の結果は、数学AIが単純な計算を超えて証明探索と検証に近づいたことを示すが、形式化された入力と長い解答時間はなお重要な制約として残っている
IMO 2024で収めた銀メダル圏の成績
- Google DeepMindは、数学推論システム AlphaProof と、幾何問題解決システムの改良版 AlphaGeometry 2 を公開
- 2つのシステムは、2024年のInternational Mathematical Olympiadの6問中4問を解いた
- AlphaProof：代数2問、数論1問を解決
- AlphaGeometry 2：幾何1問を証明
- 組合せ論2問は解けなかった
- 各問題は7点満点で、総点は42点
- システムは解いた4問すべてで満点を取り、28点 を獲得
- これは2024年IMOの銀メダル圏上位に相当する
- 2024年の金メダル基準は29点で、公式大会では609人中58人が金メダル圏に到達した
- AIシステムがIMOで 銀メダリスト水準 に相当する成績を出した初の事例
評価方法と解答条件
- 問題はIMO主催者が提供した大会問題を使用
- 解答はIMOの採点規則に従って評価された
- 評価者は、IMO金メダリストでFields Medal受賞者のProf Sir Timothy Gowersと、IMO金メダルを2回受賞しIMO 2024 Problem Selection Committee議長を務めたDr Joseph Myers
- システムが問題を理解できるよう、すべての問題はまず 形式数学言語 に手作業で翻訳された
- 公式大会では、学生は4.5時間ずつの2セッションで解答を提出する
- AIシステムは1問を数分以内に解き、他の問題には最大3日を要した
- AlphaProofが解いた問題には、2024年IMOで参加者5人だけが解いた最難問が含まれる
AlphaProof：Leanベースの形式推論
- AlphaProofは、数学命題をLean形式言語で証明するよう学習するシステム
- 事前学習済み言語モデルとAlphaZero強化学習アルゴリズムを組み合わせている
- AlphaZeroはチェス、将棋、Goを自力で習得するために使われたアルゴリズム
- 形式言語を使うことで、数学的推論を含む証明の 正確性検証 が可能になる
- 従来は人間が作成した形式証明データが非常に少なく、機械学習での形式言語活用は限定的だった
- 自然言語ベースのアプローチははるかに多くのデータを利用できるが、もっともらしく見えても誤った中間推論ステップや解答を生成し得る
- DeepMindはGeminiモデルをファインチューニングし、自然言語の問題を形式命題へ自動翻訳できるようにして、さまざまな難度の形式問題ライブラリを作成
- AlphaProofは問題が与えられると解答候補を生成し、その後Lean上で可能な証明ステップを探索して、それを証明または反証する
- 発見・検証された証明は、AlphaProofの言語モデルを強化するために使われる
- この反復プロセスは、より難しい問題を解く能力を高めるために用いられる
- IMOの準備過程では、数週間にわたり数百万件の問題を証明または反証しながら学習した
- 大会中にも、問題の自己生成した変形に対する証明を強化しながら完全な解答を探す学習ループが適用された
AlphaGeometry 2：より難しい幾何問題へ拡張
- AlphaGeometry 2は、既存のAlphaGeometryを大幅に改良したバージョン
- このシステムは、ニューラルネットワークと記号推論を組み合わせた ニューロシンボリック・ハイブリッド 構造
- 言語モデルはGeminiをベースにしている
- 以前のバージョンより1桁多い合成データでゼロから学習された
- より多くのデータと改良されたモデルにより、物体の動き、角度・比率・距離の方程式を含む、より難しい幾何問題を扱えるようになった
- AlphaGeometry 2の記号エンジンは以前のバージョンより 数十倍 高速
- 新しい問題を受け取る際には、新たな知識共有メカニズムにより、異なる探索木の高度な組み合わせを活用してより複雑な問題に対応する
- 過去25年のIMO幾何問題の解決率：
- 2024年大会前の時点で、AlphaGeometry 2は過去25年間のIMO幾何問題の83%を解くことができた
- 以前のAlphaGeometryの解決率は53%だった
- IMO 2024では、Problem 4を形式化入力後19秒以内に解いた
3件のコメント
形式数学ライブラリの開発に貢献する数学者が増えるほど、高性能な数学AIを作りやすくなるでしょう。自分で Lean 証明支援系の言語で形式化した数学理論を、Lean の数学ライブラリ Mathlib に移している韓国人は、私の知る限り現在3人います。
私は昨年、Mathlib を Lean 3 から Lean 4 へ移行する作業に少し参加し、今年は Lean 4 batteries ライブラリの未解決定理の一つを証明しました。
Hacker News の意見
この発表には本当に大きな期待を抱いているが、「まず問題をシステムが理解できるように形式的数学言語へ人間が手作業で翻訳した」という一文が、どれほど多くの作業を含んでいるのかは不明確
幾何でない問題はいずれも「…であるすべての X を求めよ」という形で、定理文は「すべての X の集合が {foo} であることを示せ」という形だった
https://storage.googleapis.com/deepmind-media/DeepMind.com/B... からダウンロードできる解答だけを見る限り、翻訳段階で人間が {foo} を決めたのか、コンピュータが見つけたのかは分かりにくい。コンピュータが見つけたと信じたいが、確認できる根拠を見つけられなかった
{1,1}、P6 では2を見つけ、それぞれの場合に Lean 証明も併せて提示した人間も形式手法を直接扱うときにこうしたことはよく起きるので、研究者たちは LLM であれ他のツールであれ、最終的にはすべての翻訳を監査する必要があると判断したのだろう
ただし、この段階を可能にするためにエージェントへどのような初期形式が与えられたのかは不明確
つまり AlphaProof が何らかの形の「問題」を受け取り、「…であるすべての X を求めよ」をどう形式化したにせよ、候補定理をおそらく Lean で生成しているように思える。例えば、集合がある式 P について
{n: P(n)}の形である、というようなものかもしれない。その後、証明を探索するもし AlphaProof が {foo} を見つけたのではなく、与えられていたのだとしたら、問題を解いたと主張するのはかなり突飛に思える。それでもこの結果には非常に期待している
確かに印象的だが、IMO が言及されるときには注意点が必要。メダルは参加者、つまり高校生の 50% に与えられ、金・銀・銅の比率は 1:2:3 なので、金・銀受賞者は全参加者の上位 25% に入る
したがって「AI が IMO 問題を学生の 75% よりうまく解いた」という表現になり、実はこれもより印象的かもしれない
しかし「1問は数分、残りの各問題は最大3日」という条件は、学生に与えられる9時間とは異なるため、真の比較とは言いにくい。学生にも9時間ではなく最大15日が与えられていたなら、この点数に到達するか上回る人はもっと多かったはず
実際には、AI は学生に与えられた9時間内では1問しか解けなかったことになり、メダル圏からは遠かった可能性が高い。これほど印象的な結果を、わざわざリンゴとオレンジの比較で曇らせる必要があるのかと思う
より客観的には、時間はよりかかったが全問題の X% を解いた、あるいは N 点満点で X 点を取った、と報告すればよい
ここで時間はそれほど興味深い軸ではない。人間は巨大な GPU クラスタのような CPU を使っているわけではないから。「十分なリソースが与えられたとき解に到達できるか」という二分法の方が興味深く、GPT/Claude の答えは明確にノーだった
カットオフに非常に近く、普通は少し進展があるだけでも1点はもらえる。ただ、技術的な理由で金メダルを取ったという報道は好ましくなかっただろうから、議論の余地がない銀メダルで満足したのだと思う
これは本当の話。AlphaGeometryは、大量の総当たり探索で非常に限られた問題集合を解いていたものだった。
今回の方法ははるかに広く、数学のやり方に大きな影響を与えると思う。自然言語の数学から形式化された数学へつなげ、そこで形式化と証明の両方を訓練できる自己供給型パイプラインを実際に実装している。
原理的には、このパイプラインは補助定義や補題の生成のような基礎的な理論構築も学べる。証明支援の聖杯に近く、私たちが自然に作る数学の大部分を形式化できるようにしてくれると思う。人間は事後的に厳密化するやり方で働き、細部を埋める作業は機械が補助するようになるだろう。
逆に、このようなオープンエンドな形式化は進展が非常に遅く、漸進的だった領域だ。5年前に隣接分野で働いていたが、この結果は従来の自動推論手法では到達不可能な水準と見てよい。
本物の自動定理証明は純粋数学よりもはるかに広く有用だ。例えば、小さなプログラミング言語の公理的意味論をLeanで書き、「この仕様を満たすプログラムが存在することを示せ」といった問いを投げられる。
このアプローチが拡張されれば、ここ数年に出てきたどの機械学習応用よりも重要になるだろう。
私たちを作った進化も、膨大な総当たり的試行で機能した探索であり、科学的方法における研究も本質的には探索だ。
https://leandojo.org/
https://machine-learning-for-theorem-proving.github.io/
https://www.youtube.com/watch?v=P5ew0BrRm_I
https://paperswithcode.com/task/automated-theorem-proving
https://old.reddit.com/r/math/comments/11mb9lx/future_of_aut...
https://github.com/RiccardoBiosas/LeanGPT
役に立つことをするのに、非常に難しい問題を証明する必要はない。簡単なことだけを証明すれば十分な場合が多い。言語モデルにタスクの完了、項目の整理、スケジュール調整、Xを実行するコードの作成などをさせると、結果をすぐには信頼しにくいが、システムが問題の一部を論理に翻訳して解を見つけられるなら、はるかに信頼できるようになる。
核心が少し埋もれているが、彼らはLeanを使っている。
これは数学の問題を超えて重要だ。機械学習モデルに証明システムと格闘させるのは、一般的なでたらめを避ける良い方法だ。
今後もっと多くの人がLeanや似たシステムで型を書き、プロンプトを書くよりずっと良いやり方として活用してほしい。
polyrithなら8文字打つだけで済む。AlphaProofがnlinarithを使うのも見た。Tim Gowersが主な注意点を説明し、文脈づけた短くて良い概説がある。彼はFieldsメダリストで、今回の作業にも参加していた: https://x.com/wtgowers/status/1816509803407040909
その通りだが、各国代表チームに入ること自体が非常に険しいプロセスだ。地域数学オリンピック、全国数学オリンピックなど、各段階で容赦なくふるい落とされる。
その後、このエリート集団向けの追加訓練が続き、場合によっては追加選抜もあり得る。
要するに、ある国のIMO代表チームに選ばれること自体が大ごとで、その中で金・銀メダルを取るのはただただ途方もない達成だ。
情報源はIMO銀メダルを取った友人。
この仕事をしながら給料をもらっている人たちが本当にうらやましい。ものすごく面白そうだし、こういう形で最先端の水準を押し上げるのは、とても満足感がありそう
仕事の満足度では、テーマよりも職場環境のほうが重要だと思う。世界を変えるテーマを扱っていても、チームがめちゃくちゃならつらい時間を過ごすことになる。あらゆる楽しさを吸い取る才能を持つ人もいるし、社内政治はどこにでもあり、特に世界を変えるテーマほどそうなりがち
逆に、顧客データをデータベースに入れるような、いちばん退屈に見えるテーマでも、親切なチーム、よく設計されたアーキテクチャ、実験と知識共有の時間があれば最高の時間を過ごせる。単純でちゃんと動くものの美しさを、ますます高く評価するようになった。そういうものは科学的ブレークスルーよりも希少かもしれない
もちろん、素晴らしい職場環境と素晴らしいテーマが同時に来ることもあり、それはほとんど大当たりなので、うらやむに値する
こういう仕事ができることにワクワクし、感謝すべきなのだろうけれど、粗雑なツール群が仕事の楽しさをかなり奪っている
(/s)
機械が人間よりチェスをうまく指すようになってから、もう何十年も経っている
それでも誰も気にしていない。みんなMagnus Carlsenを見るのに忙しい
私たちは人間なので、ほかの人間がすることに関心を持つ。機械に関心を持つのは、それが私たちの役に立つ範囲に限られる
この原理は仕事や芸術にも広く当てはまる。人間が存在する限り、こうした領域における人間の居場所は常に残るはず
しかし近い将来、AIが大半またはすべてを発見したわけではない新しい数学的進展を発表する数学者が残っているかは、かなり疑わしい。人間が最初の問いを投げかけたという理由で証明の功績を得ることはあるかもしれないが、コンピュータが意味のある数学問題を簡単に解けるのに、人間がより遅く、より高コストに解くことにこだわる世界はほとんどない
芸術にはこの原理が確実に当てはまるが、仕事には一部、または大半にしか当てはまらない
そうなると証明を理解する必要はなく、どこかの数学者がその証明を完全に理解しているかどうかを誰も気にしない。機械が証明を見つけ、確認する点で私たちより優れているのは問題なく、むしろ予想できることになる
多くの数学者はそういうことに取り組みたがらないだろう。ただしIMOと研究数学の最前線の間には、まだ大きな距離がある
定理証明は、ばかげて大きな探索空間を持つ1人用ゲームなので、AGIよりずっと前に解かれるとずっと思っていた
個人的には、AlphaProofへの最大の貢献者はLeanとMathlibの背後にいる人たちだと思う。数学全体を形式化するという途方もない仕事を引き受けたからだ
数学論文の形式化不足が、自動化の試みをずっと潰してきた。AI研究者たちは、著者固有の記法、暗黙知、省略された証明ステップといった人間的な要素と格闘しなければならなかったからだ
AGIという用語自体が定義されていないと思うが、なぜ「一般的に知的な何か」、つまり人間の中央値レベルの知能を作ることが、「Terrence Taoより数学が得意になること」よりはるかに難しいと予想するのか分からない
いちばん良い議論はここにある: https://leanprover.zulipchat.com/#narrow/stream/219941-Machi...
その最良の議論はこちらで見ることができます。 https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learnin…