テレンス・タオの最新のスピーチが公開されたが、その AI コンテンツは桁外れだ。

IMO 2024では、「Tao Shen」がAIと数学をテーマに1時間にわたる魅力的なプレゼンテーションを行いました。

AIと数学の関係性について、彼はどのように考えているのでしょうか？機械学習、大規模モデル、その他数学分野における技術の応用と発展について、彼はどのように理解しているのでしょうか？

すべての観察と意見は留保なく共有されます。

AIの助けを借りれば、特定の種類の問題1,000件を同時に処理できる未来が想像でき、真に前例のない規模で数学の研究を始めることができるようになります。

さらに、「Tao Shen」では、古代から現在までの機械支援コンピューティングの伝統と進化についても語っています。

数学研究における AI やその他の機械の独創的な応用は根拠のないものではありません。

• ピタゴラスの数の問題はコンピュータでしか解くことができません。
• ケプラーの予想は最終的にコンピューターの支援によって証明されました。
• 結び目理論における機械学習の応用: 2 つの異なる統計データ間の関係を予測するのに役立ちます。

また、彼は問題解決のインスピレーションを見つけるためにGPT-4を使用し、証明の支援にGitHub Copilotを使用したことを明らかにしました。これにより、次のステップで正解に近い証明を記述できる確率が約 20% になりました。

テレンス・タオ氏はスピーチの中で AI について語るだけでなく、最近の投稿のいくつかも AI に密接に関連しています。

ネットユーザーはこれを推奨しています:

彼は AI の誇大宣伝を支持も反対もせず、むしろこれらのツールとその機能、そして将来何が起こるかを合理的かつオープンに評価しました。

QuantumBitはタオ・シェンの最新スピーチの内容を、元の意味を変えずにまとめ、編集しました。

「Tao Shen」は、機械支援コンピューティングの伝統について議論することから始まり、その後、おおよそ次のセクションを取り上げました。

• コンピュータの最も基本的な初期使用
• 科学計算における機械の応用
• 数学研究における機械利用の創造的な現代的手法：証明支援、機械学習、大規模言語モデル

機械支援による計算の伝統は古くから存在しています。

AIがあらゆるものを変えつつあるという話は、皆さんも耳にしたことがあるでしょう。少し前にDeepMindがAlphaGeometryをリリースしました。これは、IMOの幾何学に関するいくつかの疑問に答えられるようになりました。

これらのツールが数学の研究にどのような変化をもたらし始めたかについて、さらに詳しく説明します。

これは数学コンテストとは違います。数学コンテストでは、問題を解くのに3時間もかかりません。その代わりに、数ヶ月、あるいはそれ以上の時間がかかり、時には問題が解けないこともあり、その場合は問題を変更しなければなりません。求められるスキルには多少の共通点があるものの、数学コンテストとは全く異なるものです。

これらすべては非常に刺激的で、変革をもたらし始めています。しかし一方で、継続性も感じられます。私たちは長年にわたり、コンピュータや機械を使って数学的な計算を行ってきましたが、計算方法そのものの本質が変化しているのです。

しかし実際には、これは機械による支援の長年の伝統に従っています。

では、質問です。私たちはどれくらい前から機械を使って数学をやってきたのでしょうか？答えは数千年です。

これらはローマ人が数学に使っていた機械です。そろばんはその初期の例で、さらに古いものもありました。あまり知的な機械ではなかったため、少し退屈に聞こえるかもしれません。

コンピューターはどうですか？数学にコンピューターを使うようになってどれくらい経ちますか？300年から400年くらいです。ちょっと奇妙ですね。というのも、電子コンピューターが登場したのは1930年代か40年代になってからです。

電子計算機が登場する以前は、計算機は機械的なものであり、「計算機」という用語は計算を実行する人を指すこともあり、職業と考えられていました。

かつて、人類の「コンピュータクラスター」が存在し、人々は加算器を使って弾道計算などの計算を行っていました。計算能力の基本単位はCPUではなく、キルガール、つまり1,000人の女性が1時間でこなせる計算タスクの数でした。その間、男性は皆戦争に明け暮れていました。

コンピュータの最も基本的な用途は、スプレッドシートを作成することです。

先ほども申し上げたように、人々はコンピュータをかなり昔から使ってきました。実は 17 世紀、あるいはそれ以前から使われていたのです。

当時、コンピュータの最も基本的な用途は表を作成することでした。ネイピアの対数表について聞いたことがあるかもしれません。

正弦や余弦などを計算したい場合は、コンピュータを使ってこれらの表を作成します。高校ではこれらの表の使い方を今でも習いますが、最近は段階的に廃止されてしまいました。

もちろん、今では電卓や現代のコンピューターがあります。

私が言いたいのは、数学の研究ではテーブル（現在ではデータベースと呼ばれています）に依存していますが、それらは本質的に同じものであるということです。

数学における多くの重要な発見は、当初は表を通じてなされました。

例えば、数論における最も基本的な結果の一つは素数定理です。これは、大きな数xの前に何個の素数があるかを大まかに示しており、ルジャンドル、ガウスらによる発見とされています。

当時は証明できなかったものの、ガウスらは初期の計算機を用いて、この理論が正しいと推測しました。実際、ガウス自身も計算機のように動作し、表を計算したり、パターンを見つけようとしたりしました。

後にもう一つの重要な予想、バーチ・スウィナートン＝ダイアー予想が登場しましたが、ここでは詳細は割愛します。この予想も、曲線に関する膨大なデータテーブルを調べることで人間によって初めて発見されました。

現在、私を含め多くの数学者が使用している表は、いわゆるOnline Encyclopedia of Integer Sequences (OEIS) で、大量の数学的シーケンス データが収集されています。

「1、1、2、3、5、8、13」のような数字を見たことはあるかもしれません。これはフィボナッチ数列です。OEISは、このような数列を数千個収録したデータベースです。

数学の研究では、数学者は空間の次元や集合の濃度など、変数 n に依存する可能性のある自然発生的な数列に頻繁に遭遇します。

これらの数列の最初の5、6、または10個の数を計算し、OEISに入力して比較することができます。運が良ければ、この数列は既にOEISに存在しているかもしれません。おそらく、全く別の数学の問題の研究から得られたものでしょう。

このような発見は、2つの問題の間に関連性がある可能性を強く示唆するものであり、多くの研究がこの方向に始まっています。

科学計算における機械の応用

数学の分野における機械のもう一つの重要な応用は科学的計算です。

大規模な計算を実行する必要がある場合、多数の算術演算をコンピュータにオフロードします。この手法は1920年代から広く採用されてきました。

おそらく真に科学的な計算を行った最初の人物はヘンドリック・ローレンツでしょう。

オランダ人が巨大なダムを建設しようとしていて、水の流れがどのように変化するかを調べるよう彼に依頼したのを覚えています。彼らはモデルと流体方程式を構築する必要がありましたが、ローレンツは実際に人間の「コンピューター」の集団を使って、浮動小数点演算を用いてこの問題を解きました。

彼は、多くの人が大量の計算を迅速に完了させたいのであれば、様々なサイズの数値を表すために浮動小数点数を使うべきだと気づきました。もちろん、今では私たちはコンピューターを使ってあらゆるものをシミュレートしています。

多数の線形方程式や異なる方程式を解く場合、代数問題も解ける組み合わせ計算を実行する必要があるかもしれません。IMOで見られる幾何学的問題の多くは、原理的には科学計算によって解くことができます。

10 個の点といくつかの直線と円を含むような幾何学の問題を、20 個の実数と 20 個の未知数を含む連立方程式に変換し、それをSageやMapleなどのソフトウェアに入力できる代数ソフトウェア パッケージがあります。

ただし、問題のサイズが大きくなるにつれて、それを解決するための計算の複雑さが指数関数的または二重指数関数的に増大し、従来のコンピュータ代数ソフトウェア パッケージの処理能力を超える可能性があります。

そのため、最近まで、標準的なコンピュータ代数ソフトウェアパッケージのみを使用して、これらの問題を力ずくで解くことは不可能でした。しかし今、AIの支援により、状況は変化するかもしれません。

もう 1 つの強力なタイプの科学計算は、いわゆるSAT ソルバーであり、これは特定の論理パズルを解くために使用できます。

例えば、真か偽かのどちらかである1000個の文があり、3番目の文が真であれば6番目の文も真であり、7番目の文は必ず偽であることが分かっているとします。このような制約を複数指定すると、SATソルバーはこれらの情報をすべて用いて、これらの文のうちいくつかが真か偽かを証明できるかどうかといった結論を導き出そうとします。

SMTソルバーと呼ばれるより高度なバージョンもあります。変数x、y、zと法則に関するいくつかの仮定があれば、それらの法則とその他の事実を入力し、限られた仮定の範囲内で、簡潔かつ総当たり的に結論を導き出すことができます。

これらは非常に強力ですが、スケーラビリティも低いです。繰り返しになりますが、問題の複雑さによって計算時間が指数関数的に増加する可能性があるため、命題が約1000を超えると、これらのソルバーの実行は非常に困難になります。

しかし、コンピューターは実際にいくつかの問題を解決することができます。

たとえば、組み合わせ論への応用は成功例です。組み合わせ論は、人間が支援なしでは解決不可能な問題であり、おそらくコンピューターだけが解決できる問題だと考えています。

質問はピタゴラス三つ組（またはピタゴラス三つ組）に関するものです。

自然数が赤または青に色付けされている場合、ピタゴラスの三つ組 abc を含む色が常に存在するのでしょうか?

この問題はこれまで検証されておらず、メインフレーム コンピュータで計算された後に初めて解決されました。

これで、すべての自然数をチェックする必要がないことがわかりました。

1から7824までの自然数は2色に分けられますが、どちらにもピタゴラス数列は含まれません。しかし、1から7825までの自然数には必ずピタゴラス数列が含まれます。

これは当時世界最長の証明だったと思いますが、今では2番目に長い証明です。この証明にはCPUで4年間の計算時間を要し、最終的に200TBのデータを含む証明ファイルが生成されました。これは後に86GBに圧縮されました。

これはコンピューターを使用するかなり明白な方法です。

研究におけるコンピュータ活用の3つの創造的なアプローチ

近年、私たちはコンピューターをより創造的な方法で使い始めており、特にコンピューター同士を組み合わせたり、従来のデータベース、スプレッドシート、科学計算と組み合わせたりしています。

私たちは機械学習ニューラル ネットワークを使用して、人間とは異なる方法で新しいつながりを発見し、さまざまな種類の数学が関連する方法を見つけます。

最も注目すべきは、ChatGPT や Claude などの大規模言語モデルが自然言語対話を行うことができ、場合によっては問題に対する効果的な解決策を生成できることです。

数学者が使用するもう 1 つの手法は、形式的証明支​​援ツールです。

これらのツールは本質的にプログラミング言語です。コンピュータ言語を使って実行可能なコードを書くのと同じように、形式的証明支​​援系は物事をテストするために使われる言語です。議論が正しいかどうかを検証し、データから結論を導き出すのに役立ちます。

これらのツールは最近比較的使いやすくなっており、正式な証明支援ツールの助けがなければ不可能だった多くの興味深い数学プロジェクトに役立っています。

将来的には、私が言及した他のツールとうまく統合されるでしょう。

そこで、証明支援系から始めて、現代のコンピュータや機械を使用して数学の研究を行う方法についてお話ししたいと思います。

証明アシスタント

おそらく、最初の真のコンピュータ支援による証明は、四色定理の証明でした。

この定理は 1976 年に証明されました。つまり、隣接する領域が異なる色になるように、任意の地図を 4 色だけを使用して色付けできるということです。

△画像出典：Wikipedia

彼らの四色定理の証明は、本質的には国の数に関する帰納法です。巨大な地図があれば、そこには国のサブグラフが存在することを示す必要があります。彼らは約1,000から2,000の具体的なサブグラフを挙げており、巨大な国の地図はどれも、ある意味では少なくとも1つのこれらのサブグラフを含んでいるはずです。これは彼らが確認しなければならなかった点です。

次に、サブグラフをより単純なものに置き換え可能かどうかを確認します。その単純なものを4色で塗りつぶせるなら、メイングラフも塗りつぶせます。

単純化も行われ、これらのサブグラフをそれぞれチェックする必要があります。

これらのタスクの一部はコンピューターで実行できますが、他のタスクには何時間もかけて手動で検査する必要があります。

これは再検討が必要なプロセスだと私は考えています。面倒で不完全であり、小さな誤りが散見されます。現代のコンピュータ証明の基準からすると、これはコンピュータで検証できる証明ではありません。

この状況は、約 700 個のサブグラフを使用したより単純な証明が登場した 1990 年代まで変わりませんでした。

2005 年には、 Coq証明支援を使用して、完全に形式化されたコンピュータ検証可能な証明が実現されました。

最初の証明が現れることと、それを実際にコンピューターで完全に検証できることとの間には大きな隔たりがあることがわかります。

もう一つの有名な例は、球の最密充填に関する幾何学の問題、つまりケプラーの予想です。

ケプラーの予想によれば、三次元空間における球体の最も稠密な配置は面心立方（FCC）と六方最密（HCP）である。これらの2つの配置では、球体の体積は約74.048%を占め、これは考えられるすべての配置の中で最大となる。

△画像出典：Wikipedia

この積み重ね方法が最適かどうかをどのように判断すればよいでしょうか？これは特に難しい問題であり、人間にとって完全に理解可能な推測証明は存在しません。

問題は、球の数が無限にある場合、密度は漸近的な問題であり、先験的に有限な問題ではないため、コンピューターにそのまま投げて解決することはできないということです。

ただし、有限の問題に単純化することはできます。

積み重ねのプロセスが発生するたびに、空間はボロノイ領域と呼ばれる多面体に分割されます。球体のボロノイ多面体は、球の中心に最も近いすべての点からなる領域です。これらの多面体には比体積があり、面数と表面積を計算することで、これらの統計値を得ることができます。

1950年代、トスはある戦略を提案しました。彼は、有限個のボロノイ多面体の体積に基づく特定の重み付き不等式によって、球の充填密度の上限が得られることを観察しました。

これらの多面体の間に関係性を見出すことができます。例えば、ある多面体が非常に大きい場合、近くの多面体は非常に小さくなる可能性があります。そこで、ある多面体の体積と別の多面体の体積を結びつける不等式を見つけてみましょう。

多くの研究者がこの方法を試し、成功したと主張する者もいるが、決定的な証拠として受け入れられたものはない。

最終的に、この問題はトーマス・ヘイルズとその協力者によって解決されました。彼は基本的に同じ戦略を採用しましたが、多くの技術的な調整を加えました。

彼らはボロノイ単位をさらに精密に改良し、単に体積を測定するだけでなく、体積と複数の小さな一時的な調整を組み合わせた包括的なスコアを作成しました。彼の目標は、これらの異なるスコアの間に線形不等式を確立し、最終的に密度の上限を導き出し、最適な密度を正確に達成することでした。

このアプローチは非常に柔軟ですが、利用可能なオプションの数が非常に多いため、過度に複雑になる可能性もあります。

トーマス・ヘイルズと彼の弟子サミュエル・ファーガソンは、最小化問題を解く際に困難に直面するたびに、スコアリング関数を調整することでこれらの困難を回避できることに気付きました。関数はより複雑になり、変更のたびに長い時間がかかるようになりました。

さらに悪いことに、この機能は前回の論文の内容と若干互換性がないため、前回の論文に戻って修正する必要があります。

当初はコンピューターに頼る予定はなかったが、プロジェクトが複雑になるにつれて、処理にはコンピューターに頼らざるを得なくなった。

1998年、彼らはついにプロジェクトの成功を発表し、150個の変数を持つ慎重に選択された最適化問題から線形計画法を通じてケプラーの予想の証明を導き出しました。

証明には、250 ページのメモと 3 GB のコンピュータ プログラム、データ、および結果が含まれています。

この証明は審査過程で大きな困難に直面しました。いくつかの一流数学雑誌に提出され、審査には4年かかり、専門家委員会によって実施されました。

査読プロセスの最後に、彼らは証明の正確性については99%確信していると述べたが、コンピュータ計算の正確性は検証できなかった。彼らはこの点を明確にするために、公開された論文に脚注を追加するという非常に異例の措置を取った。その後、この脚注は削除された。

当時、コンピュータ支援による証明を正式な証明として受け入れるかどうかについては、かなりの議論がありました。今ではコンピュータ支援による証明に自信を持っていますが、論文が発表された後も、それが本当に証明と言えるのかどうかについては疑問が残りました。

したがって、これは根本原理に従って問題を完全に形式化する必要がある、真に注目を集めた最初の事例となるかもしれません。この目的のために、ヘイルズはProject Flyspeckと呼ばれる言語を開発しました。

当初、彼は証明を公式化するのに20年かかると見積もっていましたが、実際には21人の協力者の協力を得て、わずか12年で証明を完了しました。そして、その成果は2014年にようやく発表されました。

したがって、私たちは今、この結果に自信を持っています。

私たちは形式化のためのより良いワークフローを模索し始めました。プロセスはまだ面倒ですが、徐々に改善されています。

ピーター・ショルツは非常に優れた若手数学者であり、多くの業績、特に「凝縮数学」と呼ばれる数学の分野を創始したことで知られています。

この分野では、代数、カテゴリー理論、その他の代数ツールを利用して、従来は代数的手法では解決できなかった関数解析や関数空間理論の問題を解決します。

ショルツは、いわゆる凝縮アーベル群やベクトル空間を含む一連の圏を確立しました。彼の主張は、大学院の授業で学ぶ関数空間の分類はすべて不正確であるか、あるいは最も自然なものではないのに対し、彼が提案した分類はより優れた性質を持っているというものでした。

しかし、彼が証明しなければならない非常に重要な消失定理があります。この定理の証明には、特定の圏論群における高度に専門的な計算が伴います。したがって、この定理は彼の理論の基礎を成すものなのです。

彼はブログ記事でこの結果について論じ、定理の証明にほぼ狂気の沙汰となるほど1年間も執念深く取り組んだと述べています。最終的に証明は紙に印刷されましたが、誰も詳細を掘り下げようとはしなかったため、彼は依然として疑問を抱き続けました。

この定理により、この凝縮された公式を関数解析に適用することが正当化される。これは極めて基本的かつ重要なため、99.9%の確実性だけでは不十分である。

凝縮数学を研究している研究グループは世界中に数多くありますが、この定理を証明できた研究グループはまだありません。証明のプロセスは面白くないので、彼はこれが最も重要な成果かもしれないと言いつつも、その正確さを保証しなければならないと述べています。

その後、 Leanと呼ばれるより現代的なプログラミング言語が使用されるようになりました。

Leanは近年登場した言語です。これは、膨大な数学ライブラリの開発を目的としたクラウドソーシングプロジェクトです。このライブラリは、数学の基本公理からすべてを導出するのではなく、学部レベルの数学の授業で扱われる可能性のある基本的な群論や位相幾何学など、多くの中間結果を証明し、形式化しています。

しかし、この理論を定式化するために、多くの追加コンテンツを追加する必要がありました。数学ライブラリはまだ完成しておらず、調和代数や層理論など、ライブラリに追加する必要のある分野がまだ多く残っていましたが、彼らはわずか18ヶ月で定理を定式化しました。

証明は基本的に正しかった。いくつか小さな技術的な問題はあったものの、大きな誤りは見つからなかった。簡略化の手法はいくつか見つかったものの、技術的な手順が複雑すぎて形式化できなかったため、近道を探さざるを得なかった。

実際には、このプロジェクトの価値はもっと間接的です。

まず、Lean Mathライブラリを大幅に強化しました。現在、このライブラリは膨大な量の抽象代数を処理でき、以前の機能をはるかに超えています。さらに、ブループリントなどのサポートソフトウェアも構築されました。

50 ページにわたるような膨大な証明を形式化するのは非常に苦痛で、証明全体を暗記しなければなりません。

正しいワークフローは、まず大規模な証明を取り、それを数百の小さなステップに分解するブループリントを作成することです。各ステップは個別に形式化でき、その後、それらをすべて組み合わせます。チーム内の異なるメンバーが、異なるステップで証明の異なる部分を形式化できます。

このプロジェクトのもう一つの成果は、数万行に及ぶコードからなる正式な証明が得られたことです。現在、この証明を人間が読める形式に変換する作業が進められています。さらに、Leanなどの言語で書かれた証明を人間が読める形式に変換するためのツールも開発されています。

たとえば、人間が理解できる形式にうまく変換された位相幾何学の問題の証明を次に示します。

したがって、これらのテキストはすべて正式な証明からコンピュータによって生成されています。人間が書いた証明と似ており、同じ種類の数学言語を使用していますが、よりインタラクティブです。

どこをクリックしても、システムが現在の仮定、何を証明しようとしているのか、そして変数は何なのかを教えてくれます。ステップが短すぎる場合は、ステップを拡張してその起源を理解し、必要な公理を深く掘り下げることができます。

これは非常に良いイノベーションだと思います。将来の教科書はこのインタラクティブなスタイルを採用するでしょう。まずは形式化され、その後、既存の教科書よりもインタラクティブなバージョンが完成するでしょう。

これに触発されて、私自身も正式なプロジェクトを始めました。

昨年、私はティム・ガワーズ氏を含む数名と共同で、ある組合せ論の問題を解きました。その問題は「小さな倍加」特性を持つ二進ハミングキューブの部分集合に関するもので、この部分集合には特定のサイズ制約がありました。

私たちは比較的短い時間でそれを形式化し、その証明は約 33 ページになりました。

実際、これはおそらく、ショルツ プロジェクトで開発されたすべての設計図を活用し、約 20 人のチームによって 3 週間で完成された、これまでで最も速く形式化された実際の研究論文です。

したがって、証明タスクはよりオープンかつ共同作業的になり、美しい視覚化も得られます。

先ほども言ったように、まず最初にすべきことは、大きな定理を多くの小さな部分に分解することです。こうして得られた定理はPFRと呼ばれ、図の下部にある小さな円に対応します。

次に、他のすべての証明を導入すると、 PFR 証明はいくつかの以前の証明に依存する必要があります。

したがって、依存関係グラフが存在し、その色は形式化されているかどうかによって異なります。緑の円は形式的に証明されたもの、青の円は定義がすべて整っているなど、まだ形式的に証明されていないが形式化の準備が整ったもの、白の円は証明がまだ形式化されておらず、記述する必要があるものを表します。

したがって、このタスク ツリーが作成されます。このプロジェクトの優れた点は、この図のさまざまな部分で、これらすべての人が独立して共同作業できることです。

参加者の中には数学者どころかコンピュータプログラマーもいましたが、彼らはジグソーパズルのような小さな課題に驚くほど長けていました。全員が取り組めそうな円を選び、3週間でプロジェクト全体を完成させました。本当に刺激的なプロジェクトでした。

数学の分野では、通常これほど多くの人と共同研究することはありません。私がこれまで見た中では最大でも5人です。これは、大規模なプロジェクトで共同研究を行う場合、全員の計算が正しいと信頼する必要があるためです。そして、ある規模を超えると、それは不可能になります。

しかし、このようなプロジェクトでは、 Lean コンパイラーによって、コンパイルできないものはアップロードできないことが自動的にチェックされるため、これまで会ったことのない人々と共同作業を行うことができます。

これは、将来、数学の研究を行う上でますます一般的な方法になると思われる例です。

ツールは改良されて使いやすくなっていますが、それでもまだ使いにくく、一定レベルのプログラミングの専門知識が必要です。

一方、証明を修正する必要がある場合、たとえば、定理が元々 12 だった場合、その 12 を 11 に変更すると、定理は若干強化されます。

通常、これを行う場合は、証明全体を書き直すか、12 を 11 に置き換えてみる必要がありますが、そのプロセスで他のエラーがないか確認する必要があります。

しかし実際には、プロセスを形式化した後、12 を 11 に変更するのに数日しかかかりませんでした。どこかで 12 を 11 に変更しただけで、Lean によって 5 か所ほどでエラーが報告されました。

現在、実際にかなりの数の大規模な形式的証明プロジェクトが進行中です。その中でも最大のものは、フェルマーの最終定理をLean で形式化するために巨額の資金を受け取ったばかりのKevin Buzzardのプロジェクトでしょう。

彼はプロジェクトの最も重要な部分は完成までに 5 年かかるだろうと述べたが、全体が 5 年で完成できるとは主張しなかった。これは興味深いことだ。

したがって、これは形式的証明支​​援系の応用です。

機械学習

次に機械学習についてお話します。

機械学習はニューラルネットワークを用いて様々な問題の答えを予測し、多くの分野で応用できます。ただし、最初に説明したニューラルネットワークを用いて偏微分方程式の解を推測する方法については割愛します。

構造理論における機械学習の応用についてお話ししたいと思います。

結び目の理論は数学の非常に興味深い分野であり、数学のさまざまな分野をまとめたものです。

結び目とは、空間におけるロープまたは曲線の閉じた輪のことです。ある結び目を別の結び目に連続的に変化させる方法があり、その過程でロープが交差することが許されない場合、2つの結び目は同等とみなされます。

△画像出典：Wikipedia

したがって、結び目理論における根本的な問いは、「2つの結び目が等しいのはいつなのか？ 一方の結び目をもう一方の結び目に変換することは可能なのか？」です。

この問題を解決するための通常のアプローチは、いわゆる結び目不変量を開発することです。

これらは様々な数値であり、多項式を含む場合もあります。これらの数値や多項式を結び目に付与すると、結び目をどのように変形させても、これらの値は変化しません。したがって、2つの結び目の不変量が異なる場合、それらは同等であるとは見なされません。

結び目不変量には多くの種類があります。そのうちの一つはシグネチャ不変量と呼ばれ、結び目を平坦化して交差を計算し、それが上向きか下向きかなどを計算し、それに基づいて特定の行列を作成するなどできます。

ジョーンズ多項式やアレクサンダー多項式など、数学の多くの分野に関連する有名な多項式がいくつかあります。

もう 1 つのタイプは、幾何学に由来する、いわゆる双曲不変量です。

結び目の補空間、つまり双曲空間を取ることができます。これは特定の幾何学的構造と距離の概念を持ち、体積やその他の不変量を保存できます。したがって、これらの不変量は実数または複素数であり、それぞれの結び目は、符号、双曲幾何学的不変量など、いくつかの組み合わせ不変量を持ちます。

さまざまな双曲変数を持つ一連の結び目があり、そのいくつかは双曲体積などと呼ばれます。

結び目に関する統計を生成するための 2 つの異なる方法が存在することは知られていますが、これまで 2 つの方法の間に何らかの関連性や共通点を見つけることはできませんでした。

最近まで、人々はこの問題を解決するために機械学習を使い始めました。

彼らは数百万の結び目を含むデータベースを作成し、このデータベースを用いてニューラルネットワークを学習させた。その結果、学習済みのニューラルネットワークは双曲幾何学的不変量をすべて利用し、約90%のケースでシグネチャを正しく予測できることが示された。

そこで彼らはブラックボックスを作成しました。このブラックボックスは、署名が何らかの形でこれらの幾何学的変数の中に隠されていることを示していますが、それがどのように行われているのかは教えてくれません。それでもなお、このブラックボックスは有用です。なぜなら、一度手に入れれば、自由に操作できるからです。

彼らが次に行ったのは、実は非常に単純な有意性分析でした。このブラックボックスは約20種類の異なる入力を受け取り、そのうちの1つが変数の型です。そして、結果、つまりシグネチャを出力します。

その結果、20 の入力のうち、経度変換と子午線変換の実数部と複素数部を含む 3 つだけが実際に出力に重要な役割を果たしていることがわかった。

どの変数が最も重要であるかが分かれば、署名をこれら 3 つの特定の入力と直接比較し、人間の判断によって結果が決定されます。

彼らはこれらのチャートを観察して推測を立てましたが、それは間違いであることが判明し、実際にニューラル ネットワークを使用してその間違いを証明しました。

彼らは失敗を通して、この現象を説明する正しい命題である修正版を提唱しました。これにより、シグネチャがこれらの特定の統計と非常に密接に関連している理由を理論的に説明できるようになりました。

これは、数学における機械学習の応用が拡大している傾向を反映していると思います。機械学習は問題を直接解決することはできませんが、データと研究の方向性との潜在的な関連性を示唆する多くの貴重な手がかりを提供することができます。しかし、こうした関連性を確立するには、依然として人間の介入が必要です。

大規模言語モデル

最後に、大規模言語モデルがあります。これは最も魅力的で、おそらく最もニュース価値のあるものです。ニューラルネットワークは20年ほど前から存在し、言語モデルは約5年ほど前から存在していますが、人間と同等の出力レベルに達したのはごく最近のことです。

你们可能都听说过GPT-4。GPT-4发布时，有一篇非常著名的论文描述了它的能力，并且它确实匹配这些能力。

这是一个来自2022年IMO的稍微简化版本的问题，对于这个特定的问题，系统给出了一个完整且正确的解决方案。

但这是一个精选的例子，他们测试了数百个IMO级别的问题，成功率大约是1% 。所以他们能够解决特定的问题，且必须以正确的方式格式化问题才行。尽管如此，这仍然非常了不起。

另一方面，这些工具的有趣之处在于，人类觉得困难的事情，AI有时可以很容易地做到，但人类觉得容易的事情，AI经常会表现很糟糕，这是一种非常正交的解决问题的方式。

在另一篇论文中，他们要求模型做一个基本的算术计算“7×4+8×8”，模型的答案是120，但当它逐步解释时，又得出了答案是92。这说明，虽然AI在某些情况下能找到正确答案，但处理过程并不总是准确无误。

因此，人们正在尝试各种方法，将这些模型与更可靠的软件连接，不需要自己做计算，可将计算任务交给Python。

你还可以强制模型只产生正确的答案，只在一种证明助手语言中输出，如果它无法编译，你就将其退回给AI，AI必须重新尝试。或者你可以直接教它做IMO题的技巧，比如尝试简单的例子，矛盾证明等。

所以人们正在尝试各种方法，虽然还没有能力解决大多数数学问题，更不用说数学研究问题，但目前正在取得进展。

除了直接解决问题外，它们还可以作为灵感来源，我自己也使用过这些模型，尝试过各种问题。

有一个问题，GPT-4给我推荐了10种方法，其中5种我已经尝试过明显无效，但有一种之前我没注意到的技术是生成特定问题的函数，我意识到这是正确的方法。所以，它在某种程度上是有用的，现在还不完美，但也不是完全无用。

还有另一种AI辅助实际上对证明助手非常有用。

正如我所说，编写形式化证明是一项非常繁琐的任务。这就像计算机语言一样，你必须准确无误地编写语法，如果漏掉一个步骤，它就无法编译。

我使用了一个叫做GitHub Copilot的工具，你可以写下一半的证明，它会尝试猜测下一行是什么。大约20%的猜测是接近正确的，然后你可以接受它并继续。

在这个例子中，我试图证明这里的命题，灰色行是Copilot建议的内容。结果显示第一行是无用的，但第二行有用。因此，你不能仅仅接受输入，因为它不一定能编译通过。

但是，如果你已经大致了解代码的工作原理，这将为你节省大量时间。

现在还有实验在尝试让AI提出一个证明方案，然后你将其反馈给编译器，如果编译错误，你就将错误信息反馈回去。

我们已经开始尝试证明那些四五行长的内容，可以通过这种方法进行约束。当然，像数千行的大型证明还远远不能立即形式化，但它已经是一个有用的工具了。

目前机器发展处于哪一阶段？

それで、私たちは今どこにいるのでしょうか?

有人希望在未来几年内我们可以使用计算机直接解决数学问题，我认为我们距离这一目标还很远。

对于非常狭窄的问题，你可以设置专门的AI来处理一小部分问题。但即便如此，它们也不是完全可靠的。它们可能有用，但仍然有限。

至少在未来几年里，它们主要还是用于辅助，不只是我们熟悉的蛮力计算辅助，人们正在尝试各种创新方法，希望AI能够非常擅长生成有见地的猜测。

我认为这是一个特别令人兴奋的方向。

我们已经看到了关于结的一个小例子，AI已经能够猜测两种不同统计数据之间的联系。因此，你只需创建这些庞大的数据集并将它们输入到AI中，它们就会自动生成不同数学对象之间的许多有价值的联系。

我们还没有真正知道如何做到这一点，部分是因为我们没有这些大型数据集，但我认为这最终是可能做到的。

证明定理是一个痛苦且费时的过程，我们通常一次只能证明一个定理，或者如果效率高的话，可能是两个或三个。但是借助AI，你可以想象将来不仅仅是试图解决一个问题，而是取一类1000个问题，然后对AI说：“好的，我要求你用这种技术来解决这1000个问题。”

使用这种技术，我能解决多少问题？如果我结合它们，我能做到什么？你可以开始探索问题的空间，而不是单独解决每个问题。

这是一个需要几十年时间，通过成百上千篇论文慢慢摸索各种技术能做什么、不能做什么的过程。

但有了这些工具，你真的可以开始以一种前所未有的规模进行数学研究。

因此，未来将非常令人兴奋。我的意思是，我们仍将以传统方式证明定理。事实上，我们必须这样做，因为如果我们自己不知道如何操作，我们将无法指导这些AI。但我们将能够做很多我们现在无法做到的事情。

参考链接： [1]https://www.youtube.com/watch... [2]https://www.reddit.com/r/sing...\_tao\_says\_ai\_could\_solve\_mathematical/