論文の概要: Adaptive Proof Refinement with LLM-Guided Strategy Selection

• arxiv url: http://arxiv.org/abs/2510.25103v1
• Date: Wed, 29 Oct 2025 02:13:47 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-30 15:50:44.982165
• Title: Adaptive Proof Refinement with LLM-Guided Strategy Selection
• Title（参考訳）: LLM誘導戦略選択による適応的証明
• Authors: Minghai Lu, Zhe Zhou, Danning Xie, Songlin Jia, Benjamin Delaware, Tianyi Zhang,
• Abstract要約: アダプティブ(Adapt)は、新しい証明改善フレームワークである。 既存の4つの手法に対して2つのベンチマークで評価する。 また、Adaptの汎用性を5つの大言語モデルにまたがって評価することで示す。
• 参考スコア（独自算出の注目度）: 6.027693145174767
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal verification via theorem proving enables the expressive specification and rigorous proof of software correctness, but it is difficult to scale due to the significant manual effort and expertise required. While Large Language Models (LLMs) show potential in proof generation, they frequently produce incorrect proofs on the first attempt and require additional strategies for iterative refinement. However, existing approaches employ fixed refinement strategies and cannot dynamically choose an effective strategy based on the particular issues in a generated proof, which limits their performance. To overcome this limitation, we introduce Adapt, a novel proof refinement framework that leverages an LLM-guided decision-maker to dynamically select a suitable refinement strategy according to the state of the proof assistant and available context of an incorrect proof. We evaluate Adapt on two benchmarks against four existing methods and find that it significantly outperforms the best baseline on both by proving 16.63% and 18.58% more theorems, respectively. Furthermore, we demonstrate Adapt's generalizability by evaluating it across five different LLMs. We also conduct ablation studies to measure the contribution of each component and compare the trade-offs of alternative decision-maker designs.
• Abstract（参考訳）: 定理証明による形式的検証は、表現力のある仕様と厳密なソフトウェア正しさの証明を可能にするが、重要な手作業と専門知識のためにスケールすることは困難である。 LLM(Large Language Models)は、証明生成の可能性を示しているが、最初の試みに関する誤った証明をしばしば生成し、反復的洗練のための追加の戦略を必要とする。 しかし、既存の手法では固定改良戦略を採用しており、生成した証明の特定の問題に基づいた効果的な戦略を動的に選択できないため、性能が制限される。 この制限を克服するために,LLM誘導決定器を利用した新しい証明改善フレームワークであるAdaptを導入し,証明アシスタントの状態や不正確な証明の状況に応じて適切な修正戦略を動的に選択する。 既存の4つの手法に対して2つのベンチマークでAdaptを評価し、それぞれ16.63%と18.58%の定理を証明し、両者で最高のベースラインを著しく上回っていることを発見した。 さらに,5種類のLLMに対してアダプティブの一般化性を評価する。 また、各コンポーネントの貢献度を測定し、代替意思決定設計のトレードオフを比較するためのアブレーション研究も行います。

関連論文リスト

• Plan before Solving: Problem-Aware Strategy Routing for Mathematical Reasoning with LLMs [49.995906301946]
  既存の手法は通常、数学的推論を行うためにLLM(Large Language Models)をガイドするための固定戦略を利用する。 分析の結果,単一戦略は問題固有の要件に適応できず,有効性と効率性のトレードオフを見落としていることが明らかとなった。 本稿では,PRISM(Planning and Routing through Instance-Specific Modeling)を提案する。
  論文  参考訳（メタデータ） (2025-09-29T07:22:41Z)
• Learning to Refine: Self-Refinement of Parallel Reasoning in LLMs [102.48588475875749]
  本稿では,新しい並列テスト時間スケーリングフレームワークであるGenerative Self-Refinement (GSR)を紹介する。 GSRは一連の候補応答を並列に生成し、その後自己精製を行い、新しい優れた解を合成する。 提案手法は,5つの数学ベンチマークにおいて,最先端性能を実現する。
  論文  参考訳（メタデータ） (2025-08-27T06:51:48Z)
• Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving [14.569345246475509]
  大規模言語モデル(LLM)は、有望な一階述語論理(FOL)推論能力を示している。 しかし、多段階のFOL還元を含む複雑な数学的推論におけるそれらの効果はいまだ研究されていない。 LLMの生成戦略の多様性と再現性を向上する自己適応型ソリューションであるDREAMを提案する。
  論文  参考訳（メタデータ） (2025-06-20T16:09:56Z)
• Towards Reliable Proof Generation with LLMs: A Neuro-Symbolic Approach [14.213719696233934]
  大型言語モデル(LLM)は厳密な論理的推論と記号的推論を必要とする形式的ドメインと競合する。 本稿では,LLMの生成強度と構造成分を組み合わせ,この課題を克服するニューロシンボリックアプローチを提案する。
  論文  参考訳（メタデータ） (2025-05-20T15:13:32Z)
• Teaching LLMs According to Their Aptitude: Adaptive Reasoning for Mathematical Problem Solving [55.895917967408586]
  大規模な言語モデルによる数学的推論への既存のアプローチは、一般化可能性(英語版)にはChain-of-Thought(英語版)(CoT)、正確な計算にはTool-Integrated Reasoning(英語版)(TIR)に依存している。 本稿では, LLM が自然に推論戦略をパーソナライズできる適応型フレームワークである TATA (Teaching LLMs according their Aptitude) を提案する。
  論文  参考訳（メタデータ） (2025-02-17T16:56:23Z)
• Faithful Explanations of Black-box NLP Models Using LLM-generated Counterfactuals [67.64770842323966]
  NLPシステムの予測に関する因果的説明は、安全性を確保し、信頼を確立するために不可欠である。 既存の手法は、しばしばモデル予測を効果的または効率的に説明できない。 本稿では, 対物近似(CF)の2つの手法を提案する。
  論文  参考訳（メタデータ） (2023-10-01T07:31:04Z)

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

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