論文の概要: Premise Selection for a Lean Hammer

• arxiv url: http://arxiv.org/abs/2506.07477v1
• Date: Mon, 09 Jun 2025 06:50:59 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-10 16:33:10.834424
• Title: Premise Selection for a Lean Hammer
• Title（参考訳）: リーンハマーのための前提選択
• Authors: Thomas Zhu, Joshua Clune, Jeremy Avigad, Albert Qiaochu Jiang, Sean Welleck,
• Abstract要約: ハマーは、退屈な推論ステップを自動化するために外部の自動定理プローバーとインターフェースするツールである。 LeanHammerは、リーンの最初のエンドツーエンドのドメイン・ジェネラル・ハンマーです。 我々の前提セレクタは、LeanHammerが既存の前提セレクタと比較して21%多くの目標を解決できることを示している。
• 参考スコア（独自算出の注目度）: 17.976801288981395
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Neural methods are transforming automated reasoning for proof assistants, yet integrating these advances into practical verification workflows remains challenging. Hammers are tools that interface with external automatic theorem provers to automate tedious reasoning steps. They have dramatically improved productivity in proof assistants, but the Lean proof assistant still does not have a hammer despite its growing popularity. We present LeanHammer, the first end-to-end domain-general hammer for Lean, built on a novel neural premise selection system for a hammer in dependent type theory. Unlike existing Lean premise selectors, our approach dynamically adapts to user-specific contexts and combines with symbolic proof search and reconstruction to create a practical hammer. With comprehensive evaluations, we show that our premise selector enables LeanHammer to solve 21\% more goals relative to existing premise selectors, and generalize well to diverse domains. Our work bridges the gap between neural retrieval and symbolic reasoning, making formal verification more accessible to researchers and practitioners.
• Abstract（参考訳）: ニューラルネットワークは、証明アシスタントの自動推論を変換しているが、これらの進歩を実践的な検証ワークフローに統合することは依然として難しい。 ハマーは、退屈な推論ステップを自動化するために外部の自動定理プローバーとインターフェースするツールである。 証明アシスタントの生産性は劇的に向上しましたが、Lean証明アシスタントは人気が高まっているにも関わらず、まだハンマーを持っていません。 LeanHammerは、依存型理論におけるハンマーのための新しいニューラルネットワークの前提選択システム上に構築された、リーンのための最初のエンドツーエンドのドメイン汎用ハンマーです。 既存のリーン前提のセレクタとは異なり、私たちのアプローチはユーザ固有のコンテキストに動的に対応し、象徴的な証明検索と再構築を組み合わせて実践的なハンマーを作ります。 包括的な評価により、私たちの前提セレクタは、LeanHammerが既存の前提セレクタと比較して21倍の目標を解決し、多様なドメインにうまく一般化できることを示す。 我々の研究は、ニューラル検索とシンボリック推論のギャップを埋め、正式な検証を研究者や実践者にとってよりアクセスしやすくする。

関連論文リスト

• Lemmanaid: Neuro-Symbolic Lemma Conjecturing [4.583367875081881]
  本稿では, 実用的神経シンボル型レムマ注入ツールLemmanaidについて紹介する。 レムマの形状を記述したレムマテンプレートを生成するためにLLMをトレーニングし、詳細を記入するためにシンボリックメソッドを使用します。 我々は,レマノイドを完全補題文を生成するために訓練されたLLMと,それ以前の完全記号推論法と比較した。
  論文  参考訳（メタデータ） (2025-04-07T11:30:36Z)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。 本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。 また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
  リーンでLLM推論を実行するためのフレームワークであるLean Copilotを紹介します。 証明のステップを提案し、証明の目標を完了し、関連する前提を選択するツールを構築します。 人間を助ける場合、Lean Copilotは平均3.86で手動で入力された証明ステップを2.08ステップしか必要としない。 定理証明プロセスを自動化する場合、Lean Copilotの74.2%の証明ステップは平均85%がエソップ(40.1%)より優れている。
  論文  参考訳（メタデータ） (2024-04-18T22:54:08Z)
• Efficient Tool Use with Chain-of-Abstraction Reasoning [63.08202389132155]
  大規模言語モデル(LLM)は、現実世界の知識に対する推論の基礎となる必要がある。 マルチステップ推論問題におけるツールの実行には,微調整LDMエージェントの課題が残されている。 マルチステップ推論におけるツールの活用方法として, LLM の新しい手法を提案する。
  論文  参考訳（メタデータ） (2024-01-30T21:53:30Z)
• Machine-Learned Premise Selection for Lean [0.8354034992258483]
  我々は、ユーザーが証明した定理の適切な前提を提案する、リーン証明アシスタントのための機械学習ベースのツールを紹介します。 ツールの設計原則は,(1)証明アシスタントとの緊密な統合,(2)使いやすさとインストール,(3)軽量で迅速なアプローチである。
  論文  参考訳（メタデータ） (2023-03-17T10:37:34Z)
• Magnushammer: A Transformer-Based Approach to Premise Selection [20.445974111113223]
  我々は、(保護状態、関連する前提)ペアのテキスト表現を含む、前提選択のための新しいデータセットを開発し、オープンソース化する。 我々の手法であるMagnushammerは、Sledgehammerと呼ばれるインタラクティブな定理の証明において、最も先進的で広く使われている自動化ツールより優れています。 さらに、PISAベンチマークでは、最先端の証明成功率を57.0%から71.0%に改善し、パラメータを4ドル減らした。
  論文  参考訳（メタデータ） (2023-03-08T10:22:00Z)
• MURAL: Meta-Learning Uncertainty-Aware Rewards for Outcome-Driven Reinforcement Learning [65.52675802289775]
  本研究では,不確かさを意識した分類器が,強化学習の難しさを解消できることを示す。 正規化最大度(NML)分布の計算法を提案する。 得られたアルゴリズムは、カウントベースの探索法と、報酬関数を学習するための先行アルゴリズムの両方に多くの興味深い関係を持つことを示す。
  論文  参考訳（メタデータ） (2021-07-15T08:19:57Z)
• Vampire With a Brain Is a Good ITP Hammer [0.0]
  我々は,効率のよい神経誘導による飽和手順の強化により,完全なMizarライブラリ上でのハンティングにおけるヴァンパイアの性能を向上させる。 節の論理的内容を考慮した従来のニューラルメソッドと比較して、これはニューラルガイダンスの大きなリアルタイム高速化につながる。 得られたシステムは、優れた学習能力を示し、Mizarライブラリ上で最先端のパフォーマンスを達成する。
  論文  参考訳（メタデータ） (2021-02-06T07:24:53Z)

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

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