論文の概要: From Verification Failures to Reusable Guidance for Coding Agents

• arxiv url: http://arxiv.org/abs/2609.39022v2
• Date: Thu, 01 Oct 2026 02:57:08 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-03 01:19:23.549311
• Title: From Verification Failures to Reusable Guidance for Coding Agents
• Title（参考訳）: 符号化エージェントの検証失敗から再利用誘導へ
• Abstract要約: コーディングエージェントは、プログラムが仕様を満たすことと、仕様が要求された振る舞いをキャプチャすることを確立する必要がある。 本研究は,検証失敗の専門診断が再利用可能なガイダンスとなる方法について検討する。 ヒューマンガイド開発キャンペーンは、セマンティクスとキットで164/164の成功率を達成する。
• 参考スコア（独自算出の注目度）: 10.7243245192525
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Coding agents need to establish that a program satisfies a specification and that the specification captures the requested behavior. We study how expert diagnosis of verification failures can become reusable guidance for this work. Our approach combines executable language definitions in the K framework with a kit of procedures for constructing specifications, repairing proofs, and auditing their adequacy. A human-guided development campaign on HumanEval, a benchmark of 164 Python programming tasks, achieves a 164/164 success rate with the semantics and the kit, measured by final AI audit Pass verdicts after two targeted repairs. To examine whether auditing detects problems that successful proofs leave unresolved, we construct 12 author-reviewed pairs of clean and defective packages. Every package passes its K proofs, and completed audits identify all defects and accept all clean packages. We then use KleverBench to test specification and proof construction for 31 programs with changed operator meanings. Comparisons with complete acceptance rules and equally long generic advice yield mixed results across two model and budget settings, motivating further work on selecting useful guidance within resource limits. Human-reviewed Optimism proofs establish expected pause reverts for six operations within declared input bounds under London semantics with unbounded gas. We report progress, difficulties, and lessons toward agents that deliver programs with checkable correctness arguments.
• Abstract（参考訳）: コーディングエージェントは、プログラムが仕様を満たすことと、仕様が要求された振る舞いをキャプチャすることを確立する必要がある。 本研究は,検証失敗の専門診断が再利用可能なガイダンスとなる方法について検討する。 提案手法は,Kフレームワークの実行可能な言語定義と,仕様の作成,証明の修復,妥当性の監査を行う一連の手順を組み合わせる。 164のPythonプログラミングタスクのベンチマークであるHumanEvalに関するヒューマンガイド開発キャンペーンは、セマンティクスとキットで164/164の成功率を達成した。 オーディションが証明が未解決のままである問題を検出するかどうかを調べるため,著者レビューによる12組のクリーンパッケージと欠陥パッケージを構築した。 各パッケージはK証明をパスし、完了した監査はすべての欠陥を特定し、すべてのクリーンパッケージを受け入れる。 次に、KleverBenchを使用して、変更された演算子の意味を持つ31のプログラムの仕様と証明を行う。 完全な受け入れルールと同等に長いジェネリックアドバイスとの比較は、2つのモデルと予算設定に混ざった結果をもたらし、リソース制限内で有用なガイダンスを選択するためのさらなる取り組みを動機付けます。 人間のレビューによるオプティミズムの証明は、ロンドンのセマンティクスの下で宣言された入力境界内での6つの操作の停止反転を未境界ガスで証明する。 我々は、チェック可能な正当性引数を持つプログラムを提供するエージェントに対する進歩、困難、教訓を報告する。

関連論文リスト

• SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs? [39.004582663385364]
  Benchprooferは、既知の正しいパッチでコーディングタスクを正式に認証されたパイプラインに変換するパイプラインです。 SWE-bench Verified に適用すると SWE-Proof が得られる。
  論文  参考訳（メタデータ） (2026-09-18T01:16:53Z)
• Task-CoEvolve: Efficient Harness Optimization via Adaptive Validation Task Selection [51.39973047614183]
  本稿では,適応型検証タスク選択によるLLMの効率向上のための新しい手法を提案する。 $textbfTask-CoEvolve$.textbfTask-CoEvolve$.textbfTask-CoEvolve$.textbfTaskは、情報的タスクの選択と、部分的な評価からフルセットのパフォーマンスの推定という2つの課題に対処することで、ハーネスでバリデーションタスクを共進化させる。
  論文  参考訳（メタデータ） (2026-08-20T15:24:54Z)
• SpecPath: Testing Coding Agents Across Contract-Equivalent Specification Histories [13.437222222971272]
  仕様パスの感度は、最終的な意味において等価な要求履歴が同一のエージェントシステムに振る舞いの異なるプログラムを作成させる障害モードである。 本稿では,契約に至るリビジョンパスのみを変更しつつ,リポジトリ,最終契約,検証,エージェントシステム,実行予算を保持する診断評価であるSpecPathを紹介する。
  論文  参考訳（メタデータ） (2026-08-10T16:19:00Z)
• Fantastic Adaptive Taxonomies and How to Use Them [100.20614173157708]
  AdaMASTは、実行トレースをコンパクトでエビデンスに基づく障害分類に変換する。 コードには手書きのコードはなく、人間による注釈もない。 エージェント・システム・サーチでは、失敗候補の分類コード診断が自由形式より優れている。
  論文  参考訳（メタデータ） (2026-07-17T17:41:16Z)
• Teaching Code LLMs to Reason with Intermediate Formal Specifications [9.552020178028576]
  SpecCoderは、検証済みの参照プログラム、振る舞いを変えるミュータント、マルチターン仕様修正トレースから学ぶトレーニングフレームワークである。 SpecCoderは、欠陥のある実行を拒否しながら正しい実行を保持する仕様を選択し、受動的アノテーションから実行可能なエビデンスに変換する。
  論文  参考訳（メタデータ） (2026-07-05T11:09:30Z)
• What to Test Next: Interpretable Coverage Gap Discovery in Driving VLMs [52.50210189669399]
  視覚言語モデル(VLM)を駆動するには,操作設計領域(ODD)が定義する様々な条件のシーンを正確に理解する必要がある SliceScorerは、欠落したスライス推薦のための決定論的スコアリングルールである。 SliceNavは, 従来のスライス発見法よりも, 高リスクカバレッジギャップを効果的に表面化することを示す。
  論文  参考訳（メタデータ） (2026-06-01T03:18:01Z)
• Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols [1.5229705287183657]
  SPECAは、明示的で分類されたセキュリティプロパティを自然言語仕様から導き出し、実装間で再利用する監査フレームワークである。 RepoAuditのベンチマークでは、SPECAは100%リコール(F1=0.94)で88.9%の精度に達し、著者が検証した12のバグを地上の真実を超えて表面化している。 Sherlock Fusaka Audit Contest(10のターゲット、366の応募)では、SPECAが専門家が強化した15の脆弱性をすべて回復し、4つの修正確認バグが浮上した。
  論文  参考訳（メタデータ） (2026-04-29T09:57:07Z)
• SlopCodeBench: Benchmarking How Coding Agents Degrade Over Long-Horizon Iterative Tasks [55.76734816061826]
  我々は20の問題と93のチェックポイントからなる言語に依存しないベンチマークであるSlopCodeBenchを紹介する。 我々は、冗長性、重複コードの割合、構造的侵食という2つの軌道レベルの品質信号を追跡する。 11モデルにまたがるエンドツーエンドの問題を解決するエージェントは存在しない。
  論文  参考訳（メタデータ） (2026-03-25T19:26:44Z)

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

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