DeepMindのAI、国際数学オリンピックの問題を銀メダル級で解く

(deepmind.google)

3 ポイント投稿者 GN⁺ 2024-07-26 | 3件のコメント | WhatsAppで共有

Google DeepMindのAlphaProofとAlphaGeometry 2が国際数学オリンピックの問題を解決
- AlphaProof: 強化学習ベースの数学的推論システム
- AlphaGeometry 2: 改良された幾何学問題解決システム
- 2つのシステムは今年の国際数学オリンピック（IMO）で6問中4問を解き、銀メダル級の成績を達成

複雑な数学問題の解決におけるAIの成果

IMOの紹介
- 1959年から毎年開催されている、最も古く権威ある青少年数学大会
- 大会の問題は代数学、組合せ論、幾何学、数論などから出題
- Fields Medal受賞者の多くがIMO出身
AIシステムのIMOへの挑戦
- AlphaProofとAlphaGeometry 2が今年のIMOの問題を解決
- 問題は公式大会ルールに従って採点
- AlphaProofは代数学の問題2問と数論の問題1問を解決
- AlphaGeometry 2は幾何学の問題1問を解決
- 2つの組合せ論の問題は解けなかった
- 合計42点中28点を獲得し、銀メダル級の成績を達成

AlphaProof: 形式的推論アプローチ

AlphaProofの動作原理
- 数学的命題を形式言語Leanで証明
- 事前学習済み言語モデルとAlphaZero強化学習アルゴリズムを組み合わせ
- 自然言語の問題を形式的命題に翻訳し、さまざまな難易度の問題を解決
- 問題を与えると、AlphaProofは解法候補を生成して証明または反証
- 証明された結果はAlphaProofの言語モデルを強化し、より難しい問題を解く能力を向上
訓練プロセス
- 数百万の問題を証明または反証しながら訓練
- 大会期間中も訓練ループを適用し、問題の変形を証明

さらに競争力を高めたAlphaGeometry 2

AlphaGeometry 2の改善点
- Geminiベースの言語モデルとニューラルシンボリックのハイブリッドシステム
- 以前のバージョンより10倍多い合成データで訓練
- 幾何学問題の解決速度と精度が向上
- 新しい問題を解く際に知識共有メカニズムを使用
IMO 2024での成果
- 過去25年間のIMO幾何学問題の83%を解決
- 今年の大会では問題4を19秒で解決

数学的推論の新たなフロンティア

自然言語推論システムの実験
- Geminiベースの自然言語推論システムを実験
- 形式言語に翻訳せずに問題解決が可能
- 他のAIシステムとの組み合わせの可能性を探求
今後の展望
- 数学者がAIツールと協力して新たな仮説を探究し、問題解決アプローチを試し、証明プロセスを短縮できる可能性
- GeminiのようなAIシステムが数学および一般的な推論能力を向上

GN⁺のまとめ

AlphaProofとAlphaGeometry 2は、数学的推論におけるAIの可能性を示している
国際数学オリンピックで銀メダル級の成績を達成し、AIの数学問題解決能力を実証
数学者がAIと協力して新しい問題解決アプローチを探求できる可能性を開いた
類似機能を持つプロジェクトとして、OpenAIのGPT-3のような自然言語処理モデルがある

3件のコメント

chabulhwi 2024-07-26

形式数学ライブラリの開発に貢献する数学者が増えるほど、高性能な数学AIを作りやすくなるでしょう。自分で Lean 証明支援系の言語で形式化した数学理論を、Lean の数学ライブラリ Mathlib に移している韓国人は、私の知る限り現在3人います。

私は昨年、Mathlib を Lean 3 から Lean 4 へ移行する作業に少し参加し、今年は Lean 4 batteries ライブラリの未解決定理の一つを証明しました。

GN⁺ 2024-07-26

Hacker News の意見

1つ目の意見
- このプロジェクトには非常に興奮しているが、数学の問題を形式言語に翻訳する過程でコンピュータがどれほど貢献したのかは不明確
- ダウンロード可能な解答では、翻訳過程で人間が決めたことなのか、コンピュータが見つけたことなのかが明確ではない
2つ目の意見
- IMOではメダルは参加者の50%に授与され、金・銀・銅メダルの比率は1:2:3である
- AIが75%の生徒よりもうまく解いたというのは印象的
- しかし、AIが問題を解くのにかかった時間は、生徒たちに試験で与えられた時間とは異なるため、直接比較するのは不適切
3つ目の意見
- AlphaGeometry は限定された問題を解いたが、今回の手法はより広く数学に影響を与えるだろう
- 自然言語の数学を形式化された数学に変換するパイプラインを実装しており、これは基本理論の構築も学習できる
- これは証明支援の聖杯であり、人間がより自然に数学を形式化できるよう助けるだろう
4つ目の意見
- システムが問題を解くのに3日かかったのなら、それは単なる総当たりと大差ない
- これは真の推論ではない
5つ目の意見
- Lean を使っている
- これは数学の問題だけでなく、一般に無意味な結果を避けるうえで重要
- より多くの人が Lean のようなシステムで型を書くようになることを願っている
6つ目の意見
- このプロジェクトに参加している人たちがうらやましい
- 最先端技術を前進させるのは非常に楽しく、やりがいがあるだろう
7つ目の意見
- 最良の議論は LeanProver の Zulip チャットで行われている
8つ目の意見
- Fields Medal 受賞者の Tim Gowers が、主な注意点を説明し、文脈を与える良い概説を提供している
9つ目の意見
- 定理証明は、探索空間が非常に大きい1人用ゲームである
- AlphaProof の最大の貢献者は Lean と Mathlib の開発者たちである
- 数学論文における形式化の不足が、自動化の試みを妨げてきた
10個目の意見
- 機械は何十年も前からチェスで人間より優れていた
- しかし、人々は今でも Magnus Carlsen を見ている
- 人間は他の人間の行動に関心がある
- 機械は、人間にとって役に立つ限りにおいてのみ関心を持たれる