Architecture-Preserving Provable Repair of Deep Neural Networks

Reference. Architecture-Preserving Provable Repair of Deep Neural Networks

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. CCS Concepts: • Computing methodologies → Neural networks; • Theory of computation → Linear programming; • Software and its engineering → Software post-development issues.

Cite

Cite as @taoArchitecturePreservingProvableRepair2023 (helia, typst) · \cite{taoArchitecturePreservingProvableRepair2023} (LaTeX)

BibTeX

bibtex · 16 lines

@article{taoArchitecturePreservingProvableRepair2023,
 title = {Architecture-{{Preserving Provable Repair}} of {{Deep Neural Networks}}},
 author = {Tao, Zhe and Nawas, Stephanie and Mitchell, Jacqueline and Thakur, Aditya V.},
 date = {2023-06-06},
 doi = {10.1145/3591238},
 url = {https://dl.acm.org/doi/10.1145/3591238},
 urldate = {2023-11-27},
 journaltitle = {Proceedings of the ACM on Programming Languages},
 volume = {7},
 pages = {443--467},
 langid = {english},
 issue = {PLDI},
 abstract = {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. CCS Concepts: • Computing methodologies → Neural networks; • Theory of computation → Linear programming; • Software and its engineering → Software post-development issues.},
 issn = {2475-1421},
 shortjournal = {Proc. ACM Program. Lang.}
}

hayagriva YAML (typst)

yaml · 23 lines

taoArchitecturePreservingProvableRepair2023:
  type: article
  title: Architecture-{Preserving Provable Repair} of {Deep Neural Networks}
  author:
  - Tao, Zhe
  - Nawas, Stephanie
  - Mitchell, Jacqueline
  - Thakur, Aditya V.
  date: 2023-06-06
  page-range: 443-467
  url:
    value: https://dl.acm.org/doi/10.1145/3591238
    date: 2023-11-27
  serial-number:
    doi: 10.1145/3591238
    issn: 2475-1421
  language: en-US
  abstract: '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. CCS Concepts: • Computing methodologies → Neural networks; • Theory of computation → Linear programming; • Software and its engineering → Software post-development issues.'
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    issue: PLDI
    volume: 7

Download: taoArchitecturePreservingProvableRepair2023.bib · taoArchitecturePreservingProvableRepair2023.yml

Cites 50 works (2 here)

With notes (2)

PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations mullerPRIMAGeneralPrecise2022POPL · 2022

Formal verification of neural networks is critical for their safe adoption in real-world applications. However, designing a precise and scalable verifier which can handle different activation functions, realistic network architectures and relevant specifications remains an open and difficult challenge. In this paper, we take a major step forward in addressing this challenge and present a new verification framework, called PRIMA. PRIMA is both (i) general: it handles any non-linear activation function, and (ii) precise: it computes precise convex abstractions involving multiple neurons via novel convex hull approximation algorithms that leverage concepts from computational geometry. The algorithms have polynomial complexity, yield fewer constraints, and minimize precision loss. We evaluate the effectiveness of PRIMA on a variety of challenging tasks from prior work. Our results show that PRIMA is significantly more precise than the state-of-the-art, verifying robustness to input perturbations for up to 20%, 30%, and 34% more images than existing work on ReLU-, Sigmoid-, and Tanh-based networks, respectively. Further, PRIMA enables, for the first time, the precise verification of a realistic neural network for autonomous driving within a few minutes.

PDF · DOI · arXiv · pldb

Provable repair of deep neural networks sotoudehProvableRepairDeep2021PLDI · 2021

Deep Neural Networks (DNNs) have grown in popularity over the past decade and are now being used in safety-critical domains such as aircraft collision avoidance. This has motivated a large number of techniques for finding unsafe behavior in DNNs. In contrast, this paper tackles the problem of correcting a DNN once unsafe behavior is found. We introduce the provable repair problem, which is the problem of repairing a network N to construct a new network N′ that satisfies a given specification. If the safety specification is over a finite set of points, our Provable Point Repair algorithm can find a provably minimal repair satisfying the specification, regardless of the activation functions used. For safety specifications addressing convex polytopes containing infinitely many points, our Provable Polytope Repair algorithm can find a provably minimal repair satisfying the specification for DNNs using piecewise-linear activation functions. The key insight behind both of these algorithms is the introduction of a Decoupled DNN architecture, which allows us to reduce provable repair to a linear programming problem. Our experimental results demonstrate the efficiency and effectiveness of our Provable Repair algorithms on a variety of challenging tasks.

PDF · DOI · pldb

External (48)

SyReNN: A tool for analyzing deep neural networks (2023)
Artifact for the PLDI 2023 Article "Architecture-Preserving Provable Repair of Deep Neural Networks" (2023)
REASSURE (GitHub BU-DEPEND-Lab/REASSURE) (2023)
Sound and Complete Neural Network Repair with Minimality and Locality Guarantees (2022)
Training language models to follow instructions with human feedback (2022)
Memory-Based Model Editing at Scale (2022)
Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound (2022)
Gurobi Optimizer Reference Manual (2022)
Fast Model Editing at Scale (2022)
Pruning and Slicing Neural Networks using Formal Verification (2021)
Using deep learning for dermatologist-level detection of suspicious pigmented skin lesions from wide-field images (2021)
Deep learning for solving dynamic economic models (2021)
Scaling the Convex Barrier with Active Sets (2021)
NNrepair: Constraint-Based Repair of Neural Network Classifiers (2021)
Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers (2021)
An Image is Worth 16x16 Words: Transformers for Image Recognition at Scale (2021)
Globally-Robust Neural Networks (2021)
PRDNN (GitHub 95616ARG/PRDNN) (2021)
SyReNN: A Tool for Analyzing Deep Neural Networks (TACAS 2021) (2021)
Minimal Modifications of Deep Neural Networks using Verification (2020)
ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks (2020)
Editable Neural Networks (2020)
AI for Science (2020)
Language Models are Few-Shot Learners (2020)
BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding (2019)
Natural Adversarial Examples (2019)
Searching for MobileNetV3 (2019)
RoBERTa: A Robustly Optimized BERT Pretraining Approach (2019)
MNIST-C: A Robustness Benchmark for Computer Vision (2019)
PyTorch: An Imperative Style, High-Performance Deep Learning Library (2019)
An abstract domain for certifying neural networks (2019)
Benchmarking Neural Network Robustness to Common Corruptions and Perturbations (2019)
ETH Robustness Analyzer for Neural Networks (ERAN) (2019)
Correcting Deep Neural Networks with Small, Generalizing Patches (2019)
Fast and Effective Robustness Certification (2018)
Efficient Formal Safety Analysis of Neural Networks (2018)
Measuring Catastrophic Forgetting in Neural Networks (2018)
Differentiable Abstract Interpretation for Provably Robust Neural Networks (2018)
Deep Neural Network Compression for Aircraft Collision Avoidance Systems (2018)
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (2017)
Deep Residual Learning for Image Recognition (2016)
SqueezeNet: AlexNet-level accuracy with 50x fewer parameters and < 1MB model size (2016)
Deep Learning (Goodfellow, Bengio, Courville) (2016)
Very Deep Convolutional Networks for Large-Scale Image Recognition (2015)
ImageNet Classification with Deep Convolutional Neural Networks (2012)
Imagenet Large Scale Visual Recognition Challenge 2012 (ILSVRC2012) (2012)
Primal-dual methods for vertex and facet enumeration (preliminary version) (1997)
A polynomial algorithm in linear programming (Khachiyan) (1979)