Year: 2022

Abstract:
We present a novel methodology for repairing neural networks that use ReLU activation functions. Unlike existing methods that rely on modifying the weights of a neural network which can induce a global change in the function space, our approach applies only a localized change in the function space while still guaranteeing the removal of the buggy behavior. By leveraging the piecewise linear nature of ReLU networks, our approach can efficiently construct a patch network tailored to the linear region where the buggy input resides, which when combined with the original network, provably corrects the behavior on the buggy input. Our method is both sound and complete – the repaired network is guaranteed to fix the buggy input, and a patch is guaranteed to be found for any buggy input. Moreover, our approach preserves the continuous piecewise linear nature of ReLU networks, automatically generalizes the repair to all the points including other undetected buggy inputs inside the repair region, is minimal in terms of changes in the function space, and guarantees that outputs on inputs away from the repair region are unaltered. On several benchmarks, we show that our approach significantly outperforms existing methods in terms of locality and limiting negative side effects.

heading: 1 INTRODUCTION
text: Deep neural networks (DNNs) have demonstrated impressive performances on a wide variety of applications ranging from transportation Bojarski et al. (2016) to health care Shahid et al. (2019). However, DNNs are not perfect. In many cases, especially when the DNNs are used in safety-critical contexts, it is important to correct erroneous outputs of a DNN as they are discovered after training. For instance, a neural network in charge of giving control advisories to the pilots in an aircraft collision avoidance system, such as the ACAS Xu network from Julian et al. (2019), may produce an incorrect advisory for certain situations and cause the aircraft to turn towards the incoming aircraft, thereby jeopardizing the safety of both airplanes. In this paper, we consider the problem of neural network repair, i.e. given a trained neural network and a set of buggy inputs (inputs on which the neural network produces incorrect predictions), repair the network so that the resulting network on those buggy inputs behave according to some given correctness specification. Ideally, the changes to the neural network function should be small so that the outputs on other inputs are either unchanged or altered in a small way. Existing efforts on neural network repair roughly fall into the following three categories.
1. Retraining/fine-tuning. The idea is to retrain or fine-tune the network with the newly identified buggy inputs and the corresponding corrected outputs. Methods include counterexample-guided data augmentation Dreossi et al. (2018); Ren et al. (2020), editable training Sinitsin et al. (2020) and training input selection Ma et al. (2018). One major weakness of these approaches is the lack of formal guarantees – at the end of retraining/fine-tuning, there is no guarantee that the given buggy inputs are fixed and no new bugs are introduced. In addition, retraining can be very expensive and requires access to the original training data which is impractical in cases where the neural network is obtained from a third party or the training data is private. Fine-tuning, on the other hand, often faces the issue of catastrophic forgetting Kirkpatrick et al. (2017).
2. Direct weight modification. These approaches directly manipulate the weights in a neural network to fix the buggy inputs. The repair problem is typically cast into an optimization problem or a verification problem. For example, Dong et al. (2020) proposes to minimize a loss defined on the buggy inputs. Goldberger et al. (2020) uses an SMT solver to identify minimal weight changes to the output layer of the network so that the undesirable behaviors are removed. In general, the optimization-based approach cannot guarantee removal of the buggy behaviors, and the verificationbased approach does not scale beyond networks of a few hundred neurons. In addition, both approaches suffer from substantial accuracy drops on normal inputs since weight changes may be a poor proxy for changes in the function space.
3. Architecture extension. The third category of approaches extends the given NN architecture, such as by introducing more weight parameters, to facilitate more efficient repairs. The so-called Decoupled DNN architecture Sotoudeh & Thakur (2021) is the only work we know that falls into this category. Their idea is to decouple the activations of the network from values of the network by augmenting the original network. Their construction allows the formulation of any single-layer repair as an linear programming (LP) problem. The decoupling, however, causes the repaired network to become discontinuous (in the functional sense). In addition, it still cannot isolate the output change to a single buggy input from the rest of the inputs.
In addition to the aforementioned limitations, a common weakness that is shared amongst these methods is that the induced changes, as a result of either retraining or direct weight modification, are global. This means that a correct behavior on another input, regardless of how far it is away from the buggy input, may not be preserved by the repair. Worse still, the repair on a new buggy input can end up invalidating the repair on a previous buggy input. The fundamental issue here is that limiting the changes to a few weights or a single layer only poses a structural constraint (often for ease of computation); it does not limit the changes on the input-output mapping of the neural network. It is known that even a single weight change can have a global effect on the output of a neural network.
In this paper, we propose REASSURE, a novel methodology for neural network repair with locality, minimality, soundness and completeness guarantees. Our methodology targets continuous piecewise linear (CPWL) neural networks, specifically those that use the ReLU activation functions. The key idea of our approach is to leverage the CPWL property of ReLU networks to synthesize a patch network tailored to the linear region where the buggy input resides, which when combined with the original network, provably corrects the behavior on the buggy input. Our approach is both sound and complete – the repaired network is guaranteed to fix the buggy input, and a patch is guaranteed to be found for any buggy input. Moreover, our approach preserves the CPWL nature of ReLU networks, automatically generalizes the repair to all the points including other undetected buggy inputs inside the repair region, is minimal in terms of changes in the function space, and guarantees that outputs on inputs away from the repair region are unaltered. Figure 1 provides an illustrative comparison of our approach with other methods. Table 1 compares our approach with representative related works in terms of theoretical guarantees. We summarize our contributions below.
• We present REASSURE, the first sound and complete repair methodology for ReLU networks with strong theoretical guarantees.
• Our technique synthesizes a patch network, which when combined with the original neural network, provably corrects the behavior on the buggy input. This approach is a significant departure from existing methods that rely on retraining or direct weight manipulation.
• Our technique is both effective and efficient – across a set of benchmarks, REASSURE can efficiently correct a set of buggy inputs or buggy areas with little or no change to the accuracy and overall functionality of the network.

heading: 2 BACKGROUND

heading: 2.1 DEEP NEURAL NETWORKS
text: An R-layer feed-forward DNN f = κR ◦ σ ◦ κR−1 ◦ ... ◦ σ ◦ κ1 : X → Y is a composition of linear functions κr, r = 1, 2, ..., R and activation function σ, where X ⊆ Rm is a bounded input domain and Y ⊆ Rn is the output domain. Weights and biases of linear function {κr}r=1,2,...,R are parameters of the DNN.
We call the first R− 1 layers hidden layers and the R-th layer the output layer. We use zij to denote the i-th neuron (before activation) in the j-th hidden layer.
In this paper, we focus on ReLU DNNs, i.e. DNNs that use only the ReLU activation functions. It is known that an Rm → R function is representable by a ReLU DNN if and only if it is a continuous piecewise linear (CPWL) function Arora et al. (2016). The ReLU function is defined as σ(x) = max(x, 0). We say that σ(x) is activated if σ(x) = x.

heading: 2.2 LINEAR REGIONS
text: A linear region A is the set of inputs that correspond to the same activation pattern in a ReLU DNN f Serra et al. (2017). Geometrically, this corresponds to a convex polytope, which is an intersection of half spaces, in the input space X on which f is linear. We use f |A to denote the part of f on A.

heading: 2.3 CORRECTNESS SPECIFICATION
text: A correctness specification Φ = (Φin,Φout) is a tuple of two polytopes, where Φin is the union of some linear regions and Φout is a convex polytope. A DNN f is said to meet a specification Φ = (Φin,Φout), denoted as f |= Φ, if and only if ∀x ∈ Φin, f(x) ∈ Φout. Example 1. For a classification problem, we can formally write the specification that “the prediction of any point in an area A is class k” as Φ = (Φin,Φout), where Φin = A and Φout = {y ∈ Rn | yk ≥ yi,∀i 6= k}1.

heading: 2.4 PROBLEM DEFINITION
text: In this paper, we consider the following two repair problems.
Definition 1 (Area repair). Given a correctness specification Φ = (Φin,Φout) and a ReLU DNN f 6|= Φ, the area repair problem is to find a modified ReLU DNN f̂ such that f̂ |= Φ.
1Note that here y is the output of the layer right before the softmax layer in a classification network.
Note that we do not require f̂ to have the same structure or parameters as f in this definition. If Φin contains a single (buggy) linear region, we refer to this as single-region repair. If Φin contains multiple (buggy) linear regions, we refer to it as multi-region repair. Definition 2 (Point-wise repair). Given a set of buggy inputs {x̃1, . . . , x̃L} ⊂ Φin with their corresponding correct outputs {y1, . . . , yL} and a ReLU DNN f , the point-wise repair problem is to find a modified ReLU DNN f̂ such that ∀i, f̂(x̃i) = yi.
We call the minimal variants of area repair and point-wise repair minimal area repair and minimal point-wise repair respectively. Minimality here is defined with respect to the maximum distance between f and f̂ over the whole input domain X . A point-wise repair can be generalized to an area repair through the following result.

heading: 2.5 FROM BUGGY INPUTS TO BUGGY LINEAR REGIONS
text: The linear region where an input x resides can be computed as follows. Lemma 1. Lee et al. (2019) Consider a ReLU DNN f and an input x ∈ X . For every neuron zij , it induces a feasible set
Aij(x) = { {x̄ ∈ X|(Oxzij)T x̄+ zij − (Oxzij)Tx ≥ 0} if zij ≥ 0 {x̄ ∈ X|(Oxzij)T x̄+ zij − (Oxzij)Tx ≤ 0} if zij < 0
(1)
The set A(x) = ∩i,jAij(x) is the linear region that includes x. Note that A(x) is essentially the H-representation of the corresponding convex polytope.

heading: 2.6 REPAIR DESIDERATA
text: We argue that an effective repair algorithm for ReLU DNN should satisfy the following criteria.
1. Preservation of CPWL: Given that the original network f models a CPWL function, the repaired network f̂ should still model a CPWL function. 2. Soundness: A sound repair should completely remove the known buggy behaviors, i.e. it is a solution to the point-wise repair problem defined in Definition 2. 3. Completeness: Ideally, the algorithm should always be able find a repair for any given buggy input if it exists. 4. Generalization: If there exists another buggy input x̃′ in the neighborhood of x̃ (e.g. the same linear region), then the repair should also fix it. For example, suppose we have an x̃ that violates a specification which requires the output to be within some range. It is almost guaranteed that there exists another (and infinitely many) x̃′ in the same linear region that also violates the specification. 5. Locality: We argue that a good repair should only induce a localized change to f in the function space. For example, in the context of ReLU DNN, if a linear region B does not border the repair regionA, i.e. B∩A = ∅, then f̂ |B(x) = f |B(x). 6. Minimality: Some notion of distance between f and f̂ such as max |f− f̂ | should be minimized. Note that this is a significant departure from existing methods that focus on minimizing the change in weights which has no guarantee on the amount of change in the function space. 7. Limited side effect: Repairing a buggy point should not adversely affect points that were originally correct. For example, repairing a buggy input x̃ in region A should not change another region from correct to incorrect. Formally, for any linear region C who is a neighbor of A, i.e. C ∩ A 6= ∅, if f |C |= Φ, then f̂ |C |= Φ. 8. Efficiency: The repair algorithm should terminate in polynomial time with respect to the size of the neural network and the number of buggy inputs.

heading: 3 OUR APPROACH
text: We will first describe our approach to single-region repair and then present our approach to multiregion repair which builds on results obtained from the single-region case.
Given a linear region A, our overarching approach is to synthesize a patch network hA such that f̂ = f + hA and f̂ |= Φ. The patch network hA is a combination of two sub-networks: a support network gA, which behaves like a characteristic function, to determine whether an input is inA, and an affine patch function network pA(x) = cx+ d to ensure (f + pA) |= Φ on A.

heading: 3.1 RUNNING EXAMPLE
text: We use the following example to illustrate our idea. Example 2. Consider repairing the ReLU DNN f in Figure 2 according to the correctness specification Φ : ∀x ∈ [0, 1]2, y ∈ [0, 2]. The DNN consists of a single hidden layer with two neurons z1 and z2, where y = σ(z1) + σ(z2), z1 = x1 + 2x2 − 1 and z2 = 2x1 − x2.
The only linear region that violates our specification is A = {x | 1 ≥ x1, 1 ≥ x2, x1 + 2x2 − 1 ≥ 0, 2x1 − x2 ≥ 0}. ( x̃ = (0.9, 0.9) ∈ [0, 1]2 but f(x̃) = 2.6 /∈ [0, 2]) The network f(x) on the linear region A is the affine function f |A(x) = 3x1 + x2 − 1. Our algorithm first sets up an affine function pA(x) that minimally repairs f on A, such that ∀x ∈ A, f(x) + pA(x) ∈ [0, 2]. Later in the paper, we will show pA(x) can be found by solving a LP problem. The resulting patch function is pA(x) = − 12x1 − 1 2x2.
However, directly apply f(x) + pA(x) as the patch network will have side effects on areas outside of A. Our strategy is to combine pA(x) with a support network gA(x) which outputs 1 on A and drops to 0 quickly outside of A. The final repaired network is f(x) + σ(pA(x) + gA(x, 10) − 1)− σ(−pA(x) + gA(x, 10)− 1). This structure makes pA almost only active on A and achieve a localized repair. Observe that this is still a ReLU DNN.

heading: 3.2 SUPPORT NETWORKS
text: Support networks are neural networks with a special structure that can approximate the characteristic function of a convex polytope. They are keys to ensuring localized repairs in our algorithm.
Assume that the linear region we need to repair isA = {x |aix ≤ bi, i ∈ I}, where |I| is the number of linear inequalities. The support network of A is defined as:
gA(x, γ) = σ( ∑ i∈I g(bi − aix, γ)− |I|+ 1) (2)
where g(x, γ) = σ(γx + 1) − σ(γx) and γ ∈ R is a parameter of our algorithm that controls how quickly gA(x, γ) goes to zero outside of A. Remark: For any x ∈ A, we have gA(x, γ) = 1, i.e. the support network is fully activated. For any x /∈ A, if for one of i ∈ I , we have aix− bi ≤ −1/γ, then gA(x, γ) = 0. Observe that gA(x, γ) is not zero when x is very close to A due to the requirement for preserving CPWL. In Theorem 3, we prove that we can still guarantee limited side effects on the whole input domain outside of A with this construction.

heading: 3.3 AFFINE PATCH FUNCTIONS
text: We consider an affine patch function pA(x) = cx+d, where matrix c and vector d are undetermined coefficients. In a later section, the design of patch network will ensure that on the patch area A, the
repaired network is f(x) + pA(x). We will first consider finding appropriate c and d such that f(x) + pA(x) satisfy the specification on A. To satisfy the specification Φ, we need f(x) + pA(x) ∈ Φout for all x ∈ A. To obtain a minimal repair, we minimize maxx∈A |pA(x)|. Thus, we can formulate the following optimization problem{
minc,d maxx∈A |pA(x)| = |cx+ d| (c, d) ∈ {(c, d) | f(x) + cx+ d ∈ Φout,∀x ∈ A}
(3)
Notice that this is not a LP since both c and x are variables and we have a cx term in the objective.
In general, one can solve it by enumerating all the vertices of A. Suppose that {vs|s = 1, 2, ..., S} is the set of vertices of A. Since Φout is a convex polytope, we have
f(x) + pA(x) ∈ Φout for all x ∈ A ⇔ f(vs) + pA(vs) ∈ Φout for s = 1, 2, ..., S. (4) and
maxx∈A |cx+ d| = maxs=1,2,...,S |cvs + d| (5) Hence, we can solve the following equivalent LP. minc,dH
H ≥ (cvs + d)i, H ≥ −(cvs + d)i, for s = 1, 2, ..., S and i = 1, 2, ...,m f(vs) + pA(vs) ∈ Φout, for s = 1, 2, ..., S
(6)
where H ∈ R and will take maxs=1,2,...,S |cvs + d| when optimal. In general, the number of vertices of a convex polytope can be exponential in the size of its Hrepresentation Henk et al. (1997) and enumerating the vertices of a convex polytope is known to be expensive especially when the input dimension is large Bremner (1997). In Appendix 7.1, we show that we can solve programming 3 via LP without vertex enumeration for many useful cases such as the classification problem in Example 1 and make our algorithm much more efficient.

heading: 3.4 SINGLE-REGION REPAIRS
text: With a support network gA and an affine patch function pA, we can synthesize the final patch network as follows:
hA(x, γ) = σ(pA(x) +K · gA(x, γ)−K)− σ(−pA(x) +K · gA(x, γ)−K) (7) where K is a vector where every entry is equal to the upper bound of {|pA(x)|+∞|x ∈ X}. Remark: For x ∈ A, gA(x, γ) = 1, then we have hA(x, γ) = σ(pA(x)) − σ(−pA(x)) = pA(x). For x /∈ A, gA(x, γ) goes to zero quickly if γ is large. When gA(x, γ) = 0, we have hA(x, γ) = σ(pA(x)−K)− σ(−pA(x)−K) = 0.
The repaired network f̂(x) = f(x) + hA(x, γ). Since f and hA are both ReLU DNNs, we have f̂ is also a ReLU DNN. We will give the formal guarantees on correctness in Theorem 1.

heading: 3.5 MULTI-REGION REPAIRS
text: Suppose there are two linear regions, A1 and A2, that need to be repaired, and we have generated the affine patch function pA1(x) for A1 and pA2(x) for A2.
IfA1 ∩A2 = ∅, then we can repair f(x) with f̂(x) = f(x) + hA1(x, γ) + hA2(x, γ) directly, since hA1(x, γ) and hA2(x, γ) will not be nonzero at the same time when γ is large enough.
However, if A1 ∩ A2 6= ∅, for any x ∈ A1 ∩ A2, both hA1(x, γ) and hA2(x, γ) will alter the value of f on x, which will invalidate both repairs and cannot guarantee that the repaired DNN will meet the specification Φ. To avoid such over-repairs, our strategy is to first repair A1 ∪ A2 with pA1(x), and then repair A2 with pA2(x)− pA1(x). Figure 3 provides an illustration of a three-region case. In general, for multi-region repair, we note {Al}l=1,2,...,L are all the buggy linear regions. Then we compute the support network gAl(x, γ) and affine patch function pAl(x) for each Al. Note that this computation can be done in parallel.
Once we have gAl(x, γ) and pAl(x), we can “stitch” multiple local patches into a final patch as follows.
h(x, γ) = ∑ l [σ(pAl(x)− pAl−1(x) + max j≥l {gAj (x, γ)}Kl −Kl)
−σ(−pAl(x) + pAl−1(x) + max j≥l {gAj (x, γ)}Kl −Kl)] (8)
where Kl is the upper bound of {|pAl(x)− pAl−1(x)|∞|x ∈ X} and pA0(x) = 0. Remark: maxj≥l{gAj (x, γ)} is a support function for ∪j≥lAj and its value is 1 for any x ∈ ∪j≥lAj .

heading: 4 THEORETICAL GUARANTEES
text: In this section, we present the theoretical guarantees that REASSURE provides, and point the readers to proofs of the theorems in the Appendix.
Theorem 1 (Soundness). The repaired DNN f̂ returned by REASSURE is guaranteed to satisfy the specification Φ. Theorem 2 (Completeness). REASSURE can always find a solution to the minimal point-wise repair or the minimal area repair problem.
For any A, the support network ensures that the patch network goes to zero quickly when x is away from A. However, it still makes a small change on the neighbors of A. The following theorem shows that for a big enough γ, the patch network would not change a correct region into incorrect. Theorem 3 (Limited Side Effect). Given a correctness property Φ = (Φin,Φout), a patch region A and the corresponding patch network h(x, γ), there exists a positive number Γ such that for any γ ≥ Γ, we have
1. for any linear region B, if B ∩ A = ∅, then f̂(x, γ) = f(x);
2. for any linear region C who is a neighbor ofA (C∩A 6= ∅), if f |C |= Φ, then f̂C(x, γ) |= Φ. Corollary 1 (Incremental Repair). For multiple-region repair, the patch for a new region A′ would not cause a previous patched region A to become incorrect. Theorem 4 (Minimum Repair). For any ReLU DNN f̃ , which is linear on a patch region A and satisfies the specification Φ, there exists a positive number Γ, such that for all γ ≥ Γ,
max x∈X |f̃(x)− f(x)| ≥ max x∈X |hA(x, γ)|. (9)
Theorem 5 (Polynomial-Time Efficiency). REASSURE terminates in polynomial-time in the size of the neural network and the number of buggy linear regions when Φout takes the form of {y | ql ≤ Py ≤ qu} where P is a full row rank matrix and −∞ ≤ ql[i] ≤ qu[i] ≤ +∞ (ql[i] and qu[i] are the i-th elements of ql and qu respectively).

heading: 5 EXPERIMENTS
text: In this Section, we compare REASSURE with state-of-the-art methods on both point-wise repairs and area repairs. The experiments were designed to answer the following questions: (Effectiveness)
How effective is a repair in removing known buggy behaviors? (Locality) How much side effect (i.e. modification outside the patch area in the function space) does a repair produce? (Function Change) How much does a repair change the original neural network in the function space? (Performance) Whether and how much does a repair adversely affect the overall performance of the neural network?
We consider the following evaluation criteria:
1. Efficacy (E): % of given buggy points or buggy linear regions that are repaired.
2. Norm Difference (ND): average normalized norm (L∞ or L2) difference between the original DNN and the repaired DNN on a set of inputs (e.g. training and testing data; more details in the tables). We use ND to measure how a repair change the original neural network on function space.
3. Norm Difference on Patch Area (NDP): average normalized norm (L∞ or L2) difference between the original DNN and the repaired DNN on patch areas (calculated on random sampled points on patch areas or near the buggy points; details in the tables). We use NDP to measure the locality of a repair.
4. Accuracy (Acc): accuracy on training or testing data to measure the extent to which a repair preserves the performance of the original neural network.
5. Negative Side Effect (NSE): NSE is only for area repair. It is the percentage of correct linear regions (outside of patch area) that become incorrect after a repair. If a repair has a nonzero NSE, the new repair may invalidate a previous repair and lead to a circular repair problem.
All experiments were run on an Intel Core i5 @ 3.4 GHz with 32 GB of memory. We use Gurobi Gurobi Optimization, LLC (2021) to solve the linear programs.
We compared REASSUREwith the representative related works in Table 1. REASSURE, MDNN and PRDNN guarantee to repair all the buggy points (linear regions). Retrain and Fine-Tuning cannot guarantee 100% efficacy in general and we run them until all the buggy points are repaired.

heading: 5.1 POINT-WISE REPAIRS: MNIST
text: We train a ReLU DNN on the MNIST dataset LeCun (1998) as the target DNN. The goal of a repair is to fix the behaviors of the target DNN on buggy inputs that are found in the test dataset. Thus, the repaired DNN is expected to produce correct predictions for all the buggy inputs.
The results are shown in Table 2. REASSURE achieves almost zero modification outside the patch area (ND) amongst all four methods. In addition, REASSURE produces the smallest modification on the patch area (NDP) and preserves the performance of the original DNN (almost no drop on Acc).

heading: 5.2 AREA REPAIRS: HCAS
text: To the best of our knowledge, Sotoudeh & Thakur (2021) is the only other method that supports area repairs. In this experiment, we compare REASSURE with Sotoudeh & Thakur (2021) on an experiment where the setting is similar to the 2D Polytope ACAS Xu repair in their paper.
Sotoudeh & Thakur (2021) does not include a vertex enumeration tool (which is required for setting up their LP problem) in their code. We use pycddlib Troffaes (2018) to perform the vertex enumeration step when evaluating PRDNN. Note that the vertex enumeration tool does not affect the experimental results except running time.
We consider an area repair where the target DNN is the HCAS network (simplified version of ACAS Xu)2 N1,4 (previous advisory equal to 1 and time to loss of vertical separation equal to 20s) from Julian & Kochenderfer (2019). We use Specification 1 (details in Appendix 7.4), which is similar to Property 5 in Katz et al. (2017). We compute all the linear regions for N1,4 in the area Φin of Specification 1 and 87 buggy linear regions were found. We apply both REASSURE and PRDNN to repair those buggy linear regions. We use Specification 2 (details in Appendix 7.4), the dual of Specification 1, to test the negative side effect (NSE) of a repair.
The results are shown in Table 3. Both REASSURE and PRDNN successfully repair all the buggy linear regions. REASSURE produces repairs that are significantly better in terms of locality (ND), minimality (NDP) and performance preservation (Acc).

heading: 5.3 FEATURE-SPACE REPAIRS
text: In general, when repairing a large DNN with a high input dimension, the number of linear constraints for one patch area A will be huge and pose a challenge to solving the resulting LP. One advantage of our approach, which can be used to mitigate this problem, is that it allows for point-wise and area repairs in the feature space in a principled manner, i.e. constructing a patch network starting from an intermediate layer. This approach still preserves soundness and completeness, and is fundamentally different from just picking a single layer for repair in PRDNN or MDNN. Experimental results on repairing AlexNet Krizhevsky et al. (2012) for the ImageNet dataset Russakovsky et al. (2015) in Appendix 7.4 show REASSURE (feature space) is still significantly better in term of locality(ND) and minimality (NDP).

heading: 6 CONCLUSION
text: We have presented a novel approach for repairing ReLU DNNs with strong theoretical guarantees. Across a set of benchmarks, our approach significantly outperforms existing methods in terms of efficacy, locality, and limiting negative side effects. Future directions include further investigation on feature-space repairs and identifying a lower-bound for γ.
2The technique in PRDNN for computing linear regions does not scale beyond two dimensions as stated in their paper. The input space of HCAS is 3D and that of ACAS Xu is 5D so we use HCAS in order to run their tool in our evaluation of area repairs.

heading: 7 APPENDIX

heading: 7.1 REPAIR VIA LINEAR PROGRAMMING
text: We consider the case Φout can be expressed as {y |ql ≤ Py ≤ qu} where P is a full row rank matrix and −∞ ≤ ql[i] ≤ qu[i] ≤ +∞ (ql[i] and qu[i] are the i-th elements of ql and qu respectively). Consider the following optimization problem.{
minT maxx∈A |T (f(x)− f(x)| ql ≤ P (T (f(x))) ≤ qu,∀x ∈ A
(10)
where T : Rn → Rn is a linear transformation on the DNN’s output space Rn. Theorem 6. On linear region A, we have f |A(x) = f1x + f2 for some matrix f1 and vector f2. Assuming that f1 is full rank3, the optimization problem in (3) and the optimization problem in (10) are equivalent.
Note that ql ≤ P (T (f(x))) ≤ qu can be achieved row by row. Thus, we can find a one-dimensional linear transformation via LPs and combine them into a single linear transformation to solve optimization problem 10.
For every row of P , say the i-th row, we can check the lower bound and upper bound of {P (f(x)) | ∀x ∈ A} on the i-th dimension by solving the following LP problems
lb[i] = min x∈A P [i](f(x)) ub[i] = max x∈A P [i](f(x)) (11)
where P [i] is the i-th row of P .
Then for each row i, we take a minimal linear transformation V [i](x) = v1[i](x) + v2[i] to transfer interval [lb[i], ub[i]] inside interval [ql[i], qu[i]]. We can take v1[i] = 1 if qu[i]− ql[i] > ub[i]− lb[i], else v1[i] = qu[i]−ql[i] ub[i]−lb[i] . And v2[i] = ql[i]− v1[i]lb[i] if |ql[i]− v1[i]lb[i]| ≤ |v1[i]ub[i]− qu[i]|, else v1[i]ub[i]− qu[i]. Since matrix P is full row rank, we can find a linear transformation T that is equivalent to V :
T = P̂−1V P̂ ⇒ P (T (f(x))) = V (P (f(x))) (12)
where P̂ = [
P P⊥
] is an orthogonal extension of P (P and P⊥ are orthogonal to each other and
P̂ is a full rank square matrix).
Once we have T , we can obtain an affine patch function pA(x) = T (f(x))− f(x).
7.2 THE REASSURE ALGORITHM
Algorithm 1 REASSURE Input: A specification Φ = (Φin,Φout), a ReLU DNN f and a set of buggy points {x̃1, . . . , x̃L} ⊂ Φin. Output: A repaired ReLU DNN f̂ .
1: for l = 1 to L do 2: Generate the patch area Al from buggy point x̃l according to Equation (1); 3: Generate a support network gA according to Equation (2); 4: Solve the linear programming problem (6) to find the optimal affine patch network pA. 5: end for 6: Combine all support networks gAl and the corresponding patch networks pAl to get the overall
patch network h according to Equation (8). 7: return f̂ = f + h
3Note that for neural networks that are trained by a stochastic method, with probability one f1 is full rank.

heading: 7.3 PROOFS OF THEOREMS
text: We prove Theorem 1 after Corollary 1, since the proof of Theorem 1 uses the result of Corollary 1. Theorem 6. On linear region A, we have f |A(x) = f1x + f2 for some matrix f1 and vector f2. Assuming that f1 is full rank4, the optimization problem in (3) and the optimization problem in (10) are equivalent.
Proof. On one side, for any c, d, since f1 is full rank, there exists a linear transformation T , such that T (f(x)) = T (f1x+ f2) = (f1 + c)x+ (f2 + d) = f(x) + cx+ d.
On the other side, for any T , since T (f(x)) − f(x) is linear, there exist c, d, such that cx + d = T (f(x))− f(x).
Lemma 2. The repaired DNN f̂ returned by REASSURE is guaranteed to satisfy the specification Φ on patch area A in single-region repair case.
Proof. By the definition of pA, we have f(x) + pA(x) ∈ Φout for all x ∈ A. For any x ∈ A, we have gA(x, γ) = 1 and hA(x, γ) = σ(pA(x)) − σ(−pA(x)) = pA(x). Therefore,
f̂(x) = f(x) + hA(x, γ) = f(x) + pA(x) ∈ Φout (13)
Thus, the patched neural network f̂ meets the specification Φ on A.
Theorem 2 (Completeness). REASSURE can always find a solution to the minimal point-wise repair or the minimal area repair problem.
Proof. For every patch area A, we can always find a support network gA. For any Φout and A, there exists an affine function pA such that pA(x) ∈ Φout,∀x ∈ A. Therefore, the LP (6) is always feasible and REASSURE can find an affine patch function pA.
Once we have gA and pA for patch area A, REASSURE returns a patch network either by Equation (7) or by Equation (8).
Theorem 3 (Limited Side Effect). Given a correctness property Φ = (Φin,Φout), a patch region A and the corresponding patch network h(x, γ), there exists a positive number Γ such that for any γ ≥ Γ, we have
1. for any linear region B, if B ∩ A = ∅, then f̂(x, γ) = f(x);
2. for any linear region C who is a neighbor ofA (C∩A 6= ∅), if f |C |= Φ, then f̂C(x, γ) |= Φ.
Proof. Since a multi-region repair is a composition of multiple singe-region repairs according to Equation (8), we can prove the limited side effect of a multi-region repair by proving the limited side effect of its constituent singe-region repairs. Below, we prove the limited side effect of a singeregion repair.
Consider patch area A = {x | aix ≤ bi, i ∈ I} and A>0(γ) = {x | h(x, γ) > 0}. 1. Since the number of neighbors for A are finite, we can take a big enough γ, such that for any B, if B ∩ A = ∅, B ∩ A>0(γ) = ∅. Thus, we have f̂(x, γ) = f(x) on B.
2. For any linear region C who is a neighbor of A, i.e. C 6= A and C ∩ A 6= ∅, f̂ is no longer a linear function on C, since there are some hyperplanes introduced by our repair that will divide C into multiple linear regions.
Specifically, those hyperplanes are {x | γ(aix− bi) + 1 = 0} for i ∈ I , {x | ∑
i∈I g(aix− bi, γ)− |I|+ 1 = 0}, {x | p(x) +K · gA(x, γ)−K = 0} and {x | − p(x) +K · gA(x, γ)−K = 0}. For any point x in those hyperplanes, it will fall into one of the following four cases.
4Note that for neural networks that are trained by a stochastic method, with probability one f1 is full rank.
(a) x ∈ {x | γ(aix − bi) + 1 = 0} for some i ∈ I , then gA(x, γ) = 0, h(x, γ) = 0 and f̂(x) ∈ Φout;
(b) x ∈ {x | ∑
i∈I g(aix − bi, γ) − |I| + 1 = 0}, then gA(x, γ) = 0, h(x, γ) = 0 and f̂(x) ∈ Φout;
(c) x ∈ {x | p(x) + K · gA(x, γ) − K = 0}, then p(x) = K − K · gA(x, γ) ≥ 0, −p(x) +K · gA(x, γ)−K ≤ 0, h(x, γ) = 0 and f̂(x) ∈ Φout;
(d) x ∈ {x | − p(x) +K · gA(x, γ)−K}, then p(x) = K · gA(x, γ)−K ≤ 0, p(x) +K · gA(x, γ)−K ≤ 0, h(x, γ) = 0 and f̂(x) ∈ Φout;
By the above analysis, we have f̂(x) ∈ Φout for the boundary of the new linear regions. Since f̂ is linear on the new linear regions and Φout is convex, f̂(x) ∈ Φout for any x ∈ C.
Remark: By Theorem 3, we have that a patch would not change a correct linear region to an incorrect one.
Corollary 1 (Incremental Repair). For multiple-region repair, the patch for a new region A′ would not cause a previous patched region A to become incorrect.
Proof. After applying the patch to linear region A, we have that the resulting network is correct on A. When applying a new patch to another linear region A′, by Theorem 3, the new patch would not make a correct linear region A incorrect.
Theorem 1 (Soundness). The repaired DNN f̂ returned by REASSURE is guaranteed to satisfy the specification Φ.
Proof. The proof has two parts:
1. to show that f̂ satisfies the specification Φ on A, and
2. to show that f̂ satisfies the specification Φ outside of A.
Part 1:
Lemma (2) shows f̂ satisfy the specification Φ for single-region repair on A. For the multi-region case, consider a set of buggy linear regions ∪1≤l≤IAl with the corresponding support neural network gAl and affine patch function pAl for each Al. For the multi-region repair construction in Equation (8), we refer to σ(pAj −pAj−1 +maxk≥j{gAk}Kj−Kj) as the j-th patch and f̂j = f + ∑ j′≤j σ(pAj′ − pAj′−1 + maxk≥j′{gAk}Kj − Kj) as the network after the j-th patch.
For any x in patch area ∪1≤l≤IAl, we can find a j such that x ∈ Aj but x /∈ Ak for all k > j. After the first j patches σ(pA1(x) + maxk≥1{gAk(x, γ)}K1 − K1), σ(pA2(x) − pA1(x) + maxk≥2{gAk(x, γ)}K2 − K2), ... , σ(pAj (x) − pAj−1(x) + maxk≥j{gAk(x, γ)}Kj − Kj), the DNN’s output at x becomes f̂j(x) = f(x) + pAj (x) which meets our specification Φ at x by the definition of pAj (x).
Since x /∈ Ak for all k > j, then by Corollary 1, the rest of the patches would not change a correct area to an incorrect area. Therefore, we have the final patched neural network f̂ meets specification Φ on ∪1≤l≤IAl. Part 2:
To show that f̂ satisfies Φ outside of A.
For any x outside the patch area ∪1≤l≤IAl, we have x lies on a correct linear region (linear region that satisfies the specification Φ). By Theorem 3, we have either f̂(x) = f(x) or f̂(x) ∈ Φout. Therefore, f̂ satisfies Φ outside of A.
Theorem 4 (Minimum Repair). For any ReLU DNN f̃ , which is linear on a patch region A and satisfies the specification Φ, there exists a positive number Γ, such that for all γ ≥ Γ,
max x∈X |f̃(x)− f(x)| ≥ max x∈X |hA(x, γ)|. (14)
Proof. We consider the general case where the linear patch function is obtained from Equation (3).
For any DNN f̃ , which is linear on patch region A and satisfies the specification Φ, we have maxx∈A |f̃ − f | ≥ maxx∈A |cx+ d| = maxx∈A |hA(., γ)| on patch area A by Equation (3). Therefore, we only need to show:
max x/∈A |hA(., γ)| ≤ max x∈A |hA(., γ)| (15)
Since parameter γ controls the slope of hA(., γ) outside of patch area A, a large γ means that hA(., γ) will drop to zero quickly outside of A. Therefore, we can choose a large enough Γ such that hA(., γ) drops to zero faster than the change of linear patch function cx+ d.
Therefore, we have that for any γ ≥ Γ, max x/∈A |hA(., γ)| ≤ max x∈A |hA(., γ)| = max x∈X |hA(., γ)|
≤ max x∈A |f̃ − f | ≤ max x∈X |f̃ − f | (16)
Theorem 5 (Polynomial-Time Efficiency). REASSURE terminates in polynomial-time in the size of the neural network and the number of buggy linear regions when Φout takes the form of {y | ql ≤ Py ≤ qu}, where P is a full row rank matrix and −∞ ≤ ql[i] ≤ qu[i] ≤ +∞ (ql[i] and qu[i] are the i-th elements of ql and qu respectively).
Proof. We consider the affine patch function solved via Equation (10). SupposeA = {x ∈ X |aix ≤ bi, i ∈ I}. For the LPs in Equation (11), |I| is the number of constraints and it is polynomial in the size of the neural network. Thus, REASSURE runs in polynomial time in the size of the neural network.
In addition, since REASSURE computes the support network gA and affine patch function pA for each A one by one (see Algorithm 1), the time complexity of REASSURE is linear in the number of buggy linear regions.

heading: 7.4 ADDITIONAL EXPERIMENT DETAILS
text: Details on Feature-Space Repairs:
For an R-layer DNN f , we split f into two submodels f1 and f2 according to a hidden layer, say the jth hidden layer, where f1 is the first j layers function, f2 is the last R − j layers function and f = f2 ◦ f1. We note the output space of f1 the feature space. And for any buggy input x̃, we note f1(x̃) the buggy feature.
Repairing in a feature space is to repair the behavior of f2 on buggy features {f1(x̃1), . . . , f1(x̃L)}. Note this will automatically repair the behavior of f on buggy points {x̃1, . . . , x̃L}. Repairing in a feature space has the benefit of making the repair process more computation-friendly and reducing the parameter overhead of the additional networks, and has the potential to generalize the repair to undetected buggy inputs with similar features. However, it loses the locality guarantee in the input space (but still preserves locality in the feature space).
Point-wise Repair on ImageNet (Feature-Space Repairs)
We use AlexNet Krizhevsky et al. (2012) on ImageNet dataset Russakovsky et al. (2015) as the target DNN. The size of image is (224, 224, 3) and the total number of classes for ImageNet is 1000. We slightly modified AlexNet: we only consider 10 output classes that our buggy images may lie on and use a multilayer perceptron with three hidden layers (512, 256, 256 nodes respectively) to mimic the last two layers of AlexNet.
The goal of the repair is to fix the behaviors of the target DNN on buggy inputs, which are found on ImageNet-A Hendrycks et al. (2021). For REASSURE, we construct the patch network starting from the third from the last hidden layer (i.e. repair in a feature space).
The results are shown in Table 4. REASSURE, PRDNN and Fine-Tuning repair all the buggy points while Retrain only repair 96% buggy points in 100 epochs. REASSURE achieves almost zero modification on validation images to the original DNN. In addition, REASSURE preserves the performance of the original DNN.
Watermark Removal
We compare REASSURE with MDNN on the watermark removal experiment from their paper. We were not able to run the code provided in the MDNN Github repository, but we were able to run on the target DNN models, watermark images, and MDNN-repaired models in the same repository.
The target DNN is from Goldberger et al. (2020), which is watermarked by the method proposed in Adi et al. (2018) on a set of randomly chosen images xi with label f(xi).
The goal is to change the DNN’s predictions on all watermarks xi to any other label y 6= f(xi) while preserving the DNN’s performance on the MNIST test data. For REASSURE, we set the prediction y = f(xi)− 1 if f(xi) > 1, and y = 10 otherwise. The results are shown in Table 5. Both REASSURE and MDNN remove all the watermarks. However, MDNN introduces significant distortion to the target DNN and as a result the test accuracy drops rapidly as the number of repair points increases. In comparison, REASSURE removes all the watermarks with no harm to test accuracy.
Area Repair: HCAS
Table 6 is the comparison with PRDNN using the last layer as the repair layer. All other settings are the same as those in Section 5.2.
Size of Neural Networks:
Point-wise Repairs on MNIST: The DNN model is a multilayer perceptron with ReLU activation functions. It has an input layer with 784 nodes, 2 hidden layers with 256 nodes in each layer, and a final output layer with 10 nodes.
Watermark Removal on MNIST: The DNN model has an input layer with 784 nodes, a single hidden layer with 150 nodes, and a final output layer with 10 nodes.
Area Repair on HCAS: The DNN model has an input layer with 3 nodes, 5 hidden layers with 25 nodes in each hidden layer, and a final output layer with 5 nodes. DNN outputs one of five possible control advisories (’wrong left’, ’weak left’, ’Clear-of-Conflict’, ’weak right’ and ’wrong right’).
Point-wise Repairs on ImageNet: modified AlexNet Krizhevsky et al. (2012) has 650k neurons, consists of five convolutional layers, some of which are followed by max-pooling layers, and five fully-connected layers.
Hyperparameters used in Repair:
We set γ = 0.5 for Point-wise Repair on MNIST, γ = 0.02 for Watermark Removal, γ = 1 for Area Repair: HCAS and γ = 0.0005 for Point-wise Repair on ImageNet.
We set learning rate to 10−3 for Retrain in the point-wise repair experiment.
We set learning rate to 10−2 and momentum to 0.9 for Fine-Tuning in the point-wise repair experiment.
PRDNN requires specifying a layer for weight modification. We use the first hidden layer as the repair layer, which has the best performance in our experiment settings, unless otherwise specified.
Specifications in HCAS: Specification 1. If the intruder is near and approaching from the left, the network advises “strong right.”
Input constraints: Φin = {(x, y, ψ)|10 ≤ x ≤ 5000, 10 ≤ y ≤ 5000,−π ≤ ψ ≤ −1/2π}. Output constraint: f(x, y, ψ)4 ≥ f(x, y, ψ)i for i = 0, 1, 2, 3.
We calculate all the linear regions for N1,4 in the area Φin of Specification 1 and totally 165 linear regions are found, including 87 buggy linear regions (DNN did not meet the specification) and 78 correct linear regions (DNN meet the specification). Specification 2. If the intruder is near and approaching from the right, the network advises “strong left.”
Input constraints: Φin = {(x, y, ψ)|10 ≤ x ≤ 5000,−5000 ≤ y ≤ −10, 1/2π ≤ ψ ≤ π}. Output constraint: f(x, y, ψ)0 ≥ f(x, y, ψ)i for i = 1, 2, 3, 4.
Also we calculate all the linear regions in the area Φin of Specification 2. And 79 correct linear regions are found. We will test if a repair will make those correct linear regions incorrect.
Point-wise Repairs vs. Area Repairs:
REASSURE automatically performs area repair on the point-wise repair experiments. This means our area repair method scales well to high-dimensional polytopes (the input dimension of MNIST is 784) whereas PRDNN does not scale beyond 2D linear regions/polytopes.
Parameter Overhead for REASSURE:
REASSURE introduces an additional network, patch network, and as a result adds new parameters to the original network. The number of new parameters depends on |I|, which is the number of linear constraints for the H-representation of A. We can remove redundant constraints in this representation in polynomial time to make the additional network smaller. For the area repair experiment on HCAS, the average number of constraints for one linear region is 3.28 and the average number of new parameters that REASSURE introduces is 66. As a comparison, the number of parameters in the original network is around 3000 and PRDNN doubles the number of parameters (as a result of the Decoupled DNN construction) regardless of the number of point-wise or area repairs.
7.5 APPLYING REASSURE TO GENERAL CPWL NETWORKS
Recall the result that an Rm → R function is representable by a ReLU DNN if and only if it is a continuous piecewise linear (CPWL) function Arora et al. (2016). We use convolutional neural networks as an example to show how REASSURE can be applied to more general CPWL networks. Convolutional neural networks (CNNs) are neural networks with convolution layers and maxpooling layers. For simplicity, we assume the CNNs also use ReLU activation functions (but in general other CPWL activation functions will also work). The convolutional layers can be viewed as special linear layers. The maxpooling layers can be converted to linear operations with ReLU activation functions as follows.
max(x1, x2, ..., xn) = max(x1,max(x2, x3, ..., xn))
max(xi, xj) = max(xi − xj , 0) + xj = σ(xi − xj) + xj where σ is the ReLU activation function. Thus, REASSURE can be used to repair CNNs as well.

Review summaries:
This paper presents a new methodology for repairing ReLU neural networks. Concretely, for a single affine region, a patch function is synthesized from an affine function that performs the repair and a support network to make sure the repair only applies to the affine region. Multiple affine regions can be fixed iteratively. The techniques are evaluated on the MNIST and HCAS benchmarks.

The paper presents a new method for the provable repair of neural networks. Both point-wise and polytope-based repairs are considered. The main idea is to synthesize a patch network and combine it with the buggy network. The patch network consists of two subcomponents: a support network that is only activated for the inputs in the linear region containing buggy inputs and an affine patch network that repairs the network in the buggy region. The experimental evaluation is performed on similar datasets and networks as prior work and shows the effectiveness of the new methodology.

The paper develops a method for repairing neural networks with ReLU activation functions. The method works by augmenting a given network with a patch function that corrects the output of the network on a given buggy input. This enables the method to be the only one among related work that is not only sound and complete but also guarantees (i) minimal distances between  the functions implemented by the original and repaired networks; (ii) unaltered behaviour of the repaired network for inputs different than the buggy one. 

This paper proposed an approach for repairing neural networks that use ReLU activation functions. Different with existing techniques that retrain the model or change the weights, the proposed approach generates a patch in the original model, i.e., add sub-models. The LP solver is used to solve the patch function for a linear region. The experimental  results demonstrated that the approach could outperform existing methods.