CPS: Small: Formally Correct Deep Perception For Cyber-Physical Systems

光探测和测距(LiDAR)和摄像头是自动驾驶汽车和无人机等自主网络物理系统中使用的传感器套件中不可或缺的一部分。这些传感器产生的数据通常由深度神经网络处理，该网络将其转换为控制回路中使用的状态估计。虽然人们可以分析错误的状态估计对控制回路的影响，但人们对如何表征深度神经网络产生的误差知之甚少。这个项目的目标是开发分析和设计技术，为这些错误的大小提供正式的保证界限。正式建立误差界将使现有系统的验证和新的自治系统的设计能够得到形式上的安全和性能保证。本项目通过两种不同的方法，即训练正确性和监督正确性，解决了在自治网络物理系统的感知管道中使用深度神经网络的挑战。第一种方法，通过训练的正确性，是基于单调神经网络的使用，可以为其建立确定性的泛化界限。使用单调神经网络的挑战在于它们的训练更具挑战性，将研究几种新的训练技术。第二种方法，监督正确性，包括在神经网络上附加一个监督器，该监督器覆盖网络输出，以实施保证的误差界。将在使用基于矩的新颖点集配准技术的LiDAR测量的本地化背景下开发监督器。这两种方法都旨在为深度神经网络计算的状态估计提供有保证的误差界。最终的贡献是在使用感知管道中的深度神经网络对控制回路的安全性和性能进行正式分析时使用这些误差界。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.