Efficient and Sound Probabilistic Verification for AI Agents

As AI agents gain the ability to interact with complex digital environments, they face significant security risks from execution errors and adversarial prompt injection. Current runtime monitors often use deterministic policies, which struggle to handle the inherent ambiguity of real-world inputs—such as noisy PII detectors or classifiers. The authors ask: how can we rigorously verify agent safety when policy predicates are probabilistic, and how can we do so without making unrealistic independence assumptions about these probabilities?

The authors propose a probabilistic verification framework that treats agent execution as a sequence of state transitions. Instead of forcing continuous probability outputs into binary decisions (which discards critical context), the framework models the agent's execution trajectory as a Datalog derivation graph. This graph captures the logical dependencies between tool calls and environmental facts.

To compute the risk of policy violation, the authors formulate an optimization problem over joint probability measures. Because solving this exactly is computationally intractable, they employ distributionally robust optimization (DRO) to compute a sound upper bound on the probability of violation. They specifically introduce a polynomially-sized semidefinite programming (SDP) relaxation that tracks second-order moments, ensuring the monitor remains efficient enough for real-time use while maintaining mathematical soundness.

The study demonstrates that this probabilistic approach significantly improves the security-utility trade-off compared to deterministic monitors. By preserving marginal uncertainties and accounting for potential correlations between predicates, the framework avoids the false negatives common in threshold-based systems. Empirical evaluations on terminal and tool-calling benchmarks show that the SDP relaxation provides a tight, rigorous bound on violation probability with low computational overhead, effectively securing agents against data exfiltration even in ambiguous environments.