AlphaGeometry: DeepMind の巨大なコンピューティング能力が再び奇跡を生み出すが、「コンピューティング能力がインテリジェンスに置き換わる」は最適な解決策ではない可能性がある
著者: 李宝珠
編集者：三陽
カバー画像の出典: Google DeepMind
DeepMind はコンピューティング能力を使って奇跡を起こしますか?高く評価されている AlphaGeometry にはどれほどの価値があるのでしょうか?
最近、Google DeepMind の Alpha シリーズに新しいメンバー、AlphaGeometry が加わり、「マイルストーン」「壮大」「人間に近づく」などの賞賛の言葉が画面に溢れ、依然として高い人気を誇っています。では、数学オリンピックの金メダル級の能力を持つと言われるこのAIシステムには、どれほどの価値があるのでしょうか？
AlphaGeometry は、Google DeepMind チームとニューヨーク大学の研究者によって共同開発されました。ニューラル言語モデルと記号演繹エンジンを組み合わせることで、複雑な幾何学問題を人間に近いレベルで解くことができる。
以前、国際数学オリンピック (IMO) の 30 の幾何学問題のベンチマーク テストで、AlphaGeometry は所定の時間内にそのうち 25 問を解決しました。 ソータ の「Wu メソッド」は 10 個の問題を解決しましたが、人間の IMO 金メダリストは平均 25.9 個の問題を解決できました。
確かに、AlphaGo の発売以来、さまざまな分野で多くの革新的な進歩が見られ、「DeepMind が開発した高品質の製品でなければならない」という位置づけが徐々に人々の心に根付いてきました。しかし同時に、業界内には合理的で弁証法的な声もあります。コンピューティング能力がインテリジェンスに取って代わることは喜ばしいことですが、実際の応用価値の方がより重要です。したがって、AlphaGeometry のリリースに伴い、これがコンピューティング能力の利点によるカーニバルなのか、それとも 科学のための AI 経路探索。
言及する価値があるのは、北京大学情報学院教授にインタビューしましたリン・ジョウチェン、関連する学術問題について議論し、研究しました。林周晨教授は、南開大学、北京大学、香港理工大学で数学と応用数学を学んだ後、北京大学数学学部に戻って博士号取得の勉強をし、人工知能の分野に参入し始めました。 (クリックすると林周晨教授の独占インタビューがご覧いただけます)
式と計算: 数学用 AI の 2 つの主要な課題
林周晨教授はこう語った。「これまで、AI が数学の定理を証明するには、数学の定理の「表現」と大規模計算が 2 つの大きな課題でした。 」
「まず第一に、非常に抽象的で論理的推論に大きく依存する主題であるため、数学が AI を受け入れるための最初のステップは、「式」の問題を解決することです。数学の定理をコンピューターが計算できる方法で表現することが、AI の基礎となります。その後の AI アプリケーション。 」
「AlphaGeometryが対象とする幾何学的問題を「表現する」ことの難しさは、数学の中でも最も低い部類に入ります。解析幾何学と代数幾何学の出現により、実際に幾何学的形状と幾何学的オブジェクトの関係を数値を使用して表現することが実現しました。加えて、ウー・ウェンジュンこの学者は 1970 年代に次のように提案しました。数学の機械化」と同様であり、ある程度までは、平面幾何定理と機械語との間に橋を架けることにもなります。 」
「第二に、学者の呉文君によって提案された「呉法」と伝統的なグレブナー基底法は、理論的には平面幾何定理の証明の問題を解決しましたが、計算能力によって制限されます。つまり、大量の記憶域と計算量が原因です。 , 特に、より難しい平面幾何学問題に直面すると、操作空間が指数関数的に増加するため、これまでの多くの方法では難しい問題を処理することが困難になります。 」
「大量の計算の問題は、明らかに資金力が豊富な DeepMind にとって主な障害ではありません。主な困難は、運用領域の指数関数的な増大をどのように回避するかです。現時点では、機械学習手法が役に立ちます。」 」
具体的には、AlphaGeometry は 1 億個の合成データでトレーニングされ、人間によるデモンストレーションなしで複雑な幾何学的課題を自律的に解決し、人間が読める証明を生成します。
下図に示すように、我が国の小中学生に最も馴染みのある「二等辺定理」を例にとると、∠ABC = ∠BCA を証明したい場合、問題を手動でコンピュータ言語に変換する必要があります。それを AlphaGeometry に入力します。
AlphaGeometry は、定理が証明されるか新しいステートメントが使い果たされるまで、定理の前提から新しいステートメントを「徹底的に」演繹する記号演繹エンジンを実行することによって証明検索を開始します。記号演繹エンジンが証明を見つけられなかった場合、言語モデルは補助点を構築し、証明可能な条件を追加し、記号エンジンを介して証明の検索を再開します。このサイクルは、解決策が見つかるまで続きます。
ソリューションは人間が読める言語に自動的に解析されるため、検証および評価できます。
AlphaGeometry はモデルのトレーニングに合成データを使用し、関連データベースの不足の問題を解決していることは言及する価値があります。
さまざまな確率定理の前提条件で既存のシンボリック エンジンを使用することにより、研究者らは 100,000 個の CPU を使用して 72 時間実行し、形式的な正規化と重複排除を経て、最終的に約 5 億の合成定理証明例を取得しました。そのうちの 100 万件には少なくとも 1 つの補助構造が含まれており、多くの証明には 200 を超えるステップがあり、これは国際数学オリンピックの幾何学問題の平均証明長の 4 倍です。
実際の問題を解決する AlphaGeometry の能力を比較テストするために、研究者たちは 2000 年以降の IMO コンテストでの幾何学的問題を、シンボリック エンジンで読み取り可能な機械語に変換しようとしました。その結果、75% のみが正常に表現できることがわかり、30 のテスト セット IMO- AG-30 は古典的な幾何学問題で構成されています。
導出閉包のサイズが異なるため、各問題の実行時間は異なります。研究者らは、実行時間は問題の難易度に相関がないことを発見しました。たとえば、IMO 2019 P6 は IMO 2008 P1a よりもはるかに難しいですが、IMO の制限時間内に解決するために必要な並列化時間ははるかに短くなります。
言語モデルのデコードプロセスは、k 個の代替補助構造を記述する k 個の異なるシーケンスを返すため、研究者らは、各ビームのスコアを値関数として使用して、k 個のオプションに対してビーム検索を実行しました。この方法は強力な並列性を備えており、並列コンピューティング リソースが利用可能な場合には検索速度を大幅に向上させることができます。
研究者らは、GPU V100 アクセラレーション言語モデルの 4 つの並列コピーを使用すると、25 の問題すべてを解決し、指定された時間内に収まるのに必要な並列 CPU の最小数が以下に示されることを発見しました。
IMO-AG-30 テスト セットの 10 の異なるモデル/メソッドのパフォーマンスを次の図に示します。興味深いことに、GPT-4 はテストで 1 問も正解できませんでした。
インテリジェンスに代わるコンピューティングパワーの背後では、アプリケーションの価値が焦点となります
過去 2 日間で、インターネット上のさまざまなレポートで、AlphaGeometry の影響について詳しく説明する必要がなくなりました。そのため、ノイズが去った後、AlphaGeometry が科学研究や AI アプリケーションの開発にどのような実用的な価値をもたらすことができるかを探っていきたいと考えています。 ？
この点に関して、林周晨教授は次のように述べています。現時点では、AlphaGeometry は AlphaGo のような「教師」となり、教育においてより大きな補助的な役割を果たすことができます。さらに、AlphaGeometry のモデル パフォーマンスにおける画期的な進歩は否定できず、「パワーは奇跡を生む」ことをさらに証明しています。つまり、強力なコンピューティング能力の利点が強力なモデル パフォーマンスを生み出し、これは強力な研究者や企業がコンピューティングの「支持」をある程度裏付けています。自信が加わりました。 」
しかし、林周晨教授は次のように述べています。AI の分野では、「インテリジェンスに代わるコンピューティングパワー」の有効性を何度も目撃してきましたが、最終的に業界の専門家を導いた最後の 1% のブレークスルーを AI で達成するのは依然として困難です。
したがって、現時点では、AlphaGeometry であれ、GPT モデルなどの他の AI ツールであれ、人々の日常生活や科学研究の仕事において、AI ツールを柔軟に使用することが一般的な傾向となっています。現実的な問題に対するコンピューティングパワーが生み出す「奇跡」は、代替困難な人間の価値です。
過去と現在の教訓から言えば、AI ツールの急速な台頭はコンピューターの普及と多くの類似点を持っています。たとえば、働き方の革命的な変化は急速に従来の方法に取って代わり、徐々に職場の能力の評価基準になりつつあります。対照的に、AI ツールの限界、つまり特異性もより顕著になります。
林周晨教授は次のように考えています。」現在のAIツールは統一性に欠ける数学という分野に限っても、学際的なAIツールはもちろんのこと、数論や幾何学向けに開発されたAIツールの間には大きな違いがあります。 AI ツールはまだ、今日のコンピューターのように簡単にアクセスできる基本的な基盤にはなっていません。現在のコンピュータ言語には、C言語、Java、Pythonなどが含まれます。これらの言語のいずれかに基づいて、数学、物理学、化学およびその他の分野の問題を解決することが可能です。これは、その多用途性を反映していますが、これはAIには当てはまりません。 Alpha シリーズを見てください。 」
したがって、Lin Zhouchen 教授は、「将来、AI ツールが抽象化されて再利用できるようになれば、科学用 AI が普及する可能性がある」と考えています。 」
これは、HyperAI が科学用 AI の開発プロセスを追跡し続けるときに観察した現象でもあり、一部の研究グループや研究チームは、自分の専門分野のメンバーに加えて、AI の開発を担当するメンバーを採用します。 AIは研究ツールとして必要ですが、科学の部分は依然として従来の科学研究者に任されています。
AI が科学研究プロセスをますます助け、改善し、新たなトレンドになりつつあることは疑いの余地はありませんが、この AI+科学チーム モデルは長期的な解決策となるのでしょうか?
リン・ジョウチェン教授は次のように考えています。「将来的には、科学担当者がさまざまな問題に対して AI ツールのコンポーネントを組み合わせて使用できるように、ある程度の統一性を達成するために AI ツールを使用するための敷居を下げる必要がある。一方、コンピューター プログラミングと同様に、科学担当者も AI の力を最大限に活用するために、AI ツールの使用能力を徐々に向上させる必要があります。」
道は閉ざされており、長いですが、道は近づいています。 DeepMind などの大手企業によって開始され、国家政策の推進と相まって、科学のための AI は、人類の発展に真の価値を生み出す前に、科学研究と産業界が協力して課題を解決する必要があります。その実装において。
最後に、この記事の執筆にあたりご協力とご協力をいただきました北京大学知能学院の林周晨教授に感謝いたします。リン・チョウチェン教授の研究グループは現在、博士課程の学生を募集しています。要件を満たす学生は、zlin@pku.edu.cn に履歴書を送ってください。
私の信条は、物理学者ルートヴィヒ・ポストマンの言葉です。「優れた理論ほど実用的なものはない」。私は現在、数学に強く（数学学部の出身である必要があるという意味ではありません）、理論分析に非常に興味のある博士課程の学生を募集しています。彼らが数学をエレガントに使って解く方法を私と一緒に楽しんでくれるでしょう。現実的な問題。遠慮なく履歴書を私に送ってください。
——林周晨