LLMの定理証明能力を2倍に向上させる「予想と証明の反復」手法とは？

論文

大規模言語モデル（LLM）は、自然言語処理だけでなく、プログラミング支援や論理的推論の分野でも急速に発展しています。その中でも 「定理証明」 は、LLMの推論能力を客観的に評価できる指標として特に注目されています。

しかし、数学の定理証明に関しては、大きな課題がありました。
それは 「学習データの不足」 です。

数学の定理や証明は専門家が作成するものであり、大規模なデータセットを構築するのが困難です。そのため、従来の手法では証明可能な定理の数が限られ、数学的推論能力の向上に大きな制約がありました。

この問題を解決するために、スタンフォード大学の研究チームが新しい手法を開発しました。
それが 「Self-Play Theorem Prover（STP）」 です。

本記事では、この革新的な手法が どのようにしてLLMの定理証明能力を2倍に向上させたのか を詳細に解説していきます。

https://arxiv.org/abs/2502.00212

目次

🔹 従来の定理証明AIの課題

これまでのLLMによる定理証明では、以下の手法が主流でした。

① 強化学習（Reinforcement Learning）

  • 定理を証明するたびにLLMに報酬を与える手法。
  • しかし、新しい定理に対する証明を生成するには 膨大なデータ が必要で、学習が指数関数的に難しくなる。

② 専門家反復（Expert Iteration）

  • LLMが証明を生成し、正しい証明が得られた場合にそれを再学習する手法。
  • しかし、「高校レベルの問題を学習したモデルが大学レベルの問題を解く」ことは難しく、知識の飛躍が生じない。

このように、従来の手法では証明可能な定理の数が限られていました。

🔹 新手法「STP（Self-Play Theorem Prover）」とは？

研究者たちは、人間の数学者が 「定理を証明するだけでなく、新しい予想を生み出す」 ことで学習を進める点に着目しました。

この考え方をLLMに応用したのが、 「Self-Play Theorem Prover（STP）」 です。
この手法では、「予想の生成」と「証明の試行」を繰り返し、LLMが独自に成長していく仕組みを採用しています。

🔹 STPの3つのステップ

  1. モデルの初期化と教師あり学習
    • 既存の数学データセットを用いて、予想を生み出すモデルと証明を行うモデルを作成。
  2. 自己対戦（Self-Play）による訓練
    • 生成した予想に対し、証明を試みることでLLMの学習を進める。
  3. 最終的な再訓練
    • 自己対戦の過程で得られた予想と証明を用い、さらにモデルを強化。

このプロセスを繰り返すことで、従来よりも 効率的に証明スキルを向上 させることができます。

🔹 STPの詳細な学習プロセス

STPでは、以下のような流れで自己対戦が行われます。

① 新しい予想を生み出す

  • 証明が得られた定理から、重要な補題を抽出。
  • その補題をもとに、予想生成モデルが新しい予想を作成。

② 予想の証明に挑戦

  • 生成された予想に対し、32回ずつ証明を試行。
  • 既存の未証明定理とも比較し、どちらが証明しやすいかを検証。

③ 証明の正しさを検証

  • 生成された証明は、Lean や Isabelle などの形式的検証システムで自動チェック。
  • 証明の中で使われた補題の情報を記録し、次の予想生成に活用。

④ 学習データの選別

  • 予想の 難易度 を評価し、適切なものを選択。
  • 不自然な予想や、あまりにも簡単すぎる予想を除外。
  • 証明の美しさ（証明の長さや論理の自然さ）を考慮。

このプロセスを繰り返すことで、LLMは 新しい数学的概念を学習しながら成長 していきます。

🔹 実験結果と成果

研究チームは、以下のデータセットを用いてSTPの有効性を検証しました。

使用したデータセット

  • LeanWorkbook（形式的数学データセット）
  • miniF2F-test（高校レベルの数学問題）
  • ProofNet-test（大学レベルの数学問題）

結果📊

✅ LeanWorkbookでの成功率が2倍向上（26.3% → 57.2%）
✅ miniF2F-testでのPass@128（1回の証明生成で成功率）57.2%達成
✅ ProofNet-testで23.1%（Pass@3200）という最高記録を達成

さらに、数学コンテスト「PutnamBench」でも、従来の最高記録（6問）を上回る 9問の解答に成功 しました。

この結果は、「予想を生み出すプロセスを取り入れることで、数学的推論能力が大幅に向上する」ことを示しています。

🔹 STPがもたらす今後の可能性

今回の研究は、LLMによる定理証明の新たな可能性を示しました。

① 数学研究への貢献

  • 新しい定理の発見を加速し、数学の発展を促進。
  • これまで人間が手がけていた証明プロセスを自動化。

② AIによる科学技術の発展

  • 物理学、暗号理論、最適化問題など、数学を基盤とする分野での応用が期待される。

③ 教育分野での活用

  • 学生向けの数学教育にLLMを活用し、個別最適化された学習を実現。

🔹 まとめ 🎯

本記事では、LLMの定理証明能力を2倍に向上させる 「STP（Self-Play Theorem Prover）」 という手法を詳しく解説しました。

✅ STPは「予想生成」と「証明」を組み合わせる新しい学習手法
✅ 従来の方法に比べ、限られたデータでも効率的に学習可能
✅ 自己対戦により、新しい定理を学習しながら証明能力を向上
✅ ベンチマークテストで過去最高の成果を達成

数学の未来を大きく変える可能性を秘めたこの手法。
あなたは、AIによる定理証明がどのように発展していくと思いますか？ 🚀✨

最新情報をチェックしよう！

論文の最新記事4件