Tao Zhexuanの論文の抜け穴がAIによって発見され、26年の予言が現実になります! 定理の名前を見て研究の方向性を推測し、AIの能力をすごいと呼んだ大神

記事のソース: New Zhiyuan

最近、GPT-4とCopilotを使って研究を行うことに熱心な数学の神様であるTao Zhexuanは、AIの助けを借りて彼の論文に隠されたバグを発見しました!

Tao Zhexuan氏は、Lean4で6ページの議論を形式化する過程で、

n = 3 および k = 2 では、実際には発散します。

このあまり目立たないバグは、Lean4のおかげで間に合いました。

その理由は、リーンが彼に02のビルドを依頼したからです。 その結果、リーンは負の 0 に基づくことはできません

幸いなことに、これはn値が小さい場合にのみ存在する小さなバグです。 この時点で、論文の定数をいくつか変更する必要があります。

一部の数学愛好家のファンは、この投稿で次のように叫びました:これは驚くべきことであり、AI証明アシスタントの普及を見て、数学研究の未来のためのより強固な基盤を築くのを見るのは素晴らしいことです。

Tao Zhexuan氏は、これは完全に可能であると述べました。

近い将来、リーンの上にAIレイヤーを構築できるかもしれません。
証明のステップをAIに記述することで、AIはリーンを使って証明を実行することができ、その過程で様々なコンピュータ代数パッケージを呼び出すこともできます。

今年6月、Tao Zhexuan氏はGPT-4のトライアル体験に関するブログで次のように予測しました。

2026年には、AIは検索ツールや記号数学ツールと組み合わされ、数学研究において信頼できる共著者となるでしょう。

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

そして、Tao Zhexuanもそれを実践し、新しい論文がGPT-4で書かれ始め、繰り返し叫びました-GitHub Copilotの驚くべき能力は私を不安にさせます!

AI祝福神数学研究

最近、Tao ZhexuanはAIの「穴」に完全に入りました。

GPT-4の助けを借りて、彼はLean4で論文を書き、数学的研究を行うことを学び始めました。

彼はこのプロセスにとても興奮し、数時間ごとにMastodonに投稿して、学んだことや経験を記録しました。

マクラフリンの不等式に関する論文を書くにあたり、タオはGPT-4、Copilot、Lean4などのAIツールを多用しました。

住所：

ここまでで、TaoはLean4の論文のセクション2の議論の修復を完了しました。

しかし、このプロセスは予想以上に退屈で、各証拠が形式化されるまでに約1時間かかりました。

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

たとえば、彼の論文の1行で、彼は不平等について次のように述べています。

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

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

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

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

結局、Taoは引数のこの部分で漸近表記を使用せず、定定数Cで不等式を確立することにしました。

そこに

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

この点に関して、一部の好奇心旺盛なネチズンは、「AIは手計算と比較して速度を証明するのにどのようですか?」と尋ねました。

Tao Zhexuanは、彼自身の観察に基づいて、コンピュータ代数パッケージや電卓にとって機械的なタイプのタスクは、正式な証明アシスタントにとって必ずしも機械的ではないと述べました。

しかし、LLMの出現により、すべてのコンピューター支援ツールを1つのユーザーフレンドリーでユニバーサルなツールに統合できるはずです。 そして、このツールには、各コンポーネントのすべての利点があります。

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

証明のステップは「数学英語」でAIに説明され、AIはリーンを使用して証明を実行しようとし、その過程でコンピューター代数パッケージを呼び出す可能性があります。

Copilot は次のステップを推測できます

以前、マクラフリンの不等式研究に関するこの論文で、Tao Zhexuanは、Copilotが次に何をしたいかを予測できることに驚いていました。

さまざまな日常的な検証に使用される複数行のコードを正しく予測できるだけでなく、Tao Zhexuanによって提供された定理の名前に基づいて、彼が研究を行う方向を推測することもできます。

これにタオ・ジェクシュアンは何度も何度も叫びました。

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

論文では、証明プロセスには1ページしかありませんが、正式な証明には200行のLean4を使用します。

たとえば、論文では、Tao Zhexuanは

は a>0 の任意の実数上で凸であり、Jensen 不等式は後で呼び出されます。 しかし、コードは約50行かかります。

その過程で、GitHub Copilotはあらゆる種類の神聖な予言を示し、Tao Zhexuanの研究の次の方向性を魔法のように予測しました。

リーンの書き換え戦略により、ターゲットを絞った置換を通じて、長い仮定や目標を修正することができます。

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

比較すると、LaTexでは、この操作ははるかに面倒です。

Tao Zhexuan氏は、Lean4の書き換え戦略を大まかにシミュレーションし、切り取りや貼り付けなどの操作を通じて、1行から次の行への長い表現に的を絞った編集を行う必要があると述べました。 これにより、入力ミスがドキュメント内の複数の行に広がる可能性があります。

Lean4は、この書き換えを自動化された検証可能な方法で行うことができます。

もちろん、リーン4は現時点では万能薬ではなく、いくつかの制限があります。 たとえば、制約変数を含む式を書き換えるのは、必ずしも簡単ではありません。

Tao Zhexuan氏は、自然言語を使ってLLMにそのような変換を依頼するのが簡単になるのを楽しみにしていると述べました。

ピットGPT-4 + GitHub副操縦士、クレイジーアムウェイ

早くも9月の初めに、Tao Zhexuanは、Pythonコードの生成におけるChatGPTの効果を称賛する投稿を投稿しました。

実験として、彼はChatGPTに、オイラーの全能関数のφが減少しない自然数nごとに1,...,nの最長部分列の長さM(n)を計算するPythonコードを書くように依頼しました。

たとえば、φ は 1,2,3,4,5 (または 1,2,3,4,6) では減少しませんが、1,2,3,4,5,6 では減少しないため、M(6)=5 となります。

興味深いことに、それは全能関数を計算するための非常に独創的なコードを生成し、それは非常に独創的だったので、タオはコードの背後にある原理が何であるかを理解する前に、数分間それを見つめなければなりませんでした。

もちろん、このコードにも偏りがあります - 任意のサブシーケンスではなく、連続する整数のサブシーケンスのみを考慮します。

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

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

すぐに、Tao Zhexuanは、ネチズンの推薦でGitHub Copilotに参加したことを再び投稿しました。

当然のことながら、Copilotのその後のパフォーマンスは彼にとって本当に驚きでした — 冒頭の段落を与え、文章を追加するだけで、AIは彼自身のビジョンに非常に近いものを推奨しました。

Tao Zhexuan はこれらの提案にわずかな変更を加えるだけで、当初の計画の半分以下の時間で完了できます。

10月、Tao Zhexuan氏は、GPT-4はゲームに直接役立つことはできないが、リーンを使い始めると、GPT-4が非常に便利になったことに気づきました。

レベルがますます難しくなるにつれて、GPTの役割が明らかになり始めます。

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

Tao Zhexuan氏は、プロ関連のコンテンツに加えて、DALL· E3とすぐに再生を開始しました。

ネチズン:LLMは優秀な人々を10,000倍良くすることができます

偉大な神が数学研究におけるAIツールに夢中になっているという事実も、ネチズンの間で激しい議論を呼び起こしました。

大神は今月初めにGPT-4の助けを借りてLean4の学習を始めたという人もいて、時々マストドンで学習の進捗状況を記録します。

また、最も成功している人々にとって、LLMは仕事を加速できることも示しています。

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

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

誰かがすぐに名乗り出て、それは本当だ、彼の友人はExcelの数式以外は何も書けなかったが、今ではGPT-4でPythonアプリケーションを書くことができると言った!

30年の開発経験を持つコーダーとして、彼はこの技術を教えてほしいと懇願する必要もあります。

彼の成功は、おそらくLLMとのコミュニケーション能力によるものです。

時間が経つにつれて、LLMを使用する人々は、自分の知性に関係なく、圧倒的な利益を享受し、試験の専門家になるためにはしごをどんどん登っていくと予測されています。

エリートはLLMから100倍、トップエンジニアは10,000倍のブーストを受けることができます。

リソース：