論文の概要: LeanExplore: A search engine for Lean 4 declarations

• arxiv url: http://arxiv.org/abs/2506.11085v1
• Date: Wed, 04 Jun 2025 16:09:54 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-22 23:32:14.565185
• Title: LeanExplore: A search engine for Lean 4 declarations
• Title（参考訳）: LeanExplore: Lean 4宣言のための検索エンジン
• Authors: Justin Asher,
• Abstract要約: 本稿では、Lean 4宣言のための検索エンジンであるLeanExploreを紹介します。 LeanExploreを使うと、ユーザーは特定のLean 4パッケージにまたがるステートメントを意味的に検索できる。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The expanding Lean 4 ecosystem poses challenges for navigating its vast libraries. This paper introduces LeanExplore, a search engine for Lean 4 declarations. LeanExplore enables users to semantically search for statements, both formally and informally, across select Lean 4 packages (including Batteries, Init, Lean, Mathlib, PhysLean, and Std). This search capability is powered by a hybrid ranking strategy, integrating scores from a multi-source semantic embedding model (capturing conceptual meaning from formal Lean code, docstrings, AI-generated informal translations, and declaration titles), BM25+ for keyword-based lexical relevance, and a PageRank-based score reflecting declaration importance and interconnectedness. The search engine is accessible via a dedicated website (https://www.leanexplore.com/) and a Python API (https://github.com/justincasher/lean-explore). Furthermore, the database can be downloaded, allowing users to self-host the service. LeanExplore integrates easily with LLMs via the model context protocol (MCP), enabling users to chat with an AI assistant about Lean declarations or utilize the search engine for building theorem-proving agents. This work details LeanExplore's architecture, data processing, functionalities, and its potential to enhance Lean 4 workflows and AI-driven mathematical research
• Abstract（参考訳）: 拡大するLean 4エコシステムは、その広大なライブラリをナビゲートする上での課題である。 本稿では、Lean 4宣言のための検索エンジンであるLeanExploreを紹介します。 LeanExploreを使うと、ユーザーは正式にも非公式にも、いくつかのLean 4パッケージ(Batteries、Init、Lean、Mathlib、PhysLean、Stdなど)でステートメントをセマンティックに検索できる。 この検索機能は、マルチソースセマンティック埋め込みモデル(形式的リーンコード、ドクストリング、AI生成の非公式翻訳、宣言タイトルから概念的意味をキャプチャする)、キーワードベースの語彙関連性のためのBM25+、宣言の重要性と相互接続性を反映したPageRankベースのスコアを統合したハイブリッドランキング戦略によって実現されている。 検索エンジンは専用のWebサイト(https://www.leanexplore.com/)とPython API(https://github.com/justincasher/lean-explore)を通じてアクセスできる。 さらに、データベースはダウンロード可能で、ユーザはサービスをセルフホストできる。 LeanExploreはモデルコンテキストプロトコル(MCP)を通じてLLMと簡単に統合可能で、ユーザーはAIアシスタントとリーン宣言についてチャットしたり、検索エンジンを使用して定理を提供するエージェントを構築することができる。 この研究はLeanExploreのアーキテクチャ、データ処理、機能、そしてLean 4のワークフローとAI駆動の数学的研究を強化する可能性について詳述している。

関連論文リスト

• Iterative Self-Incentivization Empowers Large Language Models as Agentic Searchers [74.17516978246152]
  大規模言語モデル(LLM)は、従来の手法を進化させるために情報検索に広く統合されている。 エージェント検索フレームワークであるEXSEARCHを提案する。 4つの知識集約ベンチマークの実験では、EXSEARCHはベースラインを大幅に上回っている。
  論文  参考訳（メタデータ） (2025-05-26T15:27:55Z)
• LLM4PR: Improving Post-Ranking in Search Engine with Large Language Models [9.566432486156335]
  検索エンジンにおける後処理のための大規模言語モデル(LLM4PR) 検索エンジン(LLM4PR)におけるポストランキングのための大規模言語モデル(Large Language Models for Post-Ranking)という新しいパラダイムを導入する。
  論文  参考訳（メタデータ） (2024-11-02T08:36:16Z)
• Harnessing the Power of Semi-Structured Knowledge and LLMs with Triplet-Based Prefiltering for Question Answering [2.6524539020042663]
  大きな言語モデル(LLM)はドメイン固有の知識を欠くことが多く、微調整されたモデルでさえ幻覚を起こす傾向がある。 パイプラインである4StepFocus、具体的には前処理のステップを示し、LCMの回答を大幅に改善する。 この手法は、半構造化知識ベースで三重項に基づく検索によって、直接的かつトレース可能な方法で、潜在的に正しい答えを絞り込む。
  論文  参考訳（メタデータ） (2024-09-01T22:43:27Z)
• When Search Engine Services meet Large Language Models: Visions and Challenges [53.32948540004658]
  本稿では,大規模言語モデルと検索エンジンの統合が,両者の相互に利益をもたらすかどうかを詳細に検討する。 LLM(Search4LLM)の改良と,LLM(LLM4Search)を用いた検索エンジン機能の向上という,2つの主要な領域に注目した。
  論文  参考訳（メタデータ） (2024-06-28T03:52:13Z)
• Crafting Knowledge: Exploring the Creative Mechanisms of Chat-Based Search Engines [3.5845457075304368]
  本研究の目的は,LLMを利用した検索エンジン,特にBing Chatが応答情報ソースを選択するメカニズムを解明することである。 Bing Chatは読みやすく、形式的に構造化されたコンテンツを好むだけでなく、より低いパープレキシティレベルを示す。 本調査では,RAG技術が引用するWebサイトと従来の検索エンジンの上位のWebサイトとの類似性を比較検討した。
  論文  参考訳（メタデータ） (2024-02-29T18:20:37Z)
• UFO: a Unified and Flexible Framework for Evaluating Factuality of Large Language Models [73.73303148524398]
  大規模言語モデル(LLM)は、人間の知識との整合性に欠けるテキストを生成し、事実的不正確さやテキスト・ハロシン化をもたらす。 プラグアンドプレイのファクトソースに対する事実を検証するための,LLMに基づく統一的かつ柔軟な評価フレームワークである textttUFO を提案する。
  論文  参考訳（メタデータ） (2024-02-22T16:45:32Z)
• DIVKNOWQA: Assessing the Reasoning Ability of LLMs via Open-Domain Question Answering over Knowledge Base and Text [73.68051228972024]
  大きな言語モデル(LLM)は印象的な生成能力を示すが、内部知識に依存すると幻覚に悩まされる。 検索拡張LDMは、外部知識においてLLMを基盤とする潜在的な解決策として出現している。
  論文  参考訳（メタデータ） (2023-10-31T04:37:57Z)
• Using an LLM to Help With Code Understanding [13.53616539787915]
  大規模言語モデル(LLM)は、コードを書くプロセスに革命をもたらしています。 プラグインはOpenAIのGPT-3.5-turboモデルに対して,ユーザが明示的なプロンプトを書かなくても4つの高レベルリクエストをクエリする。 本システムの評価は,32名の被験者を対象に行ったユーザスタディで行われ,本プラグインがWeb検索よりもタスク完了に有効であることが確認された。
  論文  参考訳（メタデータ） (2023-07-17T00:49:06Z)
• Synergistic Interplay between Search and Large Language Models for Information Retrieval [141.18083677333848]
  InteRにより、RMはLLM生成した知識コレクションを使用してクエリの知識を拡張することができる。 InteRは、最先端手法と比較して総合的に優れたゼロショット検索性能を実現する。
  論文  参考訳（メタデータ） (2023-05-12T11:58:15Z)

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

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