論文の概要: DAPS: Dependency-Aware Premise Selection for LLM Theorem Proving

• arxiv url: http://arxiv.org/abs/2610.41536v1
• Date: Fri, 30 Oct 2026 10:28:34 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-11-02 22:05:31.68213
• Title: DAPS: Dependency-Aware Premise Selection for LLM Theorem Proving
• Title（参考訳）: DAPS: LLM理論証明のための依存性を考慮した事前選択
• Abstract要約: リーン 4 で証明された LLM ベースの定理は急速に進歩しているが、プローバーは新しく提供された補題を活用するのは難しい。 既存のニューラルセレクタは、3つの固有の制限とともに、セマンティックな類似性によって候補をランク付けする。 DAPS、構造的近傍エンコーダ、グループレベルのコントラスト目的、Mathlib-then-Blueprint適応プロシージャを導入。
• 参考スコア（独自算出の注目度）: 57.48166976575127
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: LLM-based theorem proving in Lean 4 has advanced rapidly, but provers are difficult to leverage newly contributed lemmas, because retrieval skews toward popular foundational lemmas, leaving the right premises buried among hundreds of thousands of candidates. Existing neural selectors rank candidates by semantic similarity, with three intrinsic limitations: frequency-skewed retrieval, isolated pairwise ranking, and degradation on out-of-distribution queries such as competition problems and informal language. Given that mathematics is structured by dependencies rather than similarities, we restore this signal to both the training data and the model. We curate two underused dependency resources. We conduct the first systematic mining of 53 Lean Blueprint projects, a previously untapped corpus of 3,805 manually curated informal+formal nodes that capture rare, research-level premises absent from Mathlib4. We further pair it with the extraction of comprehensive, typed, multi-level Mathlib4 dependencies. We then introduce DAPS, a dependency-aware premise selector with a structural neighborhood encoder, a group-level contrastive objective, and a Mathlib-then-Blueprint adaptation procedure. DAPS reaches mean Recall@32 of 89.25 on Mathlib4-Heldout (+11.41 over the strong selector LeanHammer), and maintains this lead on two out-of-distribution benchmarks. Further experiments demonstrate that DAPS premises improve theorem proving on miniF2F and IMO-ProofBench. Project page: https://daps-eth.github.io/.
• Abstract（参考訳）: リーン 4 で証明された LLM ベースの定理は急速に進歩しているが、プローバーが新しく提案された補題を活用するのは難しい。 既存のニューラルセレクタは、競合問題や非公式言語などのアウト・オブ・ディストリビューションクエリにおける、周波数スキュード検索、孤立したペアワイドランキング、分解という3つの本質的な制限を伴って、セマンティックな類似性によって候補をランク付けする。 数学は類似性ではなく依存関係によって構成されていることを考慮し、この信号をトレーニングデータとモデルの両方に復元する。 2つの未使用の依存リソースをキュレートします。 我々は53のLean Blueprintプロジェクトの最初の体系的なマイニングを実施しました。これは、これまで未完成だった3,805の非公式な+形式的なノードで、Mathlib4から欠落したまれな研究レベルの前提をキャプチャします。 さらに、包括的で型付けされたマルチレベルのMathlib4依存関係の抽出と組み合わせます。 次に、DAPS、構造的近傍エンコーダ、グループレベルのコントラスト目的、Mathlib-then-Blueprint適応プロシージャを導入する。 DAPSはMathlib4-Heldout(強力なセレクタLeanHammerよりも+11.41)で平均89.25のRecall@32に達し、このリードを2つのアウト・オブ・ディストリビューションベンチマークで維持している。 さらなる実験では、DAPS 前提が miniF2F と IMO-ProofBench の定理証明を改善することが示されている。 プロジェクトページ: https://daps-eth.github.io/.com

関連論文リスト

• When Does Structured Knowledge Help Neural Theorem Proving? [0.03110995905282905]
  MathKGは364のMathlibsと9,434の型付きセマンティックエッジを接続する。 我々は4つの拡張モード(文脈、知識グラフコンテキスト、Mathlib、両方)と5つのモデルで制御されたアブレーションを実行する。
  論文  参考訳（メタデータ） (2026-09-28T07:17:43Z)
• The Laws of Context Allocation: Causal Measurement and Closed-Loop Orchestration in Generative Search [19.846305722187328]
  Retrieval-Augmented Generation (RAG)は、多様なポートフォリオ生成にシフトする。 これは2つの重要なボトルネック、すなわち証拠利用率の欠陥測定と、最適条件下予算配分によって悪影響を受けている。 本稿では,遺伝子依存を正確に分離する因果排除プローブを提案する。 モノリシック・コンテキスト・ワイドニング(モノリシック・コンテキスト・ワイドニング)の一般的な戦略は、関連性の崩壊によって罰せられるアーキテクチャ・トラップであることを示す。
  論文  参考訳（メタデータ） (2026-08-24T13:44:11Z)
• Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement [69.77146194380488]
  私たちはGoedel-Architectを紹介します。これは、青写真の生成と洗練に焦点を当てたLean 4で証明された公式な定理のためのフレームワークです。 Goedel-ArchitectがMiniF2Fテストで99.2%パス@1、PutnamBenchで75.6%パス@1を達成した。 これは、同等のオープンソースパイプラインよりも500倍低い価格で、オープンソースパイプラインの最先端のパフォーマンスを示している。
  論文  参考訳（メタデータ） (2026-06-04T17:54:44Z)
• DiscoUQ: Structured Disagreement Analysis for Uncertainty Quantification in LLM Agent Ensembles [5.647839536820347]
  著者間の不一致構造を抽出し活用し,信頼度を良好に推定するフレームワークであるDiscoUQを紹介する。 DiscoUQ-LLM の平均 AUROC は 0.802 であり、最高のベースラインを上回っている。 学習した機能は、ほぼゼロに近いパフォーマンス劣化を伴うベンチマークで一般化される。
  論文  参考訳（メタデータ） (2026-03-21T23:24:12Z)
• Test-Time Scaling with Diffusion Language Models via Reward-Guided Stitching [66.39914384073145]
  本稿では,安価な拡散サンプリング推論をステップレベル候補の再利用プールに変換する自己整合性フレームワークを提案する。 ステップレベルの再結合は、難しい問題に対して最も有益であることがわかった。 トレーニング不要のフレームワークは、6つの数学およびコーディングタスクの平均精度を最大2倍改善します。
  論文  参考訳（メタデータ） (2026-02-26T11:08:39Z)
• Semantic Bridge: Universal Multi-Hop Question Generation via AMR-Driven Graph Synthesis [3.1427813443719868]
  大きな言語モデル(LLM)のトレーニングは、高品質で推論集約的な質問応答ペアの不足という、重大なボトルネックに直面します。 textbfSemantic Bridgeは、任意の情報源から洗練されたマルチホップ推論質問を制御可能とする最初の普遍的フレームワークである。
  論文  参考訳（メタデータ） (2025-08-06T10:59:42Z)
• Optimal Multi-Distribution Learning [88.3008613028333]
  マルチディストリビューション学習は、$k$の異なるデータ分散における最悪のリスクを最小限に抑える共有モデルを学ぶことを目指している。 本稿では, (d+k)/varepsilon2の順に, サンプルの複雑さを伴って, ヴァレプシロン最適ランダム化仮説を導出するアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2023-12-08T16:06:29Z)

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

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