論文の概要: Proof of Execution: Runtime Verification for Governed AI Agent Actions
- arxiv url: http://arxiv.org/abs/2607.05397v1
- Date: Sun, 26 Apr 2026 12:30:54 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-27 00:46:12.982462
- Title: Proof of Execution: Runtime Verification for Governed AI Agent Actions
- Title（参考訳）: 実行の証明:Governed AI Agent Actionsのランタイム検証
- Abstract要約: エージェントシステムはアドバイスよりもますます実行します。
私たちはこれを実行時の証明として定式化します。
PoEは、認証、エフェクト、履歴、リプレイを単一のランタイムチェック可能なオブジェクトにバインドする。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Agent systems increasingly execute rather than advise. When an AI agent queries regulated data, invokes effectful tools, and mutates persistent state, correctness is not captured by whether a terminal output looks plausible. The operative questions are whether each step was authorized under a contract, whether the recorded history is tamper-evident, and whether the trajectory can be reconstructed deterministically. We formalize this as runtime proof of execution. An execution is a triple $x = (C, T, R)$: a contract $C$, an Execution Causal Event Stream (ECES) $T$, and a replay context $R$. A well-formedness predicate and five validator-checkable invariants form the PoE validity predicate. Five semantic guarantees describe authorization, path compliance, null effect on deny, history integrity, and replayability. We prove soundness under explicit cryptographic and deployment assumptions: any PPT adversary that produces a PoE-valid execution violating a semantic guarantee yields a signature forgery, a hash collision, or a quantified deployment-failure event. The Prime Execution Model (PEM) separates planning, enforcement, effect, and recordkeeping into distinct authority planes; a lemma reduces trace completeness to Effector-exclusive credentialing. An Execution Attestation Certificate is issued only when PoE = 1. In a single-node TypeScript prototype, PoE adds approximately 2.7 ms on a minimal flow and 4.4% overhead on concurrent batch workloads; a standard eight-event trace compresses to approximately 1.1 KB; injected Gateway-bypass and trace-mutation attacks are rejected. PoE does not replace consensus, TEEs, or zkVMs; it binds authorization, effect, history, and replay into a single runtime-checkable object so that governed execution becomes attestable under contract.
- Abstract（参考訳）: エージェントシステムはアドバイスよりもますます実行します。
AIエージェントが規制されたデータをクエリし、エフェクトフルツールを起動し、永続的な状態を変更した場合、端末出力が妥当なように見えるかどうかによって、正確性は取得されない。
作業上の疑問は、各ステップが契約の下で承認されたか、記録された履歴が不適切かどうか、軌道を決定論的に再構築できるかどうかである。
私たちはこれを実行時の証明として定式化します。
実行はトリプル$x = (C, T, R)$: a contract $C$, an Execution Causal Event Stream (ECES) $T$, a replay context $R$である。
よく形づくられた述語と5つの検証可能な不変量は、PoE妥当性述語を形成する。
5つのセマンティック保証は、承認、パスコンプライアンス、否定に対するnull効果、履歴の完全性、再生可能性を記述する。
意味的保証に違反するPoE-valid実行を生成するPPT敵は,シグネチャフォージェリやハッシュ衝突,あるいは定量化デプロイメント障害イベントを発生させる。
PEM(Prime Execution Model)は、計画、執行、効果、記録を異なる権限面に分割する。
実行証明証明書は、PoE = 1 の場合のみ発行される。
単一ノードのTypeScriptプロトタイプでは、PoEは最小フローで約2.7ms、並行バッチワークロードで4.4%のオーバーヘッドを追加している。
PoEはコンセンサス、TEE、あるいはzkVMを置き換えるものではなく、認証、エフェクト、履歴、リプレイを単一のランタイムチェック可能なオブジェクトにバインドすることで、管理された実行がコントラクト下で検証可能である。
関連論文リスト
- PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
我々は、スケジューリング、検証、メモリ、ベンチマーク、安全性をシステムレベルのサービスとして提供するPhyAgentOSを紹介します。
セッション中心のセッションは、スケジューリング、互換性、監督された実行、エビデンス収集、受け入れの最小単位として、アクションではなくセッションを扱う。
SessionVerifierは、実行終了とセマンティックタスク完了を、成功、失敗、または再計画のエビデンスに基づいて判断する。
ベンチマークはデプロイメントセッションと検証パスを再利用するので、結果は実際の実行に遡る。
論文 参考訳（メタデータ） (2026-07-18T04:46:53Z) - CAVA: Canonical Action Verification and Attestation for Runtime Governance of Agentic AI Systems [0.6526824510982799]
本稿では、異種エージェントのアクティビティを標準ランタイムオブジェクトに変換するランタイム・セマンティック・レイヤを提案する。
このコントリビューションは、デプロイ側AIガバナンスに必要な基盤として、アクションレベルの標準化とポリシー順応可能なセマンティックパターンを定式化したシステムである。
論文 参考訳（メタデータ） (2026-07-15T11:34:34Z) - Sovereign Assurance Boundary: Certificate-Bound Admission for Agentic Infrastructure [2.124730017640531]
Sovereign Assurance境界は、自動実行権限のための証明書バウンドランタイムアクセス層である。
本稿では,エアロックブローカーのアーキテクチャを詳述し,その入力と取り消しの不変性を定式化し,Goプロトタイプの予備実現可能性の測定結果を報告する。
論文 参考訳（メタデータ） (2026-06-10T03:49:57Z) - VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
本稿では,ロボットスキルコントラクトの検証誘導自己進化のためのフレームワークであるVASOを紹介する。
VASOは論理的に一貫性のないスキル契約を検証し、グローバルおよびローカルな時間的仕様に対してスキルによって誘発される計画を検証する。
Clearpath Jackal と PX4 のクアッドコプタータスクでは、VASO は100点未満の最適化サンプルを使用して97.2% の形式的な仕様準拠に達した。
論文 参考訳（メタデータ） (2026-06-03T20:02:35Z) - Proof-Carrying Agent Actions: Model-Agnostic Runtime Governance for Heterogeneous Agent Systems [0.6526824510982799]
本稿では,アクション証明書を中心としたランタイム中立ガバナンスモデルであるProof-Carrying Agent Actions (PCAA)を提案する。
PCAAは5つのチェックポイント(事前行動の許容、行動のオープン、仮定のキャプチャ、承認、結果のクロージャ)を統括する。
異種エージェント制御プレーンと開示バウンダリ評価プロトコルの参照実装を用いてモデルについて検討する。
論文 参考訳（メタデータ） (2026-06-02T18:10:35Z) - From Patches to Trajectories: Privileged Process Supervision for Software-Engineering Agents [56.31499185764872]
教師の長い軌道上の監督された微調整(SFT)は、オープンソフトウェアエンジニアリング(SWE)エージェントに調査と推論を浸透させる主要な方法である。
本稿では,P2T (Patches-to-Trajectories) を提案する。P2T (Patches-to-Trajectories) は,P2T (Patches-to-Trajectories) において,P2T (Patches-to-Trajectories) とP2T (Patches-to-Trajectories) の2つの最適化法である。
論文 参考訳（メタデータ） (2026-05-21T04:54:55Z) - Compiling Activation Steering into Weights via Null-Space Constraints for Stealthy Backdoors [48.881343993730844]
安全性に整合した大規模言語モデル(LLM)は、現実世界のパイプラインにますますデプロイされている。
敵は通常の評価では動作しないバックドアのチェックポイントを配布することができる。
最近のポストホック重み付け法は、そのようなバックドアを注入するための効率的なアプローチを提供する。
論文 参考訳（メタデータ） (2026-04-14T06:48:33Z) - A Physical Agentic Loop for Language-Guided Grasping with Execution-State Monitoring [5.437966695589128]
我々は、接地された実行状態上で動作する有界な実施エージェントとして言語誘導の把握を再構築する。
未修正の学習操作プリミティブをラップする物理エージェントループを導入する。
眼内カメラD405を用いた移動マニピュレータのループを検証した。
論文 参考訳（メタデータ） (2026-04-08T08:01:35Z) - Zero-Trust Runtime Verification for Agentic Payment Protocols: Mitigating Replay and Context-Binding Failures in AP2 [0.0]
本稿ではエージェントベースの決済システムにおいて,AP2管理ライフサイクルのセキュリティ分析を行い,実行中に発生する強制的ギャップを識別する。
本稿では,明示的なコンテキストバインディングとコンシューム・オンス・マンデート・セマンティクスを適用したゼロトラストランタイム検証フレームワークを提案する。
本稿では,コンテキストアウェアバインディングとコンシューム・オンス・エグゼクティブ・アドレスの区別と相補的アタック・クラスを示すとともに,リプレイとコンテキスト・リダイレクト・アタックの防止に必要であることを示す。
論文 参考訳（メタデータ） (2026-02-06T03:22:11Z) - Runaway is Ashamed, But Helpful: On the Early-Exit Behavior of Large Language Model-based Agents in Embodied Environments [54.67512489842682]
大規模言語モデル(LLM)は、複雑な実施環境において、強力な計画と意思決定能力を示す。
LLMをベースとしたエージェントの早期退避行動を探究する第一歩を踏み出す。
論文 参考訳（メタデータ） (2025-05-23T08:23:36Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。