論文の概要: Schwarz: Solver-Aware Agentic Program Verification

• arxiv url: http://arxiv.org/abs/2608.30803v1
• Date: Mon, 31 Aug 2026 13:54:48 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-01 18:31:31.426128
• Title: Schwarz: Solver-Aware Agentic Program Verification
• Title（参考訳）: Schwarz: ソリューション対応エージェントプログラム検証
• Abstract要約: Schwarzはエージェントによる検証ハーネスで、SMTが支援する証明の失敗を局所的に、チェック可能で、修復可能である。 我々は、CとRust/Verus用のSchwarzを実装し、1,475のタスクで評価する。
• 参考スコア（独自算出の注目度）: 1.9215527229034466
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Agentic verification systems can often generate source-level specifications that look plausible, but plausibility is not enough: the verifier must still turn those specifications into SMT obligations that the solver can prove. When this step fails, current LLM-driven loops usually expose only a coarse verifier error, timeout, or unknown solver result. The model cannot tell whether the specification is wrong, a helper lemma is missing, the proof context contains irrelevant facts, or the obligation needs a different theory view. This paper presents Schwarz, an agentic verification harness that makes SMT-backed proof failure local, checkable, and repairable. Schwarz turns failed verification into obligation-local repair tasks: program-point snapshots expose checked facts at a boundary, local lemmas let the agent propose missing proof steps, and theory-aware solver policies guide the agent toward solver-friendly formulations for numeric, quantified, memory, and floating-point obligations. We implement Schwarz for C and Rust/Verus and evaluate it on 1,475 tasks. On 475 benchmarks from recent agentic verification tools, Schwarz solves 95.2% of the tasks. On 1,000 tasks from the SV-COMP 2026 ReachSafety track, averaging 1,427 LOC, Schwarz solves 91.5% of the tasks, compared with 60.1% for CPAchecker. Ablations and comparison with a pure-agent baseline show that solver-aware repair is effective and scalable.
• Abstract（参考訳）: エージェント検証システムは、しばしば妥当に見えるソースレベルの仕様を生成することができるが、妥当性は十分ではない:検証者は、これらの仕様を解決者が証明できるSMT義務に変換する必要がある。 このステップが失敗すると、現在のLCM駆動ループは通常、粗い検証エラー、タイムアウト、未知の解決結果のみを公開する。 モデルは、仕様が間違っているか、ヘルパー補題が欠けているか、証明コンテキストが無関係な事実を含んでいるか、義務が異なる理論ビューを必要とするかを知ることができない。 本稿では,SMTが支援する証明失敗を局所的に,チェック可能で,修復可能なエージェント検証ハーネスであるSchwarzについて述べる。 プログラムポイントのスナップショットは境界でチェックされた事実を露出し、ローカルの補題はエージェントに欠落した証明ステップを提案させ、理論を意識したソルバポリシーは、数値、定量化、メモリ、浮動小数点義務の解決者フレンドリな定式化に向けてエージェントを導く。 我々は、CとRust/Verus用のSchwarzを実装し、1,475のタスクで評価する。 最近のエージェント検証ツールによる475のベンチマークで、Schwarzは95.2%のタスクを解決した。 SV-COMP 2026 ReachSafetyのトラックで平均1,427LOCの1000タスクに対して、シュワルツはCPAチェッカーの60.1%に比べて91.5%のタスクを解決した。 純エージェントベースラインに対するアブレーションと比較は、ソルバ対応の修復が効果的でスケーラブルであることを示している。

関連論文リスト

• CalibForge: Adversarial Solver Calibration for Scaling Learnable Terminal Tasks [87.1086886770395]
  CalibForgeは、自律型ターミナルタスク合成システムである。 検証されたソルバの挙動を用いて、逆ソルバの校正によって候補タスクを修正する。 CalibForgeを使って5,431の端末タスクを構築します。
  論文  参考訳（メタデータ） (2026-08-06T17:53:18Z)
• How Agent Skills Fail under Long Contexts: A White-Box Study in Code Auditing [1.5217170480235822]
  Agent Skillsパッケージ 手続き的な指示と汎用エージェントの使用のためのチェック。 そこで本研究では,本問題を製品由来のホワイトボックスコード監査ワークフローを用いて検討する。 要求の欠如、ドリフトの編集、チェックの失敗、非エージェント評価/実行時の障害などです。
  論文  参考訳（メタデータ） (2026-07-20T13:34:53Z)
• The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK [0.0]
  検証者主導のループにおいて、AIエージェントは古典的および後量子暗号、TLS 1.3、IKEv2、X.509、マトリックスクライアントにまたがるAda/SPARKのベアメタルセキュリティソフトウェアを書いて検証した。 GNATproveは49,280の証明義務を解除し、選択されたプリミティブに対して機能的正当性を確立し、残りのプリミティブに対して実行時のエラーがないことを証明した。 それぞれのレイヤが障害をキャッチし,中心的な教訓を引き出す方法を報告します。エージェントが確立するために信頼できるものは,そのフィードバックの強さに縛られているのです。
  論文  参考訳（メタデータ） (2026-07-15T20:09:05Z)
• Auditing Reward Hackability in Code RL Training Environments [0.0]
  コードRL環境が誤った解を正しく受け入れる速度を計測する。 SWE-bench Verifiedの49タクのサンプルでは、28.5%のタスクがテストスイートが弱く、Dockerで検証された不正確なパッチがそれらをパスしている。
  論文  参考訳（メタデータ） (2026-06-14T23:31:42Z)
• What to Test Next: Interpretable Coverage Gap Discovery in Driving VLMs [52.50210189669399]
  視覚言語モデル(VLM)を駆動するには,操作設計領域(ODD)が定義する様々な条件のシーンを正確に理解する必要がある SliceScorerは、欠落したスライス推薦のための決定論的スコアリングルールである。 SliceNavは, 従来のスライス発見法よりも, 高リスクカバレッジギャップを効果的に表面化することを示す。
  論文  参考訳（メタデータ） (2026-06-01T03:18:01Z)
• Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization [26.123396123145415]
  LLMエージェントが非公式なプログラミング問題を忠実な形式仕様に変換することができるかどうか、仕様自動書式化について検討する。 Codeforces問題から派生した581の仕様記述タスクのベンチマークであるVerus-SpecBenchを紹介する。 フェールモードの解析は、モデル生成仕様が重要な入力仮定を受け入れ、誤った出力を受け入れ、有効な仕様を拒否できることを示している。
  論文  参考訳（メタデータ） (2026-05-26T02:12:48Z)
• Hallucination as Exploit: Evidence-Carrying Multimodal Agents [10.441697487723568]
  マルチモーダルエージェントはますます、スクリーンショットやドキュメント、Webページからツールコールを選択している。 本稿では,自由形式モデルテキストを不許容な証拠として扱うエビデンス搬送型マルチモーダルエージェント(ECA)を提案する。 ECAは不透明なモデルの信念を検証者、スキーマ、実装レベルで監査可能な残留物に変換する。
  論文  参考訳（メタデータ） (2026-05-18T23:40:43Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• LLM Readiness Harness: Evaluation, Observability, and CI Gates for LLM/RAG Applications [51.56484100374058]
  評価をデプロイメント決定ワークフローに変換するLLMおよびRAGアプリケーションのための準備性ハーネスを提案する。 このシステムは、最小限のAPI契約の下で、自動ベンチマーク、OpenTelemetryオブザーバビリティ、CI品質ゲートを組み合わせる。 チケットルーティングとBEIRタスクのハーネスを、完全なAzureマトリックスカバレッジで評価する。
  論文  参考訳（メタデータ） (2026-03-28T18:03:32Z)
• DoVer: Intervention-Driven Auto Debugging for LLM Multi-Agent Systems [48.971606069204825]
  DoVerは、大規模言語モデル(LLM)ベースのマルチエージェントシステムのための介入駆動デバッグフレームワークである。 ターゲットの介入を通じて、アクティブな検証によって仮説生成を増強する。 DoVerは失敗試験の18～28%を成功させ、最大16%のマイルストーンを達成し、失敗仮説の30～60%を検証または否定する。
  論文  参考訳（メタデータ） (2025-12-07T09:23:48Z)
• 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)

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

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