カリフォルニア工科大学の中国人がAIを使って数学的証明を覆す！タオ・ゼシュアンの衝撃を5倍にスピードアップ、数学的ステップの80％が完全に自動化

テレンス・タオなど多くの数学者に賞賛されたこの正式な数学ツール、リーン・コパイロットが再び進化した?

たった今、カリフォルニア工科大学のアニマ・アナンドクマール教授が、チームがリーン・コパイロット論文の拡張版をリリースし、コードベースを更新したと発表しました。

写真

論文アドレス: https://arxiv.org/pdf/2404.12534.pdf

最新の実験では、この Copilot ツールが数学的証明ステップの 80% 以上を自動化できることが示されています。この記録は、以前の基準イソッ​​プよりも 2.3 倍優れています。

そして、以前と同様に、MIT ライセンスの下でオープンソースです。

写真

彼は中国人の少年ソン・ペイヤンで、UCSBの名誉CS学部生であり、カリフォルニア工科大学のコンピューティング+数理科学（CMS）学部のSURF研究者です。

ネチズンはこう叫びました。つまり、Tao Zhexuan の数学的研究は、その場で 5 倍加速できるということですか?

写真

LLM が証明戦略を提案し、人間がシームレスに介入します

チームは、人間と LLM の間のコラボレーションを開始して、100% 正確な形式的な数学的証明を作成することを期待して、このリーン コパイロット ツールをリリースしました。

これにより、リーンで LLM 推論を実行するという、中核的な技術的課題が解決されます。

このツールを通じて、LLM にリーンで証明戦略を提案させ、人間がシームレスな方法で介入して変更できるようにすることができます。

写真

このプロジェクトは、自動定理証明が今日でも依然として難しい課題であるために開発されました。

LLM は数学や推論のタスクを行うときに間違いや幻覚を起こすことが多く、非常に信頼性が低いことは誰もが知っています。

写真

したがって、これまでのところ、数学的証明はほとんどが手動で導出されており、慎重な検証が必要です。

Lean のような定理証明ツールは証明プロセスのすべてのステップを形式化できますが、人間が Lean を記述するのは非常に手間がかかります。

この場合、リーン・コパイロットの誕生は非常に重要です。

Tao Zhexuan に何度も衝撃を与えた成果物: 数学者はそれを使用する前に終わっている

LLM は定理を証明する人間を支援するツールとして使用できる この議論は Tao Zhexuan によって何度も確認されています。

彼は、26 年以内に AI が検索および記号数学ツールと結合され、数学研究において信頼できる共著者になるだろうとブログで予測しました。

その直後、彼の見解を裏付ける研究が雨後の筍のように湧き出た。

昨年 6 月、カリフォルニア工科大学、NVIDIA、MIT およびその他の機関の学者は、オープンソース LLM に基づく定理証明者である LeanDojo を構築しました。

写真

9月、Microsoft Research Asia、北京大学、北京大学、その他の機関の研究者らは、97ラウンドの「ソクラテス的」厳密推論を通じてGPT-4の作成に成功したという結論に達した。 「P≠NP」でこの千年問題を解決しました。

写真

第97ラウンドの対話で、GPT-4は、網羅的手法なしでは例を解決できないと結論付け、結論はP≠NPであることを証明しました

昨年10月、Tao Zhexuan GPT-4 と Copilot の助けを借りて、論文の隠れたバグを直接発見しました。

Lean4 を使用して 6 ページの議論を形式化する過程で、式

picture

が n=3,k=2 の場合に実際に発散することを発見しました。

この見つけにくいバグは、Lean4 のおかげで時間内に捕らえられました。その理由は、リーンが彼に 02 のみを仮定したためです。したがって、リーンは負の 0

写真

この発見は、陶哲軒の生徒たちに直接衝撃を与えました。

写真

昨年末、Tao ZhexuanはAIツールを直接使用して、多項式フライマン・ルザ予想​​証明プロセスを形式化する作業を完了することに成功しました。

写真

最後に、依存関係グラフは完全に緑色で覆われており、リーン コンパイラーは、この予想が標準の公理に完全に従っていることも報告します。

写真

この過程で、すべての第一線の数学研究者は、数学研究の破壊力に対する AI の直接的な影響を初めて感じました。

Lean Copilot により Lean がさらに使いやすくなります

そして今日、Lean Copilot によるこの研究により、Lean は直接さらに強力になりました。

この論文では、チームは証明ステップの提案 (戦略提案)、中間証明目標の完了 (証明検索)、および LLM を使用した関連する前提の選択 (前提選択) を行うためのツールを、リーン コパイロットに基づいて構築しました。

また、実験結果は、リーンにおける既存のルールベースの証明自動化と比較して、リーン・コパイロットが定理証明の自動化において人間を支援するのに効果的であることを十分に実証しています。

Lean Copilot は、CTranslate 2 を介してローカルで、またはサーバー上で LLM 推論を実行できる一般的なフレームワークを提供します。

このフレームワークを通じて、ユーザーはさまざまな自動証明ツールを作成できます。

写真

リーンは数学者の間で非常に人気のある証明アシスタントです。以下の図に示すように、リーンの証明は戦術と呼ばれる一連の証明ステップで構成されます。

写真

この戦略は、最初の目標として定理全体から開始して、すべての目標が解決されるまで、現在の目標をより単純なサブ目標に繰り返し変換します。

ユーザーは、VSCode によって駆動される IDE で対話的に戦略を作成すると、右側の情報ビュー パネルに目標が表示されます。

戦略提案を生成する

チームは、Lean Copilot を使用して、LLM を使用して戦略提案を生成するツールである assign_tropics を構築しました。

そしてそれ自体が戦略でもあります。

を適用すると、現在のターゲットをLLMに入力し、生成されたポリシー候補リストをLLMから取得します。

各オプションを調べて、1) エラーが発生するか、2) 何も問題はありませんが証明が完了しないか、3) 証明が正常に完了したかどうかを確認します。

1)の場合、この戦略は削除されます。

写真

右側のビューパネルには、エラーのない戦略のみが表示されます。

その中で、証明を正常に完了した戦略は緑色 (カテゴリ 3) でマークされ、エラーなしで証明目標を変更したが証明を完了できなかった戦略は青色 (カテゴリ 2) でマークされます。

注意!リストされているすべての戦略がカテゴリ 2 に分類される場合、この情報はユーザーにとって非常に価値のあるものになります。

この場合、残りの目標の情報は、ユーザーが次の中間証明ステップとして戦略を選択するのに直接役立ちます。

提案を見た後、ユーザーはそれらを受け入れるか、新しい戦略を開発するためのインスピレーションの源として使用するかを選択できます。

たとえば、リーン コードで定理 add_abc を定義します。その最初の目標は、図 3 の右側に示されています。

写真

suggest_tropics に入ると、右側に戦略の提案が表示されます。

最初の戦略は緑色で表示され、証明が正常に完了したことを示します。

次の 3 つの提案はすべて青色で、証明を直接完了することはできないが、エラーは発生しないことを示します。

したがって、これらは有効な中間証明ステップである可能性があります。

同時に、残りのサブ目標も表示されます。

少なくとも 1 つの戦略提案が証明できるため、「戦術状態」フィールドには「目標なし」と表示されます。

写真

完全な証拠を検索

さらに、人間も機械も一貫して正しい戦略を生み出すことはできないため、プロセスは後戻りして別の代替案を探索する必要があります。これが証拠検索です。

上記の Suggest_tropics に関しては、現在のステップの戦略を生成することしかできず、複数の戦略の証明を検索する機能はありません。

この目的のために、チームはルールベースの証明検索ツール aesop と組み合わせて、LLM ベースの証明検索ツールを構築しました。

Aesop は、リーン戦略としてベストファースト検索を実装し、ユーザーが検索ツリーの展開方法を設定できるようにします。

Pictures

検索ツリーは、ノードとしてのターゲットで構成されます。

初期状態では、元のターゲットのみがルート ノードとして存在します。各ステップで、aesop は最も有望な未展開ノードを選択し、ポリシーを適用してそれを展開し、結果のノードを子ノードとして追加します。

写真

そして、イソップが根本原因から簡単に解決できる目標に至る道筋を見つけたとき、それは探索が成功したことを証明します。

したがって、aesop のパフォーマンスは、ユーザーが効果的なルール セットを設定しているかどうかに大きく依存します。

これは、イソップに柔軟性が欠けていることを示しています。したがって、Search_proof は、各ステップで assign_tropics によって生成されるターゲット関連のポリシーをより柔軟にすることで、aesop のルール セットを強化します。

図 3 の元の目標の場合、ユーザーは search_prrof を入力し、目標を解決できる完全な証明を見つけるだけで済みます。これは情報ビュー (図 5 の右) に表示されます。

成功の証拠が見つかったので、残りの戦術状態はゴールなしであることがわかります。

写真

十分に注釈が付けられた前提を選択してください

さらに、定理証明におけるもう 1 つの困難かつ重要なタスクは、証明を短縮または完了する関連前提を見つけることです。

ソースコードライブラリと標準ライブラリの多数の前提条件に加えて、Lean には大規模な数学ライブラリ (Mathlib) もあります。

しかし、すべての図書館から候補施設を検索することは非常に困難で時間がかかります。

非常に多くの人が、リーンや他の証明アシスタントから支援を得ようとしたり、このプロセスを自動化しようとしています。

写真

Leanにおいて最も高度な前提選択手法は、Leanに直接実装されたランダムフォレスト(ランダムフォレスト)に基づくフレームワークです。

ただし、前提選択タスクは検索強化 LLM によく適しています。検索強化 LLM では、大規模モデルのトレーニング中に検索行列 (前提埋め込み) がトレーニングされ、証明対象と候補前提の間の相関関係が推定されます。

推論時に証明目標が与えられると、まず目標をベクトルにエンコードしてから、前提埋め込みと目標ベクトルの間で行列ベクトル乗算を実行します。

次に、上位 k 個のプレミス (k はユーザーが返したいプレミスの数を決定するハイパーパラメーター) を選択するには、最高スコアを持つ k 個のプレミスを返すだけです。

Lean で推論タスクを実行するには、Lean Copilot が提供する高速推論に加えて、効率的な行列乗算ライブラリと C++ numpy 行列リーダーも必要です。

研究者らは、CTranslate2 の行列乗算関数と Libnpy の C++ 高速 numpy ファイル リーダーを使用しました。

彼らは、FFI メカニズムを通じてこれらの数値を再び Lean にリンクします。

したがって、前提の埋め込みを事前に計算でき、上で紹介したライブラリを使用して後続のすべての操作を C++ で迅速に実行できるため、前提選択戦略は非常に効率的に実行できます。

帰還の前提を取得した後、研究者はさらに有用な情報を注釈として加えました。

ここで、すべての前提は、現在の環境で直接使用できる前提 (範囲内前提) と現在の環境で直接使用できない前提 (範囲外前提) の 2 つのカテゴリに分類されます。

これは、必要なパッケージがインポートされているかどうかによって異なります。

前提に必要なパッケージを既にインポートしている場合は、前提を簡単に使用できます。以下の図 6 は、注釈付きのスコープの前提を示しています。

図 7 は、注釈付きの範囲外の前提を示しています。

以下は、図 3 の定理 add_abc の使用例です。証明に select_premises を直接入力できます (図 8 左)。

その後、関連する前提条件のリストが情報ビューに表示されます (図 8、右)。

この単純な定理の場合、選択された前提はすべて自然数と加算規則に関連しているため、実際に適切であることがはっきりとわかります。

この場合、選択した 4 つの前提はすべて現在のスコープ内にあります。つまり、それらのモジュールはすでにインポートされています。

上記は、Lean Copilot を通じて研究者によって構築された 3 つの実用的な証明自動化ツールであり、戦略の提案、証明の検索、前提の選択に使用されます。

証明ステップの 81.2% はすべて自動化されています

研究者らは、リーン コパイロット フレームワークを通じて、リーン インタラクティブ定理証明 (ITP) における人間とマシンのコラボレーションが有益であるという仮説を経験的に提唱しました。

リーンの定理証明プロセスにより、主に戦略証明に焦点が当てられます。

そこで、具体的な実験では、筆者は主に「戦略提案」と「証明検索」の証明自動化ツールを評価しました。

要約すると、aesop は現在、プルーフ検索のための最も高度なルールベースのプルーフ自動化ツールです。

研究者らは、イソップと比較したLLMベースの検索証明の有効性を2つのケースで検証しました:

(1) 定理の自律的証明 (LLMは独立して完了)

(2) 人間が定理を実行する支援証明 (人間と AI が協力)

さらに、研究者らは、単一の戦略提案に加えて検索証明の利点を証明するために、検索証明と戦略提案を比較しました。

ソフトウェア プログラミングで人間が Copilot を使用するパラダイムと同様に、リーン コパイロットが ITP のプロセスで人間を効果的に支援する方法を研究します。

つまり、目標に直面したとき、まず Copilot を呼び出して、問題を直接解決できるかどうかを確認します。

そうでない場合は、目標をさらに単純化し、Copilot を再試行します。次に、Copilot が残りのターゲットを正常に解決するまで、上記のプロセスが繰り返されます。

研究者らは、この反復的なコラボレーションの例を使用して、各証明自動化ツールがどれだけの人員を自動化できるかを確認しました。

具体的な結果を以下の表1に示します。

証明検索 (search_proof) は、定理の 64% (50 個中 32 個) を自動的に証明できます。これは、イソップや戦略の提案 (suggest_tropics) よりも大幅に高いです。

人間を支援するために使用する場合、証拠検索に必要なのは手動で入力された戦略の平均 1.02 だけであり、これはイソップ (3.62) や戦略の提案 (2.72) よりも優れています。

写真

最後に、著者らはテストされた定理ごとに、3 つのツールのそれぞれによって自動化できる証明ステップの割合を計算しました。

その結果、証明検索は定理の証明ステップの約 81.2% を自動的に完了でき、これは戦略提案 (48.6%) やイソップ (35.2%) よりも大幅に高いことがわかりました。

要約すると、プルーフ検索のパフォーマンスは、ポリシー提案より 1.67 倍、ルールベースのベースライン aesop より 2.31 倍優れています。

Lean through Copilot でのネイティブ LLM 推論

Lean Copilot での戦術提案、証明検索、前提選択 これら 3 つのタスクは本質的に異なるように見えるかもしれませんが、ユーザー エクスペリエンスの要件は似ています。

それらはすべて、リーンで実行しながら、応答を十分に迅速に生成し、適度な計算要件を備えている必要があります。

ユーザーがこれらの要件を持つ理由は、ほとんどの場合、Lean 自体が環境フィードバック (残りのターゲット、エラー メッセージ、型情報など) を非常に迅速に提供できるためです。

この速度は、定理の証明の本質と一致しています。つまり、一貫した推論が必要です。

リーンコパイロットでユーザーが長時間待たされると、人間と AI のコラボレーションが難しくなります。

同様に、私たちはローコンピューティングのニーズにも応えたいと強く思っています。なぜなら、Lean での定理の証明自体には GPU が必要なく、ユーザーのローカル ラップトップで実行できるからです。

したがって、リーンユーザーにとって、ほとんどのハードウェア (GPU のないラップトップを含む) で効率的に実行できることが非常に重要です。

ユーザーは証明を書くときに CUDA 対応 GPU にアクセスできない可能性があるためです。

高速な推論と低い計算要件を満たす必要があり、一般的で効率的な深層学習フレームワークはすべて Python であるため、チームが考えた自然な解決策は、モデルを Python (ローカルまたはリモート) でホストすることでした。次に、Lean からモデルにリクエストを送信します。

ただし、このアプローチにはプロセス間通信のオーバーヘッドがあり、ユーザーは追加のセットアップ手順を実行する必要があり、Lean の従来のワークフローには適していません。

これらの問題を解決するために、Lean Copilot は、Foreign Function Interface (FFI) を通じて Lean で LLM をネイティブに実行します。

FFI は、ある言語で書かれたプログラムが別の言語のサブルーチンを呼び出すことを可能にするメカニズムです。

リーン部分は C++ で実装されており、C++ と効率的に相互運用できます。

プログラマーは関数をリーンで宣言できますが、関数本体は C++ で実装できます。実装は共有ライブラリにコンパイルされ、Lean に動的にリンクされます。

デフォルトでは、LeanDojo の事前トレーニング済み Repver モデルを使用します。これは、入力文字列を出力文字列にマッピングするエンコーダ/デコーダ コンバータ BVT5 に基づいています。

Lean Copilot は、文字列を操作する C++ 関数にモデルをラップすることで、Lean で実行できるようにします。この関数は、FFI を通じて Lean で呼び出すことができます。

写真

中国人著者は多大な貢献をしています

最新の論文の3人チームは、6月23日にオープンソースプラットフォームLeanDojoの作者でもあります。

写真

論文アドレス: https://arxiv.org/pdf/2306.15626.pdf

写真

歌ペイヤンは、カリフォルニア大学サンタバーバラ校クリエイティブスタディーズカレッジ (CCS) のコンピューターサイエンスの優等生で、リチャート・ワンとフィル・コンラッドが指導しています。

同時に、彼はカリフォルニア工科大学の計算数学科学部 (CMS) の SURF 研究者でもあり、アニマ・アナンドクマール教授とカイユ・ヤン博士が共同監督しています。

写真

さらに、彼はカリフォルニア大学バークレー校建築研究所の研究者であり、ティム・シャーウッドおよびジェレミー・ラウ博士(Google)と協力しています。

彼の研究対象は、自然言語処理 (NLP) やコンピューター ビジョン (CV) などの応用分野を含む機械学習 (ML) と、システムやプログラミング言語 (PL) などの基礎理論です。

Song Peiyang の最近の研究には主に 2 つの方向性があります。

1 つは、大規模なモデルと対話型定理証明者 (ITP) を組み合わせた、神経記号推論と人工知能数学 (AI4Math) です。

もう 1 つは、時相論理に基づくエネルギー効率の高い機械学習です。

Kaiyu Yang (杨凯媪)

写真

Kaiyu Yang は、カリフォルニア工科大学のコンピューティング + 数理科学 (CMS) 学科の博士研究員であり、アニマ アナンドクマールの指導を受けています。

彼はプリンストン大学で博士号を取得しました。指導教官は Jia Deng で、オルガ・ルサコフスキーやチェン・ダンチーとも協力しました。

彼の研究は神経象徴的な人工知能に焦点を当てており、機械学習が記号推論を実行できるようにすることを目的としており、次の 2 つの方向でこれを達成することを望んでいます:

(1) 機械学習を形式論理などの記号推論タスクに適用するまたは自然言語での数学的推論と定理の証明

(2) 機械学習モデルに記号コンポーネントを導入して、より解釈しやすく、検証しやすく、データ効率を高めます。

現在、彼は数学を理解して推論できる人工知能の研究に取り組んでいます。数学的推論は人間の知性における重要なマイルストーンであり、偏微分方程式の解法や式の検証など、科学や工学における多くの重要な問題を変革する可能性を秘めています。

アニマ・アナンドクマール

アニマ・アナンドクマールは現在、カリフォルニア工科大学の計算科学および数理科学の教授です。

写真

彼女の研究関心は主に大規模機械学習、非凸最適化、高次元統計の分野に焦点を当てています。

特に、彼女は機械学習用のテンソル アルゴリズムの開発と分析を主導してきました。

テンソル分解法は並列性とスケーラビリティが非常に高く、大規模なデータにも適用できます。最適解への収束を保証し、多くの確率モデル (マルコフ モデルなど) に対して一貫した推定結果を出力できます。

さらに広く言えば、Anandkumar 教授は、非凸最適化を加速するための効率的な手法を研究しています。

参考文献:

https://www.php.cn/link/1dd5a4016c624ef51f0542d4ae60e281

https://www.php.cn/link/ed798eec75807 d f6e79b0be391f720e4

https ://www.php.cn/link/a652e914c736dfaf8a6667ae6936f0d6

以上がカリフォルニア工科大学の中国人がAIを使って数学的証明を覆す！タオ・ゼシュアンの衝撃を5倍にスピードアップ、数学的ステップの80％が完全に自動化の詳細内容です。詳細については、PHP 中国語 Web サイトの他の関連記事を参照してください。