AI Research Portal

This paper extends Policy Predicate Abstraction (PPA) to perform probabilistic safety verification of neural policies. The core idea is to over-approximate the policy-restricted state space subgraph and iteratively refine this abstraction using a counterexample-guided abstraction refinement (CEGAR) framework adapted for probabilistic systems and neural policies (prob-CEGAR-PPA). The method decides if a neural policy π is safe with respect to a desired upper bound on unsafety probability, and can also automatically derive upper and lower bounds on unsafety probability. Empirically, the proposed algorithms can derive non-trivial bounds, and the approach is shown to be effective where encodings into state-of-the-art probabilistic model checkers are not.

The paper addresses the following bottlenecks in verifying neural policies:

Inability to account for probabilistic behavior: Existing approaches for closed-loop verification of neural network (NN) controlled systems are limited in their ability to handle probabilistic behavior.

Extension of Policy Predicate Abstraction (PPA) to probabilistic verification, enabling it to handle probabilistic transitions in addition to non-determinism.
Development of a new CEGAR method, prob-CEGAR-PPA, which integrates ideas from non-probabilistic CEGAR-PPA and probabilistic CEGAR to address the additional sources of spuriousness induced by neural policies and probabilistic behavior.
An algorithm (prob-CEGAR-PPA-pu) that decides whether a neural policy π is safe with respect to a desired upper bound on unsafety probability.
An incremental algorithm (prob-CEGAR-PPA-inc) that automatically derives upper and lower bounds on unsafety probability by re-using abstraction predicates.
Empirical demonstration that the proposed algorithms can derive non-trivial bounds, and that encodings into state-of-the-art probabilistic model checkers are ineffective for this task.

The method extends Policy Predicate Abstraction (PPA) to handle probabilistic transitions and perform probabilistic safety verification of neural policies.

Probabilistic PPA State Space: The policy predicate abstraction (PPA) of a system Θ over a set of predicates P and a policy π is defined as a Probabilistic Transition System (PTS) Θπp = (Sp, O, U, Tπp). Sp is the set of abstract states, O is the set of action operators, U is the set of updates, and Tπp is the set of transitions. A transition (sp, o, μp) ∈ Tπp exists if there is a concrete state s ∈ [sp] such that s satisfies the guard of o, the concrete update s[ū] is in the concretization of μp, and the policy π selects the label of o.

Abstract State Space Computation: The abstract transition problem for Θπp is solved by encoding it into Satisfiability Modulo Theories (SMT) using off-the-shelf solvers. This involves handling a finite-support successor distribution rather than a single successor, making the encoding more laborious than in non-probabilistic PPA.

Abstract Counterexample Computation: To verify safety in Θπp, the method checks for a counterexample (A, sp) where A is an adversary and sp is an abstract start state. This involves solving a MaxProb problem to find the maximal unsafety probability maxPr(Θπp, φo, φu). The paper uses FRET-LRTDP, which incrementally explores the reachable fragment of Θπp to compute the maximizing (A, sp).

CEGAR for Probabilistic PPA (prob-CEGAR-PPA): The core of the method is a CEGAR loop (Algorithm 1) that iteratively refines the predicate set P.

Initialization: The predicate set P starts with {φu}.
MaxProb Search: In each iteration, a MaxProb search is performed in Θπp to compute the abstract adversary A and start state sp that maximize the abstract unsafety probability Pr(A, sp, φu).
Safety Check: If Pr(A, sp, φu) ≤ pu, the policy π is proven safe. If the counterexample analysis (CeAna) returns REAL, π is unsafe. Otherwise, CEGAR iterates.
Counterexample Analysis (CeAna): This procedure (Algorithm 1, Procedure CeAna) maintains a set of abstract unsafe paths upsp ⊆ Path(A, sp, φu) and an upper bound Pmax on the maximal realizable probability of upsp. It iteratively adds paths to upsp and checks for spuriousness.
- T-analysis (T-spuriousness): This phase iteratively constructs upsp. It computes the path σp with the next highest probability. If σp is T-path spurious (not realizable in the full system Θ), the abstraction is refined (refine-T-path), and CeAna terminates. If realizable, σp is added to upsp, and Pmax is updated. Once Pmax > pu, the maximal T-realizable probability is computed via MaxSMT. If Pmax > pu, it proceeds to π-analysis. If Pmax + Punused ≤ pu, the counterexample is spurious, and the abstraction is refined (refine-T-prob).
- π-analysis (π-spuriousness): This phase checks for π-spuriousness. It restricts to a maximal T-realizable subset upsπ ⊆ upsp. If any path σp ∈ upsπ is π-path spurious (not realizable under policy π), the abstraction is refined (refine-π-path). If upsπ is not π-all realizable (i.e., there's no common start state for all paths), the abstraction is refined (refine-π-prob). Otherwise, if upsπ is π-all realizable, the counterexample (A, sp) is deemed REAL, proving π unsafe.

Automated Bound Derivation (prob-CEGAR-PPA-inc): An extension (Algorithm 2) embeds a linear search on pu into the CEGAR loop to incrementally tighten interval bounds [Plo, Pup] on the maximal unsafety probability.

Key Equations:

Accumulated unsafety probability for a set of paths ups: Pr(ups) = Σ_{σ∈ups} Π_{i=0}^{|σ|-1} μ^i(σ)(u^i(σ), s^{i+1}(σ))
Maximal unsafety probability of Θπp: maxPr(Θπp, φo, φu) = max_{A, sp} Pr(A, sp, φu)

Neural Network Architecture: Feed-forward NNs with ReLU activation ReLU(x) = max(x, 0). They consist of an input layer, arbitrarily many hidden layers, and an output layer with one neuron per label l ∈ L.
SMT Solvers: Marabou (2019) is used for NN-constrained SMT. Z3 (2008) is used for MaxSMT.
Training: Neural policies are trained using deep Q-learning (Mnih et al. 2015) and provided in PYTORCH (Ansel et al. 2024) format.
Hidden Layers: Policies have two hidden layers of size 16, 32, or 64.
Parameters:
- Minimal path probability for CEGAR: pε = 10⁻⁵.
- Default configuration for linear search on pu: pΔ = 0.05, pinit = 0.
Implementation: The approach is implemented on top of Vea's C++ code base (2024).
Resource Limits: Experiments were run with time and memory limits of 12h and 4GB respectively.

Benchmarks: Vea's benchmarks (2022) adapted from planning domains: Blocksworld, Puzzle, and Transport. These are encoded in the automata language JANI (Budde et al. 2017).
Abstract State Space Computation:
- prob-PPA incurs little performance overhead compared to non-prob-PPA.
- The distribution size |Supp(μp)| is bounded by the update support |Supp(ū)| per operator o, which is typically small.
Automated Bound Derivation (prob-CEGAR-PPA-inc):
- Terminates with a complete analysis on 16 out of 32 benchmark instances.
- Derives tightened probability bounds on remaining instances, with 5 cases having an interval size smaller than 0.3.
Verification of specific pu (prob-CEGAR-PPA-pu vs. prob-CEGAR-PPA-inc):
- Verification tailored to a specific pu can be significantly faster, especially when pu is significantly larger than the concrete unsafety probability (e.g., 4 Blocks, CA, 32, 0.5).
- Verification time during PPA-inc is often on par with prob-CEGAR-PPA-pu, demonstrating the practicality of incremental linear search on pu.
Counterexample Analysis (CeAna):
- Often a major bottleneck, with more than 50% of time spent on CeAna in 6 instances (5 timeouts).
- Costly π-spuriousness checks contribute to complexity; e.g., almost the entire CE-time on Transport instances is spent on π-path checks.
- Complexity also arises from the size of the abstract unsafe path set upspmax, which exceeds 10⁴ on 8 instances (6 timeouts).
- Particularly challenging for policies with applicability filtering (9 timeouts out of 13).
Comparison with State-of-the-Art Model Checkers:
- Probabilistic model checkers (STORM, ePMC, MODEST, PRISM, PET) are almost universally unsuccessful, exceeding time or memory limits on all benchmark instances.
- STORM's explicit engine successfully terminates on 6 Blocks (CI) NN 16 without app-filter after 180 seconds, which is more than double the runtime of prob-CEGAR-PPA-inc with pu = 0.01, 0.05 or 0.10 (less than 80 seconds).

Under-approximative π-realization check: The paper states, "We settle for an under-approximative π-realization check: Let upsπ ⊆ upsp be a maximal T-realizable subset, i.e., maxPrupsπ = Pr(upsπ) = maxPrupsp. upsp is π-probabilistic realizable if upsπ is π-all realizable under π, i.e., if there exists sº ∈ [sºp] ∩ [φo] such that for all σp ∈ upsπ, there exists σ∈ σp Λ φu with sº(σ) = sº." (section: CEGAR for Probabilistic PPA)
Limited support for NN-tailored MaxSMT solvers: The paper notes, "maxPrupsp boils down to a NN-constrained MaxSMT problem. Support for NN-tailored MaxSMT solvers is limited (Strong et al. 2023)." (section: CEGAR for Probabilistic PPA)
Path set enumeration scalability: The conclusion states, "Future work may investigate whether compact path set representations (Han et al. 2009) can be deployed to scale abstract counterexample analysis where path set enumeration is infeasible." (section: Conclusion)
Continuous state variables: The conclusion also mentions, "Another important future direction is the extension of PPA to PTS with continuous state variables." (section: Conclusion)

Method evidence: "In this work, we tackle unbounded-time safety verification in the presence of probabilistic as well as non-deterministic behavior under π. An action π(s) may label multiple outgoing transitions (non-determinism), each with a probability distribution over successors states." (section: Abstract)
Result evidence: "Our experiments show that these algorithms can derive non-trivial bounds, whereas encodings into state-of-the-art probabilistic model checkers turn out to be ineffective." (section: Abstract)
Limitation evidence: "Future work may investigate whether compact path set representations (Han et al. 2009) can be deployed to scale abstract counterexample analysis where path set enumeration is infeasible." (section: Conclusion)

Probabilistic Safety Verification of Neural Policies via Predicate Abstraction

Summary

Problem

Key Contributions

Method

Technical Details

Results

Weaknesses / Limitations

Evidence

Additional Figures