arXiv cs.LGは2026年10月15日(現地時間)、形式的定理証明のためのグラフベースの検索手法「LeanGraphSearch」を提案する研究論文を公開した。この手法はLean 4向けにMathlibの依存関係からグラフを構築し、多段階の依存関係を通じて補題を発見する。複数のベンチマークにおいて、先行手法LeanSearch v2を上回る成果を示した。
LeanGraphSearchは、形式的定理証明において重要な関連補題の検索を目的としている。既存の検索システムが、宣言間の多段階の依存関係を限定的にしか活用していない点を踏まえ、LeanGraphSearchはMathlibの前方依存関係からグラフを構築し、多段階の依存連鎖を通じて補題を特定する。
具体的には、LeanGraphSearchは各宣言をその前提にリンクさせ、グラフベースのランキングアルゴリズムを用いてセマンティックに一致した宣言からその依存関係へ関連性を伝播させる。その後、拡張された候補を元のクエリに対して再ランク付けする。
二つの数学的検索ベンチマークにおいて、LeanGraphSearchはMathlibQR上で最も強力なベースラインであるLeanSearch v2に対し、再現率を最大12%向上させた。また、MathlibMPRでは、完全なアノテーション付き証明ルートのカバー率を最大3.7%向上させた。
さらに、研究チームは、これらの検索性能の向上がエンドツーエンドの定理証明に寄与するかを評価するため、LeanGraphSearchをLeanフィードバックに導かれる反復的な証明ループに統合した。三つの定理証明ベンチマークでは、LeanGraphSearchはバニラの証明器と比較して{8, 16, 32}回のリフレクションターンでの成功率を最大40%向上させ、LeanSearch v2と比較しても最大10%の向上を示し、高い精度とコスト効率を示した。これらの発見は、定理証明における依存関係グラフ検索の価値と、証明発見のための構造を考慮した検索に関するさらなる研究の必要性を示唆している。
参考: arXiv cs.LG — 2026年10月16日 02:55 (JST)
原文ハイライト"LeanGraphSearch, a graph-based retrieval method for Lean 4"