SorryDB: Can AI Provers Complete Real-World Lean Theorems?

本論文は、GitHub の 78 の実世界プロジェクトから動的に更新される Lean 定理ベンチマーク「SorryDB」を提案し、現在の AI 証明手法が互いに補完的であることを示すとともに、実用的な数学形式化への貢献能力を評価する新たな指標を提供しています。

要約

この論文は、**「SorryDB（ソリー・データベース）」**という新しい仕組みと、それを使って AI が実際に数学の証明ができるかどうかを試した実験について書かれています。

難しい専門用語を抜きにして、日常の例え話を使って解説しますね。

1. 問題：「試験問題」だけでは実力が測れない

これまで、AI が数学の証明ができるかどうかを調べるには、**「オリンピックの数学問題」**のような、完成された難問を解かせるテスト（ベンチマーク）が使われていました。

• 例え話：
  これは、料理人の腕前を測るために「完璧なレシピが用意された高級料理」だけを作らせているようなものです。
  しかし、実際の料理人（数学者）は、レシピがない状態で、冷蔵庫にある食材（既存の定理）を組み合わせて、新しい料理（証明）を作ったり、途中で失敗して作り直したりします。
  「オリンピック問題」はすでに AI が答えを暗記してしまっている可能性が高く、**「実際の現場で使えるか？」**という本当の力を測るには不十分でした。

2. 解決策：「未完成の料理」を解かせる「SorryDB」

そこで、この論文のチームは**「SorryDB」**という新しいテストを作りました。

• 仕組み：
  世界中の数学者が GitHub（コード共有サイト）で一緒に作っている「未完成の数学プロジェクト」から、**「ここが証明できていないよ」というメモ（sorry というキーワード）**を自動的に集めます。
• 例え話：
  これは、**「未完成の料理のレシピ帳」**を集めて、AI に「この空白の部分を埋めて、美味しい料理（証明）を完成させてください」と頼むようなものです。
  • 誰かが「この材料（定理）を使えばいいはずだ」と書いておいて、実際に調理（証明）するのを誰かがやろうとしている状態です。
  • このテストは常に更新されるので、AI が答えを暗記してしまっても、すぐに新しい「未完成の料理」が出てきて、暗記では通用しなくなります。

3. 実験結果：AI はどうだった？

チームは、最新の AI（Google の Gemini や Anthropic の Claude など）や、数学専門の AI に、この「未完成の料理」を完成させるよう挑戦させました。

• 結果の要点：
  1. AI はまだ完璧ではない：
     一番強い AI でも、すべての問題を解くことはできませんでした。解ける問題と解けない問題がバラバラでした。
  2. チームワークが重要（補完性）：
     特定の AI だけが万能ではなく、**「A さんはこの料理が得意、B さんはあの料理が得意」**というように、AI 同士が得意分野を持っています。複数の AI を組み合わせれば、もっと多くの問題を解決できることがわかりました。
  3. 「失敗から学ぶ」のが最強：
     一度で正解を出そうとするより、**「試して、失敗したらエラーメッセージを見て、修正して、また試す」**という「試行錯誤（エージェント型）」のやり方が、圧倒的に成功しました。
     • 例え話：
       料理人が「まず味見して、塩味が足りなければ足す」という作業を繰り返すことで、完璧な味に近づけるのと同じです。

4. なぜこれが重要なのか？

この研究は、AI が「テストの点数を取るため」ではなく、**「数学者の実際の仕事（複雑なプロジェクトの完成）を助けること」**に焦点を当てています。

• 未来への展望：
  この「SorryDB」は生き物のように成長し続けます。AI が進化するにつれて、残る「未完成の料理（証明）」はどんどん難しくなります。これにより、AI は常に最新のレベルで数学者と協力し、新しい数学の発見を助けることができるようになるでしょう。

まとめ

この論文は、**「AI に『完璧な試験問題』ではなく、『実際の現場で起こる未完成の仕事』を任せて、その実力を測ろう」という新しいアプローチを提案し、その結果、「AI はまだ一人では完璧ではないが、失敗を繰り返して修正する『試行錯誤』の能力があれば、数学者の強力なパートナーになれる」**ことを示しました。

まるで、**「料理の修行生に、完成された高級料理の真似ではなく、冷蔵庫の食材で新しい料理を考案させる練習」**をさせたようなものですね。

技術概要

論文「SORRYDB: CAN AI PROVERS COMPLETE REAL-WORLD LEAN THEOREMS?」の技術的サマリー

本論文は、形式数学の分野、特に Lean 定理証明器における AI の実用性を評価するための新しい動的ベンチマーク「SorryDB」を提案し、その評価結果を報告するものです。既存の静的ベンチマーク（オリンピック数学問題など）の限界を克服し、実際のオープンソースプロジェクトにおける「未解決の証明義務（sorry）」に焦点を当てることで、AI 定理証明の実社会での有用性を測定することを目指しています。

以下に、問題定義、手法、主要な貢献、結果、および意義について詳細にまとめます。

---

1. 問題定義 (Problem)

現在の AI 定理証明の評価には、以下の重大な課題が存在します。

• 静的ベンチマークの飽和と汚染: 既存のベンチマーク（miniF2F, PutnamBench など）は、数学オリンピックや大学の試験問題に限定されており、すでに多くのモデルが学習済みデータとして記憶している可能性があります（データ汚染）。これにより、モデルの真の推論能力や一般化能力を正確に評価することが困難になっています。
• 実世界との乖離: 競技数学は、実際の形式化プロジェクトで直面する複雑な依存関係、文脈の広さ、および「不完全なコード（未完成の証明）」への対応とは性質が異なります。実際のプロジェクトでは、定理の全体を証明するのではなく、部分的な証明（sorry プレースホルダー）を埋める作業が頻繁に行われます。
• 評価指標の欠如: 実際のソフトウェア開発（SWE-bench など）のように、実用的な課題に対する AI の貢献度を測定する動的なベンチマークが、定理証明の分野には存在していませんでした。

2. 手法とアーキテクチャ (Methodology)

著者らは、GitHub 上のアクティブな Lean 形式化プロジェクトから「sorry」キーワードを抽出し、動的に更新されるデータセット「SorryDB」を構築しました。

データセット構築 (SorryDB)

• ソース: Lean パッケージレジストリ「Reservoir」に登録された 78 のアクティブな GitHub リポジトリ（教育用、ツール、ライブラリ、形式化プロジェクトなど多岐にわたる）を対象とします。
• 抽出プロセス:
  1. リポジトリから sorry キーワードを含むすべての証明義務を抽出。
  2. メタデータ（リポジトリ URL、ファイルパス、コミットハッシュ、Lean バージョンなど）を保存。
  3. フィルタリング: 再現性の確保のため、プロジェクトがビルド可能であることを確認。また、証明が必要（Prop 型）な sorry のみを対象とし、重複を除去して最新のものを保持。
• タスク定義: 「Fill-in-the-sorry」。与えられた sorry キーワードを、その文脈で正しい証明コードに置き換えるタスクです。定理全体を証明する必要はなく、局所的な証明義務の完了が求められます。

評価フレームワーク

• 検証パイプライン: 提案されたコードを sorry に置き換え、Lean 環境でコンパイルを実行。
  • 単なる構文チェックではなく、LeanInteract を使用して、その場所での証明状態が正常に完了し、最終的に sorry が残っていないことを厳密に検証します。
  • 各リポジトリのビルド環境を事前に準備し、効率的な評価を実現。
• 評価対象モデル:
  • 決定論的タクティク: trivial, ring, linarith, grind など。
  • 汎用 LLM: GPT-5.2, Claude Opus 4.5, Gemini Flash/Pro 3, Qwen 3 など。
  • 専門特化モデル: Kimina Prover, Goedel Prover V2 など。
  • 反復・エージェントアプローチ: 自己修正（Self-Correcting）や、ツール検索（LeanSearch）を組み合わせたエージェント（Proposer + Reviewer）構造。

3. 主要な貢献 (Key Contributions)

1. SorryDB データセットの提案:
   • 実世界の形式化プロジェクトから「未解決の証明」を抽出し、動的に更新されるベンチマークを構築。これにより、データ汚染のリスクを低減し、コミュニティの実際のニーズに合致した評価が可能になりました。
2. 自動化された検証フレームワーク:
   • 提案された証明が正しいかどうかを、人工的なラベルなしで、コンパイルと証明状態の検証を通じて自動的に判定するパイプラインを提供。
3. 大規模な評価と分析:
   • 2026 年 1 月時点の 1000 タスクのスナップショットを用いて、多様なアプローチを評価。
   • 現在のモデルが「相補的」であることを示し（それぞれ異なるサブセットの課題を解決）、反復的なフィードバック（自己修正やエージェント手法）が単発（One-shot）アプローチよりも優れていることを実証しました。

4. 実験結果 (Results)

SorryDB-2601（1000 タスク）を用いた評価結果は以下の通りです（Table 1, Figure 2, Figure 3 参照）。

• パフォーマンスの比較:
  • 最上位モデル: 自己修正（Self-Correcting）またはエージェントアプローチを採用した Gemini Flash 3 が最も高い成功率（Pass@1 で約 27-30%）を示しました。
  • 汎用 LLM vs 専門モデル: 汎用 LLM（Gemini, Claude, GPT）は、競技数学に特化して学習された専門モデル（Goedel Prover, Kimina）よりも、実世界のタスクにおいて高いパフォーマンスを発揮しました。専門モデルはベンチマークデータには強いものの、実プロジェクトの文脈では性能が低下する傾向がありました。
  • 決定論的タクティク: grind や exact? などのタクティクは、特に教育的リポジトリや単純な課題において一定の成果を上げ、LLM だけでは解けない課題を解決するケースもありました。
• 相補性 (Complementarity):
  • 異なるモデルが解決する課題の集合は重なり合っておらず、「Combined」（すべてのモデルの成果を統合）すると、単一の最良モデルよりもはるかに多くの課題（35.7%）を解決できました。これは、各アプローチが異なる強みを持っていることを示しています。
• 反復アプローチの優位性:
  • 単発（One-shot）の推論よりも、エラーメッセージをフィードバックとして利用する反復的な自己修正やエージェント手法が圧倒的に優れていました（Figure 3a）。これは、プロジェクト環境でのコンパイルとエラーフィードバックへのアクセスが、単なる推論予算の増加よりも重要であることを示唆しています。
• カテゴリ別分析:
  • 教育用リポジトリの課題は比較的容易でしたが、大規模な形式化プロジェクト（例：Carleson の定理、FLT）の課題は非常に困難でした。
  • 専門モデルはベンチマーク課題には強かったものの、他のカテゴリでは性能が低く、バージョン不一致や RL 学習データの偏りが影響している可能性があります。

5. 意義と結論 (Significance)

• 実用性の評価基準の確立: SorryDB は、AI 定理証明器が「数学オリンピックの金メダル」を取る能力だけでなく、「実際の数学者の作業を支援し、未完成の証明を埋める能力」を評価する基準を提供します。
• 動的ベンチマークの必要性: 静的なデータセットはすぐに飽和し、評価指標として機能しなくなります。SorryDB のような「常に更新され、未解決の課題が増え続ける」動的ベンチマークは、AI の進歩に追従し、飽和を防ぐための重要なインフラです。
• アプローチの多様性の重要性: 単一の「最強のモデル」が存在するのではなく、決定論的タクティク、汎用 LLM、専門モデル、そしてそれらを統合するエージェントシステムを組み合わせることで、実用的な定理証明の自動化が進展することが示されました。
• 将来展望: 著者らは、SorryDB を月次で更新し、リーダーボードを設けることで、コミュニティ全体で AI 定理証明の実用性を追跡し、より高度で使いやすい証明支援ツールの開発を促進することを目指しています。

総じて、本論文は AI 定理証明の次の段階である「実世界での適用」に向けた重要な第一歩であり、評価手法とベンチマークの革新を通じて、この分野の発展を加速させる可能性を秘めています。