  There has been significant recent interest in devising verification
techniques for learning-enabled controllers (LECs) that manage safety-critical
systems. Given the opacity and lack of interpretability of the neural policies
that govern the behavior of such controllers, many existing approaches enforce
safety properties through the use of shields, a dynamic monitoring and repair
mechanism that ensures a LEC does not emit actions that would violate desired
safety conditions. These methods, however, have shown to have significant
scalability limitations because verification costs grow as problem
dimensionality and objective complexity increase. In this paper, we propose a
new automated verification pipeline capable of synthesizing high-quality safety
shields even when the problem domain involves hundreds of dimensions, or when
the desired objective involves stochastic perturbations, liveness
considerations, and other complex non-functional properties. Our key insight
involves separating safety verification from neural controller, using
pre-computed verified safety shields to constrain neural controller training
which does not only focus on safety. Experimental results over a range of
realistic high-dimensional deep RL benchmarks demonstrate the effectiveness of
our approach.
