ビッグモデルは、テレンス・タオが問題を解決し、数学の定理を証明するのに役立ちます。数学は本当に AI の助けを借りてブレークスルーを達成する最初の分野になるのでしょうか?

ディープマインドは昨年2月、プログラミング支援ツール「AlphaCode」をリリースした。人工知能技術を使用して、プログラマーがより速くコードを書くのを支援します。コードを自動的に完成させ、コードの提案を提供し、エラーをチェックすることで、プログラミングの効率を向上させます。 AlphaCode の登場は、AI が現実世界の課題解決に向けて新たな大きな一歩を踏み出したことを意味します。

偶然にも、同じ日に、OpenAI も重要な成果を披露しました。彼らが開発したニューラル定理証明器が、国際数学オリンピックの問題 2 つを無事に解いたのです。この成果は、マイクロソフトが長年磨き上げてきた数学的 AI である Lean に基づいて達成されました。 Lean は 2013 年に開始されました。数学者は数式をコードに変換し、それを Lean に入力することで、プログラムが定理が正しいかどうかを検証できるようになります。 OpenAI の成功は、AI がプログラミングなどの応用分野の問題を解決するだけでなく、数学などの自然分野の克服にも使用できることを示しています。

写真

これは AI 研究者の単なる希望的観測ではないことは注目に値する。 AlphaCode をいち早く取り入れたソフトウェア エンジニアと同様に、フィールズ賞を受賞した Terence Tao 氏などの数学者も AI をますます頻繁に使用しています。彼は、2026年までにAIが数学研究における信頼できる共著者になるとさえ予測しました。

同時に、数学の問題に焦点を当てた AI も成長と発展を遂げています。LeanDojo と呼ばれるオープン プラットフォームは、大規模な言語モデルに基づくオープンソースの定理証明器のセットを提供しており、定理証明に機械学習手法を使用する際のプライベート コード、データ、大規模なコンピューティング要件などの障害を排除し、定理証明の分野での機械学習手法の研究を促進しています。

「数学は人工知能を通じて大きな進歩を遂げる最初の分野になると信じている」と、エヌビディアの上級AI研究科学者ジム・ファン氏は、これらの進歩を見た後、ツイートで予測した。

上記の展開に加えて、ジム・ファン氏は次のような推論も挙げています。

• 数学は簡単にコーディング問題に変換でき、その中で文字列が重要な役割を果たすため、人工知能ツールで数学の問題を簡単に処理および分析できます。
• 経験的結果に依存する分野とは異なり、数学は Lean などの定理証明器を通じて厳密に検証できます。
• 物理的な実験に依存する分野（生物学や医学など）とは異なり、数学は物理的な実験を必要とせず、まだ完全に成熟していないロボット工学や実験装置に依存する必要もありません。

数学と AI のクロスオーバーの旅において、数学者と AI 研究科学者は共同でさらなる可能性を探求しています。おそらく、テレンス・タオとジム・ファンの予測はどちらもより早く実現するだろう。

テレンス・タオの手によってAIは数学者の右腕となった

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

多くの著名な数学者の中で、テレンス・タオは ChatGPT のような大規模な AI モデルの数学的価値を最初に受け入れ、発見した人の 1 人です。今年3月、ChatGPTが鶏とウサギを同じケージに入れる問題さえ解けなかったとき、テレンス・タオは、この種の大規模モデルは、数学研究者が意味検索を行ったり、プロンプトを生成したりするのを支援するなど、いくつかの補助的なタスクを十分に実行できると考え、ChatGPTに前向きな姿勢を示しました。

写真

この例では、Terence Tao さんが尋ねた質問は、「xx に関する式を探しています。古典的な定理だと思うのですが、名前が思い出せません。何か印象はありますか?」というものでした。この質疑応答では、ChatGPT は正しい答え (Kummer の定理) を出すことができませんでしたが、出した近似的な答え (Legendre の定理) に基づいて、従来の検索エンジンと組み合わせることで、簡単に正しい答えを見つけることができます。

その後間もなく、OpenAI は数学的機能が大幅に向上した GPT-4 をリリースしました。テレンス・タオ氏もこの強力な AI ツールのロックを解除しようと試みています。

使用プロセスの中で、彼はいくつかの経験をまとめました。AI に数学的な質問に直接答えさせようとするのではなく (このようにして得られる答えはおそらく無意味です)、協力者の役割を果たさせ、戦略的な提案をするように依頼してください。

このプロンプト方式に従って、Terence Tao 氏は GPT-4 の助けを借りて数学の証明問題を無事に解決しました (GPT4 は 8 つの方法を提案し、そのうち 1 つが問題を解決しました)。

写真

Terence Tao が GPT-4 を使用して解決した問題。

上記の証明問題を解決するために、Terence Tao は GPT-4 に次のようなプロンプトを提供しました。「こんにちは、私は数学の教授です。問題解決手法を提案するのが得意な数学の専門家の協力者の役割を果たしていただければ幸いです。私は MathOverflow で次の質問に答えようとしています...」

GPT-4 によって提示されたいくつかの提案。

もちろん、この証明問題に加えて、Tao は GPT-4 を使用して、次のような他の作業も完了させています。

• 質問する: 彼は GPT-4 に最近の数学のプレプリントの最初の数ページを入力し、同僚が尋ねるのと同じような論文に関する質問を生成するように依頼しました。これにより、彼はスピーチの準備をより良く行うことができます。
• 質問への回答: 彼は現在、GPT-4 を日常的に使用して、以前は慎重に準備された検索エンジンのクエリを介して回答しようとしていたような、何気ない漠然とした質問に答えています。
• 執筆支援: 彼はかつて、執筆を支援するために、複雑な文書の下書きの提案を GPT-4 に依頼しました。

しかしタオ氏は、数学などの学術分野における AI の広範な応用は、出版部門と教育部門の両方にとって試練であるとも指摘しました。AI ガイドによる大学院入門レベルの数学論文が 1 日もかからずに生成できるようになると、研究ジャーナルは出版と引用のメカニズムをどのように変えるのでしょうか。大学院教育に対する私たちのアプローチはどのように変化するのでしょうか?学生にこれらのツールの使用を積極的に奨励し、トレーニングしていますか?タオ氏はこれらの質問には一切答えなかった。

この研究はテレンス・タオの予測が早く実現するのに役立つかもしれない

正式な定理の証明は、機械学習において常に重要な課題でした。形式的な証明は本質的にはコンピュータ プログラムですが、C++ や Python の従来のプログラムとは異なり、証明の正確さは証明支援ツール (冒頭で述べた Lean など) を使用して検証できます。定理証明は、評価が非常に厳密で、モデルを幻覚させる余地がない特殊な形式のコード生成です。

これは、現在の大規模言語モデル (LLM) にとって課題です。LLM は、コード生成においては優れた機能を示していますが、事実性と幻覚の点では依然として欠点があります。

これまで、定理証明のための LLM に関する研究は多くの障害に直面してきました。たとえば、既存の LLM ベースの証明器はどれもオープンソースではありません。それらはすべてプライベートな事前トレーニング データを使用し、数千の GPU 時間に達する計算要件があります。さらに、一部のインフラストラクチャは分散トレーニングと証明アシスタントとのやり取りのためにカスタマイズに依存しており、どちらもオープンソース コードなしでは完全に再現することは不可能です。

最近の研究では、カリフォルニア工科大学、NVIDIA、その他の機関の研究者がこの課題解決に向けて重要な一歩を踏み出し、オープンプラットフォーム「LeanDojo」を提案しました。

写真

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

プロジェクトホームページ: https://leandojo.org/

全体として、この研究には次のような貢献があります。

• まず、Lean からデータを抽出して操作するためのツールを紹介します。
• 次に、定理証明用の最初の検索強化言語モデルである ReProver を開発しました。
• 第三に、学習ベースの定理証明のための挑戦的なベンチマークを構築し、それを使用してReProverの有効性を検証します。
• 最後に、データ、モデル、コードを公開することで、定理証明のための LLM の研究が促進されます。

LeanDojo の誕生により、現状が変化すると予想されています。オープンソースのツールキット、モデルからベンチマークまで、LeanDojo により研究者は最先端の LLM ベースの証明器を適度な計算コストで入手できるようになります。 ReProver はプライベート データセットに依存せず、1 週間以内に単一の GPU でトレーニングできます。

研究の詳細

Lean は、従来のプログラムだけでなく、定理や証明を書くのにも使用できるプログラミング言語です。 Lean は 2 つのメカニズムを提供します。1 つ目は、依存型を持つ関数型プログラミングに基づいて、プログラム、数学的オブジェクト、定理、証明を定義するための統一言語を提供することです。2 つ目は、機械でチェック可能な証明を半自動的に構築するための戦術システムを提供することです。

図 2 は、Lean で定理がどのように形式化され証明されるかを示す簡単な例を示しています。

写真

戦術の構文は非常に柔軟です。パラメータを受け入れ、複合戦術に組み合わせることができます。ポリシーは、ドメイン固有言語 (DSL) のプログラムとして表示できます。ユーザーは新しい戦略を定義することで DSL を拡張できます。この離散的、組み合わせ的、かつ無制限のアクション空間により、機械学習における定理の証明が困難になります。

もう一つの課題は前提の選択でした。前提は、定理を証明するのに役立つ既存の公理または定義であり、戦略の議論として使用されます。証明では、まだ定義されていない前提を使用することはできません。また、現在のファイルにインポートされていない前提を使用することもできません。通常、前提は数十万の既存の定義と定理を含む大規模な数学ライブラリから抽出されるため、戦略を生成するときに人間と機械の両方が適切な前提を選択することが困難になります。これは定理証明における重要なボトルネックであり、研究者らは検索強化型 LLM で解決したいと考えている。

LeanDojoベンチマーク

研究者らは LeanDojo を使用して、mathlib から抽出された 96,962 個の定理/証明を含むベンチマークを構築しました。このベンチマークは、解析、代数、幾何学などの多様なトピックを網羅する、現在利用可能な最大規模の数学に重点を置いた定理証明データセットの 1 つです。

既存の Lean データセットとは異なり、LeanDojo ベンチマークには 128,163 個の前提定義も含まれており、定理だけでなく、図 2 の gcd など、前提として使用できるその他の定義も含まれています。さらに、データセットには 212,787 の戦略が含まれており、そのうち 126,058 の戦略には少なくとも 1 つの前提があります。店舗を有する戦略のうち、店舗数の平均は 2.12 でした。

LeanDojo ベンチマークは、次の 2 つの重要な質問に回答します。

• 前提条件情報

Lean リポジトリ (例: mathlib または lean-liquid) には、人間が書いた定理/証明のソース コードが含まれています。しかし、元のコードには、証明ステップ間の中間状態など、Lean を使用するときに人間が取得できる実行時情報がないため、検証者のトレーニングには適していません。

LeanDojo は、ファイルの依存関係、抽象構文木 (AST)、証明ステータス、戦略、前提など、元の Lean コードでは直接表示されない豊富な情報を含む任意の Lean GitHub リポジトリからデータを抽出できます。 LeanDojo ベンチマークには、前提（証明で使用される場所とライブラリで定義されている場所）の詳細な注釈が含まれており、定理証明における重要なボトルネックでもある前提選択のための貴重なデータを提供します。

• 困難なデータセグメンテーション

研究者らは、定理をランダムにトレーニングとテストに分割するという一般的な慣行が、以前の論文でパフォーマンスの過大評価につながることを発見した。 LLM は、トレーニング中に類似の定理の証明を記憶するだけで、一見難しい定理を証明できます。

人間が書いた Lean コードでよく使われる慣用句は、同じ数学的概念のわずかに異なる特性に対して、類似の定理/証明ブロックを持つことです。たとえば、図 3 では、最後の 2 つの定理は似ているだけでなく、証明も同じです。どちらか一方がトレーニング中であれば、モデルはメモリによってもう一方を簡単に証明できます。このショートカットにより、モデルは、証明に前提を必要とする定理も含め、一見すると自明ではない定理を証明できるようになります。

写真

LeanDojo ベンチマークでは、研究者は、トレーニングで使用されたことのない前提を少なくとも 1 つ使用していることを証明するテストを要求する、挑戦的なデータ分割 novel_pensions を設計することでこの問題を軽減しています。

たとえば、図 3 の最後の 2 つの定理はどちらも前提 conj_mul を使用しています。 1 つの定理が novel_pensions 分割のトレーニング セットに含まれている場合、もう 1 つの定理もトレーニングに含まれている必要があります。

Lean とプログラム的にやりとりする

LeanDojo のもう 1 つの重要な機能は、プログラムで Lean と対話できることです。これにより、Lean はジムのような環境になり、証明者は証明ステータスを観察し、ステータスを変更するための戦略を実行し、エラーや証明完了に関するフィードバックを受け取ることができます。この環境は、バリデーターを評価/展開したり、RL を介して証明者をトレーニングしたりするために不可欠です。

以下は、戦略を通じて Lean と対話するために使用される LeanDojo の主な形式です。 Lean はポリシーベースではない他の証明スタイルもサポートしていますが、LeanDojo はポリシーベースの証明のみをサポートしています。しかし、十分な一般性があれば、あらゆる証明を戦略スタイルの証明に変換できます。

写真

リプローバー

その後、研究者は LeanDojo ベンチマークを使用して ReProver をトレーニングし、評価しました。その中核となるのは、検索機能によって強化されたポリシージェネレーターです（図1、下）。

写真

現在の証明状態に基づいて、潜在的に有用な前提を少数取得し、状態と取得された前提間の接続に基づいて戦略を生成します。定理を証明する際、モデルは各ステップで複数の戦略候補を生成し、標準的な最適検索アルゴリズムでそれらを使用して証明を見つけます。

特に、ReProver のトレーニングには単一の GPU で 5 日間 (120 GPU 時間) しかかからず、従来の方法 (1,000 時間以上) よりも大幅に少ない計算量で済みます。

これまでの LLM ベースの証明器は、数学とコーディングの特定のデータセットで事前トレーニングされていましたが、計算コストが高く、データセットは機密情報でした。対照的に、ReProver はドメイン固有の事前トレーニングを回避し、一般的な公開されている比較的小さなモデル チェックポイントである「google/byt5-small」上に構築されています。

さらに、ReProver は人間が作成したポリシーに基づいてのみ微調整され、補助データや Lean とのオンラインのやり取りを通じて収集されたデータは使用されません。これらの直交方向は有用ですが、方法の複雑さと計算要件が大幅に増加します。

評価実験では、ReProver は定理の 51.4% を証明でき、検索なしでポリシーを直接生成するベースライン (47.5%) や、GPT-4 を使用してゼロショット方式でポリシーを生成する別のベースライン (28.8%) を上回りました。

写真

研究者らは、MiniF2F と ProofNet という 2 つのデータセットでも ReProver をテストしました。 MiniF2F の定理の 26.5%、ProofNet の定理の 13.8% を証明でき、これは強化学習における SOTA 手法とほぼ同等ですが、トレーニング中に使用するリソースははるかに少なくなります。

さらに、多くの定理には Lean における真実の証明がありません。 ReProver は、Lean で現在証明されていない 65 の定理を証明することができました。そのうち 33 の証明は MiniF2F によって、39 の証明は ProofNet によって発見されました。研究者らは、ReProver は Lean の既存の数学ライブラリを強化するための効果的なツールとしても使用できると述べています。

ChatGPTプラグイン

研究者らは、ChatGPT が Lean と対話することで定理を証明できるようにする LeanDojo ChatGPT プラグインも構築しました。定理証明用に微調整された LLM (ReProver など) と比較して、ChatGPT は、人間が証明アシスタントと対話するのと同様に、非公式の数学と正式な証明手順を織り交ぜることができます。 Lean からのエラー メッセージを解釈でき、専用の証明器よりも操作が簡単です。しかし、検索と計画の弱点により、ほとんどの場合、正しい証明を見つけることは困難です。

次に例を示します。

a + b + c = a + c + b

スターリングの公式

ガウスの和の公式

チーム情報

最後に、この記事の著者について紹介しましょう。

論文の筆頭著者であるカイユ・ヤン氏は現在、カリフォルニア工科大学の計算科学および数理科学科（CMS）のポスドク研究員であり、以前はプリンストン大学で博士号を取得しています。

Alex Gu は、Armando Solar-Lezama の指導を受ける MIT の博士課程の学生です。以前は、MIT で学士号と修士号を取得し、Meta AI Research、Jane Street、pony.ai でインターンシップの経験を積んでいました。

Peiyang Song は現在、カリフォルニア大学サンタバーバラ校 (UCSB) のクリエイティブ スタディーズ カレッジ (CCS) でコンピューター サイエンスの学部生です。彼の研究は、1) 大規模言語モデル (LLM) と対話型定理証明器 (ITP) を組み合わせたニューラル定理証明と自動推論、および 2) エネルギー効率の高い機械学習推論のための時相論理という 2 つの主な方向に焦点を当てています。

Shixing Yu は現在、米国コーネル大学でコンピュータサイエンスの博士課程に在籍しています。以前はテキサス大学オースティン校で修士号を取得し、北京大学情報科学技術学院で学士号を取得しました。