テレンス・タオのクレイジー・アムウェイ副操縦士: 1 ページの校正を完了するのに役立ち、その後のプロセスを推測することもできました

GPT-4 によって「承認」された後、副操縦士はテレンス・タオによって待ち伏せ攻撃も受けました。

彼は、プログラミング時に、Copilot は次に何をするかを直接予測できると率直に言いました。

Copilot を使用すると、研究がより便利になり、Tao Zhexuan もそれを使用して、最新の研究結果を完成させるのに役立ちました。

Tao Zhexuan 氏は、論文のこの部分は実際には 1 ページしかない、と述べました。

しかし、この 1 ページの証明を完成させるために、彼は新しく学んだプログラミング言語 Lean4 を使用して 200 行を超えるコードを書きました。

Tao Zhexuan の公開コードの GitHub ページでは、Copilot によってコードの記述速度が半分以上向上したことがわかります。

Tao Zhexuan 氏は、Lean4 を選択した理由は、長い式の対象を絞った部分置換を実行する「書き換え戦略」のためであると述べました。

たとえば、複素関数 f(x) が定義されている場合、f(114514) の式を入力したい場合、コードを使用して x を 114514 に直接「書き換え」ることができます。

Tao Zhexuan 氏は、この機能は数式を繰り返し入力する必要がある LaTeX に比べてあまり便利ではないと述べています。

それでは、Tao Zhexuan の「1 ページの証拠」は今回、どのような新しい結果を私たちにもたらしたのでしょうか?

新たな不等式の 1 ページの証明

この論文では、マクラフリンの不等式に関連する問題について説明します。

マクラフリンの不等式は、数学における古典的な不等式です。「非負の実数の算術平均は幾何平均以上である」という法則に基づいて導出されます。次のように表現できます。

y₁…y_n が非負の実数であると仮定します。k=1…n の場合、平均 S_k は次のようになります。 (分母が分子である項の数) として定義されます:

#これは、根を持つ n 次の多項式の正規化された係数として発生します。

(この式を覚えておいてください。これを式 1 と呼びます)

次に、マクラフリンの不等式は次のように表すことができます:

このうち、等号は、すべての y_i が等しい場合にのみ当てはまります。

微積分には、古典的なニュートンの不等式もあります。

任意の 1≤k はすべて非負であり、ニュートンの不等式はマクラフリンの不等式を簡単に説明できます:

しかし、この制限が追加されない場合、負の数は許可されます。用語のうち、マクローリンの不等式はニュートンの不等式を使用して表現できません。

そこで、ニュートン不等式における負の項の可能性を考慮して、Tao Zhexuan は一連の新しい不等式バリアントを提案しました:

任意の r>0 および 1≤ℓ≤n については、次の式が存在する必要があります。式２または式３が成立する。

これは、テレンス タオがこのページで証明しようとしているものです。具体的な証明プロセスは次のとおりです:

我々は、次のような多項式を構築することもできます。複素変数 z P(z):

前の式 1 と三角不等式から、次のことが得られます:

したがって、必要なのは下限を設定することだけです。

## P(z) の絶対値を取得し、対数を取得して次の結果を取得します。

任意の実数 t について、t ↦ log(e

t ^{a) は凸であり、a>0 であるため、次の不等式が得られます。}

# a=r

2

、t=2log y^j の場合、次のように結論付けることができます:

上記はテレンス タオ プロセスによる証明ですが、正規化された |S

n

|=1 の場合、次の式が成り立ちます。ステップ: 洗練されたバージョンを作成する今回言及した「1 ページの証明」に加えて、Tao Zhexuan の論文では、別の新しい定理も提案されています。つまり、任意の 1 ≤ k ≤ ℓ≤ n についてです。:

テレンス・タオ氏はブログ投稿で、次のステップはこの不等式の洗練されたバージョンを提案することであると明らかにしました。

Tao Zhexuan氏は、証明のプロセスは「練習と同じように」非常に簡単で、微積分を使って行うことができると述べた。

ただし、議論のこの部分では漸近記号が使用されているため、多少の困難があるとも彼は述べました。

新しい結論がどのようなものになるかを待ってみましょう。

One More Thing

Tao Zhexuan は AI ツールの熱心なファンであり、Copilot、GPT-4、およびその他の補助ツールを推奨しています。

今回、彼はまた、大規模モデルの開発に対する新たな期待を表明し、いつかモデルが不等式のバリアントを直接生成できるようになることを期待しています。

論文アドレス:

https://arxiv.org/abs/2310.05328

以上がテレンス・タオのクレイジー・アムウェイ副操縦士: 1 ページの校正を完了するのに役立ち、その後のプロセスを推測することもできましたの詳細内容です。詳細については、PHP 中国語 Web サイトの他の関連記事を参照してください。