Autonomous agents increasingly execute consequential actions on behalf of users, but ordinary middleware guardrails do not provide cryptographic proof that a policy was actually enforced. Their verdicts leave counterparties dependent on the operator unless they repeat the checks themselves, potentially exposing sensitive policies and inputs.
问题：中间件护栏缺乏可验证性
Autonomous agents increasingly execute consequential actions on behalf of users, but ordinary middleware guardrails do not provide cryptographic proof that a policy was actually enforced. Their verdicts leave counterparties dependent on the operator unless they repeat the checks themselves, potentially exposing sensitive policies and inputs.
方法：zkARc 与 ARc 的证明携带框架
We present zkARc, a modular proof-carrying framework that wraps each stage of Automated Reasoning checks (ARc) in an independent, succinctly verifiable zero-knowledge proof. ARc is a neurosymbolic system that translates natural language policies into formal logic and verifies AI-generated content against them using SMT solvers. zkARc certifies the planner's output, the policy's formalization, the action's formalization and both solver queries.
验证：证明属性与信任模型
The receipt binds these computations to the exact action received and, under the stated assumptions, reveals no additional information about private policies and intermediate model values beyond the declared public information and verdict. This lets a third party check the claimed policy enforcement without re-running the pipeline or trusting the operator. We prove completeness, knowledge soundness and zero knowledge for the composed receipt under explicit assumptions.
实现：Qwen2-0.5B 上的端到端策略执行
实验设置：
An implementation on Qwen2-0.5B enforces a spending policy end to end, approving two purchases and denying a third.
性能指标：
A full receipt, which also proves model inference, takes about an hour to issue with CPU-only proving and verifies in under a minute.
The solver proof alone is 88 KiB and verifies in 0.3 seconds.