SHF: Medium: More Reliable Image Networks through Scene-based Specification, Neuro-symbolic Training, and Systematic Specification-driven Testing

深度神经网络(DNN)正在成为从汽车到医疗器械等安全关键自主系统的重要组成部分。这种安全关键的自主系统中的故障可能会导致人员受伤或生命损失。虽然已经有成熟的技术来提高DNN的准确性，但这些技术并不能保证DNN的行为总是适当的。如果没有这种保证，在安全和关键任务系统中部署DNN将是有限的或不必要的危险。该项目试图通过开发改变当前两个基本实践的技术来确保基于图像的DNN的质量：1)将期望的DNN属性的规范从像素级抽象到域实体(例如，人、汽车)，以使得能够对DNN行为的正确性进行推理；以及2)这些属性的应用将渗透到DNN开发过程中，从而得到的DNN行为与这些属性一致。如果成功，这项研究将提高对包括DNN的系统的保证，从而提高公众的安全。现代图像深度神经网络可以非常复杂地接受高分辨率的图像，并通过数十个层和数千万个参数来处理它们来计算输出。经常使用评估和改进计算输出相对于标记训练数据的统计准确性的方法，但这种方法不能保证DNN的行为是适当的，特别是在异常或罕见输入的情况下。该项目旨在为开发具有行为保证的基于图像的DNN的新方法奠定基础、算法和工程进展。该项目改变了以前的研究方向，这些研究集中在像素级别的DNN正确性的有限形式的推理上，例如局部稳健性，相反，该项目的目标是使从像素级别的变化中抽象出来的更高级属性的规范能够描述行为的等价类，然后通过DNN的训练、测试和部署来纳入这样的规范。项目活动包括：1)开发一种高级符号方法，用于指定基于像素的DNN的必要的正确性属性；2)将这种规范纳入DNN的训练中，以保证其规范的一致性；以及3)评估和改进训练、测试和验证集的方法，以确保它们充分代表重要但罕见的输入，从而使DNN能够推广到这种输入。总而言之，这项工作将建立第一个高级方法来指定映像DNN的预期行为，如果成功，该项目将为构建更可靠的DNN系统提供基础。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Deep Neural Networks (DNN) are becoming an essential part of safety-critical autonomous systems, from automobiles to medical devices. Failures in such safety-critical autonomous systems may lead to injury or loss of life. Although there are mature techniques for improving the accuracy of DNNs, such techniques do not provide guarantees that the behavior of a DNN will always be appropriate. Without such guarantees the deployment of DNNs in safety and mission critical systems will be limited or unnecessarily risky. This project seeks to assure the quality of image-based DNNs through the development of techniques that change two fundamental current practices: 1) the specification of desirable DNN properties will be abstracted from the pixel-level to domain entities (e.g., people, cars) to enable reasoning about the correctness of DNN behaviors, and 2) the application of those properties will pervade the DNN development process so that the resulting DNNs behave in accordance with those properties. If successful, the research will improve assurance of systems that include DNNs and, thereby, the safety of the public. Modern image Deep Neural Networks can be extremely complex accepting high-resolution images and processing them through many dozens of layers with tens of millions of parameters to compute outputs. Methods of assessing and improving the statistical accuracy of computed outputs relative to labeled training data are in regular use, but such methods provide no guarantees that the behavior of the DNN will be appropriate, especially on unusual or rare inputs. This project seeks to establish the foundations, algorithms and engineering advances for a new approach to developing image-based DNNs with behavior guarantees. The project shifts the direction from prior research that has focused on reasoning about limited forms of DNN correctness at the pixel level, such as local robustness, and instead aims to enable the specification of higher-level properties that abstract from pixel-level variation to describe equivalence classes of behavior and then to incorporate such specifications through the training, testing, and deployment of DNNs. The project activities include developing: 1) a high-level symbolic method for specifying necessary correctness properties of pixel-based DNNs; 2) methods to incorporate such specifications into the training of DNNs so as to guarantee their specification conformance; and 3) methods to assess and improve training, test, and validation sets to ensure that they adequately represent important, but rare, inputs and thereby enable DNNs to generalize to such inputs. Collectively, this work will establish the first high-level approach to specifying the intended behavior of image DNNs and, if successful, the project will provide a foundation for building more reliable DNN-enabled systems.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.