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

光探测和测距（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.