論文の概要: Formal Runtime Verification for Tool-Using LLM Agents: An Offline Same-Benchmark Study on AgentDojo and STAC
- arxiv url: http://arxiv.org/abs/2610.09793v1
- Date: Wed, 07 Oct 2026 10:08:46 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-08 21:58:22.852396
- Title: Formal Runtime Verification for Tool-Using LLM Agents: An Offline Same-Benchmark Study on AgentDojo and STAC
- Title（参考訳）: ツール利用LDMエージェントの形式的実行検証:エージェント・ドキュメンテーションとSTACのオフライン同一ベンチマーク
- Abstract要約: ツールを使用するLLMエージェント用のガードレールは通常、アプリケーション固有のルールである。
計量一階時間論理(MFOTL)を評価する。
トレースが信頼できる履歴を公開すると,時間的モニタリングの形式的付加価値が示される。
- 参考スコア（独自算出の注目度）: 0.37475012732344193
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Guardrails for tool-using LLM agents are usually application-specific rules, which makes multi-step, data-dependent safety policies hard to specify, audit and reuse. As a declarative alternative, we evaluate metric first-order temporal logic (MFOTL), replaying the recorded trajectories that AgentDojo, STAC and R-Judge already ship through the unmodified MonPoly monitor, offline and without running an agent. On these corpora, five generic obligations flag 71.8% of STAC attack chains and 70.1% of successful AgentDojo attacks, but also fire on 29.3% of benign runs. This imprecision stems from the corpora rather than the logic: they rarely record approvals and never record timestamps, so history-dependent obligations reduce to detecting risky action types. Where the trace does carry relational context, provenance-aware policies discriminate better; that context, however, is itself attackable, and one planted line defeats a naive provenance check on 94-99% of the runs it would otherwise flag. Binding provenance to the lookup that produced it closes this evasion at no cost in detection or benign firing. Taken together, these results show that formal temporal monitoring adds value exactly when the trace exposes trustworthy history. We therefore quantify how far current benchmarks are from that point and propose a twelve-field enforcement-ready trace schema.
- Abstract（参考訳）: ツールを使用するLLMエージェントのガードレールは通常、アプリケーション固有のルールであり、多段階のデータ依存の安全ポリシーを指定、監査、再利用が困難にしている。
宣言的な代替手段として,AgentDojo,STAC,R-Judgeが未修正のMonPolyモニタを通じてすでに出荷している記録されたトラジェクトリをオフラインかつエージェントを実行せずに再生する,メートル法一階時間論理(MFOTL)を評価する。
このコーパスでは、STAC攻撃チェーンの71.8%、AgentDojo攻撃の70.1%の一般的な5つの義務が宣言されている。
承認を記録せず、タイムスタンプも記録しないため、歴史に依存した義務はリスクのある行動タイプを検出することにつながる。
しかし、その文脈はそれ自体攻撃可能であり、ある植木されたラインは94-99%のランで単純な前例チェックを破り、それ以外はフラグを立てる。
生成したルックアップにバインドする証明は、検出や良性発射のコストを伴わずに、この回避を完了させる。
まとめると、これらの結果は、トレースが信頼できる履歴を公開すると、形式的な時間的モニタリングが真に価値を付加することを示している。
したがって、現在のベンチマークがその時点からどれくらい遠いのかを定量化し、12フィールドの強制対応トレーススキーマを提案する。
関連論文リスト
- hacktrace: behavior-supervised detection of reward hacking during code generation [52.709361620508595]
コーディングエージェントは、コードを修正するか、バグを露呈するテストを削除することで、パスグレードを得ることができる。
我々はQwen3-8Bから173,561個の注釈付きマルチターン符号化トラジェクトリをリリースし、成功を活かさないショートカット動作の監視が検出を大幅に改善することを示す。
HACKTRACEは、エージェントがコードを生成する際に既に計算している内部状態を読み取る行動監視モニターである。
論文 参考訳（メタデータ） (2026-10-02T09:35:59Z) - TraceDance: An Automated System for Building Agent Behavior Benchmarks from Real-World Agent Deployment Traces [49.561879967469714]
TraceDanceは、ユーザが指定した望ましくない振る舞いのデプロイメントトレースからターゲットベンチマークを構築するエージェントシステムである。
効率的な構築のために、Anchor-and-Confirmはプログラム可能な検索と、Flash大言語モデルによる候補レベルの確認を組み合わせる。
コーディングと一般的なツールの実験では、252,557のセッションで描画され、ビルドターゲット要求の95.3%を満たす4,125のインスタンスで107のベンチマークを生成する。
論文 参考訳（メタデータ） (2026-09-27T06:58:39Z) - FORESIGHT-9: Prospective and Process-Aware Evaluation of Adaptive Trading Agents [0.0]
FORESIGHT-9は、9つの監査可能な対実的ストレスワールドラインから構築された、将来的でプロセス対応のベンチマークである。
共通契約は、各エージェントのネイティブ適応ループを保持しながら、観察と実行を標準化する。
我々は,36ランにわたる2つの基盤モデルバックボーンを持つ2つの適応型トレーディングエージェントフレームワークを評価した。
論文 参考訳（メタデータ） (2026-08-29T17:12:49Z) - ROPE: Routed Origin Policy Enforcement against Indirect Prompt Injection [61.4148196085256]
本稿では,信頼という構造概念に根ざしたROPE(Routed Origin Policy Enforcement)について述べる。
提案手法では,(1)軌道の各段階において,攻撃可能コンテンツのみを起点とする値が,原点保護パラメータに到達しない,(2)注入のリワードがない,という2つの保証が認められている。
論文 参考訳（メタデータ） (2026-08-27T01:22:14Z) - TraceCompiler: Skill-Guided Mining and Compilation of LLM Agent Traces into Mostly Deterministic Workflows [2.435006380732194]
ノイズの多いトレースをトラジェクトリにコンパイルする,スキルガイドシステムであるTraceCompilerを提案する。
あらゆるハードエッジは監査可能な証拠を持ち、あいまいな関係が疑われる。
コールの削減を計測するが、オフラインのコンパイルコストはかからない。
論文 参考訳（メタデータ） (2026-08-03T01:05:06Z) - On-Policy Self-Evolution via Failure Trajectories for Agentic Safety Alignment [54.30690671490447]
既存の安全アライメント信号は、主に応答レベルまたは政治外である。
FATEは、検証済みの失敗を専門家のデモンストレーションなしで修復管理に変換する。
FATEは攻撃成功率を33.5%、有害なコンプライアンスを82.6%削減し、外的軌道安全診断を6.5%改善する。
論文 参考訳（メタデータ） (2026-05-12T09:56:28Z) - Policy-Invisible Violations in LLM-Based Agents [10.660248467840821]
コンプライアンスがエンティティ属性、コンテキスト状態、あるいはエージェントの可視的コンテキストから欠落したセッション履歴に依存する場合。
PhantomPolicyは、8つの違反カテゴリにまたがるベンチマークで、バランスの取れた違反と安全管理のケースを示す。
本稿では,反ファクトグラフシミュレーションに基づく実施フレームワークであるSentinelを紹介する。
論文 参考訳（メタデータ） (2026-04-14T01:15:15Z) - Agentproof: Static Verification of Agent Workflow Graphs [0.0]
エージェントフレームワークは、ツール使用の振る舞いを明示的なワークフローグラフとしてエンコードする傾向にある。
本稿では,4つの主要なエージェントフレームワークから統合抽象グラフモデルを自動的に抽出するAgentproofを提案する。
汎用的なモデルチェッカーとは異なり、Agentproofは手動モデリングを必要としない。
論文 参考訳（メタデータ） (2026-03-20T13:56:20Z) - Detecting Object Tracking Failure via Sequential Hypothesis Testing [80.7891291021747]
ビデオにおけるリアルタイムのオンラインオブジェクト追跡は、コンピュータビジョンにおける中核的なタスクである。
本稿では,物体追跡を逐次的仮説テストとして解釈することを提案する。
本研究では,地中追跡情報と内部追跡情報の両方を活用することにより,教師なしと教師なしの両方の変種を提案する。
論文 参考訳（メタデータ） (2026-02-13T14:57:15Z) - The Trojan Knowledge: Bypassing Commercial LLM Guardrails via Harmless Prompt Weaving and Adaptive Tree Search [58.8834056209347]
大規模言語モデル(LLM)は、有害な出力を誘導するために安全ガードレールをバイパスするジェイルブレイク攻撃に弱いままである。
CKA-Agent(Correlated Knowledge Attack Agent)は、ターゲットモデルの知識基盤の適応的木構造探索としてジェイルブレイクを再構成する動的フレームワークである。
論文 参考訳（メタデータ） (2025-12-01T07:05:23Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。