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相比，本方法在效率、可扩展性和泛化能力方面均更优。