zkARc: Succinctly Verifiable Proofs for Neurosymbolic Natural Language Formalization and Verification

원문 초록

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. 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. 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, and the solver proof alone is 88 KiB and verifies in 0.3 seconds.