Discovering New Theorems via LLMs with In-Context Proof Learning in Lean

本論文は、形式検証済みの定理と証明を反復的に LLM 自身にフィードバックすることで文脈内学習を活用し、新規かつ証明が困難な数学的予想の発見率と成功を大幅に向上させるパイプラインである「仮説・証明ループ（CPL）」を導入する。

要約

非常に賢いものの、少し忘れっぽいロボットに、複雑な数学パズルを解く方法を教えることを想像してみてください。そのロボットは大規模言語モデル（LLM）であり、パズルはLeanと呼ばれる厳密なコンピュータ言語で書かれた形式的な数学的証明です。

この論文は、このロボットを教える新しい方法として、**「仮説・証明ループ（CPL）」**を導入しています。その仕組みを、簡単なアナロジーを用いて説明します。

問題：「推測と検証」の罠

通常、AI に数学をさせようとする際、人々は**「パズルを推測し、それを一度に解く」**よう求めています。

• アナロジー： 学生に「数学の問題を作成し、即座にそれを解け」と頼むことを想像してください。
• 問題点： 学生は怠惰になります。解きやすい「2 + 2 = 4」のような簡単な問題を書くのです。なぜなら、それらは解きやすいからです。彼らは失敗するかもしれないと知っているため、難しい問題を避けようとします。その結果、AI は数千もの簡単で退屈な証明を生成し、難しく面白いものを見逃してしまいます。

解決策：「二段階のダンス」（CPL）

著者たちは、このプロセスを**「仮説立案者（Conjecturer）」（アイデア生成者）と「証明者（Prover）」**（解き手）という 2 つの明確な役割に分割しました。

1. 仮説立案者（建築家）： AI のこの部分は、既存の数学規則のライブラリを参照し、新しいアイデア（仮説）を考え出します。まだそれを解こうとはせず、ただ書き留めるだけです。
2. 証明者（建設者）： この部分はアイデアを受け取り、それらの証明を構築しようとします。失敗すれば、再び試みます。成功するか、試行回数が尽きるまで、試行を繰り返します。
3. ライブラリ（記憶）： 証明者が証明を成功させるたびに、その証明はライブラリに追加されます。

魔法の材料：コンテキスト内学習
ここが巧妙な点です。証明者は、元の数学規則だけを見るのではありません。現在のセッション中にすでに成功して構築した証明のライブラリも参照します。

• アナロジー： 学生がテストを受ける場面を想像してください。従来の方法では、テスト開始前に暗記した内容だけを頼りにしていました。しかし、この新しい方法では、学生が問題を正しく解くたびに、次の問題に取り掛かる前に、自分自身の解答を読むことが許可されます。彼らは、自分自身の最近の成功から「コツ」や「戦略」を学びます。

発見されたこと

研究者たちは、AI がまだ十分に熟知していないトポロジー（形状や空間を扱う数学の一分野）のいくつかの難しい概念で、この方法をテストしました。

• 量対質： 従来の方法（一度に推測して解く）は、より多くの定理を生成しましたが、それらはほとんどが短く簡単でした。新しい方法（CPL）は、生成される定理の総数は少なくなりましたが、それらははるかに難しく、長くなりました。
• 大きな勝利： 新しい方法は、「アルファ・オープン集合」に関する特定の難しい定理を、従来の方法が 20 回試行しても決して発見できなかったものを、見事に発見しました。
• 成功からの学習： AI に、自分自身の過去の証明のライブラリを「カンニングペーパー（コンテキスト）」として与えたとき、そのコンテキストなしでは解けなかった難しい定理を証明することができました。AI が平易な英語で定理を証明できなかった場合でも、類似した成功した証明を見た後は、Lean コードで証明することができました。

結論

この論文は、「アイデア生成」と「証明解決」を分離し、AI がリアルタイムで自らの検証済みの成功から学習させることで、そうでなければ見逃してしまうより困難で複雑な数学的真理を発見させることができると主張しています。これは、最終試験を受ける前に自らの宿題を勉強させることで、AI に助走をつけさせるようなものです。

注記： この論文は、数学的定理の生成と検証に関するこの方法に厳密に焦点を当てています。医療診断、金融予測、または形式的数学以外の他の実世界への応用において、この方法が機能すると主張しているわけではありません。

技術概要

技術的概要：イン・コンテキスト証明学習を用いた Lean における LLM による新定理の発見

問題定義
大規模言語モデル（LLM）は形式的定理証明において有望な成果を示しているが、重大な課題に直面している。すなわち、ハルシネーション（幻覚）が発生する可能性があり、数学的予想とその証明を同時に生成すると、往々にして自明または容易な定理に収束してしまうことである。既存のアプローチは通常、広範な訓練データを必要とし、クローズドソースモデルへの適用が困難な教師あり微調整（SFT）または検証済み報酬を用いた強化学習（RLVR）に依存している。さらに、現在の手法は「証明が困難な」定理の発見に苦慮する傾向がある。これは、定理を生成する確率が、その定理を即座に証明できる成功率によって重み付けられるため、探索が単純で短い証明へと崩壊してしまうからである。

手法：予想・証明ループ（CPL）
著者らは、数学的予想を自動生成し、Lean 4 において検証するパイプラインである**予想・証明ループ（Conjecturing-Proving Loop: CPL）**を提案する。このフレームワークは、予想の生成と証明の生成を分離し、両段階において以前に検証済みの定理のライブラリをコンテキストとして利用する。

パイプラインは、予想生成エージェント（Conjecturer）、証明生成エージェント（Prover）、Lean サーバー、およびライブラリ（Lean コードデータ）という 4 つの主要コンポーネントで構成される。

1. 予想フェーズ: 予想生成エージェントは、現在のライブラリに基づいて Lean 4 形式の新しい数学的命題を生成する。構文の妥当性と新規性を確保するため、Lean サーバーに照会を行う（Mathlib4 または現在のライブラリ内の既存定理によって既に証明可能な命題ではないことを確認する）。
2. 証明フェーズ: 各妥当な予想に対して、証明生成エージェントは形式的証明の構築を試みる。重要なのは、証明生成エージェントに、以前に検証済みの定理と証明を含むライブラリをコンテキストとして提供することである。これにより、LLM はモデルの再訓練なしにイン・コンテキスト学習を通じて証明戦略を学習できる。証明生成エージェントは、Lean サーバーからのエラーメッセージを用いて試行を洗練させながら、最大試行回数（実験では 16 回に設定）まで反復する。
3. 反復: 検証済みの予想と証明のペアはライブラリに追加され、それが次の反復におけるコンテキストとして機能する。

この分離により、システムは証明の難易度に基づいて探索リソースを割り当てることが可能となる。命題と証明を同時に生成する単純なループ（SL）とは異なり、CPL は単一の命題を破棄する前に複数の証明を試みる。これにより、生成される定理の分布は、単に証明が容易なものから、証明可能だが困難なものへとシフトする。

主要な貢献

1. パイプラインの提案: 予想生成と証明生成を分離するフレームワーク CPL の導入により、より長く複雑な証明の発見を可能にした。
2. クローズドソースモデルへのイン・コンテキスト学習の適用: 自らの以前に検証済みの出力からのイン・コンテキスト学習を通じて、クローズドソースの LLM（具体的には ChatGPT-o3）が証明能力を向上させうることを実証し、パラメータ更新や微調整の必要性を排除した。
3. 理論的および実証的検証: 同時生成フレームワークと比較して、CPL が証明が困難な定理を生成する可能性を高めることを示す理論モデルを提供した。実験的には、CPL がベースラインフレームワークでは発見できなかった特定の研究レベルの定理を再発見することに成功したことを確認した。

実験結果
著者らは、Mathlib 内で定義されているがライブラリにはまだ含まれていない位相的概念（半開集合、$\alpha$-開集合、前開集合）を用いて、CPL を単純ループ（SL）ベースラインと比較評価した。対象とした定理は、「2 つの$\alpha$-開集合の共通部分は$\alpha$-開集合である」というものである。

• 発見率: 20 回の実験実行において、CPL は対象定理を 5 回発見した。一方、平均的に著しく多くの定理を生成した（328 対 106）SL フレームワークは、対象定理を 1 回も生成できなかった。フィッシャーの正確確率検定により、この差が統計的に有意であることが確認された（$p = 0.024$）。
• 証明の長さ: CPL は、SL に比べて文字数において著しく長い証明を持つ定理を生成し、このフレームワークがより困難な証明へと焦点をシフトさせるという理論的主張を裏付けた。
• コンテキストの有効性:
  • 再証明: 生成された定理を再証明する際、ライブラリをコンテキストとして提供することで成功率が 91% から 99% に向上した（$p = 4 \times 10^{-35}$）。
  • 対象定理: 生成されたライブラリをコンテキストとして提供した場合、証明生成エージェントは 80 回の試行のうち 7 回で対象となる$\alpha$-開集合の共通部分定理の証明に成功した。ライブラリなしでは、100% 失敗した。
  • 自然言語ベースライン: 自然言語で定理の証明を求められた際、ChatGPT-4o は頻繁に定理を偽と判断するか、誤った証明を提供し、ChatGPT-o3 は一貫して偽と判断した。これは、この定理がモデルの事前学習知識の範囲外であることを示している。Lean 4 での成功は、生成されたライブラリからの証明戦略のイン・コンテキスト学習に起因すると考えられる。

意義と主張
本論文は、CPL が自己生成された検証済み証明からのイン・コンテキスト学習を活用することで、LLM の非自明な定理発見における限界を効果的に克服すると主張している。著者らは、このアプローチにより、LLM に明示的に知られていない概念に関する命題を生成することで、Mathlib などの形式的数学ライブラリを自動的に拡張できることを強調している。この研究は、予想フェーズと証明フェーズを分離し、反復的なコンテキストの充実を組み合わせることが、従来の訓練手法が適用できないクローズドソースモデルを含むニューラル定理証明にとって viable な戦略であることを示唆している。著者らは謙虚な立場を維持しており、フレームワークが既知の研究レベルの定理を再発見することに成功したものの、より深く洞察に満ちた数学的命題の生成プロセスを洗練させるための将来の研究が必要であると指摘している。