論文の概要: Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification
- arxiv url: http://arxiv.org/abs/2607.10291v1
- Date: Sat, 11 Jul 2026 12:40:22 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-14 15:40:48.383943
- Title: Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification
- Title（参考訳）: 部分契約で十分:音, LLMによる回帰検証
- Abstract要約: 本稿では,契約に基づく回帰検証ツールについて紹介する。
契約の健全性は、すべての関数バージョンが振舞いと一致することを証明することによって保証される。
完全な振る舞い仕様ではなく、部分的かつ呼び出し側対応の契約で十分かどうかを問う。
- 参考スコア（独自算出の注目度）: 7.004725450780227
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Software evolves continuously, yet ensuring that a patch preserves intended behavior without re-verifying an entire codebase remains difficult. Regression verification addresses this problem, but existing techniques require expensive whole-program reasoning or rely on manually written specifications that are rarely available in practice. We present the first contract-based regression verification tool. Contract soundness is ensured by proving all function versions match the behavior. The contract then verifies program flow via assume-guarantee. We ask whether a partial, caller-sufficient contract, rather than a full behavioral specification, is enough. On Frama-C-Problems we strengthen each inferred contract past what the caller needs and measure how much tighter it becomes. It barely moves: for most targets in every model the caller-sufficient contract is already the tightest the loop reaches, and our tightness comparator rates the partial and strengthened contracts equivalent for the large majority of targets it can compare. Partial-spec contracts thus capture nearly all the attainable tightness, so stopping at caller-sufficiency costs almost nothing. The regression check underneath is sound: on the third-party EqBench-C suite it never fabricates an equivalence, returning zero false proofs and reporting an unprovable difference instead. It also surfaced nine pairs that EqBench mislabels as equivalent, more than a concurrent tool reports. The contracts themselves are inferred automatically from the checker's own counterexamples, with no separate specification step; on Frama-C-Problems and the ANSSI X509 parser this reaches a verification rate comparable to tools AutoSpec and Preguss, while a passing result certifies at least as strong a property, which we call \emph{safety-preserving conditional equivalence}: enforcement plus caller-sufficiency.
- Abstract（参考訳）: ソフトウェアは継続的に進化するが、コードベース全体を再検証することなく、パッチが意図した動作を保存することを保証する。
回帰検証はこの問題に対処するが、既存の手法では、高価なプログラム全体の推論を必要とするか、手書きの仕様に頼っている。
本稿では,契約に基づく回帰検証ツールについて紹介する。
契約の健全性は、すべての関数バージョンが振舞いと一致することを証明することによって保証される。
契約は、仮定保証者を通じてプログラムフローを検証する。
完全な振る舞い仕様ではなく、部分的かつ呼び出し側対応の契約で十分かどうかを問う。
Frama-C-Problemでは、各推論された契約を呼び出し側が必要とするものを超えて強化し、それがどれだけ厳格になるかを測定します。
すべてのモデルにおいて、呼び出し側で十分である契約は、ループが到達する最も厳密であり、我々の厳密性比較器は、それが比較できるほとんどのターゲットに匹敵する部分的および強化された契約を評価します。
したがって、部分的な契約は達成可能な厳密さのほぼ全てを捉えているため、呼び出し側で停止することはほとんど何の費用もかからない。
サードパーティのEqBench-Cスイートでは、同値を生成せず、偽証明をゼロとし、代わりに証明不可能な差を報告している。
また、EqBenchが同等と誤記している9組のツールレポートが同時に報告されている。
Frama-C-Problems と ANSSI X509 パーサでは、これは AutoSpec や Preguss に匹敵する検証率に達します。
関連論文リスト
- Dead text or binding clause? Measuring and restoring constraint influence in black-box LLM dialogues [0.0]
マルチターンダイアログは、ユーザが制約を課すのと同じくらい簡単に取り消すことができるが、取り消しが確実に効果を発揮できない。
既存の手段では、条項ごとにこの影響を測定したり、納品前に予測したり、整合した予算の下で修復したりすることはない。
sysnameはモデルAPIだけで3つのギャップを埋める。
論文 参考訳（メタデータ） (2026-08-12T21:12:32Z) - What Can Verifiable Decapsulation Tests Certify? Pass Bounds and Fault-Recognition Limits for FO-Based KEMs [0.0]
藤崎・岡本脱カプセル化のブラックボックス試験では, ハーネスが観察した検体を観察した。
本報告では, 信頼度向上型KEM変種について, 誠実な参照手法を用いて検討する。
論文 参考訳（メタデータ） (2026-06-03T04:46:17Z) - Scaling Laws for Agent Harnesses via Effective Feedback Compute [53.68149869349268]
emphEffective Feedback Compute (EFC)は、情報的、有効、非冗長な場合にのみフィードバックを信用し、その後の決定のために保持するトレースレベルのスケーリング座標である。
EFCベースの座標は、生の計算ベースラインよりも失敗率を常に予測する。
論文 参考訳（メタデータ） (2026-05-28T09:45:47Z) - RubricRefine: Improving Tool-Use Agent Reliability with Training-Free Pre-Execution Refinement [0.36165327398913766]
反復自己複製は、推論時の信頼性技術として人気がある。
しかし、コードモードツールの使用効率はフィードバック信号の構造に大きく依存する。
本稿では,事前実行型セマンティックコントラクト検証のためのトレーニング不要な手法Refineを紹介する。
論文 参考訳（メタデータ） (2026-05-10T19:57:32Z) - Kernel Contracts: A Specification Language for ML Kernel Correctness Across Heterogeneous Silicon [0.0]
MLカーネルは、その計算に関する暗黙の契約で出荷される。
最近の実証研究はシリコンプラットフォーム間のギャップを測定しているが、いずれも契約に違反していることを明記していない。
カーネル契約のための仕様言語を提案する。
論文 参考訳（メタデータ） (2026-04-23T19:46:52Z) - IMPACT-CYCLE: A Contract-Based Multi-Agent System for Claim-Level Supervisory Correction of Long-Video Semantic Memory [73.22944697933603]
既存のパイプラインは不透明でエンドツーエンドの出力を生成し、検査の中間状態は公開しない。
IMPACT-Cycleは,マルチモーダル反復クレームレベルのメンテナンスとして,長時間ビデオ理解を再構築するマルチエージェントシステムである。
論文 参考訳（メタデータ） (2026-04-22T03:03:33Z) - Correction and Corruption: A Two-Rate View of Error Flow in LLM Protocols [51.56484100374058]
そこで本研究では,単一プロトコルステップを正確なマッチングタスクで監査するためのペアアウトカム計測インタフェースを提案する。
各インスタンスについて、インターフェースはベースラインの正当性ビットと後ステップの正当性ビットを記録する。
これらのレートは精度の変化を予測し、種、混合物、パイプライン間でテスト可能な再利用可能な経験的インターフェースを定義する。
論文 参考訳（メタデータ） (2026-04-20T13:25:40Z) - AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
既存のベンチマークでは、個々の言語/ツールのみをテストするため、パフォーマンス番号は直接比較できない。
このギャップに対処するAlgoVeriは、Dafny、Verus、Leanで77ドルの古典的アルゴリズムのベリコーディングを評価するベンチマークです。
論文 参考訳（メタデータ） (2026-02-10T06:58:26Z) - SABER: Small Actions, Big Errors -- Safeguarding Mutating Steps in LLM Agents [52.20768003832476]
我々は$$-Bench (Airline/Retail) および SWE-Bench Verified 上での実行トレースを分析する。
成功を失敗に戻すための、先進的な逸脱、最初期の行動、レベル分岐を形式化する。
モデルに依存しない,勾配のない,テスト時のセーフガードである cm を導入します。
論文 参考訳（メタデータ） (2025-11-26T01:28:22Z) - Do Large Language Models Respect Contracts? Evaluating and Enforcing Contract-Adherence in Code Generation [11.445615378917578]
PACTは、プログラムアセスメントおよび契約順応評価フレームワークである。
契約違反に焦点を当てた包括的なテストスーツコーパスを提供する。
様々なプロンプト条件下でのコード生成の体系的解析を可能にする。
論文 参考訳（メタデータ） (2025-10-14T01:12:37Z) - SolBench: A Dataset and Benchmark for Evaluating Functional Correctness in Solidity Code Completion and Repair [51.0686873716938]
コード補完モデルによって生成されたSolidityスマートコントラクトの機能的正しさを評価するベンチマークであるSolBenchを紹介する。
本稿では,スマートコントラクトの機能的正当性を検証するための検索拡張コード修復フレームワークを提案する。
その結果、コード修復と検索技術は、計算コストを削減しつつ、スマートコントラクト完了の正しさを効果的に向上することを示した。
論文 参考訳（メタデータ） (2025-03-03T01:55:20Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。