arXiv:2607.05397cs.CRcs.AI2026-07被引 2

让AI执行过程可验证,确保每一步都合规且可追溯。

Proof of Execution: Runtime Verification for Governed AI Agent Actions

  • 将执行过程拆解为合同、事件流和回放上下文,形成可验证的执行三元组。
  • 在单节点原型中,执行开销仅增加2.7毫秒,8事件日志压缩至1.1KB。
  • 适合需审计、合规或可验证执行的高风险AI应用系统。

AI代理越来越多地执行而非仅提供建议。当代理查询受监管数据、调用有影响的工具并修改持久状态时,仅凭最终输出是否合理无法保证正确性。关键问题在于:每一步是否符合合同授权?记录的历史是否防篡改?轨迹能否确定性重现?本文提出运行时执行证明(PoE),将执行形式化为三元组 x = (C, T, R):合同 C、执行因果事件流(ECES)T 与回放上下文 R。通过一个良定义谓词和五个可验证不变式构建 PoE 有效性判定。五项语义保证涵盖授权、路径合规、拒绝时无副作用、历史完整性与可重放性。在显式密码学与部署假设下,任何违反语义保证的 PoE 有效执行均会导致签名伪造、哈希碰撞或量化部署失败事件。主执行模型(PEM)将规划、执行、效果与记录分属不同权限平面;引理表明,追踪完整性可归约为执行器独占凭证化。仅当 PoE = 1 时签发执行认证证书。在单节点 TypeScript 原型中,最小流程增加约 2.7 毫秒,批量并发工作负载开销为 4.4%;标准八事件日志压缩至约 1.1 KB;注入的网关绕过与日志篡改攻击均被拒。PoE 不替代共识、可信执行环境或 zkVM,而是将授权、执行、历史与重放绑定为单一可运行时验证的对象,使受控执行具备合约可认证性。

原文摘要 · Abstract (English)

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.

AI治理执行验证可追溯性合约安全

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。