AI が再び数学の世界に関与し、新しい DSP 手法により機械証明の成功率が 2 倍に

数学の定理を自動的に証明することは人工知能の本来の目的であり、常に困難な問題でした。 これまで、人間の数学者は 2 つの異なる方法で数学を記述してきました。

#1 つ目は、誰もがよく知っている方法で、自然言語を使用して数学的証明を記述する方法です。数学の教科書や数学の論文など、ほとんどの数学はこの方法で書かれています。

#2 番目のタイプは形式数学と呼ばれます。これは、数学的証明をチェックするために過去半世紀にわたってコンピューター科学者によって作成されたツールです。

今日では、コンピュータを使用して数学的証明を検証できるように思えますが、それを実行できるのは、数学記号を処理できない特別に設計された証明言語とその混合物を使用する場合のみです。数学者が使用する文書のこと。自然言語で書かれた数学的問題を正式なコードに変換してコンピューターがより簡単に解けるようにすることは、数学における新たな発見を探索できるマシンの構築に役立つ可能性があります。このプロセスは形式化と呼ばれ、自動形式化とは、数学を自然言語から形式言語に自動的に変換するタスクを指します。

形式的な証明の自動化は困難な作業であり、主に形式的なデータが不足しているため、深層学習手法はこの分野ではまだ大きな成功を収めていません。実際、形式的な証明自体は非常に難しく、それができるのは少数の専門家だけであるため、大規模なアノテーションの取り組みは非現実的です。正式な証明の最大のコーパスは Isabelle コード (Paulson、1994) で書かれており、そのサイズは 0.6 GB 未満で、視覚処理や自然言語処理で一般的に使用されるデータセットよりも桁違いに小さいです。形式的な証明の不足に対処するために、これまでの研究では、合成データ、自己教師あり学習、または強化学習を使用して追加の形式的なトレーニング データを合成することが提案されています。これらの方法ではデータ不足はある程度軽減されますが、手作業で作成された大量の数学的証明を十分に活用することはできません。

言語モデル Minerva を例に挙げてみましょう。十分なデータを使用してトレーニングした結果、その数学能力は非常に強力であり、高校の数学テストで平均よりも高いスコアを獲得できることがわかりました。しかし、このような言語モデルには欠点もあり、模倣することしかできず、数学を改善するために独自に訓練することはできません。形式的な証明システムはトレーニング環境を提供しますが、形式的な数学に関するデータはほとんどありません。

正式な数学とは異なり、非公式な数学データは豊富で広く入手可能です。最近、非公式の数学データに基づいてトレーニングされた大規模な言語モデルが、印象的な定量的推論能力を実証しました。ただし、これらは誤った証明を生成することが多く、これらの証明内の誤った推論を自動的に検出することは困難です。

Google の Yuhuai Tony Wu などの研究者は、最近の研究で、DSP (ドラフト、スケッチ、証明) と呼ばれる新しい手法を設計しました。非公式な数学的証明を正式な証明に変換し、正式なシステムによって提供される論理的な厳密さと、大量の非公式なデータの両方です。

# 論文リンク: https://arxiv.org/pdf/2210.12283.pdf

今年の初め、Wu Yuhuai 氏と数人の共同研究者は、OpenAI Codex のニューラル ネットワークを使用して自動形式化作業を実行し、大規模な言語モデルを使用して非公式なステートメントを実現可能性へ自動的に翻訳できることを実証しました。公式な声明。 DSP はさらに一歩進んで、大規模な言語モデルを使用して、非公式のプルーフから正式なプルーフ スケッチ を生成します。証明スケッチは、インタラクティブな定理証明者のような正式なシステムによって解釈できる高レベルの推論ステップで構成されます。それらは、不当な中間予想のシーケンスを含むという点で、完全な正式な証明とは異なります。 DSP の最終ステップでは、自動検証機能を使用してすべての中間予想を証明し、正式な証明スケッチが完全な正式な証明に精緻化されます。

Wu Yuhuai 氏は次のように述べています。LLM が生成する非公式証明を、検証済みの正式証明に変換できることがわかりました。

メソッド

「メソッド」セクションでは、形式的証明の自動化のための DSP メソッドについて説明します。 。ここでは、各問題には、その問題を記述する非公式命題と形式命題があると仮定します。パイプライン全体は 3 つのステージで構成されます (図 1 を参照)。

図 1.

非公式証明 初期段階

DSP アプローチの草案には、自然数学言語 (おそらく LATEX) での記述に基づいて問題の非公式な証明を見つけることが含まれます。結果として得られる非公式の証明は、後続の段階のための下書きとして扱われます。数学の教科書には通常、定理の証明が記載されていますが、場合によっては、定理の証明が欠けていたり、不完全である場合もあります。したがって、研究者らは、非公式の証明の有無に対応する 2 つの状況を検討しました。

最初のケースでは、研究者は、既存の数学理論の正式な実践である「実際の」非公式証明 (つまり、人間によって書かれた証明) が存在すると仮定します。典型的な状況。 2 番目のケースでは、研究者は、実際には非公式な証明は与えられていないというより一般的な仮定を立て、非公式な数学データでトレーニングされた大規模な言語モデルを使用して、証明の候補を作成します。言語モデルは人間による証明への依存を排除​​し、各問題に対して複数の代替ソリューションを生成できます。これらの証明の正しさを自動的に検証する簡単な方法はありませんが、非公式の証明は、適切な正式な証明スケッチを生成する次の段階でのみ役立ちます。

非公式の証明を正式なスケッチにマッピングする

正式な証明のスケッチは、ソリューションの構造をエンコードし、低レベルの詳細は脇に置きます。直観的には、これは高レベルの推測ステートメントの概要を説明する部分的な証明です。図2はプルーフスケッチの具体例です。非公式証明では低レベルの詳細が省略されることがよくありますが、これらの詳細は正式証明では除外できないため、非公式証明から正式証明への直接変換が困難になります。代わりに、この論文では、同じ高レベルの構造を共有する形式的なプルーフ スケッチに非形式的なプルーフをマッピングすることを提案します。プルーフ スケッチに欠けている低レベルの詳細は、自動プルーバによって埋めることができます。大規模な非公式と公式の対訳コーパスは存在しないため、標準的な機械翻訳手法はこのタスクには適していません。代わりに、ここでは大規模な言語モデルの数ショット学習機能が使用されます。具体的には、非公式証明とそれに対応する公式スケッチを含むいくつかのサンプル ペアを使用してモデルにプロンプ​​トを表示し、続いて非公式証明を変換し、モデルに後続のトークンを生成させて必要な公式スケッチを取得させます。このモデルは「自動フォーマライザー」と呼ばれます。

##図 2.スケッチ推測における開示の証拠

このプロセスの最後の部分として、研究者は既製の自動証明装置を実装して、証明スケッチに欠けている詳細を埋めます。ここでの「自動証明装置」とは、次のことができるものを指します。正式に検証可能な証拠を作成する、実証済みのシステム。このフレームワークは、自動証明者の特定の選択に依存しません。記号証明者 (ヒューリスティック証明自動化ツールなど)、ニューラル ネットワーク ベースの証明者、またはハイブリッド アプローチのいずれかになります。自動証明者が証明スケッチ内のすべてのギャップを正常に埋めると、問題の仕様と照らし合わせてチェックできる最終的な正式な証明が返されます。自動証明者が失敗した場合 (たとえば、割り当てられた制限時間を超えた場合)、評価は不成功とみなされます。

実験

研究者らは、miniF2F データセットから生成された問題の正式な証明を含む一連の実験を実施し、定理の大部分がこの方法を使用して自動的に証明できることを示しました。ここでは、非公式な証明が人間によって書かれるか、数学的テキストで訓練された大規模な言語モデルによって起草される 2 つの環境が研究されています。これら 2 つの設定は、既存の理論を形式化する際によく発生する状況に対応しています。つまり、非形式的な証明が存在することがよくありますが、読者への演習として残されたり、余白の制約により欠落したりする場合があります。

#表 1 は、miniF2F データセットで見つかった正式な証明に成功した割合を示しています。結果には、実験からの 4 つのベースラインに加え、人間が書いた証明とモデルが生成した証明を使用した DSP メソッドが含まれています。

11 個のヒューリスティック戦略を備えた自動証明器により、Sledgehammer のパフォーマンスが大幅に向上したことがわかります。成功率は検証セットでは 9.9% ～ 18.0%、テスト セットでは 10.4% ～ 20.9% でした。言語モデルと証明検索を使用した 2 つのベースラインは、miniF2F のテスト セットでそれぞれ 29.9% と 35.2% の成功率を達成しました。

人間が書いた非公式の証明に基づいた DSP アプローチは、miniF2F の検証セットとテスト セットで 42.6% と 39.3% の成功率を達成しました。 488 個の問題のうち合計 200 個がこの方法で証明できます。 Codex モデルと Minerva (8B) モデルは、miniF2F の問題を解決する際に非常に似た結果をもたらしました。どちらも、自動検証ツールが検証セットとテスト セットの問題の 40.6% と 35.3% を解決するように導きました。

Minerva (62B) モデルに切り替えると、成功率はそれぞれ 43.9% と 37.7% に増加しました。人間が書いた非公式の証明と比較すると、その成功率は検証セットでは 1.3% 高く、テスト セットでは 1.6% 低くなります。全体として、ミネルバ (62B) モデルは、miniF2F 上で 199 個の問題を解決できますが、これは人間が書いた証明よりも 1 個少ない問題です。 Minerva (540B) モデルは、miniF2F の検証セットとテスト セットの問題のそれぞれ 42.6% と 38.9% を解決し、199 件の成功した証明も生成しました。

DSP アプローチは、人間を使用した非公式の証明、または言語モデルによって生成された非公式の証明の両方の場合において、自動証明者を効果的にガイドします。 DSP は証明者の成功率をほぼ 2 倍にし、Isabelle を使用して miniF2F で SOTA パフォーマンスを生成します。さらに、より大きなミネルバ モデルは、自動化された形式的証明者をガイドする上で人間とほぼ同じくらい役に立ちます。 以下の図に示すように、DSP メソッドは Sledgehammer ヒューリスティック証明者のパフォーマンスを大幅に向上させ (~20% -> ~40%)、miniF2F で新しい SOTA を達成します。

Minerva の 62B および 540B バージョンは、人間の証明と非常によく似た証明を生成します。

詳細については、元の論文を参照してください。

以上がAI が再び数学の世界に関与し、新しい DSP 手法により機械証明の成功率が 2 倍にの詳細内容です。詳細については、PHP 中国語 Web サイトの他の関連記事を参照してください。