AIは数学データベースの問題の82%を証明でき、Transformerをベースにした新しいSOTAが達成されました。

科学者たちは最近、AI に数学の授業をさせることに夢中になっていると言わざるを得ません。

現在、Facebook チームもこの取り組みに参加し、定理の証明を完全に自動化でき、SOTA よりも大幅に優れた新しいモデルを提案しました。

ご存知のように、数学の定理は複雑になるにつれて、人間の力だけで定理を証明することが難しくなります。

そのため、コンピュータを使用して数学の定理を証明することが研究の焦点となっています。

以前、OpenAIはこの分野に特化したGPT-fと呼ばれるモデルも提案しており、Metamathの問題の56％を解決できるという。

今回提案された最新の方法では、この数字を82.6％まで高めることができます。

同時に、研究者らは、この方法はGPT-fに比べて時間がかかりませんし、計算消費量を10分の1に削減できると述べています。

今回はAIが数学との戦いに勝利するのでしょうか？

トランス

本論文で提案する方法は、Transformer に基づくオンライン トレーニング手順です。

大まかに3つのステップに分けられます。

まず、数学的証明ライブラリで事前トレーニングを行います。

次に、教師ありデータセットでポリシーモデルを微調整します。

3番目は、オンライントレーニング戦略モデルと判断モデルです。

具体的には、検索アルゴリズムを使用して、モデルが既存の数学的証明ライブラリから学習し、それを拡張してさらに多くの問題を証明できるようにします。

数学的な証明ライブラリには、Metamath、Lean、独自に開発した証明環境の 3 つがあります。

簡単に言えば、これらの証明ライブラリは、通常の数学言語をプログラミング言語に似た形式に変換します。

Metamath のメインライブラリは set.mm で、ZFC 集合論に基づく約 38,000 の証明が含まれています。

Lean は、IMO コンテストに参加できる Microsoft の AI アルゴリズムとしてよく知られています。 Lean ライブラリは、同じ名前のアルゴリズムに関する学部レベルの数学の知識をすべて教え、これらの定理を証明することを学習できるように設計されています。

この研究の主な目的は、問題を証明するための一連の適切な戦略を自動的に生成できる証明器を構築することです。

この目的のために、研究者らはMCTSに基づく不均衡ハイパーグラフ証明検索アルゴリズムを提案した。

MCTS はモンテカルロ木探索と訳され、ゲームツリー問題を解決するためによく使用されます。AlphaGo のおかげでよく知られています。

その動作プロセスは、検索空間内でランダムにサンプリングすることで有望なアクションを見つけ、そのアクションに基づいて検索ツリーを拡張することです。

この研究でも同様の考え方が採用されました。

検索証明プロセスはターゲット g から始まり、下方向に検索し、徐々にハイパーグラフへと発展していきます。

ブランチの下に空のセットが表示された場合、最適な証明が見つかったことを意味します。

最後に、バックプロパゲーションプロセス中に、ハイパーツリーのノード値と操作の合計数をメモします。

このセッションでは、研究者は戦略モデルと判断モデルについて仮説を立てました。

ポリシー モデルにより、判断モデルはサンプリングを実行でき、判断モデルは現在のポリシーが証明方法を見つける能力を評価できます。

検索アルゴリズム全体は上記の 2 つのモデルに基づいています。

どちらのモデルも Transformer モデルであり、重みを共有します。

次はオンライントレーニングの時間です。

このプロセス中、コントローラは検証のためにステートメントを非同期 HTPS に送信し、トレーニング データと証明データを収集します。

次に、バリデーターはトレーニング サンプルを分散トレーナーに送信し、モデルのコピーを定期的に同期します。

実験結果

テスト段階では、研究者らはHTPSとGPT-fを比較しました。

後者は、OpenAI が以前に提案した数学定理推論モデルであり、これも Transformer に基づいています。

結果は、オンラインでトレーニングされたモデルがMetamathの質問の82％を証明できることを示しており、これはGPT-fの以前の記録56.5％を大幅に上回っています。

Lean ライブラリでは、このモデルは定理の 43% を証明でき、これは SOTA よりも 38% 高い数値です。以下は、このモデルによって証明された IMO の質問です。

しかし、まだ完璧ではありません。

例えば、次の質問では、最も簡単な方法で問題を解決しませんでした。研究者は、これは注釈に誤りがあったためだと述べました。

もう一つ

四色定理の証明は、コンピュータを使用して数学の問題を証明する最もよく知られた例の 1 つです。

四色定理は、現代数学の 3 大問題のうちの 1 つです。この定理は、「4 色だけを使用して、あらゆる地図を異なる色で表示できるため、共通の国境を持つ国々を異なる色で表示することが可能になる」というものです。

この定理の証明には膨大な計算が必要だったため、提案されてから 100 年経っても誰も完全に証明できませんでした。

1976 年になってようやく、イリノイ大学の 2 台のコンピュータで 1,200 時間と 100 億回の判断を経て、地図には 4 色でマークするだけでよいことが証明され、数学界全体にセンセーションを巻き起こしました。

さらに、数学の問題が複雑になるにつれて、定理が正しいかどうかを人間の力で検証することが難しくなります。

最近、AIコミュニティは徐々に数学の問題に注目するようになりました。

2020年、OpenAIは自動定理証明に使用できる数学定理推論モデルGPT-fをリリースしました。

この方法は、テスト セット内の証明の 56.5% を完了することができ、当時の SOTA モデル MetaGen-IL を 30% 以上上回りました。

同年、マイクロソフトはIMOテスト問題を生成できるLeanもリリースしました。これは、AIがこれまでに見たことのない問題を生成できることを意味します。

昨年、OpenAIがGPT-3に検証機能を追加したところ、数学の問題を解く結果が以前の微調整方法よりも大幅に向上し、小学生レベルの90％に達した。

今年1月、MIT＋ハーバード＋コロンビア大学＋ウォータールー大学の共同研究により、彼らが提案したモデルが高度な数学に使用できることが示されました。

つまり、科学者たちは、単一科目の学生である AI が、文系と理系の両面でバランスのとれた人材になれるよう、懸命に取り組んでいるのです。