Provable repair of deep neural networks (2021-04-09T00:00:00.000000Z)

TL;DR

The Provable Repair problem is introduced, which is the problem of repairing a network N to construct a new network N′ that satisfies a given specification, and the introduction of a Decoupled DNN architecture, which allows for provable repair to a linear programming problem.

Abstract

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.

Authors

Matthew Sotoudeh

1 papers

Aditya V. Thakur

1 papers

TL;DR

Abstract

Authors

References66 items

SyReNN: A Tool for Analyzing Deep Neural Networks

Minimal Modifications of Deep Neural Networks using Verification

Editable Neural Networks

PyTorch: An Imperative Style, High-Performance Deep Learning Library

Symbolic Execution for Importance Analysis and Adversarial Generation in Neural Networks

Computing Linear Restrictions of Neural Networks

Natural Adversarial Examples

The Marabou Framework for Verification and Analysis of Deep Neural Networks

DeepHunter: a coverage-guided fuzz testing framework for deep neural networks

Patching Deep Neural Networks for Nonstationary Environments

An inductive synthesis framework for verifiable reinforcement learning

MNIST-C: A Robustness Benchmark for Computer Vision

Deep ReLU Networks Have Surprisingly Few Activation Patterns

DL2: Training and Querying Neural Networks with Logic

Optimization and abstraction: a synergistic approach for analyzing neural network robustness

Complexity of Linear Regions in Deep Networks

An abstract domain for certifying neural networks

Deep Neural Network Compression for Aircraft Collision Avoidance Systems

Decoupling Gating from Linearity

TensorFuzz: Debugging Neural Networks with Coverage-Guided Fuzzing

AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation

DeepMutation: Mutation Testing of Deep Learning Systems

Verifiable Reinforcement Learning via Policy Extraction

Concolic Testing for Deep Neural Networks

DeepGauge: Multi-Granularity Testing Criteria for Deep Learning Systems

Identifying Medical Diagnoses and Treatable Diseases by Image-Based Deep Learning

A Unified View of Piecewise Linear Neural Network Verification

Automatic differentiation in PyTorch

Safe Reinforcement Learning via Shielding

DeepTest: Automated Testing of Deep-Neural-Network-Driven Autonomous Cars

Measuring Catastrophic Forgetting in Neural Networks

Ensemble Adversarial Training: Attacks and Defenses

DeepXplore: Automated Whitebox Testing of Deep Learning Systems

Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks

Safety Verification of Deep Neural Networks

Measuring Neural Net Robustness with Constraints

End to End Learning for Self-Driving Cars

Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP 2016)

SqueezeNet: AlexNet-level accuracy with 50x fewer parameters and <1MB model size

Explaining and Harnessing Adversarial Examples

Intriguing properties of neural networks

ImageNet: A large-scale hierarchical image database

Z3: An Efficient SMT Solver

Concrete mathematics - a foundation for computer science

Quadratic programming with quadratic constraints

"PROOF"

Gurobi Optimizer Reference Manual

Wrongfully Accused by an Algorithm

2016. US opens investigation into Tesla after fatal crash

BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding

A collection of pre-trained, state-of-the-art models in the ONNX format

ETH Robustness Analyzer for Neural Networks (ERAN)

Feds Say Self-Driving Uber SUV Did Not Recognize Jaywalking Pedestrian In Fatal Crash

Facebook translates ’good morning’ into ’attack them’, leading to arrest

Deep Learning

Optimization with absolute values

MNISThandwritten digit database

Concrete mathematics - a foundation for computer science (2. ed.)

A polynomial algorithm in linear programming

Advanced calculus

This Paper Is Included in the Proceedings of the 12th Usenix Symposium on Operating Systems Design and Implementation (osdi '16). Tensorflow: a System for Large-scale Machine Learning Tensorflow: a System for Large-scale Machine Learning

RQ1 How effective is PR in finding weights that satisfy the repair specification?

Conference’17, July 2017, Washington, DC, USA

Hinton . 2017 . Ima - geNet classification with deep convolutional neural networks

RQ2 How much does PR cause performance drawdown , on regions of the input space not repaired?

Field of Study

Journal Information

Name

Venue Information

Name

Type

URL

Alternate Names