論文の概要: Lean Graph Search for Formal Theorem Proving

• arxiv url: http://arxiv.org/abs/2610.22339v1
• Date: Thu, 15 Oct 2026 17:55:21 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-17 06:09:33.271449
• Title: Lean Graph Search for Formal Theorem Proving
• Title（参考訳）: 形式的定理証明のためのリーングラフ検索
• Abstract要約: グラフに基づくLean4の検索手法であるLeanGraphSearchを提案する。 Mathlibのフォワード依存関係からグラフを構築し、それをトラバースして、サポート対象の補題を明らかにする。 3つの定理証明ベンチマークで、LeanGraphSearchは8, 16, 32リフレクションのパスレートをバニラ証明よりも40%向上させる。
• 参考スコア（独自算出の注目度）: 82.31440013289564
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Retrieving relevant lemmas is crucial for formal theorem proving, enabling provers to build machine-checkable proofs from established mathematical results. Recent retrieval systems match library declarations to a target theorem or its intermediate proof steps, but make limited use of multi-hop dependencies among declarations. These dependencies can reveal supporting lemmas that are not necessarily lexically similar to the target theorem but recur in proofs of related problems. To this end, we propose LeanGraphSearch, a graph-based retrieval method for Lean 4 that constructs a graph from Mathlib's forward dependencies and traverses it to uncover supporting lemmas through multi-hop dependency chains. Specifically, LeanGraphSearch links each declaration to the premises it depends on, uses a graph-based ranking algorithm to propagate relevance from semantically matched declarations to their dependencies, and reranks the expanded candidates against the original query. Across two mathematical retrieval benchmarks, LeanGraphSearch improves recall by up to 12% over the strongest baseline, LeanSearch v2, on MathlibQR and increases coverage of complete annotated proof routes on MathlibMPR, covering up to 3.7% of extra groups. More importantly, we evaluate whether these retrieval gains translate into improved end-to-end theorem proving by integrating LeanGraphSearch into an iterative proving loop guided by Lean feedback. Across three theorem proving benchmarks, LeanGraphSearch improves pass rate at {8, 16, 32} reflection turns by as much as 40% compared to vanilla prover and at most 10% compared to LeanSearch v2, showing higher accuracy-cost efficiency. These findings highlight the value of dependency graph search for theorem proving and motivate further research on structure-aware search for proof discovery.
• Abstract（参考訳）: 関連する補題を取得することは形式的な定理証明に不可欠であり、証明者は確立された数学的結果から機械チェック可能な証明を構築できる。 最近の検索システムは、ライブラリ宣言を目的の定理やその中間的な証明ステップと一致させるが、宣言間のマルチホップ依存を限定的に利用する。 これらの依存関係は、必ずしもターゲット定理とレキシックに似ていないが、関連する問題の証明で再帰する補題を明らかにすることができる。 この目的のために、我々はLean 4のグラフベースの検索手法であるLeanGraphSearchを提案する。 具体的には、LeanGraphSearchは、各宣言を依存する前提にリンクし、グラフベースのランキングアルゴリズムを使用して、セマンティックにマッチした宣言から依存関係への関連性を伝達し、拡張された候補を元のクエリに対して再ランクする。 2つの数学的評価ベンチマークで、LeanGraphSearchは、MathlibQR上で最強のベースラインであるLeanSearch v2よりも最大12%リコールを改善し、MathlibMPR上での完全なアノテートされた証明ルートの範囲を拡大し、最大3.7%の追加グループをカバーする。 さらに重要なことは、これらの検索が、LeanGraphSearchをリーンフィードバックによって導かれる反復的証明ループに統合することで、エンドツーエンドの定理の証明に変換されるかどうかを評価することである。 3つの定理証明ベンチマークを通じて、LeanGraphSearchは、バニラ証明よりも40%、LeanSearch v2に比べて10%もパスレートが向上し、精度とコスト効率が向上した。 これらの知見は、定理証明のための依存グラフ探索の価値を強調し、証明発見のための構造認識探索のさらなる研究を動機付けている。

関連論文リスト

• SearchAtlas: Analyzing Agentic Search Strategies via Evidential Query Graphs [30.494397052362384]
  本稿では,検索トラジェクトリを構造化グラフに変換するフレームワークであるSearchAtlasを紹介する。 我々の自動解析パイプラインは、人間の注釈付きグラフに対して86.4%の平均エッジF1を達成する。 我々は3つのベンチマークで5つの検索エージェントを分析し、検索尺度とエビデンスアグリゲーションの体系的な違いを明らかにした。
  論文  参考訳（メタデータ） (2026-09-09T23:09:26Z)
• VeriGraph: Towards Verifiable Data-Analytic Agents [71.17693022916896]
  LLMをベースとしたエージェントは、データ集約分析タスクにおいて強力な能力を示してきたが、その出力は滅多に検証されていない。 We propose VeriGraph, a traceable neuro-symbolic reasoning framework that agent can construct an explicit heterogeneous evidence directed acyclic graph。 以上の結果から,明示的なエビデンスグラフ構築がデータ分析エージェントの検証に期待できる道のりであることが示唆された。
  論文  参考訳（メタデータ） (2026-06-15T11:50:56Z)
• LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving [7.326381497366569]
  リーン4の定理を証明するには、しばしば、簡潔な証明を可能にするライブラリの補題の散在を識別する必要がある。 本稿では,このタスクのための2モード検索システムであるLeanSearch v2を紹介する。
  論文  参考訳（メタデータ） (2026-05-13T08:04:57Z)
• Query-Aware Flow Diffusion for Graph-Based RAG with Retrieval Guarantees [10.806910118253976]
  グラフベースのRetrieval-Augmented Generation (RAG)システムは複雑な関係を捉えるために相互接続された知識構造を利用する。 本稿では,各クエリの全体的意味論にグラフトラバーサルを動的に適用する学習自由フレームワークであるQuery-Aware Flow Diffusion RAG (QAFD-RAG)を提案する。 QAFD-RAGは、弱い信号対雑音条件下で、高い確率で関連部分グラフを復元する。
  論文  参考訳（メタデータ） (2026-04-21T08:53:34Z)
• TeaRAG: A Token-Efficient Agentic Retrieval-Augmented Generation Framework [62.66056331998838]
  TeaRAGは、検索内容と推論ステップの両方を圧縮できるトークン効率のエージェントRAGフレームワークである。 報奨関数は,過剰な推論ステップをペナルティ化しながら,知識マッチング機構によって知識満足度を評価する。
  論文  参考訳（メタデータ） (2025-11-07T16:08:34Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。