Provable Repair of Deep Neural Networks

TL;DR

This paper introduces provable repair algorithms for deep neural networks that can correct unsafe behaviors while guaranteeing minimality and correctness, applicable to safety-critical domains and leveraging a novel architecture.

Contribution

The paper presents the Decoupled DNN architecture and provable repair algorithms for both finite point sets and convex polytopes, enabling minimal and verifiable network repairs.

Findings

Algorithms efficiently repair DNNs to meet safety specifications.

Provable repairs are minimal and guaranteed to satisfy the specifications.

Experimental results show effectiveness on challenging tasks.

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.