テレンス・タオ「いいね！」 ChatGPT は自動的に大きな進歩を証明し、10 年後には AI が数学の世界を支配するでしょう

**出典:**新志源

**ガイド:**多くの人は認めたくありませんが、10 年以内に AI が人間の数学者を追い越す可能性は非常に高いです。

数日前、カリフォルニア工科大学とマサチューセッツ工科大学の研究者らによる、数学の定理を証明するために ChatGPT を使用した論文が爆発的に広まり、数学界で大きな注目を集めました。

Nvidia の主任科学者であるジム・ファン氏は、AI 数学のコパイロットが登場し、次に新しい定理を発見する人は完全に自動化された AI 数学者になるだろうと興奮気味に伝えました。

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

そしてTao Zhexuan自身がこの記事を再投稿しました。

Siobhan Roberts は、Machine Assisted Proofs が開催した今年の IPAM ワークショップに参加し、その後、彼女自身の経験とインタビューに基づいて AI と数学に関するこの記事を書きました

**AI も数学の世界を破壊するためにやって来ます! **

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

元グーグル社員で現在はベイエリアの新興企業で働くコンピューター科学者のクリスチャン・セゲディ氏は2019年、コンピューターシステムは10年以内に最高の人間の数学者の問題解決能力と同等、あるいはそれを超えるだろうと予測した。同氏は昨年、目標時期を２０２６年に修正した。

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

2018 年のフィールズ賞受賞者でプリンストン高等研究所の数学者であるアクシャイ・ヴェンカテシュ氏は、現在 AI の使用には興味がありませんが、AI 関連のトピックについて議論することに非常に熱心です。

昨年のインタビューで、ヴェンカテシュ氏は「この分野は大きく変わろうとしているということを学生たちに理解してもらいたい」と語った。

そして最近の彼の態度は、「人間の理解を助けるためにAIを意図的に、さらには意図的に使用することに反対はしません。しかし、AIの使用方法については十分に注意し、慎重になる必要があると強く信じています。」です。

今年2月、UCLAの理論応用数学研究所は「機械支援証明」に関するワークショップを開催した。

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

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

AI による数学的美学の破壊であれ、数学者自身への脅威であれ、数学者が AI の潜在的な脅威について心配し始めたのは近年のことです。

そして、優れたコミュニティのメンバーがこれらの問題を俎上に上げ、「タブーを破る」方法を模索し始めています。

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

ユークリッド幾何学プリミティブからコンピューター コードまで

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

ロサンゼルスのゲッティ美術館に所蔵されている 17 世紀のギリシャの数学者ユークリッドの肖像画: 彼はぼろを着て、幾何学に関する論文「元素」を掲げている

2,000 年以上にわたり、ユークリッドのテキストは数学的な議論と推論のパラダイムでした。

カーネギーメロン大学の論理学者ジェレミー・アビガド氏は、ユークリッドは当時の数学を構築するためのほとんど詩的な「定義」から始まったと述べ、基本的な概念、定義、以前の定理を使用して、それぞれの連続した手順をすべて「明らかに踏襲」していると述べた。物事を証明するような方法。

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

しかし 20 世紀以降、数学者はもはやこの直感的な幾何学的基礎に基づいて数学を構築しようとはしませんでした。

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

最終的には、そのようなシステムの下では、数学がコンピューターコードに変換される可能性があります。

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

4 色定理: 隣接する 2 つの領域が同じ色にならないようにマップを塗りつぶすには、4 つの色で十分です。

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

Proof Assistant または Interactive Theorem Prover と呼ばれるそのような数学ガジェットがあります。

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

検証プロセスは動的仕様参照ライブラリに蓄積され、他の人が利用できます。

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

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

Lean は、現在 Amazon のコンピューター科学者である Leonardo de Moura によって Microsoft 在籍中に開発されました。

Lean は、ロジックにインスピレーションを得た象徴的な AI である昔ながらの AI GOFAI を活用した自動推論を使用します。

これまでリーンは、球を裏返しにする興味深い定理と、数学領域全体のスキームを統一する重要な定理を検証しました。

ただし、証明アシスタントには欠点もあります。数学者が入力した定義、公理、または推論手順が理解できないと頻繁に不平を言うため、「証明不平不満者」とも呼ばれます。

フォーダム大学の数学者ヘザー・マクベス氏は、こうした不満があると研究は面倒になるが、一行ごとにフィードバックを提供する機能があれば、このシステムは教育にも役立つだろうと述べている。

この春、マクベス博士は「バイリンガル」コースを設計しました。彼女は黒板に書かれたすべての問題を講義ノートのリーンコードに翻訳し、学生はリーン言語と自然言語で解決策を提出する必要がありました。

マクベス博士は、証明がいつ完了したか、そして途中の各ステップが正しいか間違っているかについて即座にフィードバックを受け取ることができるため、「彼らに自信を与えた」と語った。

そして、ジョンズ・ホプキンス大学の数学者エミリー・リール氏は、ワークショップに参加した後、それを試してみました。

ジョンズ・ホプキンス大学の数学者エミリー・リール氏は、実験証明アシスタントを使用しています。

彼女は証明アシスタント アプレットを使用して、以前に公開した記事の定理を証明しました。

それを使用した後、彼女はショックを受けました。 「証明のプロセスをこれまでよりもずっと深く理解できるようになりました。私の思考は非常に明晰なので、どんなに愚かなコンピューターでも説明できるようになりました。」

数学形式化サマースクール中に学生が参加したグループプロジェクト

暴力的な推論 - これは「数学的」ではありません

コンピューター科学者がいくつかの数学的問題を解決するためによく使用するもう 1 つのツールは「暴力的推論」と呼ばれますが、数学コミュニティはこの方法を嘲笑することがよくあります。

しかし、AI 科学者は数学者の考えをあまり気にしていないようで、独自の使い慣れた方法を使用して数学の「高地」を捉え続けています。

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

「Nature」誌は記事の中で「200T の証明は史上最大の証明プロセスである。問題を解決するためにこれらのツールを使用するのは本当に数学なのか?」と述べています。

しかし、この問題を解決するための論文を自ら執筆したコンピューター科学者のヒューレ氏の見解では、「人間の能力の範囲を超えた問題を解決するには、このアプローチが必要である」という。

同様に、DeepMind はチェスのゲーム (AlphaZero) で人間に勝利した後、タンパク質のフォールディング (AlphaFold) を解決する機械学習アルゴリズムを設計しました。

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

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

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

将来的には、このプロジェクトが一般研究助手として「数学の問題を独立して解決」できる「自動数学者」に成長することを期待しているという。

数学はリトマス試験紙です

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

彼らは、人工知能技術は多くの場合、数学者が望む答えを「見つける」のに「直接」役立つと信じています。

ただし、数学者や AI の専門家には、AI がどのようにしてこの答えを見つけたのかわかりません。

DeepMind と協力したことがある数学者のジョーディ ウィリアムソンは、かつて DeepMind と協力した経験を共有しました。

DeepMind との協力の過程で、DeepMind が発見したニューラル ネットワークは、彼が非常に重要だと考えるデータ値を非常に正確に予測できます。

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

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

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

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

テクノロジーの世界では、ほとんどの場合、問題の解決策を提供するブラックボックスがあれば、テクノロジーの世界は完全に満足するでしょう。

AIというのはまさにブラックボックスです。

しかし数学者はこの状況に満足していません。

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

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

AI が数学の定理を証明できたら

AI が生成した仮説が世界に溢れたら、私たちはどうするでしょうか?

これに対してネチズンは魂の拷問を送ったが、DeepMindがすでに結び目理論でそれを行っているため、AIシステムの最初のステップとしての新しい仮説/公式には疑問を持っている。

AI が出力する新たな仮定の洪水に、コミュニティはどのように反応するのでしょうか。 AI によって作成された論理的な議論をチェックすることと、何百万もの「ああ、これは真実かもしれない」という提案に圧倒されることは別のことです。私たちの既存のレビューおよび出版システムがこれに対応する準備ができているとは思いません。

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

機械がすぐに数学を実行できるようになるわけではないと主張されているが、機械学習モデルと計算能力が生物学の分野を変えたのと同じように、研究のやり方も変わると考えられる。

一部のネチズンは、AlphaDev以来、この問題について考えてきたが、同じプログラムで並べ替えアルゴリズムを構築でき、自動証明チェッカーを使用して数学的定理を証明することもできると述べました。本当の問題は、それが単なる些細な発見ではなく、何か重要なことを証明するために使用できるかどうかです。

しかし、一部のネチズンは、GPT のようなツールが本当に貴重な真実を発見できるかどうかについて、依然として懐疑的です。

一部のネチズンはまた、「数学の理解と注意において、人間とAIには違いがあるのではないか。AIは何が真実であるかを証明するが、人間は常にそれが真実である理由に焦点を当てているのではないか」と指摘した。

参考文献: