Probabilistic Safety Verification of Neural Policies via Predicate Abstraction

Neural networks are increasingly important to learn action policies. Policy predicate abstraction (PPA) verifies safety of such a neural policy π by over-approximating the state space subgraph induced by π, and using counterexample-guided abstraction refinement (CEGAR) to iteratively refine the abstraction. So far, PPA verifies safety in non-deterministic state spaces. This paper extends PPA to probabilistic verification. Extending the abstract state space computation to the probabilistic case is relatively straightforward. Abstraction refinement, however, becomes substantially more complex, due to the more intricate form of counterexamples and the various sources of spuriousness it entails. We tackle this challenge by drawing inspiration from prior work on probabilistic CE-GAR, empowering it to deal with neural π. The resulting algorithm decides whether π is safe with respect to a desired upper bound on unsafety probability. Invoking the algorithm incrementally, we can also derive upper and lower bounds automatically. Our experiments show that these algorithms can derive non-trivial bounds. In a first comparison to state-ofthe-art probabilistic model checkers, our approach is superior.