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

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

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.