テレンス・タオは大規模モデル証明アシスタントのリーンを使用して自分の好みを示します

「正しく使用すれば、AI は 2026 年までに数学研究や他の多くの分野で信頼できる共著者になると私は予測しています。」と数学者のテレンス・タオ氏は以前のブログで述べました。

タオ・ゼシュアンはこう言い、そしてそれを実行しました。

彼は最近、GPT-4、Copilot、Lean などのツールを使用して数学的研究を行っており、AI の助けを借りて論文の隠れたバグも発見しました。

最近、テレンス タオ氏は、Lean4 プロジェクトが多項式フライマン-ルザ予想 (PFR) の証明の形式化を正常に完了したと述べました。たったの3日、1週間かかりました。同時に、リーン コンパイラは、予想が標準公理に準拠していることも報告します。これはコンピューターと AI によって証明された大成功であり、非常に興味深いものです。

上記の研究の詳細については、興味のある読者は「」を参照してください。 AIを使った陶則軒の正式な証明とは何ですか？」 PFR 予想の過去と現在を 1 つの記事で理解します。

これを見て、慎重な読者はヒントを見つけたかもしれません マスター・タオは数学的研究を行っているときにリーンについて何度も言及しました。簡単に言うと、リーンは数学者が定理を検証するのに役立つプログラミング言語であり、ユーザーは証明を書いて検証することができます。オリジナルの Lean と比較して、最新の Lean 4 バージョンでは、コンパイラの高速化、エラー処理の改善、外部ツールとの統合の改善など、多くの最適化が行われています。

リーンは数学の分野で広く使用されていますが、ラージ モデル (LLM) が普及している今日、この 2 つを組み合わせるより良い方法はあるでしょうか?

オープン プラットフォーム LeanDojo チーム (LeanDojo については、「AI 大型モデルが Tao Zhexuan の問題解決を支援し、数学の定理も証明できますか? ") とカリフォルニア工科大学の研究者は、100% 正確な形式的な数学的証明を提供することを目的として、LLM と人間の対話のために設計されたコラボレーション ツールである Lean Copilot を立ち上げました。

LeanDojo チームの研究は主に LLM を使用して定理証明を自動化することに焦点を当てていることは注目に値します。 Lean Copilot が LLM に関連していることは驚くべきことではありません。

プロジェクトアドレス: https://github.com/lean-dojo/LeanCopilot

対象この研究は、かっこいいと言うのは別として、非常に格好良くて、今でも非常に評価が高いです。

リーンで LLM を使用して数学的証明を高速化する

長い間、定理証明は自動化されてきました。多くの困難に直面しているため、数学的証明は伝統的に手動による導出に依存しており、慎重な検証が必要です。現在、AI の進歩に伴い、研究者は人工知能を使用して詳細な調査を実施し始めていますが、この問題は避けられません。つまり、LLM は数学や推論のタスクではあまり信頼できない場合があり、エラーや幻覚が発生しやすいのです。

リーン コパイロットの機能を使用すると、ユーザーは大規模な言語モデルを使用して、リーンでの証明プロセスを自動化し、証明合成の速度を向上させることができます。必要に応じて、ユーザーはシームレスに介入および変更して、マシン インテリジェンスと人間のインテリジェンスのバランスのとれたコラボレーションを実現することもできます。

リーン コパイロットを使用すると、LLM をリーンで使用して、戦略の提案を含む証明の自動化を実現できます。 、前提および検索証明

ユーザーは、LeanDojo が提供する組み込みモデルを使用するか、独自のモデルをインポートするかを選択できます。これらのモデルは、ローカル (GPU の有無にかかわらず) またはクラウドで実行できます

#つまり、リーン コパイロットは、LLM を導入してモデルを強化し、最適化する柔軟な方法をユーザーに提供します。 Lean での定理証明のプロセス。

リーン コパイロットの主な機能は次のように要約できます:

• LLM は、証明ステップを提案し、証明を検索し、大規模な数学ライブラリから有用な補題を選択することができます。
• Lean Copilot は Lean パッケージとして設定でき、Lean VS Code ワークフロー内でシームレスに実行できます。
• ユーザーは、LeanDojo の組み込みモデルを使用することも、ローカル (GPU の有無にかかわらず) またはクラウドで実行できる独自のモデルを使用することもできます。
• このツールは、Linux、macOS、Windows WSL などのさまざまなプラットフォームで実行されます。

Lean ユーザーが LLM をより利用しやすくするために、Lean Copilot は正のフィードバック ループを開始したいと考えています。自動化がより良いデータにつながり、最終的には数学的パフォーマンスにおける LLM のパフォーマンスを向上させることを証明します。 。

Copilot の効果デモ

Lean Copilot は、公式チュートリアルに従って設定できます。構成が完了したら、実験を開始できます。プロジェクトの作成者は、参考用に公式の例をいくつか提供しています。

推奨ソリューション。 LeanCopilot をインポートした後、suggest_tactics を使用して推奨ソリューションを生成できます。使用中に、推奨されるソリューションをクリックしてプルーフで使用することもできます (下の画像を参照)

プレフィックスを使用できます, たとえば、生成された戦略

検索証明を制限するには、simp を使用します。 search_proof を使用して、LLM で生成されたポリシーと aesop (Lean 4 のホワイトボックス自動化プロジェクト) を組み合わせて、複数のポリシー証明を検索します。証明を見つけたら、戦略をクリックしてエディターに挿入できます。

# 書き直された内容: 前提条件の選択は重要です。 。この戦略の目的は、潜在的に有用な前提のリストを取得することです。現在、Lean Copilot は LeanDojo の検索ツールを使用して、Lean と mathlib4 (つまり、Lean 4 数学ライブラリ) の固定スナップショットからプレミスを選択します。 # LLM を実行できます。定理の証明でも他の推論でも、リーンで LLM を実行できます。任意のモデルをローカルまたはリモートで実行できます (「独自のモデルの持ち込み」を参照)

興味のある読者のために、いくつかの高度な使用法についてもプロジェクトで説明しています。元のプロジェクトにアクセスして詳細を確認できます。

以上がテレンス・タオは大規模モデル証明アシスタントのリーンを使用して自分の好みを示しますの詳細内容です。詳細については、PHP 中国語 Web サイトの他の関連記事を参照してください。