Deep neural networks (DNNs) are becoming increasingly important components of software, and are considered the state-of-the-art solution for a number of problems, such as image recognition. However, DNNs are far from infallible, and incorrect behavior of DNNs can have disastrous real-world consequences. This paper addresses the problem of architecture-preserving V-polytope provable repair of DNNs. A V-polytope defines a convex bounded polytope using its vertex representation. V-polytope provable repair guarantees that the repaired DNN satisfies the given specification on the infinite set of points in the given V-polytope. An architecture-preserving repair only modifies the parameters of the DNN, without modifying its architecture. The repair has the flexibility to modify multiple layers of the DNN, and runs in polynomial time. It supports DNNs with activation functions that have some linear pieces, as well as fully-connected, convolutional, pooling and residual layers. To the best our knowledge, this is the first provable repair approach that has all of these features. We implement our approach in a tool called APRNN. Using MNIST, ImageNet, and ACAS Xu DNNs, we show that it has better efficiency, scalability, and generalization compared to PRDNN and REASSURE, prior provable repair methods that are not architecture preserving.

翻译：深度神经网络（DNN）正日益成为软件的重要组成部分，并被视作图像识别等多个问题的最新解决方案。然而，DNN远非无懈可击，其错误行为可能导致灾难性的现实后果。本文研究了DNN的架构保持型V-多面体可证明修复问题。V-多面体通过顶点表示定义了一个有界凸多面体。V-多面体可证明修复确保修复后的DNN在给定V-多面体内的无穷点集上满足特定规范。架构保持型修复仅修改DNN的参数，而不改变其架构。该修复方法可灵活修改DNN的多个层，运行时间为多项式级。它支持包含线性片段激活函数的DNN，以及全连接层、卷积层、池化层和残差层。据我们所知，这是首个同时具备上述所有特征的可证明修复方法。我们将该方法实现为工具APRNN。通过使用MNIST、ImageNet和ACAS Xu DNN进行的实验表明，相较于先前的非架构保持型可证明修复方法PRDNN和REASSURE，本方法在效率、可扩展性和泛化能力上均表现更优。