論文の概要: Verifier-Grounded Agentic RL for Provably Correct Code

• arxiv url: http://arxiv.org/abs/2610.19298v1
• Date: Tue, 13 Oct 2026 23:17:25 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-15 21:06:15.847876
• Title: Verifier-Grounded Agentic RL for Provably Correct Code
• Title（参考訳）: 確率的誤り訂正のための検証対象エージェントRL
• Abstract要約: 私たちはエージェント環境を構築し、その両方に報酬を与えます。 報酬は、検証者の判断よりも、検証者の診断を読み取って、それが排出する証明義務の重み付けされた部分によって候補を採点する。 整合性監査は検証を上回り、仕様を変更したり、それを証明しようとすると仮定する候補を拒絶する。
• 参考スコア（独自算出の注目度）: 20.989739880402407
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Reinforcement learning for code usually rewards passing tests, which a model can do while remaining wrong on the inputs the tests do not cover. A program verifier instead decides whether a program satisfies a formal specification for all inputs. Language models are almost always paired with verifiers at inference time only, and turning a verifier into a reward raises two difficulties. It reports only acceptance or rejection, which gives no gradient when every attempt fails, and a policy can cheat it, most simply by telling it to assume what the proof was supposed to establish. We build an agentic environment and reward that address both. The reward reads the verifier's diagnostics rather than its verdict, scoring a candidate by the weighted fraction of proof obligations it discharges, extended with hidden probes from a reference proof's annotations. An integrity audit outranks the verifier, rejecting any candidate that alters the specification or assumes what it was meant to prove. The model works as an agent against a live verifier over many turns, with a separately trained proof specialist as a frozen collaborator. Across Qwen3 models from 1.7B to 14B and a 35B Qwen3.6 mixture-of-experts model, held-out verification on code generation rises from 66.1% to 93.5% on DafnyBench and from 56.3% to 100% on SWE-Proof. This reward leads every other training signal we compare, including a binary pass-or-fail reward trained under otherwise identical settings, with the widest margin on code generation. When the agent must also deliver the repository patch, graded by each project's withheld tests, the fraction of held-out issues it resolves rises from 59.6% to 72.5%. Evaluated unchanged on three verification suites withheld from training, the checkpoints improve on all of them, including one whose language and verifier are absent from training.
• Abstract（参考訳）: コードに対する強化学習は、通常、テストの通過に報いる。 プログラム検証者は代わりに、プログラムが全ての入力に対して正式な仕様を満たすかどうかを決定する。 言語モデルはほとんどの場合、推論時にのみ検証器とペアリングされ、検証器を報酬に変換することは2つの困難を引き起こす。 承認または拒絶のみを報告し、すべての試みが失敗しても勾配を示さず、ポリシーは単純に証明が確立すべきことを仮定することでそれを騙すことができる。 私たちはエージェント環境を構築し、その両方に報酬を与えます。 報酬は、検証者の診断を判断ではなく読み、被証明者のアノテーションから隠れたプローブで拡張して、その証明義務の重み付けによって候補を採点する。 整合性監査は検証を上回り、仕様を変更したり、それを証明しようとすると仮定する候補を拒絶する。 このモデルは、凍結した共同作業者として個別に訓練された証明スペシャリストとともに、多数のターンにわたるライブ検証に対するエージェントとして機能する。 Qwen3の1.7Bから14Bまでのモデルと35B Qwen3.6のミックス・オブ・エキスパートモデルでは、コード生成の検証は66.1%から93.5%に増加し、SWE-Proofでは56.3%から100%に増加した。 この報酬は、他のすべてのトレーニングシグナルを導きます。例えば、バイナリパスまたはフェイル報酬は、まったく同じ設定でトレーニングされ、コード生成のマージンが最も大きいのです。 エージェントが各プロジェクトの非保持テストによって評価されたリポジトリパッチも提供しなければならない場合、解決するホールドアウト問題のごく一部は59.6%から72.5%に上昇する。 チェックポイントはトレーニングを受けていない3つの検証スイートで評価されないため、言語と検証者がトレーニングを受けていないものを含め、すべてのチェックポイントが改善される。

関連論文リスト

• Beyond the Verdict: Agentic Code Judging with Verifiable Feedback [54.72977295521153]
  我々は,人間の専門家による受諾プログラムと受諾プログラムを用いて,USACO 2026コンテストからUSACO-JUDGEを構築した。 次に、35Bのエージェント検証器であるARBITERを、汎用的な実行サンドボックスで強化学習して訓練する。 トレーニングは、不正なプログラムを40.61%から62.67%に、二分判定の精度を71.41%から87.41%に引き上げる。
  論文  参考訳（メタデータ） (2026-10-13T17:22:58Z)
• Verifier-Harness Co-Evolution for Training-Free Self-Improvement on Open-Ended Tasks [26.247543441302785]
  Unified Co-Evolution (UCoE) は、エージェントのハーネス状態とともに実行可能な検証プログラムを進化させる訓練不要の手法である。 UCoEは候補検証プログラムを合成し、応答コントラストでテストする。 最弱のコントラスト家族に対する差別が最高である候補者を選別し、これは私たちが運転能力と呼ぶ量である。
  論文  参考訳（メタデータ） (2026-10-13T02:29:40Z)
• Teaching Agents to Code Reliably [12.841316191115778]
  リポジトリの問題を解決するために、自律的なコーディングエージェントを訓練する方法を示す。 トレーニングがこれらの行動を政策にどう移行するかを示す。 パス@1から43.0%に上昇し、パス@8から60.7%に上昇し、検証精度を26.8%から41.7%に引き上げる。
  論文  参考訳（メタデータ） (2026-10-02T19:47:19Z)
• VeriHarness: Scaling Agentic Verification for Long-Horizon Tasks [56.74345405508208]
  LLMエージェントはますます複雑で長期のタスクをこなし、そのアウトプットを検証することがますます困難になっている。 本研究では, 基準応答へのアクセスや試験時の潤滑油の分解を行わずに, 固定ベースモデルで検証能力を強化する方法について検討する。 コンセンサスによってエラーを隠蔽できる一方で、不一致はしばしば正しい代替手段を公開することに気付きました。 これらの観察はVeriHarnessを動機付け、ジェネレータが使用する基礎となるLLMを、ワークスペース、エビデンスツール、再利用可能な検証スキルを与えることによって、エージェント検証器に変える。
  論文  参考訳（メタデータ） (2026-10-01T03:02:17Z)
• ExecCritic: Learn to Test, Test to Improve for Coding Agents [68.42713285082912]
  実行時のフィードバックは、コーディングエージェントを正しいリポジトリの修復に導くことができますが、テストが問題によって要求された振る舞いをキャプチャした場合のみです。 ExecCriticを導入し、テスト-検証-修正足場と、その中のトレーニングエージェントのためのロール固有の強化学習レシピを組み合わせる。 テストエージェントが独立してリポジトリネイティブなテストを生成し、フェイルクローズされたハーネスがそれらを調整して凍結し、リカバリエージェントがテストを変更することなく、ソースコードを実行フィードバックから修正する。
  論文  参考訳（メタデータ） (2026-09-08T17:53:37Z)
• Verification-Aware Training for Speculative Decoding [57.84976863792784]
  VAT(Verification-Aware Training)は、トレーニングステップ毎に検証をシミュレートし、その結果の受け入れパターンと拒否パターンを監督するプラグインフレームワークである。 VATはトレーニング対象のみを変更するため、ドラフトアーキテクチャやターゲットモデル、推論手順を変更することなく、既存のメソッドの上にレイヤー化することができる。 VATは平均受理期間を最大11.4%改善し、ウォールクロックのスピードアップを最大8.7%向上させ、数学、コード、チャットベンチマークで一貫した利益を得ている。
  論文  参考訳（メタデータ） (2026-08-31T01:42:10Z)
• CoVerRL: Breaking the Consensus Trap in Label-Free Reasoning via Generator-Verifier Co-Evolution [52.691495954442985]
  CoVerRLは1つのモデルがジェネレータと検証ロールを交換するフレームワークで、各機能が他方をブートストラップする。 Qwen と Llama のモデルファミリーでの実験では、CoVerRL は数理推論のベンチマークで4.7-5.9% でラベルなしのベースラインを上回っている。 自己検証の精度は55%から85%以上改善され、両方の能力が真に共存することを確認した。
  論文  参考訳（メタデータ） (2026-03-18T14:38:55Z)
• Hybrid Reinforcement: When Reward Is Sparse, It's Better to Be Dense [36.71358559780692]
  HEROは、検証者信号と報酬モデルスコアを構造化された方法で統合する強化学習フレームワークである。 HEROはRMのみのベースラインと検証者のみのベースラインを一貫して上回り、検証可能なタスクと検証しにくいタスクの両方で大きな利益を上げている。
  論文  参考訳（メタデータ） (2025-10-08T17:09:41Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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