テレンス・タオの論文の抜け穴をAIが発見。定理の名前から研究の方向性を推測。専門家はAIの能力はすごいと語る

最近、GPT-4 と Copilot を研究に積極的に使用している数学の専門家 Terence Tao 氏が、AI の助けを借りて論文に隠されたバグを発見しました。

Terence Tao 氏は、6 ページの議論を Lean4 を使用して形式化していたときに、 n=3、k=2 のときに式が実際には発散することを発見したと述べています。

この見つけにくいバグは、Lean4 のおかげで、すぐに発見されました。

その理由は、Lean は 0<n−3 を構築することを要求しますが、Tao は n>2 のみを想定しているからです。したがって、負の0<n−3に基づいてLeanを反証することはできません。

幸いなことに、これは n の値が非常に小さい場合にのみ存在する小さなバグです。この時点では、論文内のいくつかの定数を変更するだけで済みます。

この投稿で、数学愛好家のファンの中には、「これはすごい。AI証明アシスタントが普及し、数学研究の将来に向けてより強固な基盤が築かれるのは素晴らしいことだ」と叫ぶ人もいました。

そしてテレンス・タオ氏は、これは完全に可能だと語った。

おそらく近い将来、Lean の上に AI レイヤーを構築できるようになるでしょう。

証明の各ステップが AI に記述されている限り、AI は Lean を使用して証明を実行し、その過程でさまざまなコンピュータ代数ソフトウェア パッケージを呼び出すことができます。

今年 6 月、Terence Tao 氏は自身のブログで GPT-4 の経験について次のように予測しました。

2026 年には、AI は検索および記号数学ツールと統合され、数学研究における信頼できる共著者になります。

この期間中、人々はこの点を証明し続けました。たとえば、カリフォルニア工科大学、NVIDIA、MIT などの機関の学者は、オープンソースの LLM に基づく定理証明器を構築しました。

Terence Tao 氏も、GPT-4 を使用して新しい論文を執筆することで模範を示しており、「GitHub Copilot の驚くべき機能に不安を感じています」と繰り返し述べています。

AIは優れた数学研究者を助ける

過去 1 か月で、テレンス・タオは完全に AI に「はまって」しまいました。

GPT-4 の助けを借りて、彼は Lean4 を使用して論文を書いたり数学の研究を行ったりすることを学び始めました。

このプロセスは間違いなく彼を非常に興奮させたので、彼は時々（数時間おきにでも）マストドンに投稿して、学習の洞察と経験の要約を記録しました。

テレンス・タオは、マクラフリン不等式に関する論文を執筆する際に、GPT-4、Copilot、Lean4 などの AI ツールを多用しました。

論文アドレス: https://arxiv.org/abs/2310.05328

現在の進捗状況は、Terence Tao が Lean4 の論文のセクション 2 の議論の修復を完了したことです。

しかし、このプロセスは予想していたよりもはるかに面倒で、証明の各行を形式化するのに約 1 時間かかりました。

プロジェクトの最初の 1 週間は、Lean 構文とツールに慣れていないことがボトルネックでした。しかし、現在はツール自体がボトルネックになっています。ツールは、コンピュータ代数パッケージほど高度ではありません。

たとえば、彼の論文のある行では、次のような不等式が述べられています。

次のように並べ替えることができます。

すべての分母が正であると仮定すると、これは手動で計算する非常に迅速な作業であり、標準的なコンピュータ代数パッケージでかなり簡単に実行できます。

Lean には線形演算を処理するための非常に便利な自動ツールがありますが、指数を含む複雑な式を自動的に簡略化するツールは現在ありません。

したがって、指数法則や前述の他の操作を段階的に処理する必要があり、これは非常に時間のかかるプロセスです。

最終的に、タオは議論のこの部分に漸近記法を使用しないことに決め、代わりに固定定数 C を持つ不等式を定式化しました。

で、

当初、タオ氏は、C=7 のような値を使用して不等式を証明する方が「簡単」だと考えていました。しかし、既存のツールを使用して C≤7 を厳密に証明するのは非常に面倒であるため、このアイデアは放棄され、代わりにより形式的に操作可能な C 値が使用されました。現在選択されている値は約 6.16 です。

これに対して、好奇心旺盛なネットユーザーが「手作業による計算と比べて、AIは証明速度の点でどの程度優れているのか？」と質問した。

タオ氏は、自身の観察によれば、コンピュータ代数パッケージや計算機にとって機械的なタイプのタスクは、形式的な証明支援システムにとっては必ずしも機械的なものではないかもしれないと述べた。

しかし、LLM の登場により、すべてのコンピュータ支援ツールを非常にユーザーフレンドリーな共通ツールに統合できるようになるはずです。そして、このツールは各コンポーネントの利点をすべて備えています。

近い将来には、Lean の上に AI レイヤーを構築することも考えられます。

証明の手順は「数学的な英語」で AI に説明され、AI は Lean を使用してその手順を実行しようとします。その過程で、コンピュータ代数ソフトウェア パッケージが呼び出されることもあります。

副操縦士は実際に次のステップを推測できる

以前、マクローリンの不等式の研究に関するこの論文で、テレンス・タオは、コパイロットが実際に次に何をしたいかを予測できることに驚きました。

さまざまな日常的な検証のための複数行のコードを正確に予測できるだけでなく、タオ氏が提示した定理の名前に基づいて、タオ氏が研究を進めたい方向性を推測することもできます。

これにテレンス・タオは何度も「これは信じられない！」と叫んだ。

論文の定理 1.3 を証明する過程で、Terence Tao は Lean4 を使用して定理の証明を形式化しました。

論文では証明は 1 ページだけですが、正式な証明には Lean4 の 200 行が使用されています。

たとえば、論文では、タオは単純に任意の実数 a>0 に対して凸であると仮定し、次にジェンセンの不等式を呼び出しました。しかし、関連するコードには約 50 行が必要です。

このプロセスの間、GitHub Copilot はさまざまな驚くべき予測を示し、Tao の研究の次の方向性を魔法のように推測しました。

Lean の書き換え戦略により、対象を絞った置き換えを通じて長い仮定や目標を修正できます。

この機能は、常に完全な表現を入力する必要がなく、これらの表現を自由に操作できるため、非常に重要です。

相対的に言えば、この操作は LaTex でははるかに面倒です。

タオ氏は、カットアンドペーストなどの操作を使用して、長い表現を1行から次の行にかけて的を絞って編集するという、Lean4 の書き換え戦略を大まかにシミュレートする必要があったと語った。これにより、ドキュメント内の複数の行に入力ミスが広がる可能性があります。

Lean4 は、この書き換えを自動的かつ検証済みの方法で完了できます。

もちろん、Lean 4 はまだ万能ではなく、いくつかの制限があります。たとえば、バインドされた変数を含む式を書き換えるのは必ずしも簡単ではありません。

タオ氏は、自然言語を使ってLLMにそのような変換を依頼できる日を楽しみにしていると語った。

GPT-4+GitHub Copilot 入門、クレイジーなおすすめ

9 月初旬には、Terence Tao 氏が Python コード生成における ChatGPT の効果を称賛する投稿を投稿しました。ChatGPT によって、作業時間が 30 分も節約されたのです。

実験として、彼は ChatGPT に、オイラーの普遍関数 ϕ が減少しない各自然数 n について 1,...,n の最長部分列の長さ 𝑀(𝑛) を計算する Python コードを書いてもらいました。

例えば、ϕは1,2,3,4,5（または1,2,3,4,6）では非減少ですが、1,2,3,4,5,6では非減少ではないため、𝑀(6)=5となります。

興味深いことに、このプログラムは普遍関数を計算するための極めて巧妙なコードを生成しました。このコードは非常に巧妙であったため、タオはコードの背後にある原理が何であるかを理解するのに数分間じっと見つめなければなりませんでした。

もちろん、このコードには偏りがあります。つまり、連続する整数の部分列のみを考慮し、任意の部分列は考慮しません。

しかし、それは十分近いものだったので、ChatGPT によって生成されたこの初期コードを出発点として使用して、Tao は最終的に必要なコードを手動で生成し、約 30 分の作業を節約しました。

ChatGPT は非常に優れた結果をもたらすため、Tao 氏は今後、同様の計算の初期コードを提供するために ChatGPT を頻繁に使用していくと述べました。

すぐに、Terence Tao は、ネットユーザーの勧めで GitHub Copilot を使い始めたと再度投稿しました。

予想通り、Copilot のその後のパフォーマンスは彼を本当に驚かせました。冒頭の段落と一文を与えただけで、AI は彼自身のアイデアに非常に近いコンテンツを推奨したのです。

タオ氏は提案にわずかな変更を加えるだけで、当初計画していた時間の半分以下でプロジェクトを完了することができました。

10月にタオ氏が自然数ゲームの研究を行っていたとき、GPT-4はゲームに直接的な支援を提供できなかったものの、Leanを使い始めると非常に便利になることを発見しました。

レベルがどんどん難しくなるにつれて、GPT の効果が徐々に現れ始めます。

Z が明らかに X と Y の結果である場合、GPT に「X と Y がすでにわかっている場合、Z をどのように証明しますか?」と尋ねると、その過程であらゆる種類の微妙な文法上の問題を解決できます。

タオ・ゼシュアンは、プロ関連のコンテンツに加えて、DALL・E 3が使えると知ってすぐにプレイし始めました。

ネットユーザー：LLMは優秀な人材を1万倍優秀にできる

この偉人の数学研究におけるAIツールへの執着は、ネットユーザーの間でも白熱した議論を巻き起こした。

今月初めからマスターはGPT-4の助けを借りてLean4の学習を開始し、その学習の進捗状況を随時マストドンに記録しているとのことです。

これは、最も成功した人々にとって、LLM が仕事のスピードを速めることができることも示しています。

コードを書けない人でも、LLM コミュニケーターとして優秀であれば、すぐに機能を自動化できると言う人もいます。

しかし、高度なスキルを持つ人だけがLLMを効果的に活用できると、結果として人々の間の不平等が悪化する可能性があります。

すぐに誰かが名乗り出て、彼の友人は以前は Excel の数式以外は何も書けなかったが、今では GPT-4 を使用して Python アプリケーションを書けるようになったと言いました。

30 年の開発経験を持つプログラマーとして、私は今でもこの技術を教えて欲しいと彼に懇願しなければなりません。

彼の成功は、おそらくLLMとのコミュニケーションが非常に上手いからでしょう。

時間の経過とともに、LLM を利用する人々は圧倒的な利益を得て、知能に関係なく試験のエキスパートになると予測する人もいます。

エリートの場合、LLM から 100 倍の支援が得られる可能性があり、トップ エンジニアの場合、この支援は 10,000 倍になる可能性があります。