グーグルのAIがIMO金メダルを逃す：19秒で問題を解き評価委員を驚かせ、幾何学能力が人間を超える

DeepMindの最新の数学モデルが国際数学オリンピック（IMO）で銀メダルを獲得し、優れた成績を収めました。このモデルは6問中4問を完璧に解答し、金メダルまであと1点というところでした。特に第4問では、モデルはわずか19秒で解答を提示し、その解答速度と質の高さに人間の審査員を驚かせました。

AlphaProof

AlphaProofは、形式言語Leanで数学的命題を証明できるシステムです。事前学習済みの大規模言語モデルとAlphaZero強化学習アルゴリズムを組み合わせています。

機械学習における形式言語の限界（人間が書いたデータが限られている）を克服するため、研究者たちは自然言語と形式的な文の間のギャップを以下の方法で埋めました：

  1. Geminiモデルを微調整し、自然言語の問題文を自動的に形式的な文に変換する
  2. 様々な難易度の形式化された問題の大規模なライブラリを作成する

問題を解く際、AlphaProofは候補となる解を生成し、Leanで可能な証明ステップを探索することでそれらを証明または反証します。

AlphaGeometry 2

AlphaGeometry 2は、Geminiの言語モデルを使用してゼロから学習したニューラル-シンボリックハイブリッドシステムです。前身よりも難しい幾何学の問題を解くことができ、物体の動き、角度、比率、距離の方程式を含む問題にも対応します。

主な改良点は以下の通りです：

  1. 前バージョンより1桁大きい合成データで学習
  2. 以前より2桁速い記号エンジン
  3. 異なる探索木の高度な組み合わせを可能にする新しい知識共有メカニズム

AlphaGeometry 2は印象的な能力を示し、過去25年間のIMO幾何学問題の83%を解決しました（前身は53%）。今年のIMOでは、形式化された問題を受け取ってからわずか19秒で問題4を解きました。

IMOにおけるAIの性能は、数学的推論能力の大きな進歩を示しており、高度な数学における人間レベルの問題解決能力にAIを近づけています。