論文の概要: SpecGuard: Proving a Task Is Broken Before the Agent Cheats
- arxiv url: http://arxiv.org/abs/2610.09159v1
- Date: Tue, 06 Oct 2026 22:00:49 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-08 21:58:22.628745
- Title: SpecGuard: Proving a Task Is Broken Before the Agent Cheats
- Title（参考訳）: SpecGuard:エージェントのチートの前にタスクが壊れていることを証明する
- Abstract要約: タスク意図とテスト間の競合を検出し,正式に認証するSpecGuardを提案する。
コンフリクトされたSWEベンチタスクでは、SpecGuardは72.8%のコンフリクトを検出し、51.1%まで認定する。
- 参考スコア（独自算出の注目度）: 5.911617844519333
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: As autonomous coding agents get increasingly deployed, the risk that accidental or adversarially injected misspecifications in tasks lead to dangerous agent behavior is critical to address. Prior work has shown that agents given such tasks rarely flag the conflict and instead cheat, editing tests or hard-coding expected outputs, and the actions taken to cheat can cause real damage, such as deleting a security defense to make a corrupted test pass. It remains unclear whether such conflicts can be established with independently verifiable evidence before the agent acts. We present SpecGuard, which detects and formally certifies these conflicts between task intent and tests. Given only the task description and codebase, SpecGuard autoformalizes the intended behaviour into a Lean 4 specification. The tests are formalized independently, and the Lean kernel checks whether any implementation could satisfy both formalizations, producing a machine-checked certificate when none can. On conflicted SWE-bench tasks, SpecGuard detects up to 72.8% of conflicts and formally certifies up to 51.1%, with a nearly five-fold lower conflict miss rate than model-based judgment. SpecGuard provides a pre-execution safety check that identifies reward-hacking opportunities through formal certification of task-level conflicts, before any agent behavior is observed. Our code is available at https://github.com/prmbiy/specguard.
- Abstract（参考訳）: 自律的なコーディングエージェントがますます配備されるにつれて、偶然あるいは逆行的にタスクに誤特定を注入するリスクは、危険なエージェントの行動を引き起こす。
以前の研究によると、そのようなタスクを与えられたエージェントは、紛争にフラグを付けることは滅多になく、代わりに、テストの編集や、期待される出力のハードコーディングを行う。
エージェントが行動する前に、独立して検証可能な証拠でそのような紛争が成立できるかどうかは不明である。
タスク意図とテスト間の衝突を検出し、正式に認定するSpecGuardを提案する。
タスク記述とコードベースのみを前提として、SpecGuardは意図した振る舞いをLean 4仕様に自動変換する。
テストは独立して形式化され、Leanカーネルは、すべての実装が両方の形式化を満足できるかどうかをチェックし、不可能な時にマシンチェックされた証明書を生成する。
コンフリクトされたSWEベンチタスクでは、SpecGuardは72.8%のコンフリクトを検出し、51.1%まで認定する。
SpecGuardは、エージェントの動作が観察される前に、タスクレベルのコンフリクトの正式な認証を通じて報酬ハックの機会を特定する、事前実行安全チェックを提供する。
私たちのコードはhttps://github.com/prmbiy/specguard.comから入手可能です。
関連論文リスト
- MobileCybench: Evaluating Agent Vulnerability Discovery via Executable Probes [79.56668124357292]
本稿では,プローブを用いた脆弱性レポート評価フレームワークを提案する。
報告されたエクスプロイトは、アプリケーションに対してそれを再生し、プローブを実行することで評価される。
プローブが既知の脆弱性ではなくセキュリティプロパティをエンコードしているため、プローブがいつ書かれたか分からない脆弱性を検出することができる。
論文 参考訳（メタデータ） (2026-09-21T01:21:06Z) - ClashBench: Conflicts Leading Agents to Seize and Harm [90.19875881996693]
エージェントシステムでは、複数のエージェントセッションが、同じ環境で既存のユーザタスクと並行して実行されるようになっている。
十分な特権が与えられると、エージェントはそれを報告するのではなく、既存のタスクを終了または中断することでリソースの衝突を解決することができる。
この作業は、破壊的なリソースプリエンプションと呼ばれるこの障害モードを特定し、形式化します。
論文 参考訳（メタデータ） (2026-09-17T08:38:27Z) - AgentGuard: Learning Execution Guardrails from Anomalous Coding-Agent Trajectories [7.433745310331784]
本稿では,コーディングエージェントの異常な軌跡から条件付き実行制約を学習する,命令レベルのガードレールフレームワークであるAgentGuardを提案する。
AgentGuardは、繰り返し実行される障害パターンを自動的に抽出し、それらを命令レベルの動作制約に一般化し、軽量なガードレールスキルとして整理する。
AgentGuardは、異常実行率を69.0%から26.7%に下げ、正常タスク完了率を21.7%から35.0%に引き上げている。
論文 参考訳（メタデータ） (2026-09-14T19:42:03Z) - The Troy Moment of AI: Why Some Will Cheat and Some Will Follow? [0.0]
エージェントは停止するか、エスカレートするか、他のエージェントの行動が決定を変えるか、という2つの質問を調査する。
GPT-5.6 Sol, Claude Fable 5.1, Gemini 3.8 Flashの7つのImpossibleBenchタスクを単独で3エージェント設定で検討した。
この結果から,ルールの保護を目的としたあいまいさ,明示的な認証境界のモチベーション,認証状態の証明,エージェント間監視から境界交差が生じる可能性が示唆された。
論文 参考訳（メタデータ） (2026-09-14T12:46:45Z) - ExecCritic: Learn to Test, Test to Improve for Coding Agents [68.42713285082912]
実行時のフィードバックは、コーディングエージェントを正しいリポジトリの修復に導くことができますが、テストが問題によって要求された振る舞いをキャプチャした場合のみです。
ExecCriticを導入し、テスト-検証-修正足場と、その中のトレーニングエージェントのためのロール固有の強化学習レシピを組み合わせる。
テストエージェントが独立してリポジトリネイティブなテストを生成し、フェイルクローズされたハーネスがそれらを調整して凍結し、リカバリエージェントがテストを変更することなく、ソースコードを実行フィードバックから修正する。
論文 参考訳（メタデータ） (2026-09-08T17:53:37Z) - Ignorance or Incompetence? Constructing Knowledge-Gated, Verifiable Tasks for LLM Agents [16.70932968825709]
本稿では,タスク命令をコンパクトなアーティファクトから分離するナレッジ付きタスク構築プロトコルを提案する。
1つのフロンティアエージェント構成は、アーティファクトで68.0%のパスレート、それなしで0%のパスレートを達成する。
保持されたタスクがポストトレーニングを改善するという確証はない。
論文 参考訳（メタデータ） (2026-08-31T06:39:27Z) - 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) - Agent Hacks Agent: Autoresearch for Production-Agent Red-Teaming [8.592488240217625]
本研究では, 1 つのエージェント研究環境を用いて, 生産用 LLM エージェントの自動リピートについて検討した。
脆弱性仮説を提案し、ファルシファイアを構築し、有効な攻撃をインスタンス化し、サンドボックス化されたハーネスで実行し、検証された結果をVulnerability Concept Graph(VCG)にプロモートする。
直接および間接的な攻撃をカバーする3つのシナリオに関するClude CodeとCodexの裏側で、発見された概念は、モデルとエージェント間で再利用可能な脆弱性コアを明らかにしている。
論文 参考訳（メタデータ） (2026-07-13T15:31:04Z) - BlindGuard: Safeguarding LLM-based Multi-Agent Systems under Unknown Attacks [58.959622170433725]
BlindGuardは、攻撃固有のラベルや悪意のある振る舞いに関する事前の知識を必要とせずに学習する、教師なしの防御方法である。
BlindGuardはマルチエージェントシステムにまたがる多様な攻撃タイプ(即時注入、メモリ中毒、ツール攻撃)を効果的に検出する。
論文 参考訳（メタデータ） (2025-08-11T16:04:47Z) - GuardAgent: Safeguard LLM Agents by a Guard Agent via Knowledge-Enabled Reasoning [79.07152553060601]
安全ガード要求を満たすか否かを動的に確認し,目標エージェントを保護する最初のガードレールエージェントであるガードアジェントを提案する。
特にGuardAgentは、まず安全ガードの要求を分析してタスクプランを生成し、それからその計画をガードレールコードにマップして実行します。
GuardAgentは、それぞれ98%と83%のガードレール精度を持つ2つのベンチマークにおいて、異なる種類のエージェントに対する違反行為を効果的に抑制することを示した。
論文 参考訳（メタデータ） (2024-06-13T14:49:26Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。