機械学習･深層学習ミーツ
‖数学‖ØØ FunSearch AlphaGeometry
NP(完全最適化)問題は、｢正解を求めることは難しいが、評価するのは簡単｣な問題の一つである。つまり、｢正解を求める多項式時間アルゴリズムは、存在しない｣と広く信じられているが、多項式時間で”評価する手順”は、認められている。
グーグル･ディープマインドが23年12月14日にnatureでオンライン公開した論文[*1](以下、本論文)は、組み合わせ論において、既知のものを超える、新しい構成を発見した、と主張する。その発見は、グーグル･ディープマインドが自社で開発したFunSearchと呼ぶ、探索プラットフォームを使って達成された。FunSearchとは、関数空間での探索を意味する略語である。
グーグルは、同日(23年12月14日)、自社の公式ブログにFunSearchの成果を投稿した[*2]。それを受けて、MITテクノロジーレビューを含むメディアは、｢グーグル･ディープマインドは、大規模言語モデルを使って、純粋数学における有名な未解決問題を解いた｣という報道を行った。このような報道等に対して、FunSearchは、それほど大したことを成し遂げていないと主張するレビュー論文[*3]も発表された(24年1月7日)。
【1】本論論文の主張
本論文は、以下を主張している。
(1) FunSearchは、極値組み合わせ論における代表的な未解決問題：キャップ集合問題に対して、既知のものを超える、大きなキャップ集合の新しい構成を発見した。
(2) FunSearchをオンライン箱詰め問題に適用し、ベース･ラインを改善する新しいヒューリスティックスを発見することで、FunSearchの汎用性を示した。
【2】事前整理
(1) 島ベースの進化計算
進化計算は元々、生物進化のメカニズムを模倣して、データ構造を変形・合成・選択する手法[*4]である。現在では、数学的な解釈が与えられ、｢解集団に基づく確率的な多点探索法の総称｣という整理がなされている[*5]。進化計算の強みは、目的関数に関する知識を必要としないこと、並列処理が実行しやすいこと[*6]及び、多目的最適化に適した手法であること[*5]、とされる。進化計算の代表例は、遺伝的アルゴリズム(GA)であり、本論文でもGAが使用されている。また、本論文では、島ベースの進化計算が使われている。
島ベースの進化計算とは、並列化進化計算の一つである。母集団を、いくつかの｢島｣と呼ばれるサブ集団に分割することで、並列化を行う。各島における解の進化は、基本的に他の島から独立して行われるが、数世代ごとに島と島の間で｢移住｣と呼ばれる解の交換がなされ、島間での情報交換が行われる[*7]。
(2) (最大)キャップ集合問題
本論文でキャップ集合問題は『かつてテレンス･タオによって、｢おそらく、私のお気に入りの未解決問題｣と評された』と紹介(箔付け)されている。フィールズ賞受賞者(@31歳)であるテレンス･タオ†1の最初の専門領域は、調和解析であるが、フィールズ賞は整数論†2で受賞している。その後、組み合わせ論などにも専門領域を広げている(キャップ集合問題は、組み合わせ論に属する)。
1⃣ 概要[*3]
キャップ集合問題をキャッチ－に表現すると、｢極値組み合わせ理論における、中心的な未解決問題｣となる。その内容はシンプルで、幾何学的に表現すると分かり易い。まず、ベクトルの集合Sを考える。Sの中で、同一線上にないような、3つのベクトル(のセット)をキャップ集合という。ベクトルの要素数を次元nと呼ぶ。次元nが与えられたとき、n 次元の最大キャップ集合は何かを求める問題を、最大キャップ集合問題と言う。
2⃣ FunSearchでは、どのように解くのか？
最大キャップ集合問題では、特定の値n(次元)に対する最大キャップ集合の平均サイズを表す記号として cnを使用する。n＝1～6の場合には、cnの正解が知られているが、7以上では未知である。ただしn≧7の場合でも、粗い上限と下限は、簡単に求められる。具体的には、2n≦cn≦3nが知られている。
最大キャップ集合問題における数学的なチャレンジは、cnにほぼ等しいγ = lim cn1/n(n→∞)を求めることである。γの上限を求めることは難しく、γ ≤ 2.756 の上限は2017年に証明された。この証明を成し遂げた一人が、本論文の論文著者に名を連ねているJordan Ellenbergである。つまり、バリバリの第一人者である。
†1 小山[2023]に、人柄が謙虚である、と書かれている。
†2 小山[2023]に、(調和解析が専門だった当時)整数論の難解な本を(大学図書館から借りて)読んでいた、というプリンストン大学時代の逸話が紹介されている。
(3) オンライン箱詰め問題
1⃣ 概要
箱詰め問題は、英語では(つまり本論文の原語では)bin packing(ビン･パッキング)と呼ばれる。箱詰め問題は、組み合わせ最適化において良く知られた問題の一つである。先の最大キャップ集合問題とは異なり、材料の切断からジョブのスケジュール設定まで、幅広い分野で重要な役割を果たす。
箱詰め問題の目標は、さまざまなサイズの”詰め物”のセットを、最小数の固定サイズの箱に詰めることである。すべて同じサイズの箱セットと、その箱より大きくない詰め物セットが与えられる。詰め物は、細かく切り刻んで、別々の箱に入れることはできない。
オンライン箱詰め問題があるということは、オフライン箱詰め問題もある。両者の違いは、詰め物が 逐次的に1 つずつ提示されるのがオンラインである。一度に全ての詰め物が提示されるのが、オフラインである。オンライン箱詰め問題を解決するには、一つずつ提示される詰め物を、どの箱に割り当てるかを決定するための、ヒューリスティックを設計する必要がある。オンライン箱詰め問題に使用される標準アルゴリズムは、ファースト･フィットとベスト･フィットである。ファースト･フィットでは、提示された詰め物を、十分な空きスペースのある最初の箱に詰める。ベスト･フィットでは、詰め物を、まだ収まる空きスペースが最も少ない箱に詰める。
FunSearchは、ファースト･フィットとベスト･フィットよりも、優れたヒューリスティックを発見することを目指す。
2⃣ FunSearchでは、どのように解くのか？
詰め物と箱の配列(各箱の残りの容量を含む)を入力として受け取り、各箱の優先順位スコアを返すプログラムとして、ヒューリスティックを定義する。優先順位スコアを返すプログラムの引数は、次元nと優先関数である。優先関数priority(v)は、ベクトルvに優先度の数値尺度を割り当てる。このヒューリスティックに従って、まずは、最初の時点で最高スコアの箱を選択する。その後、FunSearch を使用して、このヒューリスティックを進化させる。
具体的には、⓵ORライブラリー箱詰め問題ベンチマーク並びに、⓶ワイブル分布からサンプリングされた箱詰め問題インスタンスで、ヒューリスティックを進化させた。ワイブル分布は、多くの現実世界のスケジューリング問題が従っている確率分布である、という理由から選ばれた。
【3】FunSearchの詳細
(1) FunSearch概要
FunSearchは、 ㊀プログラム･データベース(DB)、㊁サンプラー、及び㊂評価器、を備えた分散システムとして実装されている。㊀プログラムDBはプログラムを保存して提供する。㊁サンプラーは、事前学習された大規模言語モデル(LLM)を使用して、新しいプログラムを生成する。㊂評価器は、スコアに従って、プログラムを評価する。スコアは、キャップ集合問題の場合なら、入力に対するキャップ集合のサイズである。プログラムが正しく実行されなかった場合もしくは、解が無効であった場合は、Øを返す。
LLM によって生成されたプログラムは、一連の入力に基づいて評価され、スコアが付けられる。スコア付けされたプログラムは、プログラム･データベースに送信される。正しくないプログラムは破棄される。FunSearchでは、”スコア”の低いプログラムを、”スコア”の高いプログラムに進化させることで、新しい知識を発見する。従って、モデル･アーキテクチャは、(進化計算を採用しているのだから、わざわざ言及するまでもないが)強化学習に近い。👉では、強化学習を採用したらどうなるかという疑問がわく。答えは、｢当初、強化学習アプローチを試みたが、それは有望とは思えなかった。特に大きな問題サイズには対応できませんでした｣らしい[*3]。なお、オープンAIの研究者による論文[*14]には、(AIを使って数学の証明を行うという文脈で)｢強化学習を形式的な数学に、単純に(ナイーブに)適用することは成功しそうにない(unlikely)｣とある。
LLMは、PaLM2をベースとしたコード生成のためのLLM｢Codey」が使われている。Codeyは、大規模な(100万個程度)コード･コーパスに基づいて再学習されている(なお、大規模なコード･コーパスで学習された(コード作成用)LLMであれば、Codeyである必要はない)。評価器は、作話(※)や誤ったアイデアを防ぐ機能を担う。
※ 作話：confabulationの和訳。意味は、ハルシネーション(hallucination:幻覚)と同じ。一般的には、ハルシネーションが多用されるが、作話の方が意味合いを正しく、表現している。また、(AIゴッドファーザーの一人)ジェフリー･ヒントンは、confabulationという文言を好む。
(2) FunSearchの動作
FunSearchは、以下のように動作する。
1⃣ プログラムDBから、最もパフォーマンスの高いプログラムをサンプリングする。そのプログラムを、LLM の改善のためのプロンプトにフィードバックする(このプロンプトは、ベストショット･プロンプトと呼ばれる)。サンプリングは、島ベースで行われる(以下、(3)2⃣を参照)。
詳細には、以下の通り：プログラムDB内の単一の島から 2個のプログラムをサンプリングする。サンプル･プログラムは、スコアに従って並べ替えられ、スコアを示す記号が割り当てられる。その後、2つのプログラムは、単一のプロンプトに結合される。こうすることで、LLMに対し暗黙的に、サンプリングされたプログラムと、同様なフレーバーを持つ優先関数を生成するように要求している(噛み砕いて平たく言えば、2つのプログラムを提示し｢これらと似ているけれど、もっと優れたプログラムを作って｣とLLMに依頼する)。なお、サンプルするプログラムの数を2にした理由は、それを超えるとメリットが減少するためである。
2⃣ (ボイラープレート･コード(※)と、問題に関する事前知識を含む)スケルトン形式のプログラムから開始し、ロジックを制御する重要な部分のみを進化させる。たとえば、貪欲法のスケルトンを設定することで、各ステップでの意思決定に使用される優先関数を進化させる。
※ ボイラープレート･コード ：いくつかの異なるコンテキストで、ほとんどor全く変更せずに再利用できるコンピュータ言語のテキスト。
(3) FunSearchの特徴
以下のような特徴を上げることができる。
1⃣ スケルトンからスタート
最初のプログラムをスケルトン形式で作成する。そうすることで、性能が大幅に向上した。既知のプログラム構造を再構成するのではなく、重要な部分のみを進化させることにLLM リソースを集中させたため、全体的な結果が向上することがわかった、とする。
2⃣ 島ベース
探索を促進し、局所最適を回避する｢島ベースの進化計算(遺伝的アルゴリズム)｣を使用することで、多様なプログラムの大規模なプールを維持している。ただし島ベースの進化計算自体は、FunSearchに固有のスペシャリテというわけではない(つまり、一般的に用いられている)。
プログラムDBからサンプリングするには、まず島をサンプリングし、次にその島内のプログラムをサンプリングする(￢1)。サンプリングは、ボルツマン選択法(￢2)に従って行われる。これにより、スコアが高く短いプログラムが優先される。重要な点は、島の最悪の半分(最も優れた個別スコアが、最も低い島に相当)のプログラムを定期的(具体的には、4時間ごと)に破棄することで、島間で情報が流れるようにしていること(これは、｢移住｣と呼ばれる)である。FunSearchでは、これらの島プログラムを、生き残った島から最も優秀な個体クローンを作成することによって初期化された、新しい個体群に置き換える。
￢1 正確に言うと、プログラムのサンプリングは、まず島のクラスターをサンプリングする。次に、そのクラスター内のプログラムに対して、サンプリングを行う。プログラムはシグネチャ毎にクラスター化されている。シグネチャ≒スコア、と見做して良い。
￢2 ボルツマン選択法は、選択時点で評価の高い行動に、最も高い選択確率が与えられ、他の行動には、それぞれの評価価値に基づいた選択確率が与えられる行動選択法である。クラスターiを選択する確率Pi=exp(si/Tクラスター)/∑分子、である。siはクラスターiのスコア。
3⃣ スケーラビリティ
FunSearchの高度な並列性を利用することで、FunSearchを非同期的にスケールし、全体的なコストを低く抑えながら、適用範囲を大幅に広げている。通常、㈠15 個のサンプラーと 150 個の CPU評価器を使用し、㈡それぞれ 32 個の評価器を並行して実行する、5 つの CPU サーバーでサービスを提供できる、と説明されている。
(4) FunSearchの適用範囲
本論文では、｢FunSearchは現在、次の特性を持つ問題に、最適に機能する｣としている。
❶ 効率的な評価器が利用できる。
❷ 改善を定量化する｢豊富な｣スコアリング･フィードバックを提供する方法が明確である。
❸ 進化させるべき部分のみを切り出して、スケルトンに提供する能力。
(5) FunSerachでヒトが行うこと
FunSerachでヒトが行うべきことを整理する。それは、次の3つである[*3]。
1⃣ いくつかの重要なサブルーチン(本論文の場合は、優先度)を引数として取り、数学的問題に対する解の候補を生成する解決アルゴリズムの準備。本論文では、スケルトンと呼ばれる初期プログラムの準備に相当する。
2⃣ 評価器の準備。評価器は、特定の優先関数の品質を測定する。最大キャップ集合問題、シャノン容量、およびコーナー問題の場合、各優先関数は特定の数学的問題に対する単一の解を生成し、優先関数の値が解の値になる。箱詰め問題の場合、優先関数の値は、特定のベンチマーク コレクションの問題に適用される解決の平均品質となる。
3⃣ 優先関数の準備。優先関数priority(v)は、ベクトルvに優先度の数値尺度を割り当てる。
【4】FunSearchの成果
本論文(及び補足情報[*8])によれば、4つの問題について、FunSearchは、従来知られている結果よりも、優れた結果を発見した。なお本論文ではなく、補足情報で触れられている問題(シャノン容量とコーナー問題)については、割愛した。
(1) 最大キャップ集合問題
1⃣ 結果サマリー
FunSerachは、 最大キャップ集合問題において、以下の貢献を行った[*3]。
① n = 8 のサイズ 512 のキャップ集合を見つけた。以前の最もよく知られたキャップ集合のサイズは 496 であった(最も粗い下限は、28＝256)。したがって、下限 c8≥ 512 が確立された。
② γ の下限を、以前の値 2.2180 から 2.2184 に引き上げる大きな許容集合(※)を見つけた。
③ FunSearch からの出力を検査する際に、Ellenbergは、許容集合を構築する問題において、これまで知られていなかった対称性が正しく仮定されていることに気づいた。その後、Ellenberg はこの対称性を利用して、FunSearch が探索していた探索空間に焦点を合わせ、2.2202 というさらに大きな下限を作成することができた。
※ 許容集合：2つの制約条件を満たす、n次元ベクトル{0, 1, 2}nの有限集合。許容集合を使用して、サイズが大きなキャップ集合を系統的に生成する方法を構築することで、γ の下限を計算することができる[*3]。
2⃣ 深堀り[*3]
上記③について、(理解の及ぶ範囲で)詳述する。具体的に言うと、発見された優先関数は、ベクトルを高度に対称的に扱っており、そのベクトルが構築する許容集合は、互いに素な巡回置換の下で保存されていた。本論文では、そのような許容集合を、対称許容集合と呼んでいる。
FunSearchを使用して、対称許容集合が探索された。この探索は、探索範囲が制限されている一方、探索空間は小さいため、以前よりも高い次元での探索が可能である。これにより、Iの許容集合(容量C ≥ 2.219486 を意味する) と、サイズ237,984の 許容集合の部分許容集合(キャップ集合の新しい下限を意味する)が発見された。ここで、容量Cは、supn cn1/nで定義される。また、Iはフルサイズの許容集合の集合を意味する(太字にしたのは、読み易すくするためで、本論文で、そう表記されているわけではない。また、一般的な表記でもない)。
(2) オンライン箱詰め問題
1⃣ 結果サマリー
FunSearchは、⓵ORベンチマーク(OR1～OR4)では、ファースト･フィット(FF)及びベスト･フィット(BF)よりも優れた結果を示し、⓶ワイブル分布(5k、10k、100k)からサンプリングされたインスタンスでは、大幅に優れた結果をもたらすヒューリスティックを発見した。評価指標は、空隙率＝1ー充填率。具体的に述べると、⓵ではFFが5.23～6.45%、BFが4.94～6.06%であるのに対して、FunSearchは2.47～5.30%であった。⓶では、FF→4.00～4.23%、BF→3.79～3.90%に対して、FunSearch→0.03～0.68%であった。
さらに、大規模なインスタンスにも適切にスケーリングし、堅牢である(と主張している)[*9]。
2⃣ 解説
FunSearchが発見するヒューリスティックは、詰め物を最小容量の箱に詰め込むのではなく、詰め物を配置した後のフィット感が非常に厳しい場合にのみ、詰め物を最小容量の箱に割り当てる。それ以外の場合、通常、詰め物は別の箱に配置され、詰め物が配置された後に、さらにスペースが残る。この戦略により、埋められる可能性が低い小さな隙間が、箱内に残ることが回避される。
【5】考察
(0) FunSearchが、純粋数学における有名な未解決問題を解いた、という報道は、(テレンス･タオの謙虚さに照らし合わせるまでもなく)明らかにハイプである。なお、FunSearchの成果自体は、マイクロソフト(MS)の先行研究を鑑みると、驚くに当たらない。MSの先行研究とは、LLMを使って、P≠NPを結論付ける証明スキーマを生成した、という研究[*10]を指している。
(1) [*3]は、従前のAIシステムと比較して、FunSearchが数学(の未解決問題の解決)において、大きな役割を果たすかどうかは、疑わしいという立場である。
(2) FunSearchはコード作成という形で、FunSearchのロジックを”見える化”させている。つまり、｢説明可能なAI｣である。とりあえず数学を脇に置いて、新しいスタイルの｢説明可能なAI｣という意味だけでも、FunSearchは画期的であると思える。
それにしても、AlphaGo(2015年頃)[*11]から始まって、AlphaFold(1:18年→2:20年)[*12]、AlphaTensor(22年10月)[*13]、GraphCast(気象予報、23年11月)、GNoME(新規材料探索モデル、23年11月)、そしてFunSearch(23年12月)。この怒涛の研究発表ラッシュは、凄まじい。
(3) このロジックの”見える化”は、｢説明可能｣という範囲を越えて、数学や科学の発見に貢献できると思われる。従来以上のパフォーマンスを発揮する、それまで知られていなかったロジックが、一貫してコードに記述されていれば、それは未知のルール(法則)である可能性が高い。実際、本論文のキャップ集合問題でも、｢これまで認識されていなかった、対称関係｣を(Ellenbergに)気付かせた。そして、その気付きが、 さらに優れたソリューションに繋がった。このことは当然、[*3]でも触れられているが、｢そのようなことが、今後も続く保証はない｣として、数学や科学の発見への貢献に否定的な立場を採っている。つまり、見解の相違である。
(4) FunSearchは、どうすればLLMの限界(作話など)を越えて、LLMが数学や科学の発見に貢献できるかを”探索した”一つの成果と見做すことができるだろう。そう捉えると、この方向性の未来は明るいように思える。
計算機を使った数学定理の自動証明は1950年代から行われているが、大きなインパクトを与えるまでには至っていなかった。幾何問題に関して言えば、1978年の成果(Wuの方法)を超えられていなかった。その一方で、2012年以降の深層学習の華々し成功、あるいは大規模言語モデルの誕生を受けて、これらの新しい技術を自動定理証明に適用する研究も行われつつある(例えば、オープンAIの研究→【3】(4)を参照)。
そのような背景下、ニューヨーク大学とグーグル･ディープマインドの研究者は、国際数学オリンピック(IMO)で出題された幾何学問題の自動定理証明において、平均的な金メダリストの成績に近づいたと主張する論文[*15](以下、本論文)を発表した(24年1月17日@Nature)。これはAlphaGeometryと呼ぶ、(自動定理証明の)証明支援系†(theorem prover)による成果である。お馴染みの｢Alpha｣を冠している。
† 不思議な日本語ではあるが、数学の定理証明を支援するソフトウェアは、｢証明支援系｣と呼ばれる。英語では、proof assistantも使われる。
【1】本論文の主張
本論文は、以下を主張している。
(1) AlphaGeometry は人間が読める証明を生成する。
(2) IMO問題30 問のテスト･セットで、AlphaGeometry は 25 問を解いた。これまでの最良結果(Wu の方法†)では、10問だった。
(3) IMO問題より、大きく多様なテスト･セットに対しては、AlphaGeometryは、ほぼすべての問題を解決した。Wu の方法が解決したのは、3/4であった。
† 1978年、中国の数学者ウェン･ツン･ウーが開発したモデルによる結果。
【2】海外メディアの報道
(1) ニューヨーク･タイムズ(NYT)
24年1月17日付けNYTの記事[*16]によると、本論文の筆頭著者Trieu H. Trinhは、ニューヨーク大学(博士過程)で、国際数学オリンピックの幾何学問題を解くAIモデルを如何に構築するか、という問題に4年間取り組んでいた。ざっくり言うと、natureに掲載された博士論文が、本論文ということになる。Trinhは、グーグル･ディープマインドの研究者に、このプロジェクトへの参加を打診し、共同でAIモデルを開発することになった(2021～23 年まで、Trinhはグーグルに常駐した)。なおTrinhは、その前から、グーグル･ブレインのResidencyプログラムで研究し、論文(例えば、[*17])を発表している。ちなみに、23年4月に、グーグル･ブレインはディープマインドと統合している。
[*16]には、4人の専門家の意見が掲載されている。ただし、本当の専門家(コンピュータによる数学定理の自動証明)は、一人である。
まず、英エディンバラ大学で科学史の講師を務めるマイケル・バラニーの意見：｢これが意味のある数学的マイルストーンなのかどうか疑問に思っている｣、｢IMOテストは、創造的な数学とは大きく異なる｣。同講師のバックグラウンドは、学部(米コーネル大学)で数学、博士過程で科学史(米プリンストン大学)である。
次に、米カリフォルニア大学バークレー校のテレンス・タオ教授の意見：｢AlphaGeometryは、素晴らしい仕事｣であり、｢驚くほど強力な結果を達成したと考えている｣。テレンス･タオは、IMO最年少金メダリスト(@12歳)であり、フィールズ賞受賞者(@31歳)でもある。
さらに、幾何学者であり、コンピューター検証推論の専門家である米フォーダム大学のヘザー･マクベス准教授の意見：｢AlphaGeometry は、良い進歩を示しているようです｣。同准教授は、IMOメダルを 2 つ獲得している。
4人目として、認知神経科学者である仏コレージュ･ド･フランスのスタニスラス･デハーネ教授の意見：｢AlphaGeometryのパフォーマンスに感銘を受けた｣、｢しかし、AlphaGeometryは、それが解決する問題については何も『見て』いない｣。
なお最後に、AlphaGeometryの結果が正しいことを確認した、マサチューセッツ工科大学数学博士課程のエヴァン･チェンの感想が載っている(エヴァン･チェンは、IMOコーチであり、また金メダリストでもある)：｢機械がどのようにしてこれを実現しているのか知りたい｣、と同時に、｢人間がどのようにして解決策を思いつくのかも知りたい｣。NYTは、(将棋界の藤井聡太名人のように)AIを使って、数学を前進させるイメージを持っているのだろうか。
(2) フィナンシャルタイムズ(FT)
ディープ･マインドの地元である英FTの24年1月18日付け記事[*18]では、本論文の共著者Quoc V. Le(グーグル･ディープマインド)による｢これは、汎用人工知能(AGI)構築に向けた重要なステップです｣という野心を、最初に掲載している。また、(推論†エンジンと代数規則の2つで構成されている)AlphaGeometryに対するアナロジーとして、｢速い思考と遅い思考｣を持ち出している。これは、広く知られているように、心理学者･行動経済学者のダニエル･カーネマンが、より熟議的な論理的思考に高速パターン認識を利用する力を説明するために作った造語である(カーネマン自身は、行動ファイナンス理論、プロスペクト理論で有名であろう)。AlphaGeometryが人間の思考と同じ態様で、定理証明を行った、ということを強調したいのであろう。次に上げるMITテクノロジーレビューの記事でも、同様の記載がある。
専門家の意見としては、ロンドン数理科学研究所のランダウAIフェロー、ミハイル･ブルツェフ[*19]の意見を載せている：｢(AlphaGeometryの成果は、数学定理の自動証明において)大きな前進であるが、それは『それ自体が設定する課題の範囲内でのみ』｣で、｢AI がまだ答えのない問題を解決するための新しい数学を発見できるかどうかを調べる、という課題が残っている｣。先に、人間の思考と同じ態様だから成績が良いと持ち上げておいて、｢人間の創造性には比肩しない｣と落として、バランスを取って(?)いる。ミハイル･ブルツェフは、本当の専門家と言って良いだろう。
最後に、ディープ･マインドは、国際数学オリンピック出場する可能性は排除しなかった、と締めている。
† 本稿では、推論と演繹を、特に区別しない。意図的に混同して使用する。
(3) MITテクノロジーレビュー(MITTR)
MITTRは技術専門誌であるため、一般紙とは記述の趣が異なる(ある意味、丁寧で、分かり易い)。24年1月18日付けの記事[*20]は、AlphaGeometryの紹介から始まり、そのアプローチが｢ヒトのやり方によく似ている｣という中継地点に、うまく着地させている。言語モデルと記号推論を、ヒトの創造的思考と論理的推論のアナロジーとして、捉えている。
専門家の意見としては、独ボン大学のフロリス･ヴァン･ドールン教授が掲載されている：｢本当に素晴らしい｣。同教授は、(数学用)プログラミング言語かつ証明支援系であるLean(リーン)を使った形式化数学†(formalized mathematics)を専門とする[*21]。もっとも、専門家過ぎて、意見が前のめり過ぎるかもしれない。米ルイビル大学コンピューター科学工学のロマン・ヤンポルスキー准教授は、(やや置きにいった感がある)｢AlphaGeometryは、より洗練された、人間のような問題解決能力を持つ機械に向けた大きな前進を示す｣と述べている。
† もともと、数学における｢形式化｣とは、定理の証明の各ステップで、どの推論規則や公理が使われたかを例外なく全て記録することを指す。ただし、手動では多大な労力を必要とするため、コンピューター登場前は、非現実的であった。その一方で、コンピューター登場後は、証明をコンピュータで検証する(自動検証)→コンピューターで証明を行う(自動証明)、と意味合いが深化してきた。
(4) ネイチャー(ニュース)
論文とは別に、(由緒正しい著名な科学ジャーナル)nature(のニュース)に記事[*22]が掲載されている(24年1月17日付け)。特徴的な記述は、グーグルが開発したミネルバを引き合いに出した、｢自然言語で学習されたモデルは、信頼できない自然言語を出力することになる(本論文の筆頭著者Trieu H. Trinh)｣との指摘であろう。AlphaGeometryでは、このため、幾何証明を記述するための言語を新たに開発して、同言語でAIモデルを学習させている。
専門家の意見としては、2件掲載されている。
まず、インペリアル･カレッジ･ロンドンのケビン・バザード教授(数学)の｢AlphaGeometryが 25 のIMO 問題を解決でき、さらに人間が読める証明を生成できるという事実は、非常に印象的｣で、｢AIモデルが、数年後には、最も賢い学部生だけが解ける学部レベルの数学の問題を解決できるようになるかもしれないと想像できる｣が、｢現時点では、AIモデルが現代の研究レベルの数学に取り組んでいるという証拠は見当たらない｣。
続いて、独バーデン･ヴュルテンベルク連携州立大学のステファン･シュルツ教授(コンピュータ科学)の｢言語モデルと記号推論の組み合わせは、有望である｣。
また、ニューヨーク大学コンピュータ科学のHe He(何河)准教授[*23]の｢いつか人間の能力を超えるようにしたい｣という野心が語られている。同准教授は、Trieu H. Trinhの指導教官であり、本論文の共同著者である。
(5) その他
Fortune(Google DeepMind AI ソフトウェアが幾何学問題の解決に画期的な進歩をもたらす、1月18日付け)やBloomberg(DeepMind の最新 AI システムである AlphaGeometry は、高校数学で高得点を取る、1月18日付け)にも記事が掲載された。(Webでは紹介されているものの)日本のメディアでは、見当たらない。
【3】事前整理
(1) 計算機代数手法と探索手法
幾何定理証明支援系は、2 つのカテゴリーに分類される。最初のカテゴリは、計算機代数手法で、幾何学ステートメントを、その点座標の多項式として扱う。証明は、大規模な多項式の特殊な変換によって実行される。グレブナー基底(を使って代数方程式を解く方法)とウーの方法は、このカテゴリの代表的なアプローチであり、人間が判読できる証明がないにもかかわらず、IMO-AG-30(※)のすべての幾何定理の真理値を決定する、理論的保証を備えている。
AlphaGeometry は、2 番目のカテゴリに属し、探索手法(あるいは、公理的手法や合成手法)と呼ばれる。探索手法では、定理証明の問題を、一連の幾何公理を使用した段階的な探索問題として扱う。探索手法は、人間が判読できる解釈可能な証明を返す。GPT-4などの大規模言語モデルは、このカテゴリに属する。大規模言語モデルは、さまざまな推論タスクで顕著な推論能力を実証したが、IMO-AG-30で、GPT-4 の成功率は 0% であり、出力全体で構文的および意味的エラーが頻繁に発生し、幾何学の知識や問題ステートメント自体の理解をほとんど示していない(と手厳しい)。
一般に、探索手法には、証明性能に理論的な保証がなく、計算機代数手法よりも弱いことが知られている。
※ 2000 年以降の IMOコンテストの幾何学問題の中で、本論文で扱った30個の問題(テスト･セット)を指す。AlphaGeometryにおいて、幾何証明を記述するために新しく開発した言語で、表現できた問題が30問であった。
(2) 一階述語論理と二階述語論理[*24],[*25]
0⃣ 前説
ここでやりたいことは、AlphaGeometryが好成績をあげた背景に数学的な裏付けを付けたい、である。以下⓵と⓶という整理をすれば、裏付け可能だと理解している：⓵一階述語論理は、数学における推論に対して、十分な表現力を持っている。⓶特定の一階述語論理は自動定理証明が”ある程度”可能であり、AlphaGeometryが扱った問題はその範疇に入る。
ただし、これでは、AlphaGeometryが他の方法に比べて、好成績をあげた理由にはならない。それについては【5】(1)を参照されたい。以下、上記の理解に基づいて、少し詳しく書き下したい。
証明とは、定義･公理から出発して、補題の積み重ねにより目標定理に到達する過程である[*24]。AlphaGeometryは、まず記号推論を使って、証明作業を進める(証明の探索を行う)。記号推論で不十分な場合は、言語モデルを使って補助項†1を追加し、証明の探索を続行する。冒頭の文章に沿えば、証明の探索によって、補題の積み上げを行っている。数学的にカッコいい言葉を使うと、演繹的閉包†2を拡張している。(ディスっているわけではないが)雑に言うと、AlphaGeometryは、自動定理証明がうまく行く範疇に、対象とする問題を落とし込んだから、うまく行った、と考えられる。 FTで、ロンドン数理科学研究所のミハイル･ブルツェフによる｢AlphaGeometryの成果は『それ自体が設定する課題の範囲内でのみ』｣であるという発言は、そういうことを言っているのであろう。
†1 幾何学における補助項(あるいは補助構造)の、もっとも分かり易い例は、｢補助線を引く(あるいは補助点を追加する)｣、｢円を描く｣、あるいは｢角度を二等分する｣等であろう。数学的には｢補助項｣の方がカッコいいので、以下、補助項とする。
†2 演繹的閉包とは、論理式の集合に推論規則及びデフォルト規則を繰り返し適用して得られる、論理式の集合である。デフォルトについては、(4)デフォルト理論を参照。
1⃣ 一階述語論理
次のような論理を、一階述語論理と呼ぶ[*25]。
㊀ 解釈とモデルが与えられれば、論理式の真偽が決まる。
㊁ 全ての可能な解釈と、全ての可能なモデルから伴意関係、妥当性を判定できる。
より原始的な命題論理は、次のように定義される。
㊀’ モデルが与えられれば、論理式の真偽が決まる。
㊁’ 全ての可能なモデルから伴意関係、妥当性を判定できる。
命題論理は表現力が乏し過ぎて、数学推論、あるいは、人間の思考に沿った自然な推論には不十分である。一階述語論理は、オブジェクト及びオブジェクト間に｢関係｣が定義されていて、｢解釈｣が可能となっている。[*24]は、一階述語論理の範疇で、コンピュータ証明(自動定理証明)が成就する具体的な条件を書き下している：以下❶～❸のみで構成される文は、自動定理証明が、”ある程度”上手くいく(そのような文を[*24]ではR文と呼んでいる)。ただし、変数は実数とする。
❶ 有理係数の多変数多項式
❷ 等号、不等号
❸ 論理記号
自動定理証明が”ある程度”上手くいく理由は、一階述語論理に、3つの性質(量子化除去(あるいは限量記号消去)、完全性、決定可能性)があるからである。そして、AlphaGeometryが扱った幾何問題は、このR文として表現できると理解している。
なお”ある程度”の意味は明確にされていないが、｢上手くいくと期待することは、十分に合理的である｣程度の意味であると解釈している。当然、必ず自動定理証明が成功するはずはない。
2⃣ 二階述語論理[*24]
為参考ではあるが、｢自然数全体、関数や集合｣を対象とする場合には、二階述語論理が必要となる。先の3つの性質でいうと、 二階述語論理は、完全性において大きく劣る。｢すべての妥当な一階述語論理の文を導出できる、完全な証明系が存在する｣のに対して、｢すべての妥当な二階述語論理の文を導出できる、完全な証明系は存在しない｣。 つまり、二階述語論理で自動定理証明は難しい。
ただし[*24]では、｢大規模証明ライブラリから、コンピュータが『経験と勘』を学ぶことができるようになれば、それが二階の(述語論理で自動定理証明は難しい、という)壁を超える突破口になるかもしれない｣と書かれている。本論文で、(ユークリッド平面幾何学のみという)限定的ではあるが、大規模証明ライブラリが構築されたから、一歩前進ではないだろうか。
なお、最初期を除いて、ほとんどの証明支援系は、二階述語論理(あるいは高階述語論理)に対応しているらしい。
(3) デフォルト理論[*26],[*27],[*28]
デフォルト理論(W,D)は、一階述語論理を発展させた論理(論理式の集合)である。ここで、Wは一階述語論理の閉論理式の集合である。これは、常に正しい知識を表す(→単調推論)。Dは、デフォルトの集合である。デフォルトとは、間違いを起こし得る知識を表す。デフォルト理論の推論(デフォルト推論：default reasoning)は、Wと、Wと矛盾を起こさないDの極大部分集合を使った、非単調推論である。
知識が不完全であることを前提とする非単調推論では、新しい知識の追加によって、結論が変わる。｢公理や補題が不足して、定理の証明が未だできない状態に、新しい補題を追加して、証明にまで到達する｣という枠組みは、非単調推論で定式化される。AlphaGeometryの記号推論エンジンは、(一階述語論理の部分クラスである)ホーン節論理に従った、デフォルト理論推論を採用している。つまり、
Q(x) ← P1(x),…, Pk(x)
という形式の含意式を用いる。xは点を意味する。QやPi(i=1～k)は、｢等しい線分｣とか｢同一線上に存在する｣、｢2つの点 AとB を与えて、正方形ABCDを作成する｣などである。ちなみに、←の左側を帰結部あるいはヘッドと呼ぶ。右側は、条件部あるいはボディと呼ぶ。カンマ(,)は連言(論理積、あるいはAND)を表す。
(4) オープンAIの証明支援系
ここでは、あくまで(言語モデルー具体的には、トランスフォーマーを使った、自動定理証明の)先行研究例として上げるだけで、特に、AlphaGeometryとの比較を行わない。
オープンAIは、2020年9月7日にarXivで公開された論文[*29]で、自動定理証明に対してトランスフォーマー･ベースの言語モデル(GPT-f)の適用可能性を探った。GPT-fは、従来よりも短い証明を”発見”し、それらはMetamath証明ライブラリに加えられた。その後、2022年2月3日にarXivで公開された論文[*30]では、この取り組みを進め、GPT-f が｢十分に多様な難易度の形式的ステートメントのセットから、段々と困難になる問題のカリキュラムを解決できることを実証した｣と主張した。
なお、オープンAIの証明支援系は、命題をプログラミング言語のLeanを使った形式で表現し、Leanによる証明が出力される。
【4】AlphaGeometryの詳細
(0) AlphaGeometryの付帯情報
1⃣ AlphaGeometryにおける言語モデルのアーキテクチャ
基本設定でのトランスフォーマーの学習には、Meliadライブラリ†を使用した。トランスフォーマーには 12 層があり、埋め込み次元 1,024、アテンション･ヘッドは8 つ、および ReLU活性関数を備えた、次元 4,096 の相互アテンション全結合層がある。 入力ヘッドと出力ヘッドの埋め込み層を除いて、1 億 5,100 万個のパラメーターがある。カスタマイズされたトークナイザーは、SentencePieceを使用して、単語モードで学習され、語彙サイズは 757 である。コンテキストの最大長を 1,024 トークンに制限し、T5(Text-to-Text Transfer Transformer)形式の相対位置埋め込みを使用する。学習中、アテンション層の前および全結合層の後に、5% のドロップアウト率が適用される。
TPUv3の 4 × 4 スライスが、ハードウェア･アクセラレータとして使用された。事前学習では、コアあたり 16 のバッチ サイズと、1千万ステップで 1×10-2から1×10-3に減衰するコサイン学習率スケジュールで、トランスフォーマーを学習する。再学習のために、さらに1百万ステップにわたって最終学習率1×10-3を維持する。
事前学習を行わないセットアップでは、学習率を1百万ステップで1×10-2から1×10-3に減衰させる。
ハイパーパラメータの調整は行っていない。
† Meliadライブラリーは、深層学習における様々なアーキテクチャの改善に関する進行中の研究の一環として開発されているモデルのコレクションである。ライブラリーは現在、いくつかのトランスフォーマーのバリエーションで構成されており、一般的なトランスフォーマー･アーキテクチャを拡張して、長いシーケンスにわたる言語モデリングをよりよくサポートする方法を探求している。出典：https://github.com/google-research/meliad
2⃣ AlphaGeometryにおける証明探索に対する設定
証明探索は、言語モデルと記号推論エンジンが交互に実行されるループである。定理の結論が見つかるか、ループが最大反復回数に達すると、証明探索は終了する。言語モデルは、k 個の補助項を記述する k 個の異なるシーケンスを返すため、これら k 個のオプションに対してビーム探索￢1を実行する。このセットアップは、ビーム間で高度に並列化できるため、並列計算リソースがある場合に大幅な速度向上が可能になる。
具体的には、ビーム･サイズ k = 512￢2、最大反復回数は 16、各ノードの分岐係数(つまり復号化バッチ･サイズ)は32を使用する。これは、推論時間の最大バッチ サイズである。これは、GPU V100 のメモリに収まるサイズである。
￢1 ビーム探索とは、枝刈りをしながら木･グラフを探索するヒューリスティックな探索アルゴリズムである。 ビーム探索は、枝刈りを行うことで幅優先探索を省コスト化したもので、幅優先探索は全探索を行うが、ビームサーチでは事前に決めておいた数の候補から、最良のものを選ぶ。
￢2 言語モデル出力の上位512個を用いて探索する、という意味である。
3⃣ AlphaGeometryにおいて、幾何表現に使用した形式言語
Leanなどの汎用形式言語で、IMO 幾何学問題を記述するためには、依然として大量の下準備が必要である。この障壁を回避するために、AlphaGeometryでは、GEX、JGEX、MMP/Geometer、あるいはGeoLogic で使用される、より特殊な形式言語を採用した。結果として、すべての IMO 幾何学問題の 75% を、この表現に適合させることができた。
4⃣ AlphaGeometryにおけるダイアグラム構築言語
AlphaGeometryでは、複数のオブジェクトを含む多くの(定理証明に用いる)前提を、自由にサンプリングするのではなく、一度に前提内の 1 つのオブジェクトを構築するために、JGEXで使用されているものと同様の、構成的なダイアグラム構築言語を開発した。これにより、自己矛盾する一連の定理前提の生成を回避できる。
構築アクションには、特定の方法で他のオブジェクトに関連する新しい点を作成する指示や、例えば｢数値αを与えたとき、∠ABX = αとなるように点Xを作成する｣というように数値を設定する指示がある。
5⃣ 学習データとして、合成データセットを生成した
誤解を恐れずに極めて粗っぽく言うと、｢入力を大量にランダム生成して、その入力によるデータベース検索をかけて返ってきた出力とのペア｣を学習データとした。人手に依らないところがポイントである。
㈠ 前置き
ほとんどの数学領域では、｢ヒトによる定理証明を、機械検証可能な言語に翻訳した｣学習データが不足している。このため、機械学習ベースでの自動定理証明は、困難である。幾何学は、幾何学特有の翻訳の難しさのため、Leanなどの汎用数学形式言語での証明例が、特に少ない。全体として、これらがボトルネックを生み出し、機械学習ベースでの自動定理証明において幾何学が、特に遅れをとっている原因となっている。幾何学に対する自動定理証明のアプローチは依然として、主に記号的手法とヒトが設計した探索ヒューリスティックに依存している。
このような問題意識の下で、AlphaGeometryでは、合成データを使用した自動定理証明の代替方法を提案している。こうして、ヒトが提供した証明例を翻訳する必要性を回避している。
㈡ 具体的なプロセス
定理(の証明に用いる)前提のランダム集合をサンプリングし、記号推論エンジン(推論データベース)への入力とする。記号推論エンジンは、定理の証明に必要な前提を入力すると、到達可能な結論を出力する。出力形式は、有向非巡回グラフである。約10 億個の前提をサンプリングした。合成データ生成プロセスを 100,000 の CPU ワーカーで 72 時間実行した後、約 5 億の合成証明サンプルが得られた。証明ステートメントを正規形式に再フォーマット(例えば、個々の用語の引数を並べ替えたり、同じ証明ステップ内の用語を並べ替えたりするなど)し、それ自体およびテスト･セットに対する浅い重複排除を回避した。最終的には、1 億個の固有の定理証明の例が得られた。合成データには IMO-AG-30 の問題は見つからなかった。
㈢ 合成データのグラフ構造
有向非巡回グラフの各ノードが到達可能な結論であり、トレースバック･アルゴリズムにより、エッジ(辺)が親ノード(頂点)に接続される。そのセットアップ下でのトレースバック･プロセスが、任意のノード N から再帰的に実行され、最後にその依存関係サブグラフG(N) が返される。ルートは N、リーフはサンプリングされた前提のサブセットになる。このサブセットを P とすると、合成データ (前提、結論、証明) = (P, N, G(N)) が得られる。この合成データで、言語モデルを学習する。
(1) 記号推論エンジンと代数規則
1⃣ 記号推論エンジン(DD)
記号推論エンジンの中心機能は、定理の前提に基づいて新しい真のステートメントを推定することである。平たく言えば、証明完了に向かって、証明作業を自動的に進めていく、ことを指している。推論は、｢X であれば Y｣などの幾何学的規則を使用して実行できる。この場合、X と Y は、｢A、B、C が同一直線上にある｣などの幾何学的ステートメントのセットである。ちなみに演繹的閉包を見つけるために必要な時間は、標準的な非アクセラレータハードウェアで、｢数秒｣である。
AlphaGeometryにおけるDDの実装は、標準形式の文字列を使用するのではなく、グラフデータ構造を使用している。グラフ構造を使用することで、関数の引数の対称的な順列だけでなく、推移律(transitivityあるいはtransitive law)、共線性(同一直線上にある)、共円性(同一円周上にある)も捕捉できた、とする。
ちなみにDDはDeductive Databaseの略であるが、本論文中では、記号推論エンジン(symbolic deduction engine)もDDと略している。この理由は、｢幾何学において、記号推論エンジンは、推論データベースである｣からだろう。DDは、幾何学的ルールによって前提から新しいステートメントを効率的に推論する機能を備えており、明確なホーン節の形で推論規則に従う。
また、deductiveあるいはdeductionなので、演繹と訳す方が妥当かもしれないが、先述の通り、推論と演繹を混同させ、ここでは(も)、記号推論と訳している。
2⃣ 代数規則(Algebraic Rule：AR)
推論をさらに強化するために、代数規則(AR)を通じて推論を実行する機能も AlphaGeometry には組み込まれている。AR により、式変形を通じて、角度、比、距離に対する証明が可能になる。このような証明ステップは、幾何学的規則によっては、カバーされていない。ガウスの消去法により、可能なすべての線形演算子の演繹的閉包が、｢数秒｣で見つかる。
例えば、角度に関する証明問題であれば、以下のようなステートメントとなるだろう：まず四角形のような図形があって、辺の中点から垂線を降ろして･･･といった前提が続き、最後に、どこそこの角度(例えば、同一直線上にない点A,B,Cから構成される角度∠ABC)が90度であることを証明せよ(正確に言うと、角度はπ表記されるので、90度はπ/2と表記される)。この問題を解くとき、人は”代数的に”、つまり式を変形することで、∠ABC＝π/2を求める。∠ABC＝変形していき、･･･＝π/2。この幾何学的な量(角度、線分、比など)を、式変形をして代数的に求められるようにするために、ARが搭載されている。なお、角度の等式∠ABC = ∠XYZは、s(AB) − s(BC)= s(XY) − s(YZ)と表される。また、比の等式AB:CD = EF:GH は、log(AB) − log(CD) = log(EF) − log(GH) と表される。
3⃣ DDとARの融合
AlphaGeometryの記号推論エンジンは、DDとAR の複雑な統合であり、演繹的閉包の拡張が停止するまで、DDとARを交互に適用する。 このプロセスは通常、標準の非アクセラレータ･ハードウェアでは、数秒から長くても数分以内に終了する。
(2) トレースバック
1⃣ 概論
各推論ステップは、ステップの結論を出すために必要な、直接の親ステートメントの最小限のセットを返す。AlphaGeometryでは、この返しを、トレースバック･アルゴリズムと呼んでいるらしい。トレースバックは、もれなく｢最小限のセット｣を返す必要がある。不必要な推移律を通じて、証明に寄与する余分な補助項を回避するために、この｢最小限｣という縛りは必須である。例えば、a = cが他の推移律を通じて直接取得できる場合、a = bとb = cは必要ない可能性がある。
言葉を変えて表現するなら、AlphaGeometryが好成績を上げるためには、余分な補助項の回避は必須であり、トレースバックは重要、となるだろう。
2⃣ 幾何学的規則推論のためのトレースバック
トレースバックを実行するために、推移律グラフを記録する。 共線性と共円性を扱う場合には、推移律グラフとして、 3辺または 4辺のハイパーグラフG(V, E) が使用される。このとき、トレースバックの実行は、NP困難となる。したがって、貪欲アルゴリズムが用いられる。
※ 木構造やグラフの探索を行うためのアルゴリズム。 始点となるノードから隣接するノードを探索し、そこからさらに隣接するノードに対して探索を繰り返して、目的のノードを見つける。幅優先探索は、全ノードを網羅的に探索していくため、しらみつぶし法とも言える。
(3) 改めて、AlphaGeometryとは何か？
0⃣ 適用範囲とモデルのタイプ
射程は、ユークリッド平面幾何定理の証明問題である。モデルのタイプは、探索タイプである。
1⃣ 独自性
まず、記号推論を用いて証明を進める。行き詰ると、言語モデルが補助項を追加して、記号推論による証明の探索を実行する。言語モデルは、自然言語ではなく、幾何問題を表現するのに適した形式言語で学習しているので、不確かな(confabulationを起こすような)出力をしない。
細かな工夫は、数多く行っている。幾何問題を取り扱うので、学習データはグラフ構造を持たせている。不要な(余分な)補助項を回避するための機構(トレースバック･アルゴリズム)も備えている。
2⃣ AlphaGeometryにとって極めて重要な、補助項について
アブレーション分析の結果(下記【5】(1)3⃣)を先回りして述べると、AlphaGeometryの好成績は、補助項による貢献が大きい。一般的な自動定理証明の文脈では、補助項は外生項生成の例であり、探索ツリーに無限の分岐点を導入するため、意味のある補助項を、効率的に生成することは難しい。従前は、手作りのテンプレートとドメイン固有のヒューリスティックに基づいていた(どちらにしても、専門家のマンパワーに依っていた)。AlphaGeometryが、その部分を自動化した。
AlphaGeometryでは、意味のある補助項を生成するために、トレースバック･アルゴリズム(探索の枝刈り)の他に、｢証明の枝刈り｣も行っている。証明の枝刈りは、前提Pと証明G(N)の最小性を保証するために行う(G(N)とは、Nのグラフを意味している)。本論文において最小性は、｢結論Nの到達可能性を失わずに、G(N)とPをさらに枝刈りすることができない特性である｣と定義されている。証明の枝刈りは以下のように行われた："徹底的な試行錯誤を実行"し、より小さい前提Pの部分集合で DD+ARを再実行して、結論Nの到達可能性を検証する。最後に、全試行にわたって取得可能な最小限の証明G(N)を返す。
意味のある補助項のみを生成することは、効率的に補助項を生成することにも貢献する。効率的な生成には、並列化計算の採用、単純なマシンパワーの向上も貢献している。
【5】比較結果
(1) IMO-AG-30 ベンチマーク
1⃣ 成績結果の発表
AlphaGeometryを含む10 個のソルバーに対して、成績を比較した。2/10は計算機代数手法(①Wuの方法と。②グレブナー基底を使った手法)で、8/10が探索手法である。なお、⑩AlphaGeometryについては、⑪事前学習†1なし版及び、⑫再学習†2なし版もある(ので、厳密にはソルバーは12個)。⑧AlphaGeometry以外は、③GPT-4、④full-angle法、⑤演繹データベース(DD)、⑥DD＋ヒトが設計したヒューリスティクス、⑦DD＋代数規則(AR)、⑧DD＋AR＋GPT-4を使った補助項付き、⑨DD＋AR＋ヒトが設計したヒューリスティクス、である。
成績は、問題30個中、解けた個数で計測する。結果は、①10個、②4個、③0個、④2個、⑤7個、⑥9個、⑦14個、⑧15個、⑨18個、⑩25個、⑪21個、⑫23個、であった。
†1 事前学習は、(純粋な記号推論の証明を含む)合成的に生成された 1 億個の証明すべてに対して、実行された。
†2 再学習は、事前学習データ全体の約 9%(つまり 900 万個)の証明を占める、補助項を必要とする証明の部分集合で実行された。
2⃣ 比較結果の定性的解釈
定性的には、｢GPT-4が無力であること、DD+ARは有効であること、 ヒトが設計したヒューリスティクスは有効であること｣、がわかる。 GPT-4が無力であることは、まさに【2】(4)ネイチャー(ニュース)に書かれている｢自然言語で学習されたモデルは、信頼できない自然言語を出力することになる｣を体現している。また、事前学習や再学習がなくても、AlphaGeometryの成績は、際立って良いこともわかる。
3⃣ 比較結果の定量的解釈
定量的には、⑤→⑦→⑩は、ある意味｢アブレーション分析｣になっている。DDをベースライン(7個)とすると、ARで7個が上乗せされ14個になる。そして、言語モデルによる補助項を加えることで、11個が上乗せされて計25個になっている。言語モデルによるサポートが、極めて強力に効いていることが分かる。
なお他には、次のような定量的結果が示されている(俄には信じられないが･･･)：㊀学習データが、フルセットの20%でも、21個の問題を解いた。㊁ビームサイズを1/64(つまり8本)でも21個の問題を解いた。㊂ビームサイズが512であれば、最大反復回数を16から2に減らしても、21個解いた。
4⃣ 宿題の答え
ここで【3】(2)1⃣の宿題に答えると、｢幾何表現に適した形式言語で学習した言語モデルによって、補助項を生成できるようにした｣ことが、AlphaGeometryが従前の方法と比べて、優れている理由と言えるだろう。ちなみに一階述語論理の文脈で言うと、｢言語モデルによって、補助項を次々と生成して、補助項を加えて｣推論を続けていく過程は、(一階述語論理の部分クラスに属する)ホーン節論理に従うデフォルト理論による推論、ということになる(はず)。
(2) 231 の幾何学問題からなる、より大きく多様なテスト セットに対しては、AlphaGeometry がほぼすべての問題(98.7%)を解決した。Wu の方法は 75% を解決し、DD+AR+ヒトが設計したヒューリスティックは、92.2% を解決した。
【6】考察
(1) 探索手法が、計算機代数手法を上回った構図は、画像認識タスクにおいて、大量データをベースとした人工知能(AlexNet:畳み込みニューラルネットワーク)がルールベースの人工知能に圧勝した2012年を再現したとも言える。これまでは、数学において、大量データを用意することが難しかったため、探索手法は真価を発揮できなかった。
(2) 事前学習なしでもAlphaGeometryは、好成績を修めているから、必ずしもAlexNetの再現とは言えないだろうが、データ駆動型の自動定理証明が”ドライブする”きっかけになることが期待される。
今後の一つの方向性として、より幅広く幾何問題を扱える形式言語の研究があるだろう(もちろん幾何以外の問題についても、引き続き形式言語の研究は必要だろうが･･･)。その先は、2階述語論理の攻略が続くのだろう。
(3) 1900年に行われた第一回国際数学者会議でダフィット･ヒルベルトが、23個の未解決問題を掲げて進路を示したように、自動定理証明が目指すところを示したらどうだろうか。
なお[*31]には、2014年の国際数学者会議でDigital Mathematics Library(DML)構築のためのワーキング･グループが創設された、という話題が掲載されている。DML構築にあたって解決すべき課題と解決策を検討するワークショップが2016年に開かれたものの、その後、具体的な進展は内容である([*31]は2020年の資料)。もちろん、DML構築と自動定理証明の指針表明とは、大きな隔たりがあるが、かけ離れてもいないように思う。
(4) AlphaGeometryは、｢補題を証明して、補題を積み重ねる｣という作業に行き詰ると、問題を細分化して、補題の証明を探索する。その試行錯誤を数百万回繰り返す、まさに力技である。斜に構えた見方をすると、"普通程度の"難問は、力技で解くことができる！ことが疎明された。単純に考えて、この方向で、何処まで行けるか試す(どこまでが、普通の難問かを探る？)というのは、一つの道であろう。
(5) もちろん、ヒトは何百万回という試行錯誤をしていないから、ヤッパり凄いという見方もできる。ヒトと機械の差分を縮めるという道が、研究としては王道だろうが、そこには別次元のイノベーションが必要なのだろう。ただし、差分が縮まらないと考えることに、合理性はないと思っている。
【尾注】
*1 Bernardino Romera-Paredes et al.、Mathematical discoveries from program search with large language models、https://www.nature.com/articles/s41586-023-06924-6
*2 https://deepmind.google/discover/blog/funsearch-making-new-discoveries-in-mathematical-sciences-using-large-language-models/
*3 Ernest Davis、Using a large language model to generate program mutations for a genetic algorithm to search for solutions to combinatorial problems:Review of (Romera-Paredes et al., 2023).、https://cs.nyu.edu/~davise/papers/FunSearch.pdf
著者は、ニューヨーク大学コンピューター･サイエンス学部の教授である(https://cims.nyu.edu/people/profiles/DAVIS_Ernest.html)
*4 伊庭斉志、電子情報通信学会『知識の森』◆ S3 群－ 4 編－ 3 章 進化計算、https://www.ieice-hbkb.org/files/S3/S3gun_04hen_03.pdf
*5 佐藤寛之･石渕久生、進化型多数目的最適化の現状と課題、オペレーションズ･リサーチ学会機関誌 62巻3号(2017)、pp.156-163、https://orsj.org/wp-content/corsj/or62-3/or62_3_156.pdf
*6 https://www.bbo.cs.tsukuba.ac.jp/research-j/%E9%80%B2%E5%8C%96%E8%A8%88%E7%AE%97%E3%81%A8%E5%BC%B7%E5%8C%96%E5%AD%A6%E7%BF%92%E3%81%AE%E7%B4%B9%E4%BB%8B
*7 廣安知之他、分散確率モデル遺伝的アルゴリズム、情報処理学会論文誌：数理モデル化と応用、Vol.45 No.SIG2(TOM 10)、https://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=17231&item_no=1&attribute_id=1&file_no=1
*8 https://static-content.springer.com/esm/art%3A10.1038%2Fs41586-023-06924-6/MediaObjects/41586_2023_6924_MOESM1_ESM.pdf
*9 ちなみに、堅牢でないのは明らかだ、と主張しているサイトがある。https://www.eugenevinitsky.com/posts/Funsearch.html
*10 Qingxiu Dong et al.、Large Language Model for Science:A Study on P vs.NP、https://arxiv.org/pdf/2309.05689.pdf
*11 AlphaGoはAlphaGo Zero、AlphaZero、MuZeroへと進化した。AlphaZeroは、学習データを必要とせず、自己対戦だけで成長することができ、囲碁だけでなく、チェスや将棋でも世界チャンピオン･プログラムに勝利した。MuZeroは、ゲームのルールすら与えられていない状態から学習し、AlphaZeroに匹敵する強さに至った。出典：https://www.jst.go.jp/crds/pdf/2022/FR/CRDS-FY2022-FR-04/CRDS-FY2022-FR-04_20106.pdf
*12 1も2も、タンパク質の立体構造を予測するが、裏で回っているロジックは大きく違う。
*13 AlphaTensorは、AlphaZeroをベースとして「行列の積を計算する最適な方法を求める」というゲームを実行させたものである。出典：https://www.jst.go.jp/crds/pdf/2022/FR/CRDS-FY2022-FR-04/CRDS-FY2022-FR-04_20106.pdf
*14 Stanislas Poluet al.、Formal Mathematics Statement Curriculum Learning、https://arxiv.org/pdf/2202.01344.pdf
*15 Trieu H. Trinh et al.、Solving olympiad geometry without human demonstrations、https://www.nature.com/articles/s41586-023-06747-5
*16 A.I.’s Latest Challenge: the Math Olympics Watch out, nerdy high schoolers, AlphaGeometry is coming for your mathematical lunch.、https://www.nytimes.com/2024/01/17/science/ai-computers-mathematics-olympiad.html
*17 Trieu H. Trinh & Quoc V. Le、A Simple Method for Commonsense Reasoning、https://arxiv.org/pdf/1806.02847.pdf
*18 DeepMind approaches gold standard in complex maths in latest AI breakthrough、https://www.ft.com/content/c4153a8e-8eeb-4000-b16e-fa09c828bd72
*19 https://lims.ac.uk/profile/?id=114
*20 ディープマインドの新AI、数学オリンピック級の幾何学問題を解く、https://www.technologyreview.jp/s/327299/google-deepminds-new-ai-system-can-solve-complex-geometry-problems/
*21 https://florisvandoorn.com/
*22 DeepMind AI solves geometry problems at star-student level、https://www.nature.com/articles/d41586-024-00141-5
*23 https://hhexiy.github.io/
*24 照井一成、コンピュータに証明できる こと・できないこと、https://www.kurims.kyoto-u.ac.jp/~terui/suugakuseminar.pdf
*25 二宮崇、知識工学第6回、http://aiweb.cs.ehime-u.ac.jp/~ninomiya/ke/ke-6-slide.pdf
*26 櫟粛之・石田亨、デフォルト論理に基づく知識プログラミングシステムとそのプログラム変換の理論的枠組み、人工知能学会誌 Vol.7 No.2 March 1992、pp.280-291、https://www.jstage.jst.go.jp/article/jjsai/7/2/7_280/_pdf
*27 坂間千秋・井上克己、特集|｢論理に基づく推論研究の同行｣ 解集合プログラミング、人工知能学会誌 25巻3号(2010年5月)、pp.368-378、https://web.wakayama-u.ac.jp/~sakama/jsai2010asp.pdf
*28 馬場口登、特集|不完全な知識の下での推論 非単調推論、日本ファジィ学会誌 Vol.4 No.4、pp.608-619 (1992)、https://www.jstage.jst.go.jp/article/jfuzzy/4/4/4_KJ00002087699/_pdf/-char/ja
*29 Stanislas Polu ＆ Ilya Sutskever、Generative Language Modeling for Automated
Theorem Proving、https://arxiv.org/pdf/2009.03393.pdf
*30 Stanislas Polu et al.、Formal Mathematics Statement Curriculum Learning、https://arxiv.org/pdf/2202.01344.pdf
*31 佐藤雅彦、査読付き論文|証明支援系と型理論、科学哲学53-2 (2020)、pp.3-23、https://www.jstage.jst.go.jp/article/jpssj/53/2/53_3/_pdf/-char/ja
‖参考文献‖
小山信也、素数って偏ってるの？～ABC予想、コラッツ予想、深リーマン予想～、技術評論社、2023
