When an AI agent acts on your behalf, how can a seller be sure the agent followed your rules without you revealing the rules themselves? Current methods like trusted hardware or audit trails force someone to either trust blindly or redo all checks. zkARc solves this by wrapping each step of a neurosymbolic pipeline, which translates plain-English policies into logical formulas and then checks AI actions against them, in its own zero-knowledge proof. These proofs combine into a single receipt that any third party can verify in under a minute without seeing the private policy. The key result is that a full receipt, including proof of the AI model's inference, takes about an hour to produce but verifies in about 33 seconds; the logical check alone produces an 88-kilobyte proof that verifies in 0.3 seconds.
Zero-knowledge proofs let AI agents prove they followed policies without exposing the rules
The zkARc framework produces a cryptographic receipt that binds policy enforcement to each action, verifiable in under a minute.
Big Tech
Wyatt Benno (ICME Labs) · Alberto Centelles (Imperial College London) · Aman Goel (Amazon Web Services) · Benjamin Kiesl-Reiter (Amazon Web Services)
Research Digest··3 min read
Thread:Agent Security & Attacks
In one line
zkARc produces succinct zero-knowledge proofs that a neurosymbolic system correctly enforced natural language policies on AI actions.
Before you read this
Three ideas this paper builds onverificationChecking outputs for correctness before accepting them, often to catch errors or reward hacking.323 papers →agent safetyRisks from AI agents including timing errors, shutdown avoidance, collusion, overclaiming, and unsafe execution, mitigated by constrained decoding, safety harnesses, and swarm governance.178 papers →large language modelA neural network trained on massive text corpora to generate coherent text and perform diverse language tasks.301 papers →
Read it as
Researchers present zkARc, a system that adds zero-knowledge proofs to each step of a neurosymbolic pipeline that translates natural language policies into formal logic and checks AI actions against them.
The authors extended the Automated Reasoning (ARc) pipeline, which uses language models to convert natural language policies and agent actions into SMT logic and an SMT solver to determine compliance, by adding zero-knowledge proofs for each stage.
How it works
stage by stageThe Daily Edition
The front page in your inbox each weekday morning: the lead, the picks, and why each one earned its place.