ArXiv Preprint
As neural networks become more integrated into the systems that we depend on
for transportation, medicine, and security, it becomes increasingly important
that we develop methods to analyze their behavior to ensure that they are safe
to use within these contexts. The methods used in this paper seek to certify
safety for closed-loop systems with neural network controllers, i.e., neural
feedback loops, using backward reachability analysis. Namely, we calculate
backprojection (BP) set over-approximations (BPOAs), i.e., sets of states that
lead to a given target set that bounds dangerous regions of the state space.
The system's safety can then be certified by checking its current state against
the BPOAs. While over-approximating BPs is significantly faster than
calculating exact BP sets, solving the relaxed problem leads to
conservativeness. To combat conservativeness, partitioning strategies can be
used to split the problem into a set of sub-problems, each less conservative
than the unpartitioned problem. We introduce a hybrid partitioning method that
uses both target set partitioning (TSP) and backreachable set partitioning
(BRSP) to overcome a lower bound on estimation error that is present when using
BRSP. Numerical results demonstrate a near order-of-magnitude reduction in
estimation error compared to BRSP or TSP given the same computation time.
Nicholas Rober, Michael Everett, Songan Zhang, Jonathan P. How
2022-10-14
