論文の概要: Lean Finder: Semantic Search for Mathlib That Understands User Intents

• arxiv url: http://arxiv.org/abs/2510.15940v1
• Date: Wed, 08 Oct 2025 19:51:49 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-26 16:57:26.456341
• Title: Lean Finder: Semantic Search for Mathlib That Understands User Intents
• Title（参考訳）: Lean Finder: ユーザインテントを理解するMathlibのセマンティック検索
• Authors: Jialin Lu, Kye Emond, Kaiyu Yang, Swarat Chaudhuri, Weiran Sun, Wuyang Chen,
• Abstract要約: Lean Finderは、LeanとMathlibのセマンティック検索エンジンである。 数学者の意図を理解し、一致させる。 LLMベースの定理証明器と互換性があり、形式的推論によるブリッジング検索が可能である。
• 参考スコア（独自算出の注目度）: 19.454158593716578
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We present Lean Finder, a semantic search engine for Lean and mathlib that understands and aligns with the intents of mathematicians. Progress in formal theorem proving is often hindered by the difficulty of locating relevant theorems and the steep learning curve of the Lean 4 language, making advancement slow and labor-intensive. Existing Lean search engines, though helpful, rely primarily on informalizations (natural language translation of the formal statements), while largely overlooking the mismatch with real-world user queries. In contrast, we propose a user-centered semantic search tailored to the needs of mathematicians. Our approach begins by analyzing and clustering the semantics of public Lean discussions, then fine-tuning text embeddings on synthesized queries that emulate user intents. We further align Lean Finder with mathematicians' preferences using diverse feedback signals, encoding it with a rich awareness of their goals from multiple perspectives. Evaluations on real-world queries, informalized statements, and proof states demonstrate that our Lean Finder achieves over $30\%$ relative improvement compared to previous search engines and GPT-4o. In addition, Lean Finder is compatible with LLM-based theorem provers, bridging retrieval with formal reasoning. Lean Finder is available at: https://leanfinder.github.io
• Abstract（参考訳）: Lean Finderは、数学者の意図を理解し、一致させる、LeanとMathlibのセマンティック検索エンジンです。 形式的定理証明の進歩は、しばしば、関連する定理の特定とリーン4言語の急激な学習曲線の難しさによって妨げられ、進歩が遅く、労働集約化される。 既存のリーン検索エンジンは役に立つが、主に非公式化(形式文の自然言語翻訳)に依存している。 対照的に,数学者のニーズに合わせてユーザ中心のセマンティックサーチを提案する。 当社のアプローチはまず、パブリックリーンの議論の意味を分析し、クラスタ化し、それからユーザの意図をエミュレートする合成クエリにテキストの埋め込みを微調整することから始まります。 さらに、さまざまなフィードバック信号を使って、Lean Finderと数学者の好みを一致させ、複数の視点から目標を十分に認識してエンコードします。 実世界のクエリ、非公式なステートメント、証明ステートの評価は、我々のLean Finderが以前の検索エンジンやGPT-4oと比較して30\%以上の相対的な改善を達成していることを示している。 さらに、Lean Finder は LLM ベースの定理証明器と互換性があり、形式的推論による検索をブリッジする。 Lean Finder は以下の https://leanfinder.github.io で利用可能だ。

関連論文リスト

• LeanExplore: A search engine for Lean 4 declarations [0.0]
  本稿では、Lean 4宣言のための検索エンジンであるLeanExploreを紹介します。 LeanExploreを使うと、ユーザーは特定のLean 4パッケージにまたがるステートメントを意味的に検索できる。
  論文  参考訳（メタデータ） (2025-06-04T16:09:54Z)
• 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)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• Evaluating Language Models for Mathematics through Interactions [116.67206980096513]
  大型言語モデル(LLM)と対話し,評価するためのプロトタイププラットフォームであるCheckMateを紹介した。 我々はCheckMateと共同で3つの言語モデル(InstructGPT, ChatGPT, GPT-4)を、学部レベルの数学の証明支援として評価する研究を行った。 我々は、人間の行動の分類を導き、概して肯定的な相関にもかかわらず、正しさと知覚的有用性の間に顕著な相違点があることを明らかにする。
  論文  参考訳（メタデータ） (2023-06-02T17:12:25Z)

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

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