論文の概要: Lean Finder V2: Semantic Search for Mathlib That Disambiguates User Queries

• arxiv url: http://arxiv.org/abs/2610.30843v1
• Date: Thu, 22 Oct 2026 07:19:43 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-24 02:08:44.267739
• Title: Lean Finder V2: Semantic Search for Mathlib That Disambiguates User Queries
• Title（参考訳）: Lean Finder V2: ユーザクエリを曖昧にするMathlibのセマンティック検索
• Abstract要約: Lean Finder V2はMathlibのセマンティック検索フレームワークである。 相手のトレーニングと入力レベルの書き換えによって、ユーザのクエリを曖昧にする。 Human-curated MathlibQRベンチマークでは、Lean Finder V2が新しい最先端技術を設定している。
• 参考スコア（独自算出の注目度）: 9.010960562321237
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We introduce Lean Finder V2, a semantic search framework for Mathlib that disambiguates user queries through complementary model-level adversarial training and input-level query rewriting. Human mathematicians and coding agents rarely search Mathlib by providing detailed context. In practice, they query short properties, notation, aliases, or hypotheses, leaving much of the intended mathematics implicit. In contrast, existing Mathlib search engines unrealistically assume context-rich queries. The scarcity of real-world short queries paired with ground-truth Mathlib statements makes this ambiguity even more intractable. We argue that this is essentially a data problem. Through adversarial training, we scale up the generation of labeled short and ambiguous queries, and learn to disambiguate user queries at both model-level fine-tuning and input-level query rewriting. On the human-curated MathlibQR benchmark, our Lean Finder V2 sets a new state of the art, with at least 11% relative improvement over the previous best Mathlib semantic search engines. On top of our state-of-the-art retriever, optimized query rewriting further improves MathlibQR retrieval. On unlabeled queries from human and coding-agent interactions, Lean Finder V2 is ranked as the strongest system. Integrated with Claude Code, Lean Finder V2 improves proof success on downstream theorem-proving task. Lean Finder V2 is available at: https://leanfinder.github.io/
• Abstract（参考訳）: 我々は、モデルレベルの相補的なトレーニングと入力レベルのクエリ書き換えを通じて、ユーザクエリを曖昧にするMathlibのセマンティック検索フレームワークであるLean Finder V2を紹介する。 人間の数学者やコーディングエージェントは、詳細な文脈を提供することでMathlibを検索することは滅多にない。 実際には、短い性質、表記法、エイリアス、仮説を検索し、意図された数学の多くを暗黙的に残している。 対照的に、既存のMathlib検索エンジンは文脈に富んだクエリを非現実的に想定している。 実世界の短いクエリと地味なMathlib文のペアが不足していることは、この曖昧さをさらに難解なものにしている。 これは本質的にデータの問題である、と私たちは主張する。 逆行訓練により、ラベル付き短いクエリとあいまいなクエリの生成をスケールアップし、モデルレベルの微調整と入力レベルのクエリ書き換えの両方で、ユーザクエリの曖昧さを学習する。 Human-curated MathlibQRベンチマークでは、Lean Finder V2が新しい最先端技術を設定し、前回のMathlibセマンティック検索エンジンと比較して少なくとも11%改善しました。 最先端の検索機能に加えて、最適化されたクエリ書き換えにより、MathlibQR検索がさらに改善される。 人間とコーディングエージェントのインタラクションからのラベルなしクエリでは、Lean Finder V2が最強のシステムとしてランク付けされている。 Claude Codeと統合されたLean Finder V2は、下流の定理証明タスクにおける証明の成功を改善する。 Lean Finder V2 は以下の https://leanfinder.github.io/ で利用可能だ。

関連論文リスト

• Lean Graph Search for Formal Theorem Proving [82.31440013289564]
  グラフに基づくLean4の検索手法であるLeanGraphSearchを提案する。 Mathlibのフォワード依存関係からグラフを構築し、それをトラバースして、サポート対象の補題を明らかにする。 3つの定理証明ベンチマークで、LeanGraphSearchは8, 16, 32リフレクションのパスレートをバニラ証明よりも40%向上させる。
  論文  参考訳（メタデータ） (2026-10-15T17:55:21Z)
• SABER-Math: Automated Benchmark for Information Retrieval Evaluation in Mathematics [4.685475117723465]
  専門家のアノテーションを使わずに数理IRを評価するための,最初の完全自動ベンチマークであるSABER-Mathを紹介する。 SABER-Mathは283Kのハイスクールレベルの数学問題から始まり、3つのステップでタスクのランク付けに挑戦する。 我々は、語彙検索器、特殊数式検索システム、最近の埋め込みモデルを評価する。
  論文  参考訳（メタデータ） (2026-06-29T07:32:50Z)
• AlignCoder: Aligning Retrieval with Target Intent for Repository-Level Code Completion [55.21541958868449]
  リポジトリレベルのコード補完フレームワークであるAlignCoderを提案する。 我々のフレームワークは、初期クエリとターゲットコードのセマンティックギャップを橋渡しする拡張クエリを生成する。 我々は、拡張クエリにおける推論情報を活用してより正確な検索を行うAlignRetrieverのトレーニングに強化学習を採用する。
  論文  参考訳（メタデータ） (2026-01-27T15:23:14Z)
• Lean Finder: Semantic Search for Mathlib That Understands User Intents [19.454158593716578]
  Lean Finderは、LeanとMathlibのセマンティック検索エンジンである。 数学者の意図を理解し、一致させる。 LLMベースの定理証明器と互換性があり、形式的推論によるブリッジング検索が可能である。
  論文  参考訳（メタデータ） (2025-10-08T19:51:49Z)
• Reasoning-enhanced Query Understanding through Decomposition and Interpretation [87.56450566014625]
  ReDIは、分解と解釈によるクエリ理解のための推論強化アプローチである。 我々は,大規模検索エンジンから実世界の複雑なクエリの大規模データセットをコンパイルした。 BRIGHT と BEIR の実験により、ReDI はスパースと密度の高い検索パラダイムの両方において、強いベースラインを一貫して超えることを示した。
  論文  参考訳（メタデータ） (2025-09-08T10:58:42Z)
• FLARE: Faithful Logic-Aided Reasoning and Exploration [47.46564769245296]
  タスク分解を用いて問題空間をトラバースする新しい手法を提案する。 我々はLarge Language Modelsを使ってソリューションを計画し、クエリを事実に軟式化し、論理プログラミングコードを使って述語する。 提案手法は,生成したコードに対する推論プロセスの忠実度を計算し,外部の解法に頼らずにマルチホップ探索のステップを解析する。
  論文  参考訳（メタデータ） (2024-10-14T19:39:11Z)
• A Semantic Search Engine for Mathlib4 [3.4826238218770813]
  本稿では,非公式な問合せを受け付け,関連する定理を求めるMathlib4のセマンティック検索エンジンを提案する。 また,各種検索エンジンの性能評価のためのベンチマークを構築した。
  論文  参考訳（メタデータ） (2024-03-20T05:23:09Z)
• UniKGQA: Unified Retrieval and Reasoning for Solving Multi-hop Question Answering Over Knowledge Graph [89.98762327725112]
  KGQA(Multi-hop Question Answering over Knowledge Graph)は、自然言語の質問で言及されているトピックエンティティから、複数のホップを持つ回答エンティティを見つけることを目的としている。 我々は、モデルアーキテクチャとパラメータ学習の両方において、検索と推論を統合することで、マルチホップKGQAタスクの新しいアプローチであるUniKGQAを提案する。
  論文  参考訳（メタデータ） (2022-12-02T04:08:09Z)

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

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