テレンス・タオはそれを見て彼を専門家と呼んだ！ Google などは LLM を使用して定理を自動的に証明し、カンファレンスで優秀な論文を受賞しました。コンテキストが完全であればあるほど、証明はより優れたものになります。

Transformer のスキル ツリーはますます強力になっています。

マサチューセッツ大学、Google、イリノイ大学アーバナシャンペーン校 (UIUC) の研究者らは最近、完全な定理を自動的に生成するという目標を達成することに成功した論文を発表しました。証拠。

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

これBaldur (北欧神話のトールの兄弟) にちなんで名付けられたこの研究は、Transformer が完全な証明を生成できることを初めて実証し、モデルに追加のコンテキストを提供することでモデルの以前の証明を改善できることも示しました。

この論文は、2023 年 12 月に ESEC/FSE (ACM European Joint Conference on Software Engineering and Symposium on Fundamentals of Software Engineering) で発表され、Outstanding Paper Award を受賞しました。

#誰もが知っているように、ソフトウェアにはバグが避けられず、平均的なアプリケーションや Web サイトではそれほど大きな問題を引き起こすことはありません。ただし、暗号化プロトコル、医療機器、スペースシャトルなどの重要なシステムの背後にあるソフトウェアについては、バグがないことを確認する必要があります。

- 一般的なコード レビューとテストではこの保証は得られないため、正式な検証が必要です。

形式的検証について、ScienceDirect の説明は次のとおりです:

形式モデルを使用して記述されたシステムの動作が、指定されたプロパティを満たします。これも形式モデルを使用して記述されます。

は、形式モデルによって記述されたシステムの動作が指定されたプロパティを満たしているかどうかを数学的にチェックするプロセスを指します。

簡単に言うと、数学的解析手法を使用してアルゴリズム エンジンを通じてモデルを構築し、テスト対象の設計の状態空間の徹底的な解析と検証を実行します。

正式なソフトウェア検証は、ソフトウェア エンジニアにとって最も困難なタスクの 1 つです。たとえば、Coq 対話型定理証明器で検証された C コンパイラである CompCert は、ユビキタスな GCC や LLVM などで使用される唯一のコンパイラです。

ただし、手動による形式的検証 (証明の作成) のコストは非常に膨大です。C コンパイラの証明は、コンパイラ コード自体の証明の 3 倍以上です。

したがって、形式的な検証自体は「労働集約的」な作業であり、研究者らは自動化された方法も模索しています。

Coq や Isabelle などの証明アシスタントは、一度に 1 つの証明ステップを予測するようにモデルをトレーニングし、そのモデルを使用して可能な証明空間を検索します。

Baldur はこの記事で、この分野における大規模言語モデルの機能、自然言語テキストとコードのトレーニング、証明の微調整機能を初めて紹介しました。

Baldur は、一度に 1 ステップずつではなく、定理の完全な証明を一度に生成できます。

#上の図に示すように、証明生成モデルへの入力として定理ステートメントのみを使用し、モデルから証明試行を抽出します。イザベルを使用して証明検査を実行します。

イザベルがエラーなしで証明の試みを受け入れた場合、証明は成功します。そうでない場合は、別の証明の試みが証明生成モデルから抽出されます。

Baldur は、6336 個の Isabelle/HOL 定理とその証明のベンチマークで評価され、完全な証明の生成、修復、コンテキストの追加の有効性を経験的に実証しています。

さらに、このツールが Baldur と呼ばれている理由は、現在最良の自動プルーフ生成ツールが Thor と呼ばれているためかもしれません。

Thor は、より小さな言語モデルと、証明の次のステップを予測するために可能な証明の空間を検索する方法を組み合わせて使用​​することで、より高い証明率 (57%) を持っていますが、Baldur の利点は、完全な証拠。

しかし、トールとバルダーの兄弟も協力することができ、証明率が 66% 近くまで高まる可能性があります。

完全な証明を自動的に生成

Baldur は、科学論文や数学を含む Web ページで使用される Google の大規模言語モデルである Minerva を利用しています。証明と定理に関するデータに基づいてトレーニングされ、微調整されました。

Baldur は、証明結果をチェックする定理証明アシスタントの Isabelle と協力できます。定理ステートメントが与えられたとき、Baldur はほぼ 41% の確率で完全な証明を生成することができました。

Baldur のパフォーマンスをさらに向上させるために、研究者はモデルに追加のコンテキスト情報 (他の定義や理論文書の定理ステートメントなど) を提供しました。これにより校正率は 47.5% に増加します。

これは、Baldur がコンテキストを取得し、それを使用して新しい正しい証明を予測できることを意味します。これは、関連するメソッドとコードを理解している場合にそうする可能性が高いプログラマーと同様です。プログラムのバグ。

例は次のとおりです (fun_sum_commute 定理):

この定理は、Formal Proof Archives の Polynomials と呼ばれるプロジェクトから来ています。

手動で証明を書く場合、セットが有限であるか有限でないという 2 つのケースが区別されます。

つまり、モデルの入力は定理ステートメントであり、ターゲットの出力はこの手動で書かれた証明です。

Baldur はここで帰納法の必要性を認識し、infinite_finite_induct と呼ばれる特別な帰納法を適用しました。これは人間が書いた証明と同じ一般的なアプローチに従いますが、より簡潔です。

帰納法が必要なため、イザベルが使用するスレッジハンマーはデフォルトではこの定理を証明できません。

トレーニング

プルーフ生成モデルをトレーニングするために、研究者は新しいプルーフ生成データセットを構築しました。

既存のデータセットには単一の証明ステップの例が含まれており、各トレーニング サンプルには証明の状態 (入力) と適用される次の証明ステップ (目標) が含まれています。

単一の証明ステップを含むデータセットがあるとすると、証明全体を一度に予測するようにモデルをトレーニングするために、新しいデータセットを作成する必要があります。

研究者らは、データセットから各定理の証明ステップを抽出し、それらを連結して元の証明を再構築しました。

#修理の証明

# 上記の fun_sum_commute を例として取り上げます。

Baldur が最初に生成した証明の試みは、証明チェッカーで失敗しました。

Baldur は帰納法を適用しようとしましたが、最初に証明を 2 つの場合 (有限集合と無限集合) に分解することができませんでした。イザベルは次のエラー メッセージを返します:

これらの文字列から証明修復トレーニングの例を導き出すために、ここでは、定理ステートメント、失敗した証明試行、およびエラー メッセージが、人間が作成した正しいコードを使用して入力として連結されます。ターゲットとしての証拠。

#上の図は、トレーニング データの作成プロセスを詳しく示しています。

証明生成モデルを使用して、元のトレーニング セットの各質問に対して温度 0 の証明をサンプリングします。

Proofing Assistant を使用して、失敗したすべての校正とそのエラー メッセージを記録し、新しい校正/修正トレーニング セットの構築に進みます。

元のトレーニング サンプルごとに、定理ステートメント、証明生成モデルによって生成された (間違った) 候補証明、および対応するエラー メッセージを連結して、新しいトレーニング サンプル シーケンスの入力を取得します。 。

#コンテキストの追加

追加のコンテキストとして、定理ステートメントの前に理論ファイルの行を追加します。たとえば、下の図は次のようになります。

Baldur のコンテキスト付き証明生成モデルは、この追加情報を利用できます。 fun_sum_commute の定理ステートメントに出現する文字列は、このコンテキストでも再び出現するため、それらを囲む追加情報は、モデルがより適切な予測を行うのに役立ちます。

コンテキストは、ステートメント (定理、定義、証明) または自然言語の注釈です。

LLM の利用可能な入力長を活用するために、研究者らはまず、同じ理論ファイルから最大 50 個のステートメントを追加しました。

トレーニング中、これらのステートメントはすべて最初にトークン化され、次にシーケンスの左側が入力長に合わせて切り詰められます。

#上の図は、コンテキストありとコンテキストなしの生成モデルの証明成功率と証明試行回数の関係を示しています。コンテキストを伴う証明生成モデルが、単純な生成モデルよりも一貫して優れていることがわかります。

上のグラフは、さまざまなサイズと温度のモデルについて、検証された定理と推論コストの比率を示しています。

生成されたモデルの証明成功率、8B モデルと 62B モデルのコンテキストと証明試行回数の関係も確認できます。

コンテキストを含む 62B は、生成モデルがコンテキストを含む 8B モデルよりも優れていることを証明します。

ただし、著者らはここで、これらの実験にはコストがかかるため、ハイパーパラメーターを調整することができず、最適化すれば 62B モデルのパフォーマンスが向上する可能性があることを強調しています。

以上がテレンス・タオはそれを見て彼を専門家と呼んだ！ Google などは LLM を使用して定理を自動的に証明し、カンファレンスで優秀な論文を受賞しました。コンテキストが完全であればあるほど、証明はより優れたものになります。の詳細内容です。詳細については、PHP 中国語 Web サイトの他の関連記事を参照してください。