目次

1.はじめに
 2.国際数学オリンピックについて
 3.AlphaGeometryの性能
 4.AlphaGeometryの仕組み
 5.AlphaGeometryの評価結果
 6.AlphaGeometryの今後
 7.最後に

1 はじめに

2024年1月17日、Natureに掲載された論文でGoogle DeepMindが開発したAlphaGeometryという幾何学の問題を解くことに特化したAIが、国際数学オリンピックで出題された幾何学の問題を金メダル受賞者レベルで解いたという報告がありました。最近の動向として、従来生成AIが苦手とされてきた数学分野でも高い能力を持つ生成AIが登場してきました。そして今回登場したAlphaGeometryは、より難解な数学の問題を解くことができるようになりました。本記事では、AlphaGeometryついてご紹介したいと思います。

2 国際数学オリンピックについて

国際数学オリンピック(IMO:International Mathematical Olympiad）は、高校生以下を対象に毎年行われる数学の問題を解く能力を競う国際大会です。世界各国で選抜された数学の才能に溢れる参加者たちが難問に挑みます。
競技は、2日間に掛けて行われ参加者は1日4時間30分で3問ずつ問題を解きます。出題範囲は、「整数問題、幾何、組合せ、式変形等の問題が題材」となっており、各問題7点満点で満点は42点（7点ｘ3問ｘ2日＝42点）です。参加者には成績に応じて、金メダル(上位8%)、銀メダル(上位17%)、銅メダル(上位25%)が授与されます。

3 AlphaGeometryの性能

今回の論文で報告されているAlphaGeometryの国際数学オリンピックの幾何学問題の成績は以下の表の通りです。

国際数学オリンピックの幾何学問題の成績(AlphaGeometryの論文より引用)

AlphaGeometryは、2000年から2022年までの国際数学オリンピックの問題から編集された30問の幾何学問題のベンチマークセット(IMO-AG-30)を解いて、競技時間内に25問正解しました。この成績は、金メダリスト(25.9問)に匹敵する結果となっています。また、これまで最先端の方式であったWu's methodの正解数(10問)と比較しても性能が大きく進化しています。注目すべきことして、AlphaGeometryは、人間が読んで理解できる形で証明を作成し、さらに、2004年の国際数学オリンピックの問題に示された定理について、より一般化された定理が存在することを発見しました。

AlphaGeometryによる一般化された証明(AlphaGeometryの論文より引用)

上図は、実際AlphaGeometryによって行われた証明です。このように、AlphaGeometryは人間が読んで理解できる証明を作成します。また、元の問題では結論である$P、B、C$が同一直線上にあることを示すために、点$O$が$BC$の中点であるという前提を仮定していましたが、AlphaGeometryはこの前提がなくとも$P、B、C$が同一直線上にあるというより一般化された定理が存在することを証明をしました。

AlphaGeometryは、GitHub上に公式リポジトリが公開されています。

4 AlphaGeometryの仕組み

AlphaGeometryの概要

AlphaGeometryは、Language modelとSymbolic engineで構成され、この2つが連携して複雑な幾何学の定理の証明を見つけます。
Language modelが「直感的な早い思考」でアイデアを提供し、Symbolic engineが「慎重で合理的な意思決定」を行います。

AlphaGeometryの概念図(Google DeepMind公式ブログより引用)

AlphaGeometryは、与えられた問題とその定理の前提に対して、Symbolic engineが解を探します。解が見つからなかった場合、Language modelが解決に至るため潜在的に有用と判断した構成要素を追加し、再度Symbolic engineが解を探します。このループを解が見つかるまで繰り返します。

単純な問題を解決するAlphaGeometry(Google DeepMind公式ブログより引用)

上記の例題は、$\triangle{ABC}$において、$AB = AC$の前提が与えられた時、$\angle\mathrm{ABC} = \angle\mathrm{BCA}$ が成り立つことを証明する問題です。
AlphaGeometryは、はじめにSymbolic engineで証明を試みますが、前提だけでは証明することができません。そこで、次にLanguage modelが$BC$の中点$D$を追加します。そして、再度Symbolic engineで証明を試みます。

$BC$の中点$D$を追加
$\triangle{ABD}$と$\triangle{ACD}$において、$AB = AC$(前提)、$BD = DC$($D$は$BC$の中点)、$AD = AD$(共通の辺)となり、3組の辺がそれぞれ等しいので、$\triangle{ABD}\equiv \triangle{ACD}$(合同)である。よって、$\angle\mathrm{ABD} = \angle\mathrm{DCA}$が成り立つ
$B、C、D$は同一直線上にあるため、$\angle\mathrm{ABD} = \angle\mathrm{ABC}$、$\angle\mathrm{ACD} = \angle\mathrm{ACB}$
以上より、$\angle\mathrm{ABC} = \angle\mathrm{BCA}$が成り立つ

AlphaGeometryは、上記のステップで問題を解決します。

オリンピックの問題を解くAlphaGeometry(Google DeepMind公式ブログより引用)

上図は、2015年国際数学オリンピックの問題3です。問題を証明するために、109の論理ステップを必要としたことが分かります。

Language modelの学習

数学の定理の証明(特に幾何学の定理の証明)に関して、これまで学習データとして利用できる「定理と証明」のデータセットが少なかったため、AlphaGeometryでは自律的に学習データを作成する方針を取っています。
はじめにランダムな図形を10億個生成します。

AlphaGeometry によって生成された合成データの視覚的表現(Google DeepMind公式ブログより引用)

次にSymbolic engineを使用して、各図に含まれているすべての証明を見つけてから、それらの証明に必要な追加構成があれば逆算して見つけます。(記号演繹とトレースバック)

AlphaGeometryの学習データ作成のプロセス(AlphaGeometryの論文より引用)

大まかなイメージとしては、ランダムにサンプリングされた前提を持つサンプル(図$a$)から導出できる問題と証明(図$c$)を作成します。

上図では、ランダムにサンプリングされた前提を持つ$\triangle{ABC}$(図$a$)をSymbolic engineに入力すると、図$a$の前提(premises)から、Symbolic engineが四角形$EADH$は、円に内接する(対角の和$\angle\mathrm{ADH} + \angle\mathrm{AEH}$の和が$180^\circ$となるため)という問題と証明を作成しています。また、四角形$EBCD$は、四角形$EBCD$は円に内接する($\angle\mathrm{BEC} = \angle\mathrm{BDC} = 90^\circ$より円周角の定理の逆を満たすため)ことから、$\angle\mathrm{EDH} = \angle\mathrm{ECB}$を経て、$\angle\mathrm{EDB} = \angle\mathrm{ECB}$(円周角の定理)が成り立つことを証明しています。図$c$の一番下のサンプルでは、$HA \perp BC$より$AH$の延長線と$BC$との交点(図$a$では点$F$)は、$AF \perp BC$が成り立ちますが、この定理を証明する際、$HA \perp BC$と無関係の点$D$、点$E$の関係(補助線$DE$)を使用しています。この補助線$DE$が上述した新たに必要になった追加構成となります。
ここで、導出されたすべての構成要素は有向非巡回グラフとして表現できます。さらに、$N$をある結論(conclusion)とすると結論の証明(proof)となる有向非巡回グラフの部分集合$G(N)$が定まります。(数学的には厳密ではないのですが、図$c$の中の1つのサンプルには1つ結論があり、そのサンプルの方向に向かう、図$b$内の構成要素の経路が有向非巡回グラフの部分集合になるというイメージです。)$P$を前提(premises)とした時、データセットは、(premises, conclusion, proof) = $(P, N, G(N))$の組で表されます。
AlphaGeometryのLanguage modelでは、$(P, N, G(N))$のデータセットから重複を排除した1億個をデータセットに対して、<premises><conclusion><proof>の構造を持つシリアル化されたテキスト文字列をパラメータ数1.51億個を持つTransformerで事前学習しました。さらに、補助線が必要なデータセットを900万(全体の約9%)使用してファインチューニングを行いました。

Symbolic engineによる推論

Symbolic engineは、Deduction Database(DD) と Algebraic Rules(AR) で構成されています。

Symbolic engineによる推論の例(AlphaGeometryの論文より引用)

Deduction Databaseは、保存されている幾何学の法則と事実に従って、追加の事実を結論付けることが可能なデータベースです。Algebraic Rulesは、幾何学の法則に従い角度や長さの計算を行います。この2つを組み合わせることで、より難しい問題を証明することが可能になります。さらに、Symbolic engineでは「最小前提抽出アルゴリズム」を使用して、より一般化された前提に対して成り立つ、不必要なステップを排除した簡潔な(Symbolic engineが最小ステップと推論した)証明を作成します。

5 AlphaGeometryの評価結果

2000年から2022年までの国際数学オリンピックの問題から編集された30問の幾何学問題のベンチマークセット(IMO-AG-30)を用いて、AlphaGeometryとその他の手法を比較した結果は以下の通りです。

様々な手法でIMO-AG-30を解いて正解した問題数の比較(AlphaGeometryの論文より引用)

AlphaGeometryは30問中25問に正解しこの中では最も正解数が多い結果となっています。一方、GPT-4は1問も問題を解くことができませんでした。ここで、AlphaGeometryを構成するDeduction Database(DD)を見てみると、Deduction Database(DD)は単体で7問解けています。Deduction Database(DD) + Algebraic Rules(AR) (= Symbolic engine)では14問も解答できています。この結果からSymbolic engine単体でも、従来のこれまで最先端の方式であったWu's methodの正解数を上回っていることが分かります。また、事前学習とファインチューニングに着目すると、それぞれ事前学習なしの場合の正解数は21問、ファインチューニングなしの場合の正解数は23問であることから、事前学習とファインチューニングを実施した方がAlphaGeometryでより多くの問題を解くことができています。

6 AlphaGeometryの今後

以下の表では、幾何学以外にAlphaGeometryのアプローチが適用できる可能性のある領域の例が示されています。

AlphaGeometryのアプローチが応用可能な幾何学以外の数学の領域(AlphaGeometryの論文より引用)

今回、AlphaGeometryが取り組んだ国際数学オリンピックの幾何学の問題では、適切な補助線や点を新たに導入することが証明を作成する上で必要不可欠な手順でした。同様に、今回のような適切なAuxiliary Construction(補助的な構成)を与えられることで、問題を証明することが可能になる領域においては、AlphaGeometryのアプローチを応用できる可能性があります。

7 最後に

この記事では、AlphaGeometryについてご紹介しました。個人的に特に印象に残ったことは、AlphaGeometryが幾何学の問題に対して、より一般化された定理を発見したことでした。現時点でAlphaGeometryは、初等的な幾何学の問題は解くことができますが、より高度かつ抽象的な問題はまだ解くことができていません。将来的にAlphaGeometryのようなAIが研究者レベルの数学の問題を解くことができるようになれば、数学の研究においてもAIの役割が大きくなっていくのではないかと思います。

参考文献

Solving olympiad geometry without human demonstrations(AlphaGeometryの論文)
AlphaGeometry: An Olympiad-level AI system for geometry(Google DeepMind公式ブログより引用)
AlphaGeometry GitHub
AlphaGeometry: 数学オリンピック金メダリスト級(幾何学限定)の「ファスト＆スロー」なハイブリッド生成AI
AlphaGeometryの技術を読み解く〜生成AIが数学オリンピックに挑戦
国際数学オリンピック(Wikipedia)