論文の概要: Learning to Repair Lean Proofs from Compiler Feedback

• arxiv url: http://arxiv.org/abs/2602.02990v1
• Date: Tue, 03 Feb 2026 01:53:56 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-04 18:37:15.185314
• Title: Learning to Repair Lean Proofs from Compiler Feedback
• Title（参考訳）: コンパイラのフィードバックからリーンの証明を修復する学習
• Authors: Evan Wang, Simon Chess, Daniel Lee, Siyuan Ge, Ajit Mallavarapu, Vasily Ilin,
• Abstract要約: 教師付き学習問題としてリーン証明修復について検討する。 APRIL(Automated Proof repair in Lean)は、260,000の教師付き定理のデータセットである。 我々は、診断条件付き監視を、フィードバックを利用するプローバーのための補完的な訓練信号と見なしている。
• 参考スコア（独自算出の注目度）: 4.55626337217127
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: As neural theorem provers become increasingly agentic, the ability to interpret and act on compiler feedback is critical. However, existing Lean datasets consist almost exclusively of correct proofs, offering little supervision for understanding and repairing failures. We study Lean proof repair as a supervised learning problem: given an erroneous proof and compiler feedback, predict both a corrected proof and a natural-language diagnosis grounded in the same feedback. We introduce APRIL (Automated Proof Repair in Lean), a dataset of 260,000 supervised tuples pairing systematically generated proof failures with compiler diagnostics and aligned repair and explanation targets. Training language models on APRIL substantially improves repair accuracy and feedback-conditioned reasoning; in our single-shot repair evaluation setting, a finetuned 4B-parameter model outperforms the strongest open-source baseline. We view diagnostic-conditioned supervision as a complementary training signal for feedback-using provers. Our dataset is available at \href{https://huggingface.co/datasets/uw-math-ai/APRIL}{this link}.
• Abstract（参考訳）: 神経定理プローバーがますますエージェント的になるにつれて、コンパイラのフィードバックを解釈し、作用する能力は不可欠である。 しかし、既存のリーンデータセットは、ほぼ完全に正しい証明で構成されており、失敗を理解し、修復するためのほとんど監督を提供していません。 誤証明とコンパイラフィードバックを与えられた場合、同じフィードバックに基づいて修正された証明と自然言語の診断の両方を予測する。 APRIL(Automated Proof repair in Lean)は、260,000の教師付きタプルのデータセットで、コンパイラの診断とアライメントされた修復と説明のターゲットを備えた、体系的に生成された証明失敗をペアリングする。 APRIL上での訓練言語モデルは、修復精度とフィードバック条件の推論を大幅に改善し、単発補修評価設定では、微調整された4Bパラメータモデルが最強のオープンソースベースラインを上回ります。 我々は、診断条件付き監視を、フィードバックを利用するプローバーのための補完的な訓練信号と見なしている。 データセットは \href{https://huggingface.co/datasets/uw-math-ai/APRIL}{this link} で利用可能です。

関連論文リスト

• Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
  大規模言語モデル(LLM)は,*検証リワード*(RLVR)を用いた強化学習を通じて,強力な数学推論能力を示した。 多くの先進的な数学的問題は証明ベースであり、単純な解マッチングによって証明の真性を決定するための保証された方法はない。 自動検証を実現するには、完全な証明プロセスを確実に評価できるリワードモデル(RM)が必要である。
  論文  参考訳（メタデータ） (2026-02-02T17:42:53Z)
• Refinement Provenance Inference: Detecting LLM-Refined Training Prompts from Model Behavior [58.751981587234916]
  本稿では,Refinement Provenance Inference (RPI)監査タスクをRefinement Provenance Inference (RPI)として定式化する。 本稿では,ロジットレベルの信号で教師が強制する可能性機能を融合させるロジットベースのフレームワークであるReProを提案する。 トレーニング中、ReProはシャドウファインチューニングを通じて転送可能な表現を学び、訓練データアクセスなしで、見えない犠牲者の証明を推測するために軽量のリニアヘッドを使用する。
  論文  参考訳（メタデータ） (2026-01-05T10:16:41Z)
• Rethinking the Capability of Fine-Tuned Language Models for Automated Vulnerability Repair [5.847724760751716]
  微調整された言語モデルを利用する学習ベースの自動脆弱性修正(AVR)技術は、脆弱性パッチの生成を約束している。 私たちの経験的研究は、最先端のモデルはトレーニングセットに過度に適合し、相互に排他的でないトレーニング、検証、テストセットを用いて評価されることを明らかにします。 学習ベースに適したテストベースベンチマークであるL-AVRBenchを導入し、マッチングベースのメトリクスの限界を克服し、モデルの真の修復能力を検証した。
  論文  参考訳（メタデータ） (2025-12-27T16:12:43Z)
• Repairing vulnerabilities without invisible hands. A differentiated replication study on LLMs [5.10123605644148]
  自動脆弱性修復(AVR: Automated Vulnerability repair)は、プログラム修復の急激な分岐である。 近年の研究では、大きな言語モデル(LLM)が従来の手法より優れていることが示されている。
  論文  参考訳（メタデータ） (2025-07-28T16:39:16Z)
• STRIVE: Structured Reasoning for Self-Improvement in Claim Verification [30.15803409441136]
  自己改善検証のための構造化推論を提案する。 本稿では,Crim Decomposition,Entity Analysis,Evidence Grounding Verificationを用いた構造化推論設計を提案する。 その後、すべてのトレーニング例に対して推論連鎖を生成するために適用され、その後の自己改善トレーニングのために正確で構造的に健全なもののみを選択する。
  論文  参考訳（メタデータ） (2025-02-17T16:07:07Z)
• Small Language Models Need Strong Verifiers to Self-Correct Reasoning [69.94251699982388]
  大規模言語モデル(LLM)の推論性能を高めるための有望なソリューションとして自己補正が登場した。 この研究は、小さい(=13B)言語モデル(LM)が、より強いLMから最小の入力で推論タスクを自己補正できるかどうかを考察する。
  論文  参考訳（メタデータ） (2024-04-26T03:41:28Z)
• Learning to Check: Unleashing Potentials for Self-Correction in Large Language Models [5.463333911506443]
  我々は,タスクチェックのためのトレーニングデータを構築することで,大規模言語モデル(LLM)の自己チェック能力を向上させることを目指している。 ステップCoTチェック(Step CoT Check)と呼ばれる特殊なチェックフォーマットを提案する。 実験により、"Step CoT Check"フォーマットによる微調整により、LCMの自己チェックと自己補正能力が大幅に向上することが示された。
  論文  参考訳（メタデータ） (2024-02-20T14:23:23Z)
• Lyra: Orchestrating Dual Correction in Automated Theorem Proving [63.115422781158934]
  Lyraは新しいフレームワークで、ツール補正とConjecture Correctionという2つの異なる補正メカニズムを採用している。 ツール補正は幻覚の緩和に寄与し、それによって証明の全体的な精度が向上する。 Conjecture Correctionは命令で生成を洗練させるが、ペア化された(生成、エラー、改善)プロンプトは収集しない。
  論文  参考訳（メタデータ） (2023-09-27T17:29:41Z)

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

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