論文の概要: Let the Library Speak: Self-Advertised Method Selection for Formal Proving

• arxiv url: http://arxiv.org/abs/2610.09401v1
• Date: Wed, 07 Oct 2026 04:03:49 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-08 21:58:22.711342
• Title: Let the Library Speak: Self-Advertised Method Selection for Formal Proving
• Title（参考訳）: 図書館を語る:形式的証明のための自己適応型メソッド選択
• Abstract要約: LLMベースの形式証明器は関連する補題や先行証明を検索できるが、関連性だけでは、数学的な方法が現在の定理で利用できるかどうかは定かではない。 我々はこれを適用可能性を考慮したメソッド選択問題として定式化し、自己広告を導入する。 モデルはそれぞれの問題固有の提案を生成し、目標のどの部分、どのアクションを取るか、どのアクションが必要なのかを記述します。
• 参考スコア（独自算出の注目度）: 31.49391158449015
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: LLM-based formal provers can retrieve relevant lemmas and prior proofs, but relevance alone does not say whether a mathematical method can be used on the current theorem. A method has prerequisites, a target, an intended action, and obligations that its use leaves to prove. Methods that look equally related to a theorem may therefore differ substantially in whether they offer a plausible next step. We formulate this as an applicability-aware method-selection problem and introduce self-advertisement: before candidates are ranked, a model generates a problem-specific proposal for each one, stating what part of the goal it targets, what action it would take, and what conditions that action requires. We organize 82 reusable methods from Putnam 2000-2014 as Method Contracts, which pair applicability descriptions with Mathlib anchors, a checked example or scaffold, and expected proof obligations. A single batched call elicits proposals across the library; vague or unsupported proposals are demoted, yielding a ranked shortlist accompanied by inspectable claims about each candidate's use. We analyze when similarity-based representations cannot distinguish methods with different applicability, how errors in applicability estimates affect shortlist quality, and what a checked scaffold guarantees under its stated assumptions. Against lexical, embedding, and embedding-plus-LLM reranking baselines, self-advertisement achieves 95.0% hit@5 on Putnam 2015-2025, compared with 84.2% for the strongest reranker. On IMO ProofBench, it achieves 91.7% compared with 88.3%. These results indicate improved coverage of annotated methods in the retrieved shortlists, particularly on Putnam.
• Abstract（参考訳）: LLMベースの形式証明器は関連する補題や先行証明を検索できるが、関連性だけでは、数学的な方法が現在の定理で利用できるかどうかは定かではない。 方法には、前提条件、目標、意図された行動、そしてその使用が証明するために残される義務がある。 したがって、定理に等しく関連しているように見える方法は、それらが妥当な次のステップを提供するかどうかで大きく異なるかもしれない。 我々は、これを適用可能性を考慮したメソッド選択問題として定式化し、自己広告を導入する: 候補者がランク付けされる前に、モデルが各候補に対して問題固有の提案を生成し、目標のどの部分、どのようなアクションを取るか、その動作に必要な条件を述べる。 我々はPatnam 2000-2014の82の再利用可能なメソッドを Method Contracts として整理し、Mathlib アンカーとペア適用性記述、チェックされたサンプルまたは足場、および期待された証明義務を記述した。 1つのバッチコールが図書館全体に提案を誘導し、あいまいまたは支持されていない提案が取り下げられ、各候補の使用に関する検査可能なクレームが伴ってランク付けされたショートリストが生成される。 類似度に基づく表現が異なる適用性を持つメソッドを区別できない場合、適用可能性推定における誤差がショートリストの品質にどのように影響するか、チェックされた足場が想定した仮定に基づいて保証するかを分析する。 語彙、埋め込み、埋め込み+LLMのリランクベースラインに対して、自己広告はPutnam 2015-2025で95.0%のヒット@5を達成した。 IMO ProofBenchでは91.7%、88.3%である。 これらの結果は,検索したショートリスト,特にパットナムにおける注釈付きメソッドのカバレッジの改善を示唆している。

関連論文リスト

• Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization [10.775710068605006]
  本稿では,評価問題とボトルネック帰属問題の両方として,忠実な文の形式化について検討する。 ツール拡張されたエージェントは89.5%のコンパイルに到達したが、コンセンサスの忠実度は60.5%に過ぎず、29.0ポイントのコンパイルパスを持つが、コンセンサスに反するギャップを露呈する。
  論文  参考訳（メタデータ） (2026-06-30T00:27:53Z)
• The Attribution Impossibility: No Feature Ranking Is Faithful, Stable, and Complete Under Collinearity [0.0]
  機能がコリニアである場合には,機能ランキングを忠実に,安定的に,かつ完全なものにすることはできない。 この不合理性を証明し、4つのモデルクラスを定量化し、アンサンブル平均化(DASH)によってそれを解決し、305のLean 4定理でそれをマシン検証する。 設計空間の定理、診断、そして不合理性はLean 4(16の公理から305の定理、残念なことに0の定理)で機械的に検証されます。
  論文  参考訳（メタデータ） (2026-04-08T10:11:45Z)
• A Principled Approach to Randomized Selection under Uncertainty: Applications to Peer Review and Grant Funding [61.86327960322782]
  本稿では,各項目の品質の間隔推定に基づくランダム化意思決定の枠組みを提案する。 最適化に基づく最適化手法であるMERITを導入する。 MERITが既存のアプローチで保証されていない望ましい公理特性を満たすことを証明している。
  論文  参考訳（メタデータ） (2025-06-23T19:59:30Z)
• Probabilistic Conformal Prediction with Approximate Conditional Validity [81.30551968980143]
  本研究では,共形手法の柔軟性と条件分布の推定を組み合わせ,予測セットを生成する手法を開発した。 我々の手法は、条件付きカバレッジの観点から既存の手法よりも一貫して優れています。
  論文  参考訳（メタデータ） (2024-07-01T20:44:48Z)
• Composed Image Retrieval with Text Feedback via Multi-grained Uncertainty Regularization [73.04187954213471]
  粗い検索ときめ細かい検索を同時にモデル化する統合学習手法を提案する。 提案手法は、強いベースラインに対して+4.03%、+3.38%、+2.40%のRecall@50精度を達成した。
  論文  参考訳（メタデータ） (2022-11-14T14:25:40Z)
• Double logistic regression approach to biased positive-unlabeled data [3.6594988197536344]
  後続確率と確率スコア関数の結合推定問題に対するパラメトリックなアプローチを考察する。 そこで本研究では, 交互表現に基づく最大解法と2番目の解法という, 2つの推定手法を提案する。 実験の結果,提案手法は期待最大化方式に基づく既存手法と同等か優れていることがわかった。
  論文  参考訳（メタデータ） (2022-09-16T08:32:53Z)
• Achieving Equalized Odds by Resampling Sensitive Attributes [13.114114427206678]
  等価性の概念をほぼ満足する予測モデルを学習するためのフレキシブルなフレームワークを提案する。 この微分可能な関数は、モデルパラメータを等化奇数に向けて駆動するペナルティとして使用される。 本研究は,予測規則が本性質に反するか否かを検出するための公式な仮説テストを開発する。
  論文  参考訳（メタデータ） (2020-06-08T00:18:34Z)

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

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