論文の概要: When Correctness Feedback Erases Evidence: Phase-Separated Completeness Auditing in Verus
- arxiv url: http://arxiv.org/abs/2610.20676v1
- Date: Wed, 14 Oct 2026 14:43:24 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-16 19:13:15.977535
- Title: When Correctness Feedback Erases Evidence: Phase-Separated Completeness Auditing in Verus
- Title(参考訳): 正当性フィードバックが証拠を消去する時--動詞における相分離完全性監査
- Abstract要約: 正当性フィードバックは、仕様完全性監査が明らかになるように設計されていることを示す。
提案手法は、4つのモデルファミリーを対象とした12のVerus/Rustタスクにおいて、一致したコール予算の下で、この目的を逆転させるものである。
- 参考スコア(独自算出の注目度): 0.12062777974093623
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Correctness feedback suppresses the very evidence that specification-completeness auditing is designed to uncover: programs that satisfy a written contract but violate intended behavior. We demonstrate this objective reversal on 12 Verus/Rust tasks across four model families under matched call budgets. Independent no-feedback discovery more than doubles certified-witness yield relative to IntentShield's corrective-feedback loop (59.0% versus 27.1%). A format-matched iterative control places the larger share of this gap in feedback content, not independent restarts. The advantage holds in every model family and survives parser repair. A separate phase-separated execution matches the aggregate yield without reusing responses; most certified witnesses also fail held-out cases. Preserving these witnesses delivers stronger specification repair: Phase-Revised contracts achieve 81.3% implementation success, versus 62.5% for IS-Revised, with Direct-Revised close behind. Both no-feedback witness sources substantially outperform weakened contracts. The effect does not reproduce in the available Dafny and Lean evaluations, establishing an empirical boundary around the studied Verus/Rust workflow. Completeness auditing and correctness repair have opposing immediate objectives. Preserve and certify the admitted failure before repairing it.
- Abstract(参考訳): 正確性フィードバックは、仕様完全性監査が、記述された契約を満たすが意図された振る舞いに反するプログラムを明らかにするように設計されているという、まさに証拠を抑圧する。
提案手法は、4つのモデルファミリーを対象とした12のVerus/Rustタスクにおいて、一致したコール予算の下で、この目的を逆転させるものである。
IntentShieldの修正フィードバックループ(59.0%対27.1%)と比較すると、独立なノンフィードバック発見は認定ウィットネスの利得を倍増させる。
フォーマットマッチングされた反復制御は、このギャップの大部分を独立した再起動ではなく、フィードバックコンテンツに配置する。
アドバンテージは、すべてのモデルファミリに存在し、パーサの修復を生き残る。
異なるフェーズ分離された実行は、レスポンスを再利用せずに総収率と一致します。
フェーズ修正契約は81.3%、IS修正契約は62.5%、ダイレクト修正契約は62.5%である。
双方の証人情報筋は、契約の弱さを大きく上回った。
この効果は、利用可能なDafnyとLeanの評価では再現されず、調査されたVerus/Rustワークフローの周りに実証的な境界を確立する。
完全性監査と正当性修復は即時目的に反するものである。
修復する前に、確認された失敗を保存し、認定する。
関連論文リスト
- ClaimScope: Label-Blind Witness Verification for Mathematical Claim Auditing [2.0474890225194193]
ClaimScopeは、検証、スコープ、反例、修復を通じて提案されたクレームを監査するための72タスクのベンチマークである。
証人チェッカーはモデルが提出した状態のみを評価する。
検証対象のフィードバックは、無効なクレームに対する23ドル/39ドル、セーフコンプリートに対する25ドル/72ドル、チェッカーフリーのジェネリックフィードバックに対する15ドル/39ドルと20ドル/72ドルである。
論文 参考訳(メタデータ) (2026-10-15T09:29:02Z) - Are We Measuring Anticipation? Auditing Privileged Information in Procedural Video Evaluation [0.0]
予測モデルのみでなく,評価プロトコルによってライセンスされた推論を監査する。
プロトコルは、特権のある中間表現を供給しながら、時間的に因果関係を保つことができる。
論文 参考訳(メタデータ) (2026-10-02T09:13:22Z) - Right Answers, Wrong States: Hidden Information Failures in Multi-Agent Collaboration [69.14904049421806]
共同作業は、即時決定が正しい場合でも、腐敗した情報状態に置き去りにすることができる。
GPT、Gemini、Qwenモデル全体では、標準的なコラボレーションは、状態の信頼性よりもはるかに強力なタスクパフォーマンスを示している。
我々は、矛盾する証拠を解決し、共有された事実を検証し、信頼された国家を再構築するReGroundを紹介します。
論文 参考訳(メタデータ) (2026-10-01T07:42:27Z) - VeriHarness: Scaling Agentic Verification for Long-Horizon Tasks [56.74345405508208]
LLMエージェントはますます複雑で長期のタスクをこなし、そのアウトプットを検証することがますます困難になっている。
本研究では, 基準応答へのアクセスや試験時の潤滑油の分解を行わずに, 固定ベースモデルで検証能力を強化する方法について検討する。
コンセンサスによってエラーを隠蔽できる一方で、不一致はしばしば正しい代替手段を公開することに気付きました。
これらの観察はVeriHarnessを動機付け、ジェネレータが使用する基礎となるLLMを、ワークスペース、エビデンスツール、再利用可能な検証スキルを与えることによって、エージェント検証器に変える。
論文 参考訳(メタデータ) (2026-10-01T03:02:17Z) - Exact Feedback Is Not Control: Evaluating Text-based Closed-Loop Revision in LLMs [11.49266427505128]
本稿では, 正確な長さ, 語彙, 構成制約にまたがるすべての違反を, 決定論的検証を行う固定予算修正プロトコルを提案する。
フィードバックの正しさと完全さの修正はモデル側のリビジョン動作を分離する。
一致した状態の介入は、最終的な成功を確実に改善することなく、現在のドラフトを保持しながら以前の対話を削除し、フィードバックが変更を修正したことを示している。
論文 参考訳(メタデータ) (2026-09-23T14:06:52Z) - TwinCheck: Evidence-Grounded Negative-Twin Verification for Stateful Tool Agents [1.1279808969568255]
TwinCheckは、トレースがトレースローカル障害仮説に結びついている証拠条件を満たす場合にのみ、置換を検討するポリシーである。
ペア評価の場合、正確なリプレイはエージェントのパースされた応答とアクションを保持し、最初の置換が受け入れられるまで固定される。
論文 参考訳(メタデータ) (2026-09-22T18:09:40Z) - Looping Is Not Reliability: State-Bound Evidence and Typed Revision Contracts for Agentic Code Repair [36.56438114281786]
正しいパッチの発見と保持、検証、提出のギャップについて検討する。
我々はエビデンスバウンド型ループ契約を導出し、その機械的に強制可能なサブセットを参照実装でインスタンス化する。
論文 参考訳(メタデータ) (2026-07-27T16:05:23Z) - HLE-Verified: A Systematic Verification and Structured Revision of Humanity's Last Exam [63.84155758655084]
HumanityのLast Exam (HLE)は、フロンティアの大規模言語モデルを評価するために広く使われているベンチマークである。
HLE-Verifiedは,透過的検証プロトコルときめ細かい誤り分類法を備えたHLEの検証および改訂版である。
我々は,HLEとHLE-Verifiedの7つの最先端言語モデルを評価し,平均7~10ポイントの絶対精度を観測した。
論文 参考訳(メタデータ) (2026-02-15T02:50:15Z) - Illusions of Confidence? Diagnosing LLM Truthfulness via Neighborhood Consistency [78.91846841708586]
完全な自己整合性で答えられた事実でさえ、軽微な文脈干渉の下で急速に崩壊することを示します。
本研究では,概念的近傍における応答コヒーレンスを評価する信念の構造尺度であるNighbor-Consistency Belief(NCB)を提案する。
また、文脈不変の信念構造を最適化し、長い知識の脆さを約30%低減する構造意識訓練(SAT)を提案する。
論文 参考訳(メタデータ) (2026-01-09T16:23:21Z) - CARE What Fails: Contrastive Anchored-REflection for Verifiable Multimodal [84.71254539482369]
検証可能な報酬を伴うグループ相対的強化学習(RLVR)は、しばしば、すでに失敗している最も情報に富むデータを浪費する。
エラーを監督するマルチモーダル推論のための,障害中心のポストトレーニングフレームワークであるCAREを提案する。
CAREは正確さを改善し、スムーズさをトレーニングすると同時に、障害からの学習信号のシェアを明示的に増やします。
論文 参考訳(メタデータ) (2025-12-22T16:34:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。