Abstract
Autonomous systems are increasingly implemented using end-to-endlearning-based controllers. Such controllers make decisions that are executedon the real system, with images as one of the primary sensing modalities. Deepneural networks form a fundamental building block of such controllers.Unfortunately, the existing neural-network verification tools do not scale toinputs with thousands of dimensions -- especially when the individual inputs(such as pixels) are devoid of clear physical meaning. This paper takes a steptowards connecting exhaustive closed-loop verification with high-dimensionalcontrollers. Our key insight is that the behavior of a high-dimensionalcontroller can be approximated with several low-dimensional controllers. Tobalance the approximation accuracy and verifiability of our low-dimensionalcontrollers, we leverage the latest verification-aware knowledge distillation.Then, we inflate low-dimensional reachability results with statisticalapproximation errors, yielding a high-confidence reachability guarantee for thehigh-dimensional controller. We investigate two inflation techniques -- basedon trajectories and control actions -- both of which show convincingperformance in three OpenAI gym benchmarks.