Terence Tao さんがリポストして「いいね！」しました！ ChatGPTは自動的に大きな進歩を証明し、AIは10年後に数学の世界を支配するだろう

数日前、Caltech と MIT の研究者が ChatGPT を使用して数学の定理を証明した論文が話題となり、数学界で大きな注目を集めました。

写真

Nvidiaの主任科学者ジム・ファン氏は興奮気味にこの投稿を転送し、「AI数学コパイロットが登場し、次に新しい定理を発見するのは完全に自動のAI数学者になるだろう」と述べた。

ニューヨークタイムズも最近、AIが10年以内に人間の最高の数学者に追いつくか、あるいは追い越すだろうから、数学者は備えておくべきだという記事を掲載した。

写真

そして、テレンス・タオ自身もこの記事を転送しました。

写真

シボーン・ロバーツは、今年のIPAMワークショップにマシン・アシスト・プルーフズが参加し、自身の経験とインタビューに基づいてAIと数学に関するこの記事を執筆しました。

AIは数学の世界も覆すことになる！

今日、数学者は最新の革命的な力である AI に立ち向かわなければなりません。

2019年、元Googleで働き、現在はベイエリアのスタートアップ企業で働くコンピューター科学者のクリスチャン・セゲディ氏は、コンピューターシステムが10年以内に最高の人間の数学者の問題解決能力に匹敵するかそれを上回るだろうと予測した。昨年、彼は目標日を2026年に修正した。

カーネギーメロン大学の論理学者ジェレミー・アビガド氏（青）と形式数学サマースクールの学生たち。

プリンストン高等研究所の数学者で、2018年のフィールズ賞を受賞したアクシャイ・ベンカテシュ氏は、現在はAIの利用には興味がないが、AI関連の話題について議論することには非常に熱心だ。

昨年のインタビューで、ベンカテシュ氏は「この分野が劇的に変化していくことを学生たちに理解してもらいたい」と語った。

彼の最近の姿勢は、「人間の理解を助けるために AI を思慮深く、意図的に使用することには反対しません。しかし、AI をどのように使用するかについては、注意深く慎重になる必要があると強く信じています。」というものです。

今年2月、カリフォルニア大学ロサンゼルス校の理論応用数学研究所が「機械支援による証明」に関するセミナーを開催した。

写真

このセミナーの主催者は、2006年のフィールズ賞受賞者であり、UCLAに勤務する数学者テレンス・タオ氏です。

彼は、数学の証明を支援するために AI を使用することは、実際には大いに注目に値する現象であると指摘しました。

数学者が、AI が数学の美学を破壊するという点でも、数学者自身に脅威を与えるという点でも、AI の潜在的な脅威を懸念し始めたのは近年になってからのことである。

優れたコミュニティメンバーはこれらの問題を議論に持ち込み、「タブーを破る」方法を模索し始めています。

サマースクールの主催者、左から右へ：アビガド、パトリック・マソ、ヘザー・マクベス

ユークリッドの原論からコンピュータコードまで

何千年もの間、数学者は論理と推論の最新の進歩に適応してきました。しかし、彼らは人工知能の準備ができているのでしょうか?

写真

ロサンゼルスのゲティ美術館にある 17 世紀ギリシャの数学者ユークリッドの肖像画。ぼろぼろの服を着て幾何学の論文『原論』を掲げている。

ユークリッドの著作は 2,000 年以上にわたって、数学的な議論と推論のパラダイムとして機能してきました。

ユークリッドは、ほとんど詩的な「定義」から始めて、それを基に当時の数学を築き上げた。つまり、基本概念、定義、以前の定理を使って、それぞれの後続のステップが前のステップから「明らかに続く」ような方法で物事を証明したのだ、とカーネギーメロン大学の論理学者ジェレミー・アビガド氏は言う。

写真

ユークリッドの「明白な」ステップのいくつかはそれほど明白ではないと不満を言う人もいるが、アビガド博士は、そのシステムは機能すると述べた。

しかし、20 世紀以降、数学者はもはやこの直感的な幾何学的基礎の上に数学を築こうとはしなくなりました。

代わりに、彼らは正確な記号表現と機械的な規則を備えた正式なシステムを開発しました。

写真

https://kilthub.cmu.edu/articles/journal_contribution/A_Formal_System_for_Euclid_s_Elements/6490703

最終的には、このシステムにより、数学をコンピューター コードに変換できるようになります。

写真

1976 年、四色定理は総当たり計算の助けを借りて証明された最初の主要な定理となりました。

4色定理: 4色あれば地図を塗りつぶすのに十分であり、隣接する2つの領域が同じ色になることはない。

不満を言うAI: 申し訳ありませんが、あなたの定理は理解できません

証明補助装置、または対話型定理証明器と呼ばれる小さな数学ツールがあります。

数学者は証明を段階的にコードに変換し、ソフトウェア プログラムを使用して推論が正しいかどうかを確認します。

検証プロセスは、他のユーザーが参照できる動的な仕様参照ライブラリに蓄積されます。

写真

https://www.andrew.cmu.edu/user/avigad/Papers/formal_turn.pdf

ホスキンソン形式数学センター所長のアビガド博士は、ユークリッドが当時の数学をトランスコードしようとして基礎を築いたのと同じように、この種の形式化が今日の数学の基礎を築いたと述べた。

最近、オープンソースの証明支援システム Lean が再び注目を集めています。

写真

Lean は、現在 Amazon に勤務するコンピューター科学者の Leonardo de Moura 氏が Microsoft に在籍していたときに開発されました。

Lean は、ロジックにヒントを得たシンボリック AI である GOFAI と呼ばれる旧式の AI を活用した自動推論を使用します。

写真

これまでに、リーンは球体を内側から外側に回転させるための興味深い定理と、数学の分野を統一するための重要な定理を検証しました。

写真

写真

写真

写真

しかし、証明支援システムにも欠点があります。数学者が入力した定義、公理、または推論手順を理解していないと文句を言うことがよくあるため、「証明不平屋」とも呼ばれています。

こうした苦情は研究を煩雑にする可能性があるが、行ごとのフィードバックなどの機能により、このシステムは教育にも役立つ可能性があると、ノースカロライナ州ダーラムのフォーダム大学の数学者ヘザー・マクベス氏は言う。

写真

https://leanprover-community.github.io/courses.html

この春、マクベス博士は「バイリンガル」コースを設計しました。このコースでは、黒板上の各問題を配布資料の Lean コードに翻訳し、学生は Lean と自然言語の両方を使用して解決策を提出することが求められました。

写真

https://hrmacbeth.github.io/math2001/

「これにより、生徒は自信を持てるようになります」とマクベス博士は言う。なぜなら、生徒は証明が完了したかどうか、またその過程の各ステップが正しかったか間違っていたかについて即座にフィードバックを受けるからである。

セミナーに参加した後、ジョンズ・ホプキンス大学の数学者エミリー・リール氏もそれを試してみた。

写真

ジョンズ・ホプキンス大学の数学者エミリー・リールは、実験的な概念実証プログラムを使用して、

彼女は、以前に発表した論文の定理を証明するために証明支援アプレットを使用しました。

それを使用した後、彼女はショックを受けました。 「私は今、以前よりもずっと深く証明を理解しています。私の考えは非常に明確なので、最も愚かなコンピューターにも説明できます。」

写真

学生たちは数学形式化に関するサマースクール中にグループプロジェクトに参加した。

力ずくの推論 - これは「数学的」ではない

コンピューター科学者が数学の問題を解くためによく使用するもう 1 つのツールは、ブルート フォース推論と呼ばれますが、数学界ではこのアプローチがしばしば嘲笑されます。

しかし、AI科学者は数学者の考えをあまり気にしていないようで、数学の「高み」を征服するために、自分たちが使い慣れた方法を使い続けている。

2016 年、カーネギーメロン大学のコンピューター科学者である Heule 氏は、200T の「SAT ソルバー」ファイルを使用して「ブール ピタゴラスの 3 倍問題」を解きました。

写真

https://cacm.acm.org/magazines/2017/8/219606-the-science-of-brute-force/fulltext

しかし、ネイチャー誌の記事では、「200T の証明は歴史上最大の証明プロセスです。これらのツールを使って問題を解くのは本当に数学なのでしょうか?」と述べられています。

写真

しかし、この問題を解決した論文を書いたコンピューター科学者のヒューレ氏は、「このアプローチは人間の能力を超えた問題を解決するために必要だ」と考えている。

写真

同様に、DeepMind はチェスで人間に勝利した後 (AlphaZero)、タンパク質の折り畳みを解く機械学習アルゴリズムを設計しました (AlphaFold)。

DeepMind は、これらの結果を達成した方法は、AI を使用して人間の直感を導き、数学を進歩させることであったと主張する論文を発表しました。

写真

https://www.nature.com/articles/s41586-021-04086-x

元グーグルのコンピューター科学者で、現在はベイエリアで起業しているユーフアイ・ウー氏も、自身のビジネスの方向性は機械学習を使って数学の問題を解くことだと語った。

写真

彼の現在のプロジェクトである Minerva は、数学モデルを解くための微調整された大規模言語モデルです。

将来的には、このプロジェクトが「数学の問題を自力で解く」ための総合的な研究アシスタントとして機能できる「自動化された数学者」へと成長することを彼は期待している。

写真

数学は試金石である

一方、AI技術に深く関わってきた数学者の多くは、数学研究においてAIが真剣に受け止められていないことに懸念を表明している。

彼らは、人工知能技術が数学者が求める答えを「見つける」のに「直接」役立つことが多いと信じている。

数学者や AI の専門家は、AI がどのようにこの答えを見つけるのか確信が持てません。

DeepMind で働いた経験のある数学者のジョーディ・ウィリアムソン氏は、かつて DeepMind で働いた経験について語ったことがあります。

DeepMindとのコラボレーション中に、DeepMindは、彼が重要だと考えたデータ値を非常に正確に予測できるニューラルネットワークを発見しました。

写真

彼は AI がそれをどのように実行したかを理解しようと懸命に努力しました。これは定理の基礎となる可能性があるからです。

しかし結局、彼はAIのロジックを理解できず、DeepMindの人々も同様でした。

ユークリッドと同様に、ニューラル ネットワークは何らかの方法で真実を見つけますが、その論理的な理由は理解しにくいものです。

一方、この数学者の観点から見ると、推論は数学の本質ですが、機械学習では常にパズルの欠けているピースでした。

技術界では、ほとんどの場合、問題の解決策を提供できるブラックボックスがあれば、技術界は非常に満足するでしょう。

AIはまさにブラックボックスです。

しかし、数学者たちはこの状況に満足していない。

この数学者にとって、ニューラル ネットワークがどのように機能するかを理解しようとすると、興味深い数学的な疑問が生じます。

これらの問題を解決することで、数学者は「世界に有意義な貢献」をすることができるようになる。

AIが数学の定理を証明できたらどうなるでしょうか?

AIが生成した仮説が世界に溢れたら私たちはどうすればいいのでしょうか？

ネットユーザーはこれについて、内省的な疑問を投げかけています。AI システムの新しい仮説や公式を提案することが最初のステップであるとは思えません。なぜなら、DeepMind はすでに結び目理論でこれを行っているからです。

AI が出力する新たな仮説の洪水にコミュニティがどのように反応するのか興味があります。 AI によって作成された論理的議論を確認することと、「ああ、それは本当かもしれない」という提案が何百万も押し寄せてくることは別の話です。現在のレビューおよび出版システムはこれに対応できていないと思います。

これは人々の数学への信頼にどのような影響を与えるのでしょうか?

写真

機械がすぐに数学の研究を行えるようになることはないと主張する人もいるが、機械学習モデルと計算能力が生物学の分野を一変させたのと同じように、機械が研究のやり方を変えることはあり得るだろう。

写真

別のネットユーザーは、「AlphaDev の頃からこの問題について考えていたが、同じプログラムでソートアルゴリズムを構築でき、自動証明チェッカーを使って数学の定理を証明することもできる」と述べた。本当の問題は、それが単なる些細な発見ではなく、何か重要なことを証明するために使用できるかどうかです。

写真

写真

しかし、一部のネットユーザーは、GPT のようなツールが本当に価値ある真実を発見できるかどうかについて依然として懐疑的です。

写真

一部のネットユーザーは、人間とAIの数学に対する理解と関心には違いがあるかもしれないと指摘した。AIは真実を証明しますが、人間は常になぜそれが真実なのかに焦点を当てています。