OpenAIが数学定理推論モデルGPT-fを初めてリリース、23の導出結果が専門データベースに収録

この記事はLeiphone.comから転載したものです。転載する場合は、Leiphone.com公式サイトにアクセスして許可を申請してください。

最近、GPTファミリーに新しいメンバー、 GPT-fが加わりました。

GPTファミリーといえば、今年大人気となったGPT-3が真っ先に思い浮かびます。Transformerアーキテクチャをベースにしたこの言語モデルは、人間を騙せるほど優れたテキスト生成能力を持っています。

少し前、GPT-3 を使って専門家になりすまして Reddit の投稿に返信した人がいて、何度も「高い評価」を得ていました。そのコンテンツが人間によって書かれたものではないことがネットユーザーによって発見されたのは、それから 1 週間後のことでした。

GPT-3と同様に、最新のGPT-fもTransformer言語モデルに基づいていますが、違いは自動定理証明(ATP)の問題を解決することを目的としている点です。

GPT ファミリーの創設企業である OpenAI は、Transformer アーキテクチャが自然言語処理、コンピューター ビジョン、音声認識の分野で大きな進歩を遂げており、比較的未開発の推論タスクの分野でも十分な可能性を秘めていると考えています。

そして彼らは、GPT-f に関する最新の研究論文でこれを実証しました。

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

GPT-f: 言語モデルで数学の問題を解く

自動定理証明は人工知能研究の分野で非常に重要なトピックであることが知られています。そのタスクは、数学で提案された定理や推測を証明または反証する方法を見つけることです。したがって、自動証明システムには、仮定に基づいて推論する能力だけでなく、一定の判断力も必要になります。

Transformer 言語モデルにはまさにそのような機能があり、その生成能力は、既存の研究の大きな制限、つまり基本的な数学用語の生成も解決できます。

GPT-f は、数学的推論の分野における Transformer 言語モデルの拡張と見なすことができ、自動定理証明を通じてこの点での言語モデルの実現可能性を検証します。

研究者のグレッグ・ブロックマン氏はツイートした。

GPT-f は、既存の定理のより単純な証明だけでなく、まだ決定されていない証明も含め、32 の正式な定理証明を発見しました。これらの証明は Metamath データベースに含まれています。

Githubアドレス:

https://github.com/metamath/set.mm/pull/1547

https://github.com/metamath/set.mm/pull/1710

その中でも、Metamath データベースは現在最も包括的かつ権威のある正式な数学コミュニティです。 Metamath は、抽象数学の定理を表現でき、コンピュータ プログラムによって検証できる証明を伴った小さな言語です。

GPT-f の自動定理証明の組み込みは、正式な数学コミュニティがディープラーニング システムによって提供される証明を採用した初めてのケースとなります。

研究論文の筆頭著者であるスタニスラス・ポル氏も、GPT は自動定理証明における既存の研究の中で最高の SOTA を達成したと述べていることは特筆に値します。

私たちの実験では、GPT-f は既存の自動定理証明器よりも優れており、テストセット内の証明の 56.22% を完了できるのに対し、既存の SOTA モデル MetaGen-IL は定理の 21.16% しか証明できないことがわかりました。

さらに、この論文では、GPT-f が自動定理証明の分野で以下の新しい発見をしたことが示されています。

• 生成的な事前トレーニングによりモデルのパフォーマンスが大幅に向上し、数学的なデータの事前トレーニングは、Web ページの一般的なテキストの事前トレーニングよりも優れたパフォーマンスをもたらします。

• 使用される Metamath データセットは比較的小さいですが、モデル サイズはパフォーマンスと正の相関関係にあります。

• この研究では、言語モデルによって生成された文に対して価値関数を繰り返しトレーニングすることで証明プログラムのパフォーマンスを向上できることがわかり、証明者によって生成された証明に基づいた継続的なトレーニングという継続的な自己改善の戦略が提案されました。

• GPT-f モデルは、Metamath 環境テストを使用して、形式的推論における Transformer アーキテクチャの実現可能性を実証しました。

次に、GPT-f がどのように機能するかを詳しく見てみましょう。

自動証明器と証明支援装置に基づくモデル

論文によると、研究者は GPT-2 や GPT-3 に似た純粋なデコーダー Transformer を使用しました。最大のモデルには 36 層と 7 億 7,400 万のトレーニング可能なパラメーターがあります。

この言語モデルに基づいて、GPT-f は Metamath 形式言語に自動証明器と証明アシスタントの 2 つの部分を提供します。

自動証明器の中核は証明検索プロセスにあります。証明検索には、ルート目標から始めて各目標を探索するための複数の戦略のセットである証明ツリーの維持が含まれます。累積対数確率（Logprob）の優先度によってターゲットが拡張されます。

この研究では正式な環境としてMetamathを採用しています。メインの Metamath ライブラリは set.mm と呼ばれ、ZFC 集合論に基づく約 38,000 の証明が含まれています。

証明検索を実行するには、Metamath モデルとの緊密な結合が必要であることに注意することが重要です。ここで、研究者らは、モデルによって生成された用語がMetamath文法に準拠しているかどうかを確認するための修正されたLR(0)パーサーと、証明ツリーの目標と戦略オブジェクトを表すためのMetamath置換を実装したPythonでMetamathカーネルを作成しました。

全体として、この証明検索プロセスと、それにバンドルされている Metamath 形式検証器が一緒になって、GPT-f 自動検証器を構成します。

実験結果は、トレーニング データセットのサイズが限られているにもかかわらず、モデルのサイズが GPT-f のパフォーマンスに依然としてプラスの影響を与えることを示しています。下の図からわかるように、モデルが大きくなるほど、トレーニングとベンチマーク中に使用される計算量も多くなります。

サンプル データの反復回数が増えるにつれて、モデルのパフォーマンスも向上し続けます。次の図は、反復学習値関数データ生成および再トレーニング中の 160m および 700m (Webmath) パラメーター モデルのパフォーマンスを示しています。

さらに、研究者らはMetamath数学ライブラリに23の定理の簡略化された証明を提供したが、それらはすべてGPT-f自動検証ツールによって生成されたことにも注目すべきである。より短い証明方法を見つけるために、研究者らはset.mmライブラリから命題証明をサンプリングし、GPT-fモデルによって見つかった解と真理値の長さを比較し、短い証明が追加の定理に依存しないことを確認しました。

GPT-f では、オンライン証明アシスタントがモデルのインタラクティブな証明構築を支援できます。論文では、研究者らはこれを用いて200以上の定理と演習を形式化し、モデルのパフォーマンスが大幅に向上したことを発見した。

Proof Assistant は、既存の定理をユーザーの希望する検索ベースに適合させ、使用する定理を提案することで、ほとんどの Metamath 証明に必要なさまざまな簡単な技術的検証手順を自動的に生成できます。

推奨される定理が間違っている場合でも、GPT-f モデルは通常正しい定理を選択しますが、間違った定理は通常、人間が簡単に修正できます。

証明アシスタントは Metamath コミュニティでも使用されています。研究者らは、ユーザーからのフィードバックを自動的に収集しながらコミュニティの効率性を向上させ、それがモデルの精度向上につながるようにすることが目標だと述べた。

論理的な問題を解決するために言語モデルを使用することは本当に信頼できるのでしょうか?

この研究結果は多くのネットユーザーやTwitter上の有力者の注目と議論を集めた。 GPT-f を数学の定理に適用することに疑問を呈する人もいます。

あるネットユーザーが言ったように、GPT-f を過大評価しないでください。ニューラル ネットワークは優れたパターン ファインダーですが、パターン ファインダーにすぎず、アルゴリズム ファインダーではありません。

AIソフトウェア会社のCEOで、アメリカ総合人工知能会議の議長を務めるベン・ゲルツェル氏も、GPT-fは理解せずに定理証明を導く奇妙な実験だと直接書いている。

彼の見解では、GPT の根本的な欠点と一致して、GPT-f は GPT-2 や GPT-3 よりも数学を理解する能力が高くありません。さらに、GPT-3 が真に人間的な言語能力を実現するための適切な研究方向ではないのと同様に、GPT-f は真に人間的な（ましてや優れた）数学定理証明を実現するための適切な研究方向ではありません。

ベン・ゴーツェル氏も自身の意見を表明するブログを書いた。

ブログアドレス: https://multiverseaccordingtoben.blogspot.com/2020/09/gpt-f-one-more-funky-experiment-in.html

しかし、彼はまた、全体的な背景から見ると、ATPにおけるGPT-fの応用は有意義な発展であり、この研究はこの分野の他の専門家によって行われている広範な研究の進歩と一致していると述べた。

実際、Transformer アーキテクチャに基づく GPT-3 モデルはテキスト生成においては優れたパフォーマンスを発揮しますが、チューリング テストに合格したことがなく、単純な数学的推論には明らかな欠陥があります。

同じくTransformerモデルをベースにしたGPT-fも、言語モデルが数学定理間の論理関係を本当に理解しているのか、それとも単に意味を理解しているだけなのか、といった疑問が必然的に生じます。