論文の概要: Fix, Not Just Resample: Bounded Compiler-Guided Repair in Lean 4

• arxiv url: http://arxiv.org/abs/2610.26942v1
• Date: Sun, 18 Oct 2026 04:21:55 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-21 21:58:47.403566
• Title: Fix, Not Just Resample: Bounded Compiler-Guided Repair in Lean 4
• Title（参考訳）: 修正、単なるリサンプルではない - リーン4のコンパイラガイドによる修正境界
• Abstract要約: Leanのような証明アシスタントのための、バウンダリでオンラインのステップレベルの修復モジュールを導入しています。 失敗した戦術を捨てる代わりに、プリトレーニング済みの修復モデルにコンパイラのエラーメッセージを送って、個別に拒否されたステップを修正します。 このアプローチは、テスト対象のすべての予算に対してサンプリングのみのベースラインよりも解決率を向上する。
• 参考スコア（独自算出の注目度）: 12.82165181026639
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automated theorem provers often rely on sampling language models, but proof assistants like Lean reject each failed step with a precise error message --- information that pure sampling discards. To overcome this, we introduce a bounded, online step-level repair module. Our search samples $K$ candidate tactics at each step and repairs a failed tactic at most $R$ times. Instead of discarding failed tactics, we feed the compiler's error message to a pretrained repair model to fix individual rejected steps in place. This approach improves the solve rate over a sampling-only baseline across all tested candidate budgets ($K \in \{1,3,5,8\}$), achieving up to a $32\%$ relative gain and solving $82$ additional theorems on a $1{,}990$-theorem subset of the LeanDojo benchmark. Repair is not free: it trades extra runtime for reachable proofs. But the trade is predictable: repair pays most when sampling is constrained; its return is front-loaded, with the first repair attempt capturing $84\text{--}96\%$ of the total gain; and the gain comes almost entirely from shallow tactic-execution failures rather than structural errors such as type mismatches. This targeted repair successfully replicates on a second benchmark (Lean Workbook), nearly doubling the solve rate with zero regressions.
• Abstract（参考訳）: 自動定理プローバは、しばしばサンプリング言語モデルに依存するが、Leanのような証明アシスタントは、失敗するステップごとに正確なエラーメッセージ -- 純粋なサンプリングが破棄される情報 -- を拒否する。 これを解決するために,オンラインのステップレベル修復モジュールを導入する。 われわれの検索は、各ステップで$K$の候補戦術をサンプリングし、失敗した戦術を少なくとも$R$の回数で修復する。 失敗した戦術を捨てる代わりに、プリトレーニング済みの修復モデルにコンパイラのエラーメッセージを送って、個別に拒否されたステップを修正します。 このアプローチは、テスト対象のすべての予算(K \in \{1,3,5,8\}$)にわたるサンプリング専用ベースライン(K \in \{1,3,5,8\}$)の解決率を向上し、LeanDojoベンチマークの1{,}990$-theoremサブセットで、32\%の相対的なゲインを達成し、82ドルの追加定理を解決します。 修復は無料ではなく、到達可能な証明のために余分なランタイムを交換する。 しかし、この取引は予測可能であり、サンプリングが制限された場合、リターンはフロントロードされ、最初の修理試行で合計利得の84\text{--}96\%が取得され、その利益は、型ミスマッチのような構造的エラーではなく、ほとんど完全に浅い戦術的実行失敗から得られる。 この目標とする修復は、第2のベンチマーク(Lean Workbook)で成功した。

関連論文リスト

• Make Every Expansion Count: Learning to Search Efficiently in LLM Code Repair [63.277419653843594]
  修正プログラムの生成とテストの前に編集を優先する学習ポリシであるCodeTriageを紹介する。 ホールドアウトの修理タスクでは、CodeTriageは、各メトリックで最強のベースラインよりも21%少ないプログラム修正と12%少ないアウトプットトークンの修正を見つける。
  論文  参考訳（メタデータ） (2026-10-11T20:19:05Z)
• Learning from the Gap Between Pass@K and Pass@1 [5.390994765967647]
  本研究では,各クエリが検索なしで1つの応答を受信する単一サンプル復号法について検討し,検索対象の振る舞いをモデルに吸収できるかどうかを問う。 既存のトレーニング後レシピは、Kサンプル内で回収された障害から、最初のデコードで既に解決されている問題を一般的に区別するものではない。 本稿では、ソースチェックポイントの単一サンプル結果とPass@K-Pass@1ギャップ上の微調整によってトレーニングエビデンスを選択するGapFTを紹介する。
  論文  参考訳（メタデータ） (2026-09-17T04:34:33Z)
• Sampling-based Certified Planning with Graphs of Convex Sets [3.732244093761483]
  凸上の平面は、凸領域が衝突のない場合、建設によって衝突のない軌道を返す。 私たちはその答えを認定するプランナーを構築します。 あらゆる29ドルのタスククエリに対してゼロの無効な回答を、参照に対して21ドル、最初の認定された回答を0.11ドル、参照の未検証クエリに対して1.59ドル、参照が物理的に有効であるすべてのクエリに対して正確に参照最適化を再現する。
  論文  参考訳（メタデータ） (2026-08-30T12:57:53Z)
• Calibration, Not Compilation: Detecting and Repairing Misspecified Probabilistic Programs Written by Language Models [31.082191748525137]
  言語モデルはますます確率的プログラムを書くようになる(NumPyro、Stan、Pyro) すべてのユニットテストをコンパイルし、実行し、パスするプログラムは、偶数論的に間違っている。 したがって、正しい検証はテストスイートではなく、ベイズワークフロー自身である。
  論文  参考訳（メタデータ） (2026-06-30T13:16:39Z)
• Correction and Corruption: A Two-Rate View of Error Flow in LLM Protocols [51.56484100374058]
  そこで本研究では,単一プロトコルステップを正確なマッチングタスクで監査するためのペアアウトカム計測インタフェースを提案する。 各インスタンスについて、インターフェースはベースラインの正当性ビットと後ステップの正当性ビットを記録する。 これらのレートは精度の変化を予測し、種、混合物、パイプライン間でテスト可能な再利用可能な経験的インターフェースを定義する。
  論文  参考訳（メタデータ） (2026-04-20T13:25:40Z)
• Reinforcement Learning with Verifiable yet Noisy Rewards under Imperfect Verifiers [90.50039419576807]
  RLVR(Reinforcement Learning with Verifiable Rewards)は、人為的なラベル付けを避けるために、自動検証に対するポリシーを訓練する。 認証ハッキングの脆弱性を軽減するため、多くのRLVRシステムはトレーニング中にバイナリ$0,1$の報酬を破棄する。 この選択にはコストがかかる:textitfalse negatives(正しい回答、FNを拒絶)とtextitfalse positives(間違った回答、FPを受け入れる)を導入する。
  論文  参考訳（メタデータ） (2025-10-01T13:56:44Z)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
  本稿では,自動定理証明のためのモデルに依存しないエージェントフレームワークであるAPOLLO (Automated PrOof repair viaLLM and Lean cOllaboration)を提案する。 エージェントのセットは、証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動化されたソルバを利用し、残りの目標に対してLLMを呼び出す。 この結果から,LLM出力を目標としたコンパイラ誘導型修復は,効率と正確性の両方において劇的に向上することが示された。
  論文  参考訳（メタデータ） (2025-05-09T03:38:31Z)
• Bias Mimicking: A Simple Sampling Approach for Bias Mitigation [57.17709477668213]
  本稿では,新しいクラス条件サンプリング手法であるBias Mimickingを紹介する。 Bias Mimickingは、4つのベンチマークで3%の精度でサンプリングの精度を向上する。
  論文  参考訳（メタデータ） (2022-09-30T17:33:00Z)

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

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