論文の概要: Repair, Retry, and the Cost of Hindsight: Verifier Feedback in Formal Theorem Proving
- arxiv url: http://arxiv.org/abs/2610.22698v1
- Date: Thu, 15 Oct 2026 22:03:07 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-20 00:56:07.685901
- Title: Repair, Retry, and the Cost of Hindsight: Verifier Feedback in Formal Theorem Proving
- Title（参考訳）: 視力の修復, 回復, コスト:形式的定理証明における検証フィードバック
- Abstract要約: 検証済みの自己修復条件は、重み付けをせずに再度試みる前に失敗した試みからのフィードバックに関するモデルである。
我々は、汎用モデルであるQwen3.6-27Bと、特殊な証明器であるDeepSeek-Prover-V2-7Bを、難解なMiniF2F問題でテストした。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Verifier-guided self-repair conditions a model on feedback from failed attempts before it tries again, without weight updates. Yet two findings in prior work are in tension: verifier feedback can improve repair of failures, but self-repair itself can provide little-to-no advantage over independent resampling. We reconcile these findings in Lean theorem proving through controlled one-step experiments that hold the preceding failure fixed while varying whether the failed proof is shown, whether the compiler error corresponds to that failure, and the retry instruction. We test frozen Qwen3.6-27B, a general-purpose model, and DeepSeek-Prover-V2-7B, a specialized prover, on difficult MiniF2F problems. We find two opposing effects. Showing the model its failed predecessor reduces success and sharply increases copying of it, while on Qwen adding that attempt's compiler error recovers the loss, to the level of the diagnostic alone. Replacing the predecessor with another theorem's failed proof largely removes the degradation on both models; on Qwen, replacing the diagnostic with another problem's error substantially reduces the recovery. Without the failed proof, correct diagnostics show no resolved advantage over wrong-diagnostic controls on either model. The failed-proof penalty persists with and without the retry instruction, whereas Qwen's diagnostic recovery is weaker without it. In 11-problem sequential experiments through 64 attempts, Qwen retains a correct-diagnostic benefit within failed-proof histories, while DeepSeek-Prover shows no resolved recovery. However, no tested one-step feedback condition establishes an advantage over instruction-only resampling, nor does 64-attempt sequential repair with failed proofs and correct diagnostics at equal token budgets. Verifier feedback can thus improve repair without overcoming the performance loss from conditioning on a failed attempt.
- Abstract（参考訳）: 検証済みの自己修復条件は、重み付けをせずに再度試みる前に失敗した試みからのフィードバックに関するモデルである。
検証者からのフィードバックは障害の修復を改善することができるが、自己修復自体が独立した再サンプリングに対してほとんどメリットを得られない。
これらの結果は,失敗証明が示されるか否か,コンパイラエラーがその失敗に対応するか否か,再試行命令を変更しながら,前回の失敗を固定する制御された一段階の実験を通じて,Leanの定理で検証する。
我々は、汎用モデルであるQwen3.6-27Bと、特殊な証明器であるDeepSeek-Prover-V2-7Bを、難解なMiniF2F問題でテストした。
対立する効果は2つある。
さらにQwenでは、試行のコンパイラエラーによって損失が回復し、診断レベルのみが回復する、と付け加えている。
Qwenでは、診断を他の問題の誤りに置き換えることで、回復を大幅に減少させる。
証明が失敗しない限り、正しい診断は、どちらのモデルでも間違った診断不能な制御に対して解決された優位性を示す。
予防的治療の失敗はリトライ命令なしで継続するが、Qwenの診断回復はそれなしでは弱くなる。
64回の連続的な実験で、Qwenは失敗に終わった歴史の中で正しい診断の利点を保ち、DeepSeek-Proverは解決された回復を示さなかった。
しかし、テストされた1段階のフィードバック条件は、命令のみのリサンプリングよりも有利であり、64段階のシーケンシャルな修正や、同じトークン予算での証明の失敗や正しい診断を行なわない。
これにより、検証者フィードバックは、失敗した試行の条件付けによる性能損失を克服することなく、修復を改善することができる。
関連論文リスト
- Failure Is the Mother of Success: Recovering Supervision with Grounding Hindsight [51.276336727283]
Replay-Selected Hindsight Distillation (RSHD)について述べる。
ポリシーは、参照された回答やソリューションを見ることなく、失敗した各試みについて修正ノートを書き、その後、そのノートで問題をコンテキストで再解決する。
ポリシーのみをトレーニングし、唯一の判断は結果検証であり、デプロイメントはノートや追加の推論を必要としない。
論文 参考訳（メタデータ） (2026-10-14T23:33:22Z) - When Correctness Feedback Erases Evidence: Phase-Separated Completeness Auditing in Verus [0.12062777974093623]
正当性フィードバックは、仕様完全性監査が明らかになるように設計されていることを示す。
提案手法は、4つのモデルファミリーを対象とした12のVerus/Rustタスクにおいて、一致したコール予算の下で、この目的を逆転させるものである。
論文 参考訳（メタデータ） (2026-10-14T14:43:24Z) - Wrong Prediction, Right Answer: Recovering Evidence from Collapsed LLM Sequence Scores [31.709549159768727]
多様な推論ベンチマーク間で一貫した読み出しギャップを観察する。
隠れ状態プローブは、ネイティブシークエンススコアが完全に崩壊しても正解を復号することに成功した。
以上の結果から,無作為な内部論理を隠蔽する表現障害が明らかにゼロショット推論の欠点であることが明らかとなった。
論文 参考訳（メタデータ） (2026-08-31T16:43:55Z) - Diagnosis Before Recovery: Turning Agent Failures into Selective Self-Correction [22.654396704495934]
開発セット障害は、どのリカバリ介入が許容可能かを決定することにより、欠落診断基板の一部を回復することができる。
DARCは、タスクファミリー障害モードをプロファイリングし、共有リカバリライブラリから不正な介入を発生させ、検証者選択によるデプロイメント成功コストポリシーを凍結する、診断誘導型リカバリハーネスである。
論文 参考訳（メタデータ） (2026-08-12T08:14:45Z) - FailForge: Distilling Procedural Competence from Persistent Failures into Code Agents [49.519184792774304]
FailForgeは、失敗したロールアウトをトレーニングシグナルに変換するエージェントフレームワークである。
FailForgeは、これまで失敗したインスタンスの26%を、限界的な追加コストでリカバリする。
論文 参考訳（メタデータ） (2026-08-09T08:22:57Z) - Reflective Recovery: A Self-Supervised Method for Reasoning by Learning from Mistakes [70.64622557376505]
リフレクティブリカバリは、推論中のミスを認識し、修正するようにモデルに教える。
AIME 2025では30.0%から37.5%、Minervaでは37.6%から47.8%に精度が向上している。
論文 参考訳（メタデータ） (2026-07-24T02:51:42Z) - Beyond Fail-to-Pass: Iterative Hardening of Co-Generated Bug Reproduction Tests and Fixes [55.114939648705395]
大規模言語モデル(LLM)は、現実のバグに対して、プログラムの自動修正をますます実用的にしている。
バグ再現テスト(BRT)は、バグレポートを実行可能なバグ固有の信号に変換することで、このギャップを埋めるのに役立つ。
本稿では,ループ内収束基準としてLax信号を用いるコジェネレーションフレームワークであるCoHardenを提案する。
論文 参考訳（メタデータ） (2026-07-22T07:30:07Z) - Code Correctness Signals in LLM Hidden States: Pre-Generation Probing and Repair Geometry [0.0]
モデルのファーストアタプティブコードの正しさは、プロンプト-ファイナル隠れ状態から線形にデオード可能である。
モデルが失敗した最初の試みを修復しようとするケース236では、失敗した試みからその修復への隠れ状態シフトが統計的に検出可能なコントラスト方向をもたらす。
論文 参考訳（メタデータ） (2026-06-12T15:06:15Z) - VIBEPASS: Can Vibe Coders Really Pass the Vibe Check? [46.85901599242161]
emphFault-Triggering Test Generation(FT-Test)とemphFault-targeted Program repair(FPR)の2つの組み合わせタスクを評価した。
故障対象推論は一般的な符号化能力ではスケールしないことがわかった。
自己生成テストが障害の発見に成功すると、結果として得られた修復結果が外部から提供されたテストによってガイドされた修復と一致したり、性能が低下する。
論文 参考訳（メタデータ） (2026-03-16T21:14:28Z) - Learning to Repair Lean Proofs from Compiler Feedback [4.55626337217127]
教師付き学習問題としてリーン証明修復について検討する。
APRIL(Automated Proof repair in Lean)は、260,000の教師付き定理のデータセットである。
我々は、診断条件付き監視を、フィードバックを利用するプローバーのための補完的な訓練信号と見なしている。
論文 参考訳（メタデータ） (2026-02-03T01:53:56Z) - CARE What Fails: Contrastive Anchored-REflection for Verifiable Multimodal [84.71254539482369]
検証可能な報酬を伴うグループ相対的強化学習(RLVR)は、しばしば、すでに失敗している最も情報に富むデータを浪費する。
エラーを監督するマルチモーダル推論のための,障害中心のポストトレーニングフレームワークであるCAREを提案する。
CAREは正確さを改善し、スムーズさをトレーニングすると同時に、障害からの学習信号のシェアを明示的に増やします。
論文 参考訳（メタデータ） (2025-12-22T16:34:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。