論文の概要: LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving

• arxiv url: http://arxiv.org/abs/2605.13137v2
• Date: Thu, 14 May 2026 05:15:13 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-15 15:19:49.917394
• Title: LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
• Title（参考訳）: LeanSearch v2: リーン4の定理を証明するグローバルな前提
• Authors: Guoxiong Gao, Zeming Sun, Jiedong Jiang, Yutong Wang, Jingda Xu, Peihao Wu, Bryan Dai, Bin Dong,
• Abstract要約: リーン4の定理を証明するには、しばしば、簡潔な証明を可能にするライブラリの補題の散在を識別する必要がある。 本稿では,このタスクのための2モード検索システムであるLeanSearch v2を紹介する。
• 参考スコア（独自算出の注目度）: 7.326381497366569
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Proving theorems in Lean 4 often requires identifying a scattered set of library lemmas whose joint use enables a concise proof -- a task we call global premise retrieval. Existing tools address adjacent problems: semantic search engines find individual declarations matching a query, while premise-selection systems predict useful lemmas one tactic step at a time. Neither recovers the full premise set an entire theorem requires. We present LeanSearch v2, a two-mode retrieval system for this task. Its standard mode applies a hierarchy-informalized Mathlib corpus with an embedding-reranker pipeline, achieving state-of-the-art single-query retrieval without domain-specific fine-tuning (nDCG@10 of 0.62 vs. 0.53 for the next-best system). Its reasoning mode builds on standard mode as its retrieval substrate, targeting global premise retrieval through iterative sketch-retrieve-reflect cycles. On a 69-query benchmark of research-level Mathlib theorems, reasoning mode recovers 46.1% of ground-truth premise groups within 10 retrieved candidates, outperforming strong reasoning retrieval systems (38.0%) and premise-selection baselines (9.3%) on the same benchmark. In a controlled downstream evaluation with a fixed prover loop, replacing alternative retrievers with LeanSearch v2 yields the highest proof success (20% vs. 16% for the next-best system and 4% without retrieval), confirming that retrieval quality propagates to proof generation. We have open-sourced all code, data, and benchmarks. Code and data: https://github.com/frenzymath/LeanSearch-v2 . The standard mode is publicly available with API access at https://leansearch.net/ .
• Abstract（参考訳）: リーン4で定理を証明するには、しばしば、グローバル前提検索と呼ばれる簡潔な証明を可能にするライブラリの補題の分散セットを特定する必要がある。 セマンティック検索エンジンはクエリにマッチする個々の宣言を見つけ、前提選択システムは一度に1つの戦術的なステップを予測する。 いずれの定理もすべての前提集合を回復しない。 本稿では,このタスクのための2モード検索システムであるLeanSearch v2を紹介する。 標準モードでは、階層的非形式化されたMathlibコーパスを埋め込み再帰パイプラインで適用し、ドメイン固有の微調整なしで最先端の単一クエリ検索を実現する(nDCG@10: 0.62 vs. 0.53 for the next-best system)。 その推論モードは、検索基板として標準モードに基づいており、反復的なスケッチ-検索-反射サイクルによるグローバルな前提検索をターゲットとしている。 研究レベルのMathlib定理の69クエリのベンチマークでは、推論モードが10の候補のうち46.1%の基幹前提群を回復し、強い推論検索システム(38.0%)と前提選択ベースライン(9.3%)を同じベンチマークで上回っている。 固定された証明ループによる下流評価では、代替の検索器をLeanSearch v2に置き換えると、最も高い証明成功(20%対16%、検索なし4%)が得られ、検索品質が証明生成に伝播することを確認した。 すべてのコード、データ、ベンチマークをオープンソースにしています。 コードとデータ:https://github.com/frenzymath/LeanSearch-v2 標準モードはhttps://leansearch.net/で公開されています。

関連論文リスト

• Reproducing Complex Set-Compositional Information Retrieval [11.891887979573925]
  複雑な情報には、接続性、解離性、排他性を使った集合合成クエリが含まれる。 我々は,QUESTとQUEST+変数について,主要な検索ファミリと推論対象手法のベンチマークを行った。
  論文  参考訳（メタデータ） (2026-05-05T14:51:40Z)
• Agentic Forecasting using Sequential Bayesian Updating of Linguistic Beliefs [1.7470133607730627]
  BLF (Bayesian Linguistic Forecaster) は二進予測のためのエージェントシステムである。 ForecastBenchのリーダーボードからの400のバックテスト質問に対して、BLFはすべての主要な公開メソッドを上回ります。
  論文  参考訳（メタデータ） (2026-04-20T17:57:51Z)
• From BM25 to Corrective RAG: Benchmarking Retrieval Strategies for Text-and-Table Documents [0.0]
  スパース, 密度, ハイブリッド融合, クロスエンコーダリグレード, クエリ拡張, インデックス拡張, 適応検索にまたがる10の検索戦略をベンチマークした。 我々はRecall@k,MRR,nDCGによる検索品質とNumber Matchによるエンドツーエンド生成品質を評価する。
  論文  参考訳（メタデータ） (2026-04-02T07:53:40Z)
• PeopleSearchBench: A Multi-Dimensional Benchmark for Evaluating AI-Powered People Search Platforms [14.675528528017653]
  PeopleSearchBenchはオープンソースのベンチマークで、119の現実世界のクェリで4人の検索プラットフォームを比較します。 Criteria-Grounded Verificationは,クエリ毎に明確で検証可能な基準を抽出する,事実関連パイプラインだ。 専門のAIピープルサーチエージェントであるLessieは、第2級システムよりも65.2, 18.5%高いスコアで、総合的に最高の成績を収めている。
  論文  参考訳（メタデータ） (2026-03-29T02:21:09Z)
• LLM-guided Hierarchical Retrieval [54.73080745446999]
  LATTICEは階層的な検索フレームワークであり、LLMは対数探索の複雑さで大きなコーパスを推論し、ナビゲートすることができる。 LLM誘導探索における中心的な課題は、モデルの関連性判断がノイズが多く、文脈に依存し、階層性に気付かないことである。 我々のフレームワークは、推論集約型BRIGHTベンチマークで最先端のゼロショット性能を実現する。
  論文  参考訳（メタデータ） (2025-10-15T07:05:17Z)
• Eigen-1: Adaptive Multi-Agent Refinement with Monitor-Based RAG for Scientific Reasoning [53.45095336430027]
  暗黙的な検索と構造化された協調を組み合わせた統合フレームワークを開発する。 Humanity's Last Exam (HLE) Bio/Chem Goldでは,48.3%の精度を実現している。 SuperGPQAとTRQAの結果はドメイン間の堅牢性を確認した。
  論文  参考訳（メタデータ） (2025-09-25T14:05:55Z)
• BRIGHT: A Realistic and Challenging Benchmark for Reasoning-Intensive Retrieval [54.54576644403115]
  BRIGHTは、関係する文書を検索するために、集中的推論を必要とする最初のテキスト検索ベンチマークである。 私たちのデータセットは、経済学、心理学、数学、コーディングなど、さまざまな領域にまたがる1,384の現実世界のクエリで構成されています。 クエリに関する明示的な推論を取り入れることで、検索性能が最大12.2ポイント向上することを示す。
  論文  参考訳（メタデータ） (2024-07-16T17:58:27Z)
• ExcluIR: Exclusionary Neural Information Retrieval [74.08276741093317]
  本稿では,排他的検索のためのリソースセットであるExcluIRを提案する。 評価ベンチマークには3,452の高品質な排他的クエリが含まれている。 トレーニングセットには70,293の排他的クエリが含まれており、それぞれに正のドキュメントと負のドキュメントがペアリングされている。
  論文  参考訳（メタデータ） (2024-04-26T09:43:40Z)
• An In-Context Learning Agent for Formal Theorem-Proving [10.657173216834668]
  我々は、LeanやCoqのような環境で、形式的定理コンテキストのためのコンテキスト内学習エージェントを提示します。 COPRAは大規模言語モデルに対して、ステートフルなバックトラック検索から戦術的応用を提案することを何度も求めている。 我々はCompCertプロジェクトのMiniF2FベンチマークとCoqタスクセットに対するCOPRAの実装を評価した。
  論文  参考訳（メタデータ） (2023-10-06T16:21:22Z)

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

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