Light Detection and Ranging (LiDARs) and cameras are an indispensable part of the sensor suite used in autonomous cyber-physical systems such as self-driving cars and unmanned aerial vehicles. The data generated by these sensors is often processed by a deep neural network that transforms it into state estimates used in control loops. Although one can analyze the impact that erroneous state estimates have on control loops, less is known about how to characterize the errors produced by deep neural networks. The objective of this project is to develop analysis and design techniques that provide formally guaranteed bounds on how large these errors can be. Formally establishing error bounds will enable the verification of existing systems as well as the design of new autonomous systems for which formal guarantees of safety and performance can be given.

This project addresses the challenge of using deep neural networks in the perception pipeline of autonomous cyber-physical systems by following two different approaches, termed correctness-by-training and correctness-by-supervision. The first approach, correctness-by-training, is based on the use of monotone neural networks for which deterministic generalization bounds can be established. The challenge of using monotone neural networks is that their training is more challenging and several novel training techniques will be investigated. The second approach, correctness-by-supervision, consists of attaching a supervisor to the neural network that overrides the network output so as to enforce guaranteed error bounds. A supervisor will be developed in the context of localization using LiDAR measurements using novel point-set registration techniques based on moments. Both approaches aim to provide guaranteed error bounds on the state estimates computed by deep neural networks. The ultimate contribution is to use these error bounds in the formal analysis of safety and performance of control loops using deep neural networks in the perception pipeline.