LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
LeanSearch v2 は、Lean 4 の定理証明に必要なライブラリ補題の完全な集合を特定する際に最先端のパフォーマンスを達成する 2 モード検索システムであり、既存のセマンティック検索および前提選択ツールを大幅に凌駕し、下流の証明成功率を直接的に向上させます。
原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。 免責事項の全文を読む
巨大で複雑なジグソーパズルを解こうとしていると想像してください。10 万個のピースが入った巨大な箱（Mathlib ライブラリ）があり、その目標は特定の絵（数学的証明）を完成させることです。
問題なのはピースがないことではなく、ピースが部屋中に散らばっており、手順書に「ここには青空のピースを使いなさい」と書かれていないことです。代わりに、「幾何級数」に関するピースと「円分多項式」に関するピース（一見全く無関係に聞こえる）が、実はあなたの特定の課題を解決するために組み合わさる必要があることを、あなた自身が見つけ出さなければなりません。
これがこの論文が取り組む課題です。論文は、Lean 4 というコンピュータ言語で作業する数学者のために、正しいパズルのピースを見つけるように設計された新しいツールLeanSearch v2を紹介しています。
以下に、論文が用いた単純な比喩を用いて、その内容を分解して示します。
1. 課題：「グローバルな前提の検索（Global Premise Retrieval）」
著者らは、既存のツールは 2 種類の異なる種類の助手のようですが、どちらも完璧ではないと述べています。
- セマンティック検索エンジン：これは、キーワードに一致する単一の書籍を見つける司書のようなものです。「素数」と尋ねれば、素数に関する書籍を見つけます。しかし、パズルを解くためにライブラリの 3 つの異なるセクションから3 つの特定の定理が必要であることは知りません。
- 前提選択器：これは、パズルの1 ステップずつを助けるチューターのようなものです。「さて、この特定の動きに対してはこのピースを使いなさい」と言います。しかし、彼らは全体像を見ていません。仕事を完了させるために、3 つの遠く離れた概念を結びつけるようなライブラリ内の経路を計画する必要があることを知りません。
論文はこの欠けている能力を**「グローバルな前提の検索」**と呼んでいます。これは、問題を見て、「これを解くためには、ライブラリからこれら 3 つの特定の、一見無関係な補題を引っ張り出して、それらを連鎖させる必要がある」と言える能力のことです。
2. 解決策：LeanSearch v2
著者らは、2 つの異なる性格を持つ賢い研究助手のように機能する 2 モードのシステムを構築して、この課題を解決しました。
モード A：「スタンダードモード」（スーパー司書）
これは基盤となる部分です。ライブラリ向けの高速検索エンジンとして機能します。
- 仕組み：10 万を超える数学的な宣言の全ライブラリを取り込み、それらを「コンピュータコード」から「人間に優しい説明」へと翻訳します。その後、2 段階のプロセスを使用します。
- 埋め込み（Embedding）：すべてのテキストを数学的な「指紋」に変換し、類似の概念を見つけます。
- 再ランク付け（Reranking）：上位 50 件の一致結果を取得し、より賢い 2 番目の AI を用いてそれらを再ソートし、絶対的に最良のものを選び出します。
- 結果：数学データに特化して訓練されていなくても、これまでにないどのツールよりも正確な単一の情報を見つけ出します。まるで、ライブラリを熟知している司書が、曖昧な説明を聞くだけで必要な正確な書籍を見つけられるようなものです。
モード B：「推論モード」（探偵）
これが大きな革新です。1 つのピースを探すだけでなく、証明に必要な全体セットのピースを見つけようとします。
- 仕組み：「スケッチ - 検索 - 反省（Sketch-Retrieve-Reflect）」ループを使用します。これは謎を解く探偵のようなものです。
- スケッチ：AI が証明の「物語」を推測します（例：「まず X を行い、次に Y を使い、その後 Z を行う」）。
- 検索：その物語の各ステップに対応する実際のピースを見つけるために、「スタンダードモード」の司書を使用します。
- 反省：「裁判官」AI が結果を確認します。ピースは適合しましたか？もし司書がステップ Y のピースを見つけられなかった場合、裁判官は「その物語は機能しない」と言います。
- 修正：AI は戻り、物語（スケッチ）を変更して、再度試みます。
- 結果：定理を解決するために実際に互いに機能する一貫したライブラリ補題のセットが見つかるまで、ループを繰り返します。
3. 証拠：機能しましたか？
著者らは、このシステムを 2 つの主要な課題でテストしました。
- 検索テスト：説明に基づいて特定の定理を見つけるようシステムに求めました。LeanSearch v2が勝利し、競合他社よりも高い頻度で正解を見つけました。
- 「グローバル」テスト：69 の困難な大学院レベルの数学問題を与え、それらを解決するために必要な補題のグループを見つけるよう求めました。
- 競合他社：古いツールは、正しいピースのグループを約 9% から 38% の頻度でしか見つけられませんでした。
- LeanSearch v2：正しいピースのグループを**46.1%**の頻度で見つけました。
- 「証明」テスト：このツールを証明を作成しようとするロボットに組み込みました。LeanSearch v2を使用した場合、ロボットは**20%の頻度で証明を成功裏に完了しました。ツールなしでは、成功した頻度はわずか4%**でした。
4. 結論
この論文は、LeanSearch v2が、単なる「検索」タスクではなく、「推論」タスクとして数学検索を初めて成功させたシステムであると主張しています。
- 比喩：従来のツールは、次の曲がるべき通りを教えることしかできない GPS のようなものでした。LeanSearch v2は、目的地に到達するために、存在を知らなかった地区を通る風景の良いルートを取る必要があることに気づき、そこに到達するための正確な曲がり角を知っている、旅行全体を計画できる GPS のようなものです。
著者らは、これは証明そのものを生成するためのものではなく、正しいツールを見つけるための検索ツールであることを強調しています。ただし、より良い検索は明らかに証明生成プロセスの成功をより頻繁に助けます。彼らは、コードとデータのすべてを公開しており、他の人々がこの「探偵」アプローチを数学の問題解決に活用できるようにしています。
自分の分野の論文に埋もれていませんか？
研究キーワードに一致する最新の論文のダイジェストを毎日受け取りましょう——技術要約付き、あなたの言語で。