Provable repair of deep neural networks

Reference. Provable repair of deep neural networks

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.

Cite

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

BibTeX

bibtex · 15 lines

@inproceedings{sotoudehProvableRepairDeep2021,
 title = {Provable Repair of Deep Neural Networks},
 author = {Sotoudeh, Matthew and Thakur, Aditya V.},
 date = {2021-06-19},
 isbn = {978-1-4503-8391-2},
 doi = {10.1145/3453483.3454064},
 url = {https://dl.acm.org/doi/10.1145/3453483.3454064},
 urldate = {2023-11-27},
 booktitle = {Proceedings of the 42nd {{ACM SIGPLAN International Conference}} on {{Programming Language Design}} and {{Implementation}}},
 pages = {588--603},
 publisher = {ACM},
 langid = {english},
 eventtitle = {{{PLDI}} '21: 42nd {{ACM SIGPLAN International Conference}} on {{Programming Language Design}} and {{Implementation}}},
 location = {Virtual Canada}
}

hayagriva YAML (typst)

yaml · 23 lines

sotoudehProvableRepairDeep2021:
  type: article
  title: Provable Repair of Deep Neural Networks
  author:
  - Sotoudeh, Matthew
  - Thakur, Aditya V.
  date: 2021-06-19
  page-range: 588-603
  url:
    value: https://dl.acm.org/doi/10.1145/3453483.3454064
    date: 2023-11-27
  serial-number:
    doi: 10.1145/3453483.3454064
    isbn: 978-1-4503-8391-2
  language: en-US
  parent:
  - type: proceedings
    title: Proceedings of the 42nd {ACM SIGPLAN International Conference} on {Programming Language Design} and {Implementation}
    publisher:
      name: ACM
      location: Virtual Canada
  - type: conference
    title: '{PLDI} ''21: 42nd {ACM SIGPLAN International Conference} on {Programming Language Design} and {Implementation}'

Download: sotoudehProvableRepairDeep2021.bib · sotoudehProvableRepairDeep2021.yml

Cited by (1)

Architecture-Preserving Provable Repair of Deep Neural Networks taoArchitecturePreservingProvableRepair2023PLDI · 2023

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.

PDF · DOI · pldb

Cites 61 works (0 here)

External (61)

SyReNN: A Tool for Analyzing Deep Neural Networks (2021)
Editable Neural Networks (2020)
Minimal Modifications of Deep Neural Networks using Verification (2020)
Gurobi Optimizer Reference Manual (2020)
Wrongfully Accused by an Algorithm (New York Times) (2020)
Optimization and abstraction: a synergistic approach for analyzing neural network robustness (2019)
BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding (2019)
Symbolic Execution for Importance Analysis and Adversarial Generation in Neural Networks (2019)
Complexity of Linear Regions in Deep Networks (2019)
The Marabou Framework for Verification and Analysis of Deep Neural Networks (2019)
Patching Deep Neural Networks for Nonstationary Environments (2019)
TensorFuzz: Debugging Neural Networks with Coverage-Guided Fuzzing (2019)
An abstract domain for certifying neural networks (2019)
DeepHunter: a coverage-guided fuzz testing framework for deep neural networks (2019)
An inductive synthesis framework for verifiable reinforcement learning (2019)
Deep ReLU Networks Have Surprisingly Few Activation Patterns (2019)
DL2: Training and Querying Neural Networks with Logic (2019)
PyTorch: An Imperative Style, High-Performance Deep Learning Library (2019)
Natural Adversarial Examples (2019)
MNIST-C: A Robustness Benchmark for Computer Vision (2019)
Decoupling Gating from Linearity (2019)
A collection of pre-trained, state-of-the-art models in the ONNX format (github.com/onnx/models) (2019)
Feds Say Self-Driving Uber SUV Did Not Recognize Jaywalking Pedestrian In Fatal Crash (NPR) (2019)
ETH Robustness Analyzer for Neural Networks (ERAN) (2019)
Computing Linear Restrictions of Neural Networks (2019)
AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation (2018)
Identifying Medical Diagnoses and Treatable Diseases by Image-Based Deep Learning (2018)
DeepGauge: multi-granularity testing criteria for deep learning systems (2018)
DeepMutation: Mutation Testing of Deep Learning Systems (2018)
Concolic testing for deep neural networks (2018)
DeepTest (2018)
Ensemble Adversarial Training: Attacks and Defenses (2018)
Safe Reinforcement Learning via Shielding (2018)
Deep Neural Network Compression for Aircraft Collision Avoidance Systems (2018)
Measuring Catastrophic Forgetting in Neural Networks (2018)
Verifiable Reinforcement Learning via Policy Extraction (2018)
Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks (2017)
Facebook translates 'good morning' into 'attack them', leading to arrest (2017)
Safety Verification of Deep Neural Networks (2017)
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (2017)
ImageNet classification with deep convolutional neural networks (2017)
DeepXplore (2017)
A Unified View of Piecewise Linear Neural Network Verification (2017)
Automatic differentiation in PyTorch (2017)
TensorFlow: A System for Large-Scale Machine Learning (2016)
Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP 2016) (2016)
End to End Learning for Self-Driving Cars (2016)
SqueezeNet: AlexNet-level accuracy with 50x fewer parameters and <0.5MB model size (2016)
Measuring Neural Net Robustness with Constraints (2016)
Deep Learning (Goodfellow, Bengio, Courville) (2016)
US opens investigation into Tesla after fatal crash (BBC) (2016)
Explaining and Harnessing Adversarial Examples (2015)
Intriguing properties of neural networks (2014)
Optimization with absolute values (Northwestern optimization wiki) (2014)
MNIST handwritten digit database (2010)
ImageNet: A large-scale hierarchical image database (2009)
Z3: An Efficient SMT Solver (2008)
Concrete Mathematics: A Foundation for Computer Science (2nd ed.) (1994)
A polynomial algorithm in linear programming (Khachiyan, Doklady Akademii Nauk 244) (1979)
Quadratic programming with quadratic constraints (1972)
Advanced Calculus (Loomis, Sternberg) (1968)