Provable Editing of Deep Neural Networks using Parametric Linear Relaxation
Authors: Zhe Tao
Aditya Thakur
Venue: NeurIPS 2024 poster (2024)
Keywords: Provable editing
provable repair
provable training
trustworthiness
linear programming
local robustness
verification
Primary area: safety_in_machine_learning
TL;DR: Efficient technique for provably editing the DNN parameters such that the DNN satisfies a given property for all inputs in a given polytope.

Abstract: Ensuring that a DNN satisfies a desired property is critical when deploying DNNs in safety-critical applications. There are efficient methods that can verify whether a DNN satisfies a property, as seen in the annual DNN verification competition (VNN-COMP). However, the problem of provably editing a DNN to satisfy a property remains challenging. We present PREPARED, the first efficient technique for provable editing of DNNs. Given a DNN $\mathcal{N}$ with parameters $\theta$, input polytope $P$, and output polytope $Q$, PREPARED finds new parameters $\theta'$ such that $\forall \mathrm{x} \in P . \mathcal{N}(\mathrm{x}; \theta') \in Q$ while minimizing the changes $\lVert{\theta' - \theta}\rVert$. Given a DNN and a property it violates from the VNN-COMP benchmarks, PREPARED is able to provably edit the DNN to satisfy this property within 45 seconds. PREPARED is efficient because it relaxes the NP-hard provable editing problem to solving a linear program. The key contribution is the novel notion of Parametric Linear Relaxation, which enables PREPARED to construct tight output bounds of the DNN that are parameterized by the new parameters $\theta'$. We demonstrate that PREPARED is more efficient and effective compared to prior DNN editing approaches i) using the VNN-COMP benchmarks, ii) by editing CIFAR10 and TinyImageNet image-recognition DNNs, and BERT sentiment-classification DNNs for local robustness, and iii) by training a DNN to model a geodynamics process and satisfy physics constraints.

Provable Editing of Deep Neural Networks using Parametric Linear Relaxation
Zhe Tao University of California, Davis Davis, CA 95616, USA zhetao@ucdavis.cm edu
Aditya V. Thakur University of California, Davis Davis, CA 95616, USA
avthakurQucdavis. edu
Abstract
Ensuring that DNN satisfies desired property is critical when deploying DNNs in safety-critical applications. There are efficient methods that can verify whether DNN satisfies property, as seen in the annual DNN verification competi- tion (VNN-COMP). However, the problem provably editing DNN to satisfy property remains challenging. We present PREP PREPARED[] the first efficient tech- nique for provable editing of DNNs. Given a DNN N with parameters 0, input polytope P, and output polytope Q, PREPARED finds new parameters such that vx P. (xxx; 0) E Q while minimizing the changes I - 0|| Given a DNN and a property violates from the VNN-COMP benchmarks, PREPARED able to provably edit the DNN to satisfy this property within 45 seconds. PREPARED is efficient because relaxes the NP-hard provable editing problem to solving linear program. The key contribution is the novel notion of Parametric Linear Relaxation, which enables PREPARES to construct tight output bounds of the DNN that are parame-
terized by the new parameters Ò We demonstrate that PREP ARED is more efficient and effective compared to prior DNN editing approaches i) using the VNN-COMP benchmarks, ii) by editing CIFAR10 and TINYIMAGENET DNNs, and BERT classfentclassiffcattinn DNNs for local robustness. and iii) by training DNN to model geodynamics process and satisfy physics constraints.
recognitonn
Introduction
Ensuring that DNN correct and avoids harmful behaviors is critical when deploying them, especially in safety-critical contexts 8. In such scenarios, it is vital to guarantee that DNN satisfies given property, e.g., a safety specification (35). Towards this end, DNN verifiers aim determine whether a DNN satisfies the given property [. There efficient methods for DNN verification that can handle a wide-range of DNN architectures and properties, as seen the annual DNN verification competition (VNN-COMP) (5] However, the success of DNN verification reveals the next challenge: provably editing a DNN to satisfy property. Formally, we define the provable editing problem as:
Definition 1.1. Given a DNN A with parameters 0, an input polytope P def [x Dx S e) and an output polytope Q def {y Ay < b). the provable editing problem is find new parameters 0 that
min
0|
s.t. Vx (x 0)
(I)
Provable editing can be used, for instance, to ensure that classifier DNN is locally robust for an input x. In this case, the input polytope def
x ol I c} the _ ball around x with PREPARED stands for PRovable Editing using PArametric linear RElaxation of Deep neural networks.
38th Conference on Neural Information Processing Systems (NcurIPS 2024).

---

y def
(x)
def ReLU(x))
def ReLU(r)
(a)
(b)
(c)
Figure 1: Linear relaxations for y def ReLU(x). and denote the upper and lower bounds, denotes the relaxation. (a) Relaxation in prior approaches [4] 39], where the bounds are overapproximated using linear functions, and the upper bound is only sound within given input bounds [r, ; (b) This work exactly represents the upper bound for any imput upper bound variable 2, results tighter approximation; (c) Illustration of how this work exactly represents the upper bound T7 (-) by capturing the epigraph (1996) of ReLU(z) with the linear constraint ÿ 2 0 T 2 E.
The lower bound y (-) uses a linear relaxation y def
că with a constant E [0, 1].
radius and the output polytope Q {y A < <yi} requires that the output label is I; viz., arg max = I. Moreover, provable editing can be used either during training to guarantee that the DNN satisfies a property, or post-deployment to repair a given DNN.
The provable editing problem is challenging due to the presence of the universal quantifier; viz., finding new parameters such thatfor all inputs in the polytope P, the output of the edited network lies in the polytope Q. There are no existing approaches for efficiently and effectively solving the provable editing problem. Regularizationnbasse during training, but are unable to guarantee the property-sattsfaction satisfaciiioon S.MT-based approaches [14] [6] provide guarantees, but are not efficient because they directly solve NP-hard problem. Prior LP-based approaches [41 [2 are efficient because they can only handle a restricted class of provable editing problems; e.g., they assume that the vertices of the input polytope or the linear regions of the DNN can be efficiently enumerated, or the DNN architecture can be modified.
approaches (26 10 28 24 encode the property into the loss
This paper presents PREPARED, the first efficient technique for provable editing of DNNs that runs in polynomial time (Theorem 3.4). Given a DNN and property it violates from the VNN-COMP'22 benchmarks, PREPARED is able provably edit the DNN to satisfy this property within 45 seconds.
PREPARED approaches the problem of provable editing by constructing tight parametric bounds of the output N (x: 0) for all inputs x in the input polytope P in terms of the parameters ê and then constraining these parametric bounds lie within the output polytope Q. These parametric bounds are constructed compositionally per layer of the DNN, and are expressed as linear constraints, so that efficient Linear Programming (LP) solvers can be used to find optimal solution.
Our key insight is to represent the parametric bounds indirectly via underapproximations of the epigraph and hypograph of the DNN layer. Consider the ReI.U layer y ReLU(z). Prior ap- proaches (49 39 overapproximate its upper bound with a linear function (- in Figure I(a) using constant input bounds [z. T.. Such linear relaxation is loose, and is only sound within the given constant input bounds x T.. Our approach is able to exactly represent the upper bound of ReLU output for any input upper bound variable 3 (- in Figure l(b)). This is done by capturing the
epigraph (Feae in Figure I(c) of ReLU(ø) with a linear constraint.
Our key contribution is a novel Paramelric Linear Relaxation for DNN layers, which defines tight parametric bounds using linear constraints in terms of the layer parameters. Consider e def zúb which is a simplified representation of an Affine layer. We would like to construct bounds for all E [g. z) terms of the variable parameter w.. Prior approaches could achieve a sound, but loose linear relaxation that is not in terms of the layer parameters (Figure 2(a). In contrast, our approach exactly represents the output bounds without any relaxation (Figure 2(b) building upon our key insight of capturing the epigraph and hypograph of the DNN layer in terms of the parameters (Figure 2

---

x i
i
T.
10 107
w
Our are purametorized
by any variable weight
E
(a)
(b)
(c)
Figure 2: Linear relaxations for bounding v def
xu for all x E E]. with variable parameter it and denote the upper and lower bound overapproximations.
denotes the relaxation. (a) A loose relaxation for all x E xr. - and for all i E w. w) where i is not treated as a parameter but another input within constant bounds (w, W. (h) This work exactly represents the bounds for all inputs x E I F.. parameterized by variable w without any relaxation. Here we plot a case when O, while our parametric bounds exact for any w. (c) Illustration of how our parametric
bounds are defined for the function v def ab in terms of the variable parameter tb _ denotes the true output region for all slope (input) x E [r. The upper bound V (-) is exactly captured by the epigraph (Erzz)), defined by linear constraint (Ü 2 Tú A T 2 FÙ); the lower bound è (-) is
exactly captured by the hypograph (BWWE)) defined by linear constraint < Tw A TÚ)
We evaluate PREPARED i) using the VNN-COMP benchnarks, ii) by editing CIFARIO and TINYIM- AGENET image-recognition DNNs, and BERT sentiment-classfication DNNs for local robustness, and iii) by training a DNN to model a geodynamics process and satisfy physics constraints. Because there were no prior efficient approaches for provable editing, we implemented new provable fine- tuning baselines by integrating prior DNN editing approaches with a verifier in the loop. PREPARES ARED outperformed such baselines demonstrating its effectiveness and efficiency.
Related work
Regularized training 20
45 30
10
19
22
47 incorporates constraints as regularization into the
training loss, but does not guarantee constraint-satisfactie in the trained DNN. For the DNN editing problem we addressing, which involves universally-quantifee logical formulas, DL2 (T0) is the state-of-thc-art regularized training method.
Certified training 126
is type of regularized training geared towards adversarial robustness. SABR 28 and STAPS 24 are state-of-the-art certified training approaches.
15|
36
31
28
24
However, they also do not guarantee constraint sitrraintt-sissfction....
SMT-based editing approaches 14 23 16
directly solve the NP-hard provable editing problem using an SMT solver. Thus, they are inefficient and do not scale beyond small DNNs. For instance, the recent DeepSaDe approach [16 incorporates an SMT solver during training, but only uses the SMT solver to edit the last layer. However, it still can take 500x longer than regularized training.
42 relax the provable editing problem to solving an LP problem, which makes them efficient. However, prior approaches can only handle a restricted class of provable editing problems. The state-of-ther the--rt provable editing approach APRNN 42 efficient for editing input points. However, it does not scale to the general provable editing problem of Definition 1.1 due to the need for enumerating vertices of the input polytope. PRDNN (41] was the precursor to APRNN and suffers from similar limitations; moreover, PRDNN modifies the architecture of DNN and requires enumeration of linear regions to edit an input polytope. REASSURE [12 repairs linear region of DNN by adding a patch DNN for each such linear region. Thus, it also requires enumeration of linear regions to edit an input polytope. Further, has been shown to unsound and incomplete (Section of [2),, and suffers from significant runtime and memory overheads (Section 7.8 of [42)..
LP-based editing approaches
3

---

46 9 4 aims to determine whether a DNN satisfies given property. As shown Section provable editing can be used when a verifier determines that a DNN violates a property. Most verification techniques use linear relaxations to bound the DNN output. However, these linear relaxations cannot be used for provable editing because they are not parameterized in terms of the DNN parameters. Instead, verification techniques assume that the parameters are constant and focus on designing linear relaxations for activation layers like ReLU [34 43 However, it is not clear how even these activation layer relaxations could be used for provable editing. For instance, these relaxations require constant input bounds; loose constant input bounds result in loose linear relaxations. In the context of provable editing. if the ReLU layer follows an Affine layer with editable parameters, then the constant input bounds to the ReLU layer would be very loose (e.g., [- sol) in order to be sound for all possible edits. Hence, the resulting linear relaxation would also be loose. In contrast, our technique does not require constant input bounds for any layer, and produces an exact upper bound for the ReLU layer (Theorem 3.9 Applying our Parametric Linear Relaxation to DNN verification remains future work.
DNN verification 38 39 49
37
48
3 Provable editing of DNNs using Parametric Linear Relaxation
We use R to denote scalar, E R. to denote column vector, and W R to denote matrix. Blue-colored variables with dot denote LP decision variables, e.g., &, X, W, b, etc. The proofs for all theorems can be found in Appendix A
Definition 3.1 (DNN), Let y (xx;0) denote an L-layer deep neural network (DNN) N with parameters 0, input and output y. The DNN is defined iteratively as x x((+1) del (100(()) 0(0) for
each layer (( with parameters g(t), where x (0) def y. x (L) and 0 S t < L.
For ease of exposition, we defer our approach for the general provable editing problem of Defini- tion 1.1 to Appendix B In this section, we consider the following provable interval editing problem, where the input and output constraints are constant interval bounds:
Definition 3.2. Given a DNN N with parameters 0, constant input bounds [x. x and constant output bounds y). the provable interval editing problem is to find new parameters 0 that
min 0 A11 s.t. Vx E
X E yy.
3.1 Parametric Linear Relaxation
Consider a DNN N with variable parameters 0 and input bounds [x. x]. our goal is to construct sound parametric output bounds yy. of A in terms of and x.. The exact definition is
S min (x(x;) 0) & x AY> max {x 0) & x
However, this bution novel Parametric Linear Relaxation, a poly-size linear formula that implies Equation 3
non-linear formula is expensive to solve 66 77. Our key contri-
Definition 3.3. The Parametric Linear Relaxation EN (.,,,,,))) for N is a poly-size linear formula that implies Vx E X N
yy,y]
In other words, any satisfying assignment (y, (y. x. x, of the formula (I..,, yields sound output bounds y for NN, viz., Vx E Xx (xx 0) E Fy. The size of the formula E (y.y,, &, x; 0) is polynomial in the size of the DNN, i.e., the number of parameters, layers, and the input and output dimensions of each layer.
3.2 Provable editing via Parametric Linear Relaxation
The following theorem shows how Parametric Linear Relaxation can be used to solve the provable interval editing problem.

---

Theorem 3,4. Given provable interval editing problem (Definition 3.2 for DNN N and parame- ters 0 with input bounds [x. x] and output bounds y. let (N. ....N.X... 0) be Parametric Linear Relaxation for N. Then the following linear program can be solved in polynomial time in the size of the DNN N, and whose solution is a solution to the provable interval editing problem:
min |
811 Ex(2.8.x.::)) A < sy
(4)
3.3 Compositional construction of Parametric Linear Relaxation
Definition 3.5.
Given L-layer DNN N with parameters 0, constant input bounds [x. and
Parametric Linear Relaxation Evor for each layer NOC), we define the compositional Parametric
Linear Relaxation ΣN
follows, where y
(L) {(1) and [x -
.x(0)
yyyyy
def
Pvvco ((+1) ((++1) (1) (0)) 6
(5)
OWt<L
Theorem 3.6. Definition 3.5 is a Parametric Linear Relaxation for the DNN N.
By Theorems 3.4 and 3.6 see that solve the provable editing problem, we just need to construct Parametric Linear Relaxations (y.c) x: 0) for each DNN layer N/00, In practice, E 0) is defined by separate formulas Farce 2. 0) and Livo (v.2x::) for the upper and lower bounds, respectively: T (y. 0) def
PArto y X; A For brevity, we describe how construct Parametric Linear Relaxation for ReLU and Affine layers. Appendix C presents Parametric Linear Relaxations for Tanh, Sigmoid and ELU layers.
3.4 Parametric Linear Relaxation for ReLU layer
Definition 3.7. y def ReLU(x) with input x E Rm and output E R" is defined as y K max 0}.
Definition 3.8. For a ReLU layer with variable input bounds [x. x]. its Parametric Linear Relaxation defined as ERLLD yyy.&, P x) A x) where:
PReLU (
LROLD LRei (2)) def y = ex
(6)
and c E R are constants such that S C; I
Because ReLU is convex function, seen in Figure I(c) the upper bound constraint
Y X; A y, 2 0 for each y, exactly captures the epigraph (FREE) of ReLU(X.). For each lower
bound Y we use a linear relaxation = = (-) of ReLU(*), with a constant c, S
Theorem 3.9. Definition 3.8 is Parametric Linear Relaxation for the ReLU layer that captures the exact upper bound.
3.5 Parametric Linear Relaxation for Affine layer
Definition 3.10. y Affine(x: W, b) with input E Imm output y E R", weight W E paxm and bias E Rn is defined as
def Wx + b, which expands to
def E Wi: +bj.
In DNN verification, bounding Alfine layers straightforward, because the parameters are constants. However, in provable editing, this is challenging, because the parameters are variables. In particular, we need to bound the multiplication variable weight tt. As seen in Figure 2(a) (a) if the bounds for zú are not parameterized by tb, linear relaxation would require constant bounds (wz, w) for tt, resulting in loose bounds. Our approach constructs tight parametric output bounds using Parametric Linear Relaxation. We now describe our approach for an Affine layer i) with constant input bounds [x, x] when the first layer of DNN. and ii) with variable input bounds [ X] when it is not.
between the
-urastiiyg input & [z, Ø and the

---

y def Tanh(x)
y पef Sigmoid(x)
y der ELU(Ø)
Σ
(a) Tanh
(b) Sigmoid
ELU
Figure 3: Illustration of Parameterized Linear Relaxations for Tanh, Sigmoid and ELU, - and denote the upper and lower bound approximations: B00 and B000
denotes the convex underapproxi-
mations (ū 3) and op i =) for the epigraph and hypograph; denotes relaxation.
3.5.1 Affine layer with constant input bounds
Definition 3.11. For an Affine layer with constant input bounds [x, x] and variable parameters W, b, its Parametric Linear Relaxation is defined as To. Pare V. PAZe ( X, b) where:
W b) P (V.X, W. b) ^
(oxx der Av,= = Σ V + by A V
Wx
Lutt YxX.X, W,b)
ΛE Σ by
Wx
The core of this definition is constructing parametric bounds (ò. 8) for the multiplication zú for all
[z, Ø in terms of the variable weight t. As in Figure 2(c) for all [I. the upper bound
(-) of aw is defined by a piecewise-linen, convex function ( max {zrb, Tw). Hence, the
upper bound constraint ü 2 z A 2 EW exactly captures the epigraph (B903) of f(w). Similarly, the
lower bound (-) of æi defined by piecewise-linear concave function {(bb) def min Fti). Hence, the lower bound constraint
rbb A è Etb exactly captures the hypograph (bumm of f()).
Theorem 3.12. Definition 3.17 is Parametric Linear Relaxation for the Affine layer with constant imput bounds [x, x that captures the exact lower and upper bounds.
3.5.2 Affine layer with variable input bounds
We freeze the parameter weight W to be constant W (e.g., the original weight) when the input bounds are variable avoid non-linearity.
Definition 3.13. For Affine layer with variable input bounds [ x).
constant weight W and variable der
bias b, its Parametric Linear Relaxation defined as E.rr ( y. X. W. b) LAst y, X X, W. b) where:
Patt ( x, W. b)
PAcr 2 W. def Av V je + +b,
V def W and
def W if 20 V
where
2Ne ( &
Λg
Σ V +b,
del X W
del W j otherwise
Using constant weight W avoids non-linearity due to the multiplication xw where x is universally- quantified variable bounds i v.. Thus, the bounds (v. d. of aw for all [ x are determined
by the sign of the constant w; viz.. '. J. [iw, Tw) if w 2 O. otherwise [v. T 2w).

---

Time (8)
(L2 time (8)
(PR time (8)
600
PFI(000)
100%
100%
3000
(AP
100
10x
100
10x
0.1x
0.1x
Better
10
100 600
10
100
600
# instances succeeded
PREPARED time (s)
PREPARED time (S)
(a) Left: cactus plot of runtime for 423 single-property editing problems. with 600 seconds time limit for each problem. PREPARED succeeded on all 423 problems, while PFT(BL2) succeeded on 185, and PFT(APRNN) succeeded on 117. Middle: speed for PREPARES vs PFT(D)2). Right: speed up for PREPARED vs (PP(X))
Time (s)
PFT(D22) time (s)
PFT time
3600
3600
10000
(FT(A)
PFT(UL))
1000
100
1000
100x
PREPARED
10x
100
1x
1x
5000
0.1x
0.1x
10
10
Beter
12
45.48
6266
1000
# instances succeeded
PREPARED time (8)
PREPARED time (s)
(b) Left: cactus plot of runtime for 66 all all-properties editing problems, with 3600 scconds time limit for cach problem. PREPARE ARED succeeded 62 problems, while PFT(DL2) succeeded on 45, and (FT(A))M)) succeeded 48. Middle: speed up for PREPARED PFT(D12). Right: speed up for PREPARED vs PFT(AFRU)).
Figure 4: Results of (a) single-property and (b) all-properties editing problems from VNN-COMP'22
Theorem 3.14. Definition 3.13 is Parametric Linear Relaxation for the Affine layer with variable input bounds [ x) that captures the exact upper and lower bounds.
3.6
Parametric Linear Relaxation for Tanh, Sigmoid and ELU layers
Our approach also handle other activation layers like Tanh, Sigmoid and ELU. Figure 3 Fillustrates their Parametric Linear Relaxations with detailed description deferred to Appendix C
3.7 On scalability
As described in Appendix B our approach can restrict the edits to only the last layers of the DNN N,, freezing the parameters of the first L - & layers. Consequently, the resulting Parametric Linear Relaxation a linear formula whose size is polynomial in the size of only the last editable layers (k=L) instead of the entire DNN A. This flexibility enables our approach to scale to large DNNs and BERT transformers, as demonstrated in Section
4 Experimental evaluation
We have implemented PREPARED in PyTorch 32 and use Gurobi 17 the LP solver. We
demonstrate the effectiveness and efficiency of PREPARED on different tasks that use a wide-range of DNN architectures and properties. All experiments were run machine with Dual Intel Xeon Silver 4216 Processor 16-Core 2. GHz with 384 GB memory, SSD and RTX-A6000 with 48 GB of GPU memory running Ubuntu 20.04. Additional details about these experiments in Appendix [
Baselines. Because there were no efficient prior approaches for provable editing, we implemented provable fine-tuning PFT() baselines that combine prior (non-provable) DNN editing approaches with
7

---

verifier in the loop: the editing stops when the verifier confirms that the DNN satisfies the property
(Appendix D.I. We consider the sfate-of-the art DNN editing approaches DL2 [TO], APRNN [42]. SABR (28 and STAPS [24] as introduced in Section 2 We use PFT() to denote the provable fine- tuning baseline instantiated with DL2. We use verifiers or, 0.33-RRON [46 [4], MN-BaB [9. or DeepT [4]
depending on the task. To the best of our knowledge, ours is the first to provide a comprehensive
evaluation of such verifier-in-the-lop baselines for provable editing.
4.1 Provable editing on VNN competition benchmarks
Setup. We compare PREPARED against PFT(DL22) and PFT(APRM)) on VNN-COMP'22 benchmarks (29). The VNN-COMP'22 22 benchmarks consist of DNNs along with one or more of their associated safety properties. For verification, the task would be determine whether DNN satisfies each of its properties. In the context of provable editing, we use these benchmarks in two scenarios: i) Sin- gle-property editing: Given DNN and a property it violates, edit it to satisfy this single property with a time limit of 600 seconds. There are 423 such DNN-property instances. it) All-properties editing: Given a DNN that violates at least one of its associated properties, edit it satisfy the conjunction of all (satisfied or violated) properties associated with it with time limit of 3600 seconds. There are 66 such proppryy instances.
PFT(SABR) and PST(ST) are not used because they do not handle all properties and DNN architectures in this experiment. In particular, SABR and STAPS have not diseussed how to handle general logical formula with disjunctions, and their current implementations are designed for local robustness training. PFT(SABR) and PFT(STAPS) are used for local robustness editing in Section 4.2
Metrics. The effectiveness is measured using the number of provably edited instances, and the efficiency is measured using the runtime. We were unable to determine the impact on the predictive performance (accuracy), because VNN-COMP does not come with such evaluation metries and data.
Results. As shown in Figure 4 PREPAREI ARED is the best provable editing approach, significantly outperforming PFT(B12) and (PPAM)) in terms of both effectiveness and efficiency. As shown in the cactus plots (Left in Figures 4(a) and 4(b)., PREPARED can provably edit more instances in less time. As shown in the speed-up plots (Middle and Right in Figures 4(a) and (b)). PREPARED completes most problems in 10 seconds, taking a maximum of 45 seconds for single-property editing; it achieves from 10x to more than 100x speed-up over PFT(DL22 and PFT(APRMX) Specifically, PREPARED succeeds on all 423 single-propery, editing problems, while PFT(DL2) and (PP succeed on 185 and 117 problems, respectively. PREPARED succeeds on 62 out of 66 multi-property editing problems, while PFT(DL2) and PFT(APRMI) only succeed on 45 and 48 problems, respectively.
4.2 Local robustness editing for image-recognition DNNs
Definition 4.1. Consider a classifier DNN N : I." - R" and a dataset D of input-label pairs (x, E RT x Z. The DNN N correctly classifies and the standard accuracy of a DNN on dataset D is the percentage of correctly classified input-label pairs in DD. Given perturbation e E R. the DNN A is I I.--locally-rooust
input-label pair (x, 1) iff arg [Vxx)\(x) = 1,
an input-label pair (x, 1) iff N correctly classifies all perturbed inputs x' in the I box centered at x with perturbation e, The certified accuracy of DNN on a
viz., Vx' E _ ||x' x | S dataset D is the percentage of - -o--localyy-rbus input-label pairs in D.
+ arg max N Nx(')
Setup. We compare PREPARED against PFT(DL2), PFT(SABR). and APRNN on I See--ocll-rousteess editing for image-recognition DNNs. We edit CNN7 DNNs for CIFAR 10 [1] and TINYIMA- GENET (33), trained in prior work (28), to be locally-robust for images in the edit set. The CIFARIO DNN has 17.2M parameters, 79.24% standard accuracy and 75.77% certified accuracy (e = 0.5/255) The TinylmageNet DNN has 51.9M parameters, 28.85% standard accuracy and 20.46% certified accuracy (e 1/255). For CIFARIO 10 and TINYIMAGENET, the edit sets consist of 50 misclassified fog-corrupted images from CIFARIO-C [8] and TINYIMAGENET-C C [18, respectively. The gener- alization sets consist of 200 variant images with different corruption-eevels, four variants per image in the edit set. We use MN-BaB 9 to compute the certified accuracy.
Metrics. Efficacy is measured using the certified accuracy (Definition 4.1 on the edit set. The original certified accuracy on the edit set is 0%. Efficacy the most important metrie: a provable edit must guarantee 100% efficacy. The standard accuracy and certified accuracy on the full
8

---

Table 1: Local robustness editing for aanae-recoggitionn DNNs. Comparison of efficacy (Effic.), standard (Acc.), certified (Cert.) and generalization (Gen.) accuracy. Rows with <100% efficacy are shaded. Best results are highlighted.
CIFAR 10 with g=0.5525
TINYIMAGENET with e= s=155
Method
Effic.
Acc.
Cont.
Gen.
Time
Effic.
Acc.
Cort.
Gon.
Time
PFT(UL2)
50/50
73.59%
70.42%
197/200
4780s
47/50
22.83%
15.06%
190/200
14400s
PPT(SABR)
50/50
57.10%
52.72%
200/200
38s
50/50
20.24%
13.38%
192/00
230s
(FT
50/50
57.38%
54.26%
197/200
15s
50/50
20.880 20.84%
13.14%
191/200
112s
APRXN
5/50
16.9
15.14%
113/200
20s
12/50
28.75%
18.61%
11.5200
417s
PREPARED
5Q/50
75.25% %
71.45%
189/200
88s
50/50
28.16%
16.80%
149/200
663s
Timcout four bours.
Table 2: Local robustness editing for sentiment-classiffaaiie transformers. Comparison of the lower bound of efficacy before (Og. Effic.) and after edit (Effic.),, as well as the stand accuracy (Acc.). Rows with < 100% efficacy are shaded, Best results are highlighted.
Method
Og
Eifli.
Og. Eilie.
Acc.
Time
(F
$2/66
82.97%
12108s
23/26
79.67%
5610s
APRUN
60/66
61/666
83.47%
6s
25/26
23/26
81.32%
5s
PREPARED
66/66
83.52%
981s
26/26
82.42%
326s
test set are also important metrics: good provable edit should have high accuracy. However, those accuracy metrics are relevant only if efficacy is 100%. The generalization accuracy on the generalization set measures how well the edit generalizes to inputs that are similar the edit set. However, the generalization accuracy is relevant only if the efficacy is 100% and the standard and certified accuracies are good; that is, the predictive power of the edited DNN should not be sacrificed for better generalization. The runtime metric measures the time taken to edit the DNN.
Results. As shown in Table 1 PREPARED overall the best approach. PREPARED achieves the best standard and certified accuracy, good generalization and short runtime. In particular, PFT(S)BR) and (STAA)) have significantly lower standard and certified accuracy: PFT(DL22) takes significantly longer time, and was unable to achieve 100% efficacy in four hours in the TINGEMAGENET experi- ment: APRNN was unable achieve 100% efficacy.
4.3 Local robustness editing for sentiment classification BERT transformers
Setup. We compare PREPARED against PFT(DL2) and APRNN on provable - local-robustness editing for BERT centiment-classifccan transformers. We conduct this experiment the Stanford Sentiment Treebank (SST) 40 DNNs. We use DeepT 4 as the verifier in this experiment. We take the "wider" 12-layer BERT transformer used in the DeepT paper [4]. The standard accuracy of this network is 84.07%. Because DeepT cannot handle all sentences in the SST dataset with arbitrary e, construct two editing sets from the SST validation set: all 66 verifiable sentences with le-4, where 60 of them are certified to be locally-robust; all 26 verifiable sentences with e = 5e-4, where 24 of them are certified to be locally-robust. PFT(SABR) and PFT(STAPS) are not compared in this experiment because SABR and STAPS do not handle the BERT transformer architecture.
Metrics. Efficacy is measured using the certified accuracy (Definition 4.1 the edit set. Because DeepT is incomplete, we can only compute a lower bound of the efficacy. Efficacy is the most important metric: provable edit must guarantee 100% efficacy. The original efficacy (Og. Effic.) is also presented in Table The standard accuracy on the full test set is also an important metric: a good provable edit should have high accuracy. However, the standard accuracy is relevant only if efficacy is 100%. The runtime metric measures the time taken to edit the DNN.
Results. As seen in Table 2 PREPARED is the only approach that achieves 100% efficacy in this task. PREPARED also achieves good accuracy and short runtime. Both PFT(DL2) and APRNN were unable to achieve 100% efficacy, and decreased the efficacy in most experiments.

---

Table 3: Global physics property repair for geodynamics DNN, Comparison of relative error (Rel. Err.), continuity (Cont. Err.) and boundary-conditin (BC Err.) errors. Errors on the test set (Ref.) are shaded. Best results are highlighted.
Method
Rel. Em
Cont. Err.
BC Err.
Time
Ref.
1.42 x 10 12
1.74 x 10 12
DL2
1.59%
1.58 10
5.08
6747
GD
0.26%
1.59 10 6
5.86
395s
(D(PP))))
0.50%
5.57 x 10
4.96 x 10
570s
CD(PRERARE
0.50%
1.42
10-12
2.29 10-7
084s
4.4 Provable training for physics-plausible DNNS
Numerical model.
We consider a classic model of a buoyancy-drive mantle flow with a central circular plume 113. which is an incompressible flow with variable viscosity. The state of the system
is vector field F def (u, u, 77.7) p) of velocity field U def (u,u), v), viscosity and density p. over space (x, y) E Ω and time & E T. We consider the following two physics constraints: i) Conservation of mass V U from the continuity equation; Hi) Dirichlet boundary condition U
on the
boundary a where n is the outward normal of On.
Setup. We compare CD(PREPARED), combination of crrdieet-descenr (GD) and PREP ARED, against DL2, GD and GD(APRM)) on the task of provably training DNN to model the geodynamics process and satisfy physics constraints. We discretize the space into 31x31 grid and implement the numerical model to generate data for 150 time steps. We evenly split the data into training, validation and test sets. We train ReLU ResNet with one single residual block of four conv2d layers with 32 channels and 3x3 kernel size. For DL2, we add the physics constraints as an unsupervised-learnin regularization to the supervised training. For GD(APRN)) and GD(PREPARED), we first use vanilla gradient- descent (GD) to train a base model, then edit it with the constraints. Specifically, GD(APRNX) edits all training points, and GD(RREARRD)) edits the convex-hull of all training points satisfy the constraints.
Metrics. The relative error on the test set, the constraint-satisfacete errors, viz., continuity error, for the conservation of mass, and coundary-conditton error, and the runtime are the metrics.
Results. As shown Table 3 GD(PREPARED) overall the best approuch. GD(PREPARED) has good relative error, and its constraint-satiifaction error is significantly better than other approaches. Notably, its continuity error at the same magnitude as the reference data, close to the theoretical value, zero, and is 10 to 10 times better than other approaches. GD achieves the best relative error and the shortest runtime. DL2 has the worst errors and takes significantly longer amount of time.
Conclusion
We have presented PREPARED, the first efficient approach for provable editing of DNNs that runs in polynomial time. We presented novel methods for constructing tight parametric bounds for the DNN output using Parametric Linear Relaxation, enabling PREPARED to edit. To demonstrate its effectiveness and efficiency, PREP ARED was used to provably edit DNNs and properties from the VNN-COMP'22 222 benchmark, provably edit CIFAR 10 and NGEETT image- recognition DNNs, and BERT sentiment-classificaii DNNs for local robustness, and provably train geodynamics DNN satisfy physics constraints.
LP solver find an
Societal impact. PREPARED represents a step towards the goal of ensuring safety, trustworthiness, and reliability of DNNs, which is crucial given their use in autonomous safitt-critical systems. However, being a general technique for editing DNNs, it could be used to remove or add malicious behavior such bias, backdoor attacks, etc.
Limitations. PREPARED requires as input a property that we wish the DNN to satisfy. These properties would need to formally encode the notions of safety, reliability, or trustworthiness, which may not always be possible or easy to do. e.g., defining safety properties for L.se- chatbots. However, the machine learning and formal methods communities are making progress towards this goal; e.g., developing proxy specifications for complex properties that are easier define and learning safety specifications from data (8).
10

---

and precise certification of transformers. https://gittuue www.://oeeteteseeeeeeeeeeeeeeeee tree/ 1Dffe440751111177777222222444466 Acknowledgments and Disclosure of Funding
We would like to thank the anonymous reviewers for their feedback and suggestions, which have greatly improved the quality of the paper. This work is supported in part by NSF grant CCF-2048123 and DOE Award DE-SC0022285.
References
[1] Aws Alharghouthi. Introduction to neural network verification. Found. Trends Program. Lang., 7(1-2):
1-157, 2021. doi: 10.1561/2500000011.
[2] Mislav Balunovic Martin Vechev. Adversarial training and provable defenses: Bridging the gap. In International Conference on Learning Representations, 2020. [tKL/https:/oppereviiee wwwp:/rwwwwww....eeeeeeeeeeeeeee ner/forum?
Td=Sxxs
[3] Gregory Bonaert, Dimitar I. Dimitrov, Maximilian Baader, and Martin T. Vechev.
Fast
2021.
[4] Gregory Bonaert, Dimitar 1. Dimitrov, Maximilian Baader, and Martin T. Vechev. Fast and precise certification of transformers. In Stephen N. Freund and Eran Yahav, editors. PLDI '21: 42nd ACM SIGPLAN International Conference Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021, pages 466 466-481. ACM, 2021. doi: 10.1145/3455488334550553 URL https://doi.. org/ 10. 011144///34333 3444444483344456 3454056
[5] Christopher Brix, Mark Niklas Müller, Stanley Bak, Taylor T. Johnson, and Changliu Liu. First three years of the international verification of neural networks competition (ynn-comp), 2023.
[6] George E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In
H. Brakhage. editor, Automata Theory and Formal Languages, pages 134-183, Berlin, Heidelberg, 1975. Springer Berlin Hcidelberg. ISBN 978-3-540-37923
[7] George E. Collins and Hoon Hong. Partial cylindrical algebraic decomposition for quantifier climination. Journal of Symbolic Computation, 12(3):299-328, 1991. ISSN 0747-7171. doi: https://doi.or//10. 1016/8077477717100880133333 URL http://ttte//..ccceeneeeeiieeeee http:e/cccccccccceee/cccccc///p/ 50747717108801526
[8] David Dalrymple, Joar Skalse, Yoshua Bengio, Stuart Russell, Max Tegmark, Sanjit Seshia, Steve Omohun- dro, Christian Szegedy, Ben Goldhaber, Nora Ammann, Alessandro Abate, Joe Halpem, Clark Barret, Ding Zhao, Tan Zui-Xuan, Jeannette Wing, and Joshua Tenenbaum. Towards guaranteed safe ai: A framework for ensuring robust and reliable systems. arXiv preprint arXiv:2405.066 2024.
[9] Claudio Ferrari, Mark Niklas Müller, Nikola Jovanović, and Martin Vechev, Complete verification multi- neuron relaxation guided branch-and-bound. In International Conference on Learning Representations, 2022.
[10] Mare Fischer, Mislav Balunovie, Dana Drachsler-Colen Timon Gehr, Ce Zhang, and Martin T. Vechev. D1.2: training and querying neural networks with logic. In Proceedings of 36th International Conference on Machine Learning (ICML), volume 97 of Proceedings of Machine Learning Research. PMLR, 2019.
[11] Mare Fischer, Mislav Balunovic, Dana Drachsler- Timon Gehr, Ce Zhang, and Martin T. Vechev. DL2: Training and querying neural networks with logic. https:://// htttps://github.. http://ggttuuu.oooooee heam//thh-siiie sthhsshsssss/111 tree/ 2023.
[12] Feisi Fu and Wenchao Li. Sound and complete neural network repair with minimality and locality guarantees. In 10th International Conference on Learning Representations, ICLR 2022, Lisbon, Portugal, Oct 27-28, 2022. OpenReview.net, 2022.
//rxivv./////////// org/ abs//110....22.. 2200000080000
[13] Taras Gerya. Introduction to numerical geodynamic modelling. Cambridge University Press, 2019.
[14] Ben Goldberger, Guy Katz, Yossi Adi, and Joseph Keshet. Minimal modifications of deep neural networks using verification. Elvira Albert and Laura Kováes, editors, LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning. Alicante, Spain, May 22-27, 2020, volume 73 of EPiC Series in Computing, pages 260-274 278.. EasyChair, 2020, doi: 10.29007/6999. URL https: //di.. org/ 29007 /699q

---

[15] Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovic, Timothy Mann, and Pushmeet Kohli. On the effectiveness of interval bound propagation for training verifiably robust models, 2019.
[16] Kshitij Goyal, Sebastijan Dumancic, and Hendrik Blockeel. Deepsade: Learning neural networks that guarantee domain constraint satisfaction. Proceedings of the AAAI Conference on Artificial Intelligence, 38 (11):12199- 12207, Mar. 2024. doi: 16.1609a v38i11 138:11.29109 291999. URL https://ojss aaaii .rggindee index
php/ Att.AA/AAaaatttleeeeaeaa 22999 29109
[17] Gurobi Optimization, LLC, Gurobi Optimizer Reference Manual, 2022. URL https:/::///ww gurobi com
[18]
Dan Hendrycks and Thomas G. Dietterich. Benchmarking neural network robustness to common corrup- tions and perturbations. In 7th International Conference on Learning Representattinns, ICLR 20/9, New Orleans, LA, USA, May 6-9, 2019, OpenReview.net, 2019, [ttp:stts///oopereeeiet nww.:/reeeet/rrrrre/ id-HJ26t1Cqym
[19] Nick Hoernle. Rafael Michael Karampatsis, Vaishak Belle, and Kobi Gal. Multiplexnet: Towards fully satisfied logical constraints in neural networks. Proceedings of the AAAI Conference on Ar- rificial Intelligence, 36(5):5700-5709 Jun. 2022. doi: (0.16699aaai..3665.2222 20512. //ojs. waa..aaai.oom wawaai..or/iineee. wwweg/iindx...o
URL https?
[20] Zhiting Hu, Xuezhe Ma. Zhengzhong Liu, Eduard Hovy, and Eric Xing. Harnessing deep neural networks with logic rules. In Proceedings of the 54th Annual Meeting of the Association for Computational Linguis- tics (Volume 1: Long Papers), pages 2410-2420, Berlin, Germany, August 2016. Association for Computa- tional Linguistics. doi: 10. 10.18663/v 1/P16 1228. URL U.K./ttta://aalantooll. orgg/16--- -128
[21] Alex Krizhevsky, Vinod Nair, and Geoffrey Hinton. Cifar- 10 (canadian institute for advanced research). (ttp:/tt///wwr cs. toronto..... edu/ "ttp// cifar. html
[22] Zenan Li, Zehua Liu, Yuan Yao, Jingwei Xu, Taolue Chen, Xiaoxing Ma, and Jian [X) Learning with logical constraints but without shortcut satisfaction. In The Eleventh International Conference on Learning Representations, 2023. URL httpaapss//pppprrviiieee net/forumiid-aa -iNmmiiiieNNNuNNiii..
[23] Dmitry Malioutov and Kuldeep Meel. Mlic: A maxsat-based framework for learning interpretable classification rules. International Conference on Principles and Practice of Constraint Programming, pages 312-327. Springer, 2018.
[24] Yuhao Mao, Mark Niklas Mueller, Mare Fischer, and Martin Vechev. Connecting certified and adversarial training. In Teinth Conference on Neural Information Processing Systems, 2023. URL https wwwpreewwww..ee//foorrrdddddaaae
[25] Yuhao Mao, Mark Niklas Mueller, Mare Fischer, and Martin Vechev. TAPS: Con-
necting certified and adversarial training. https://github.cc www.:tt.cc/e/eeeeeeeooooooo wwwmm/thh-rr/tttt.ee wtt.stss/tteseeeeeeeee /tree/ 2023.
[26] Matthew Mirman, Timon Gehr, and Martin T. Vechev. Differentiable abstract interpretation for provably robust neural networks. In Jennifer G. Dy and Andreas Krause, editors, Proceedings of the 35th Interna- tional Conference on Machine Learning, ICMI. 2018, Stockholmsmässsan Stockholm, Sweden, July 10-15, 2018, volume 80 of Proceedings of Machine Learning Research, pages 3575-3583. PMLR, 2018. URL http://proceedinggs mlr, wwwpppessss.... ht01//00m/mmmmmmmm mirnn188b........ html
[27] Mark Niklas Mueller, Franziska Eckert, Mare Fischer, and Martin Vechev. SABR: Small adversarial bounding boxes. https://giithu www.ettttt.oooo sri/sabr 2023.
[28] Mark Niklas Mueller, Franziska Eckert, Marc Fischer, and Martin Vechev. Certified training: Small boxes are all you need. In The Eleventh International Conference on Learning Representations, 2023. URL https:///penrrevier
[29] Mark Niklas Müller, Christopher Brix, Stanley Bak, Changliu Liu, and Taylor T. Johnson. The third international verification of neural networks competition (van-comp 2022): Summary and results, 2022. URL (RLL/htts://arxit
orgp://i.oorrrooeooeoe abs 2212. 10376
[30] Yatin Nandwani, Abhishek Pathak, Mausam, and Parag Singla. primal dual formulation for deep learning with constraints. H. Wallach, H. Larochelle, A. Beygelzimer, d'Alché-Bue Buch, E. Fox. and R. Garnett, editors, Advances in Neural Information Processing Systems, volume 32. Curran As- sociates, Inc., 2019 URL https: http::/ppooccedeeee neurips http://peee.iiispeppeeeeee//eeee E.770ffcddecc(333sddddd4d3333333
12

---

[31] Alessandro De Palma, Rudy Bunel, Krishnamurthy Dvijotham, M. Pawan Kumar, and Robert Stanforth. 1bp regularization for verified adversarial robustness via wranch-andd-oundd 2023.
[32] Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Köpf, Edward Z. Yang. Zach DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang. Junjie Bai, and Soumith Chintala. Pytorch: An imperative style, high-performance deep learning library. CoRR, abs/1912.01 703, 2019. URL http::ttta//iiivv. http:////aaaii..oaaaa///////////
01703
[33] Hadi Pouransari and Saman Ghili. Tiny imagenet visual recognition challenge. CS 231N, 7, 2014.
[34]
Hadi Salman, Greg Yang. Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang. A convex relaxation barrier to tight robustness verification of neural networks. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelz- imer, Florence d' Alché-Buc, Emily B. Fox, and Roman Gamett, editors, Advances in Neural Information Processing Systems 32: Annual Conference on Newral Information Processing Systems 2019, NeurlPS 2019, December 1-1,, 2019, Vancouver, BC, Canada, pages 9832 9842, 2019, URL wttp:ttttptppoeeeeliiieiee Abstract.hmml
[35] Sanjit A. Seshia, Dorsa Sadigh, and S. Shankar Sastry. Toward verified artificial intelligence. Commun. ACM, 65(7):46 55, 2022. doi: 10. 10.1145/3503914 /RRLL/ttts:///oo.rrg// http:////000100r111011111/11/11
[36] Zhouxing Shi, Yihan Wang. Huan Zhang. Jinfeng Yi, and Cho-Jui Hsieh. Fast certified robust training with short warmup. In /CML, 202/ Workshop on Adversarial Machine Learning, 2021. URL. https
[37] Zhouxing Shi, Qirui Jin, Zico Kolter, Suman Jana, Cho-Jui Hsich, and Huan Zhang. Formal verification for neural networks with general nonlinearities via branch-and-boume 2023.
[38] Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin T. Vechev. Fast and effective robustness cortification. Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa- Dasa-Bianchi, and Roman Gamett, editors, Advances Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NewrIPS 2018, December 3-8, 2018, Montréal, Canada, pages 10825-10836, 2018 URL https: /ttp://////cceengge../.. werroceednnge.neurip.... wwweurip..ccpppppeeeee
2018 2018/haah/ htaaaa//t22444666eeeee/eeeddd///
html
[39] Gagandeep Singh, Timon Gehr, Markus Plschell and Martin T. Vechev, An abstract domain for certifying neural networks. Proc. ACM Program. Lang., (:1PL)::111-41:::5 2019. doi: 10. 145/22433293354 URL
https::/doi. org/ 10. 1145/3290354
[40] Richard Socher, Alex Perelygin, Jean Wu, Jason Chuang, Christopher D Manning, Andrew Y Ng, and Christopher Potts. Recursive deep models for semantic compositionality over a sentiment treebank. In Proceedings of the 2013 conference empirical methods in natural longuage processing, pages 1631-1642, 2013.
[41] Matthew Sotoudeh and Aditya Thakur. Prdun. https:// http:/uww..cc.//516aa//////////. 2021.
[42] Zhe Tao, Stephanie Nawas, Jacqueline Mitchell, and Aditya V. Thakur. Architecture- preserving provable repair of deep neural networks. Proc. ACM Program. Lang.. 7(PDDI,, jun 2023. doi: 10.1 10.1145/3591 URL http:::ttt//ooii org.://oo...rrroooo 10. 1145/3591138
[43] Christian Tjandraatmadja, Ross Anderson, Joey Huchette, Will Ma, Krunal Patel, and Juan Pablo Vielma. 'The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neu- ral network verification. In Hugo Larochelle, Mare' Aurelio Ranzato, Raia Hadsell, Maria- Florina Balcan, and Hsuan- Lin, editors. Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, Decem- ber 6-12, 2020, virtual, 2020. URL https: http:p////ccccedng....mm (B626804466609994956686888888 www.:e44220---sratt...om Abstract.html
wtwp:ipppccppppp/eeeeeee 22000/hash/
[44] Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J. Zico Kolter. Beta- crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. In Mare' Aurelio Ranzato, Alina Beygelzimer, Yann N. Dauphin, Percy Liang, and Jen- nifer Wortman Vaughan, editors, Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurlPS 2021, December 6-14. 2021, virtual, pages 29909-29921, 2021. URL #aa77/aadddcddffeeeeeeefffffaaaa htw.:eaaess22a--ttttttttttt.t
neure neur ips. cc/paaprr/202//ase
13

---

[45] Jingyi Xu, Zilu Zhang, Tal Friedman, Yitao Liang, and Guy Van den Broeck. A semantic loss function for deep learning with symbolic knowledge. In Jennifer Dy and Andreas Krause, editors, Proceedings of the 35th International Conference on Machine Learning, volume 80 Proceedings of Machine Learning Research, pages 5502-5511. PMLR, 10-15 5 Jul 2018. URL httphttts////rrceedding mlr wtt.:/swwww....../eeeeeeeee press/v80/ xu18h html
[46] Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsich. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In 9th International Conference Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net, 2021. URL BRLhhttp::/ ptsttps://peerrviee... www.:e/w..nee.oorrreeeo http
[47] Ziwei Xu, Yogesh Rawat, Yongkang Wong, Mohan S Kankanhalli, and Mubarak Shah. Don't pour cereal into coffee: Differentiahle temporal logic for temporal action segmentation. In S. Koyejo, Mohamed, A. Agarwal, D. Belgrave, K. Cho, and A. Oh, editors, Advances in Neural Information Processing Systems, volume 35, pages 14890-14903. Curran Asso- ciates, Inc., 2022. URL https: /ttp://///.occcee....s..a neurrii cc/ cc/paper.e... wwtpppppe..ielseppeeeeeeeeeeeeee 05962334660888229997/11113..3333 Paweee-Paaaperereeeeeeeeee
pdf
[48] Huan Zhang, Tsui-Wei Weng. Pin-Yu Chen, Cho-Jui Hsich, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi, and Roman Gar- nett, editors. Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada, pages 4944-4953, 2018. URL httpa://proceeddnge wwwpeeeeddnnnnnenuip.......m wwwrips.cc/papeet.ee cc/paper 004653
html
[49] Huan Zhang. Tsui- Wei Weng, Pin-Ye Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. Advances in neural information processing systems, 31, 2018.
[50] Huan Zhang, Zhouxing Shi, Kaidi Xu, Yihan Wang. Shiqi Wang, Linyi Li, Jinqi (Kathryn) Chen, and Zhuolin Yang. auto LiRPA: An automatic linear relaxation based perturbation analysis library for neural networks and general computational graphs. https: / /ttptbbttbbbt////////////t com Verified- Intel batellly wwwggnceeeaaeeeeeeee autoo_
LiRPA 2023.
14

---

A Proofs
Theorem 3,4. Given provable interval editing problem (Definition 3.2 for DNN N and parame- ters 0 with input bounds (x. x] and ouiput bounds v let EN xx.V.x.&. 0) be Parametric Linear Relaxation for N. Then the following linear program can be solved in polynomial time in the size of the DNN N. and whose solution is solution to the provable interval editing problem:
min | 0ll S.L. E.(2,V.X.::) 3 SyAysy)
Proof. Equation is a linear program that can be solved in polynomial in the size of the DNN N because by Definition 3.3 Ev (y...x x, x: 0) is poly-size linear formula whose size is polynomial in the size of the DNN N I.e., the number of parameters, layers, and the input and output dimensions of each layer.
Equation tion 3.3
is a solution to the provable interval editing problem (Definition 3.2) because by Defini-
x.X.X 0) implies Vx E x (x: E y..
Theorem 3.6. Definition 3.5 is Parametric Linear Relaxation for the DNN N.
Proof. Recall Definition 3.5
Σ (
(x
(((+)) "0.""
0SteL
where yy.y] def Ix x 4 and
x0)) del
X
Our goal is prove that (. 0) is
poly-size linear formula that implies
E X Nxx: 0) [y.vl
We first show that EN (y. 0) is poly-size linear formula. For Parametric Linear (1)
Relaxation Evrol ((+1) x ((+ x
0 0'3) for any layer A10 by Definition 3.3 we have
Exvee( (6+1) (((+)) x (8)
a poly-size linear formula whose size is polynomial the num- ber of parameters, input and output dimensions of layer A10), Therefore, we have E (y. Vxy x: 0) a poly-size linear formula whose size is polynomial in the number of parameters, layers, and the input and output dimensions of each layer.
Then we show that EN (. implies Vx E x x). NN 0) E yl. By Definition 3.3 we
have that the Parametric Linear Relaxation Evro (e+1) ((++)) implies the following formula:
(2) (0 )00) for any layer A/(e)
(1 E [x 1000 (x(00))))))) E (++11 (x
Therefore, have EN (y.F. lowing formula:
AusecLEyrool (Ett)) ((+))) x sel( (00)
implies the fol-
Vx (8) E (0, A (000)) E [x (++1) x((-))
OSFCL
where [y.y
def
x and xx (0) x del x). By induction, the formula above implies
Vxx E
x).
. (x: 0)
J. Therefore, proved that E xx, is poly-size linear for-
mula that implies Vx E xx x (x: y.
15

---

A.1 Proofs for Parametric Linear Relaxation of ReLU layers
Lemma A.I. EROLD FannyyJ... (y..& defined in Definition 3.8 a poly-size linear formula.
ReLu y. x) is a linear formula. Let be the number of input dimensions of ReI.U. E ERLLU y y. X x) has 3m linear constraints over 4m variables (& E Rmm
Proof. As seen in Definition 3.8
x E RR",, y E R and ÿ E R. Hence, EBALO ( y. &, x) is poly-size linear formula whose size is polynomial in the number of input dimensions of the ReLU layer.
Lemma A.2. E EROLD (y,,,,&)
def
FEOLU x) A PROLU (x, defined in Definition 3.8 implies
VX E x.. ReLU(x) y.y.
Proof. For the upper bound, recall that by Definition 3.8 we have
ReLl (V
xxy 2
Our goal is to prove that FROLU
x) implies
Vx E x. ReLU(x)
which is equivalent
2 max (ReLU(x) x x S }]
By the definition of the ReLU layer (Definition 3.7 we expand the formula above to
2 max { (max (x, 0}
x
Because max(x, 0} increases monotonically with respect the above formula is equivalent to
y 2 max(X, 0}
Because max 0} is convex function, the above formula equivalent
X 0
which is the definition of PReLD (V, X) in Definition 3.8 vx E [x. x). y 2 ReLU(x).
Therefore, we proved that FReLU (V. X) implies
For the lower bound, recall that by Definition
3.8 have
LRLLD
c
where T are constants such that 0 < C, S 1. Our goal is to prove that LROLD (,,8) implies
Vx
ReLU(x)
which is equivalent to By the definition of the ReLU layer (Definition 3.7 expand the formula above to
y min (ReLU(x)
x S x x
S min {max 0) X S x < X
Because max(xx 0} increases monotonically with respect to x, the above formula is equivalent to
Y S max 0}
which is equivalent to
i x V 5
Given constant vector e where < c < 1, Looto (8))
y cx implies the above formula.
Therefore, we proved that Lnewy (y implies Vx E \ x]. y S ReLU(x).
16

---

Lemma A.3. EneIo y. x)
def
PReLu (Y, A LRoL defined in Definition 3.8 implied by
y= = max (ReLU(x) x x - x). hence captures the exact upper bound.
Proof. Recall that by Definition 3.8
have
PReLU (
x)
def
For any solution (y' x. y max |ReLU (x)
x
we have
del max (R)
x
By the definition of ReLU layer (Definition function, the definition above is equivalent to
3.7
because ReLU is a monotonically increasing
max [x.0}
To prove that (F x) captures the exact upper bound, will show that (y", 3)) is a solution to PROLU (7, x). In other words, the following instantiated formula PReLU .)) is true:
BeLL
X y 20
By substituting y" defined in Equation aabvve our goal becomes
max X 0} 2 x A max X 0} 2 0
which is true. Hence, have proved that ERLLO (.......) captures the exact upper bound.
Theorem 3.9. Definition 3.8 a Parametrie Linear Relaxation for the ReLU layer that captures the exact upper bound.
Proof. By Lemma A.1 and Lemma A.2 we proved that RRLu (y, x) is poly-size lin- ear formula that implies Vx E x). ReLU(x) [y hence a Parametric Linear Relax- ation (Definition
3.3 for ReLU. By Lemma A.3] we proved that FRGLD (yyY X) is implied by
y max (x)
S x). hence captures the exact upper bound.
A.2 Proofs for Parametric Linear Relaxation of Affine layers with constant input bounds
Lemma A.4. Excr (y. W. b) defined in Definition 3.11 1111 is poly-size linear formula.
Proof. As seen in Definition 3.11 Facr V.V. W, b) a linear formula. Let m and n be the number of input and output dimensions of the Affine layer. T Ny,,x,, W, b) has 2n + 4mn linear constraints over 2m + 3n + 3mn variables (x E Rm R. R",
RR.ye R", W R V E Raxm and V R"xm). Hence, Earr (y. W. b) a poly-size linear formula whose size is polynomial in the number of input and output dimensions of the Affine layer.
Lemma A.5. Eett (y 1y x. W, b)
ARE x,, W,b) A Late (,, W.b) b) defined in Defini-
tion 3.11 implies vx E x x Affine (x: W.b) b) E yl.l
Proof. For the upper hound, recall that by Definition 3.11 have
Pa W, def
- V> Wx A V
Wx
our goal is to prove that Pett ( X.X. W. W.b) b) implies
Vx x 2 Affine(x; W.
We prove the above formula by proving for each Wy:
y, 2 max Affinee( W.b), / 1
17

---

By the definition of the Affine layer (Definition 3.10 we expand the formula above to
yj 2 max
Σ x, W, + +b
x SX
which is implied by the following formula
max
x;
Wii
X: S x;
+b;
k=0
Because PAsE (V. W, b) implies yy > ji by. by substituting the left-hand-side y, of the formula above with Di= + by. our goal becomes:
bj max (WWW, x 5x +b,
By subtracting by from both sides, our goal becomes:
max
xx W/r
x S x SX
1=0
1=0
Then we prove the above formula by proving for each
2 max
x; W/:
x. S x S
Because x, Wj changes monotonically with respect to X;, max
x; W/:
x S x; S 2x. is taken
x X.W X W3s }
when x; or x, In other words, max x, Wys
x; ك max
By substituting the sight-hand-side the above formula, our goal becomes:
V, J4 max
x W
W
The formula above is equivalent to VJ plied by (Y W) Therefore, we have proved that Fass (Y, W. b) implies Vx E y 2 Affine(x; W,b).
x j
V
X which is im-
For the lower bound, recall that by Definition 3.11 have
Pase X
Λ& +b, A v Wx A S Wx
our goal is to prove that Lers ( X.X. X. W. b) implies
Vx E x x y < Affine(x:W) W.b)
by proving for each j where y
ビ min Affine(x: W.b), x x
By the definition of the Affine layer (Definition 3.10p. we expand the formula above to
min Σ x Wr + +b, x
which is implied by the following formula
min
W/s X X +b,
0
18

---

Because Lare (,, W.b) implies Y = Ei= Vgj + bj. by substituting the seft-hand-side ", of the formula above with
Σ Vj: ji + bj, our goal becomes:
Σ
Vi + by s
min x; Wis
x Sx, SX. +b;
1=0
1=0
By subtracting b, from both sides, our goal becomes:
m
m
min
X
S x; S
Then we will prove for each i:
V S min
x S x Sx.
Because x, W/a changes monotonically with respect to x,, min
xx W/;
x, xx Sx. is taken
when x x; x, In other words, min Wx: x S < min By substituting the right-hand-side of the above formula, our goal becomes:
{ I Wi x W
Lix min & Wje W.W }
The formula above equivalent to L S x, W plied by & W. Therefore, we have proved that SArt S W. implies Vx E x S Affine(x: W)b.
X jo which is im- VI S x,
Lemma A.6. F.F... W.
de Patt (F.. A EaTr E W.b) de-
sined in Desinition 3.11
implied by y= max (Affine (x; W.b) Y min {Affine(x; W. b) x x<xsa x).
x x
hence captures the exact upper and lower bounds.
Proof. For the upper bound, recall that by Definition 3.11
we have
W)b)
Σ A =
by A V
Z
Wx
x
Wx
input y max ( (Affine W. defined as
Given
constant
bounds
X X
for any we have the exact constant output upper bound
solution
y
b)
to
max /Affine (x: W, x x By the definition of Affine layer (Definition 3.10p. it is equivalent to
def
max {x: x 5 x b
(10)
To prove that PAze captures the exact upper bound, we will show that by substituting (F" X. W b) in PAte xx W. b), the instantiated formula PArr (F' X. W. W.b). as shown below, is satisfiable:
Pusr .x,,
AT Σ
ji + by ^ V Wx
A
V>
wx
which is equivalent to prove the following formula for any index j::
Σ
+ b, A V2 Wx A V> Wx
By substituting y7 defined in Equation 10 above, our goal becomes
Σ max (x, W
x <<x< + by
Σ V H +b; A V2 Wx A V> wx
19

---

which is implied by
max W W x V V W
W y
If WW, ys 2 0, this formula. Hence, we have proved that Pass X. x, W b) is satisfiable and FaEt y X. W, b) captures the exact upper bound. For the lower bound, recall that by Definition 3.11
jt is solution to this formula; otherwise
w n is solution to
we have
Catt (f X.
AE
v + bb
V Wx
Wx
constant y min /Affine(x; W. b) defined as
Given
input
bounds
x x
for any we have the exact constant output lower bound
solution ( W.b) to
x X
min Afffine (x; W.b) x x x
By the definition of Affine layer (Definition 3.10). it equivalent
del
min W x x b,
(11)
To prove that Larg captures the exact lower bound, we will show that by substituting (y x X, W,b) in Late (y X.X, b), the instantiated formula Larr (y X.X, W,
W, b), as shown below, satisfiable:
Exre ly X.X.
del Ay ΣV bb A V A V Wx
which is equivalent to prove the following formula for any index j:
ΣE, +b, A V Wx A V < Wx
By substituting Y defined in Equation II above, our goal becomes
Σ min x W
x x +b, = ΣV, +b, A V Wx A V Wx
which is implied by
min x W
x Y A V, < W W V, W
W / 2 0. def x is solution this formula; otherwise V def W J solution to this formula. Hence, we have proved that Pase (y", X.X. b) is satisfiable and Paat x W, b) captures the exact lower bound.
Theorem 3.12. Desinition 3. Parametric Linear Relaxation for the Affine layer with constant inpul bounds x x] that captures the exact lower and upper bounds.
Proof. By Lemma A.4 and Lemma A.5 we proved that Eerr (V. W.b) is poly-size linear formula that implies Vx E x). Affine (x: W. b) y]. hence is Parametric Linear Relax- ation (Definition 3.3) for the Affine layer. By Lemma A.6 we proved that Earr (y. X W. 6) is
implied by y max { |Affine (x; W, b) x x) Ay min {Affine(x; W.b) x S x
hence captures the exact upper and lower bounds.
20

---

A.3 Proofs for Parametric Linear Relaxation of Affine layers with variable input bounds Lemma A.7. Earr (y. X, W. b) defined in Definition 3.13 is poly-size linear formula.
Proof. As seen in Definition 3.13 Last &, b) a linear formula. Let m and n be the number of input and output dimensions of the Affine layer. ( f.J.K,.. W, b) has 2n linear constraints over 2m + 3n variables & Rmm I E R". y E R and y R*). Hence, Parr y. X, W, b) is poly-size linear formula whose size is polynomial in the number of input and output dimensions of the Affine layer.
Lemma A.8. Part y.y.&. W, b)
FAZt & W, Lare &Y, W, b) defined Defini- tion 3.13 implies that Vx E X x Affine x: W. b) y.yl.
Proof. For the upper bound, recall that by Definition 3.13,
we have
X.W, if 20
Past ( W. b) del AJ, Σ ja + b, where
W ji otherwise def
Our goal to prove that Fxrr (. &. X, W, b) implies
Vx E y 2 Affine(x: W)
We prove the above formula by proving for each y;;
y, max Affine(x; W. b), x x
By the definition of the Affine layer (Definition 3.10p. expand the formula above
y, 2 max
Σ W + +b
|
which is implied by the following formula
WNx & Sx S 82, + +b;,
By Definition 3.13 Pacc ( X W, b) implies y, = Σ + by. By substituting the left-hand-
side y, of the formula above with Σ 4 + b,. our goal becomes:
m
by max Wr x S x;
xx, +b,
By subtracting b, from both sides, our goal becomes:
max {x, W
& 5x {x}
Then we prove the above formula by proving for each
j max (x, Wi
* < x [x
X, W
W 2 0
For the left-hand-side, we have j
j W
For the right-hand-side, be-
otherwise"
ji
cause x, W/r changes monotonically with respect to x,, and W jt is given constant,
21

---

have max x Wji & S x; S x inition of the left-hand-sin V ji VX E [x y 2 Affine W, b).
X
ji ji
W 20
which is the same as the def-
X
W
otherwise"
Thus, we have proved that ( W,b) b) implies
For the lower bound, recall that by Definition 3.13 we have
def X Waa ji Wx20
Late V..
AE EV: i + by where
V X W otherwise
Our goal is to prove that Lift (y x W. b) implies
Vx x y S Affineex: W.b)
We prove the above formula by proving for each y
- min
A W. b)j
By the definition of the Affine layer (Definition 3.10). we expand the formula above
Y min Σx Wy; +b,
85
which is implied by the following formula
min (x W
S x, I {:} + +b; X;
2=0
By Definition 3.13 Care y X X, W, b) implies Y,
i== + by. By substituting the left-hand-
m
side y of the formula above with m Vgs by. our goal becomes:
by min (x, W
x; S x.) + b
By subtracting b, from both sides, our goal becomes:
m
min [x, Wj:
x S x;
S
Then we prove the above formula by proving for each
V S min
(x, W/r
x S x, {
W Ja 2
For the left-hand-side, we have def
For the right-hand-side, be- cause W,W changes monotonically with respect to X;, and W given constant, we X W
x, W otherwise
W 20 0 which is the same as the def- X,W ja otherwise'
have min x W/ x x [x}
inition of the left-hand-side Vza- Vx E &
Thus, we have proved that ( W. b) implies
x). y S Affine(x; W, b).
Lemma A.9. Excs (y.y, W.b) de PArt ( A Lect ( W b) de-
fined Definition
3.13
implied by y= max (Affine(x: W. b)
x
y min (Affine(x: W. b)
x < hence captures the exact upper and lower bounds.
22

---

Proof. For the upper bound, recall that by Definition 3.13 we have
del W ja 20
PAZE ( AV, - Σ + bj where
ja otherwise
For any solution xx" b, yo max (Affine(x: W. stant output upper bound defined as
x we have the exact con-
max Affine (x: W.b) x < x
By the definition of Affine layer (Definition 3.10 equivalent
max x, W
Σ b,
(12)
To prove that PAtt captures the exact upper bound, we will show that XXX, b) is solution to
PArt & W, b). In other words, the following instantiated formula PArt ( X, W.b) is true:
PAZS V
X b)
AJJ = Σ s
where V def x W W ,i 2 0, otherwise
def
W já-
This formula is equivalent to prove the following formula for any index j:
y
+ bb;
By substituting yj defined in Equation 12 above, goal becomes
Σ max {x W j
<x xxxxx++
+b;
-V +b;
which is implied by
max x, W ji
< X j
If W ja O, max x W ji x < x max x W X x X X W,,
x, W,W, V ji. the above formula is true; Otherwise, the above formula true. Hence, we have proved that Are X.X, W, b) is true and A ( W b) captures the exact upper bound.
jis
For the lower bound, recall that by Definition 3.13 we have
del W a if W,,0
Larr S W.b)
Λ ΣV, f + by where
der
ja otherwise
For any solution (y' X, b) to min (Affine W.b) stant output lower bound defined as
x/. we have the exact con-
min (Affine (x: W.b) x S
By the definition of Affine layer (Definition 3.10p. it is equivalent to min {x, W S x x bb
def
(13)
To prove that Lart captures the exact lower bound, we will show that (y" (y",x,X, x, is solution to
P ( & x, W. b). In other words, the following instantiated formula Leet (y", xx W,b) is true:
Lace xxx,x, W.b) def Ax EV js + b,
23

---

where V def W if W f 2 0, otherwise V def X W
This formula is equivalent to prove the following formula for any index j:
Σ V b,
By substituting y defined in Equation 13 above, our goal becomes
Σ min {x. x<x +b, = VV, +b
which is implied by
min ( ji
Vi
W ji 2 O, min {x, W x < = x W = V jis the above formula is true; Otherwise, min x, W X x = X,W, W ji = ji the above formula is true. Hence, we have proved that X.X, W, b) is true and Latt X X, W.b) b) captures the exact lower bound.
Theorem 3.14. Definition 3.13 is Parametric Linear Relaxation for the Affine layer with variable input bounds & x that captures the exact upper and lower bounds.
Proof. By Lemma A.7 and Lemma A.8 we proved that Eate (yV. W, is poly-size linear formula that implies Vx [x. Affine W. b)
[ y]. hence is Parametric Linear Relax-
ation (Definition 3.3) for the Affine layer. By Lemma
A.9 we proved that Eere (y.8,, W, b) is
implied by y = max Affine (x; W. () X < S x) Ay = min (Affine W. x x hence captures the exact upper and lower bounds.
B General provable editing via Parametric Linear Relaxation
In this section we present our approach for solving the general provable editing problem (Defini- tion 1.1b
Definition B.1. Given Parametric Linear Relaxation E
xx for DNN N with parameters
0, an input polytope P def {x Dx S e). an output polytope Q {y Ay S b}. Given hyperpa- rameter & so that we only edit the DNN layers A((k=) starting from the kth layer. Then solution to the following linear program is a solution to the provable editing problem of Definition I.I
s.t. Ex (k) (k), (1:2)
min |
01l
(14)
where a sound constant interval bound (x) x(k] for the input (A) to the slice (((k=) to edit is computed by a sound bound propagation tool of DNNs like DeepPoly [39], auto LiRPA (50) and DeepT [4:
_uto_LiRPA
def
Compute Compute_Bound,yye (P; (00k))
(15)
The output constraint cyy v.,4A. b) encodes Ay < b for all E y..] using the parametric output
bounds y is defined as follows:
A A 20
di (Yy.AAAbb)
E b, where Egj
(16)
A Auyy
otherwise

---

B.1 Provable editing for multiple properties via Parametric Linear Relaxation
Given n properties defined by input polytopes P,
def
{x
,Dx ,e), and output polytopes
Q def
y Ay .b). This work can directly generalize to provably edit multiple properties:
min ||0 0|l
s.t.
A 0Si<n
P. N(x 0) Q
(17)
In particular, most of our experiments in Section 4 involve editing DNNs for multiple properties altogether. Here we present our formulation for provably editing multiple properties, which encodes the conjunction of the constraints for each property.
Evaus Fx (x ( A 0S*<
min |
01l
s.t.
(18)
where
x
Srnpute_Bounde wrois (Pos) 0(0kk))))
B.2 Provable editing for disjunctive properties via Parametric Linear Relaxation
Given a property defined by an input polytope P {x Dx S <e). and possible output polytopes
Qj y Ay S ,b}. this work can directly generalize to provably edit disjunctive property:
min 0 Oll s.t. Vx
V 0$j<n
N(x: EQ
(19)
by using a mixed-integer linear programming (MILP) solver. In particular, some properties in VNN-COMP (Section 4.1) involve editing DNNs for such disjunctive properties. Here we present our formulation:
min 0 Oll s.t.
T E
(k)
V 05j<n
((,,),JA,,b))
(20)
where (k)
[k)
((0:k)).
C Parametric Linear Relaxation for Tanh, Sigmoid and ELU layers
C.1 Parametric Linear Relaxation for Tanh layers
Definition C.1. y def Tanh(x) with input R and output y E R is defined as y; def tanh(xx).
Definition C.2. For Tanh layer with variable input bounds x), its Parametric Linear Relaxation is defined as Tran (,,
der
Frank (y, Lrann (y,x) where:
P (,))
def
Tanh
y "x b"
(21)
Tanh
A
b'
where Rmm a" E R.m b" E I are constants that satisfy the following two conditions: i) let f(x) = a + bj, the line defined by function fx) is tangent the concave piece of tanh at some x 2 0: ii) axxx + bb 3 = Txnh(x"); viz., the line defined by function f(x) intersects with convex piece of tanh at x²" where x"" O.
m b' E " are constants that satisfy the following two conditions: i) let f(x) a b/, the line defined by function f(x) is tangent the convex piece of tanh some 0: ii) x +b' Tanh(x'); viz., the line defined by function f(x) intersects with concave piece of tanh at x where x 0.
Similarly, x' E _ al E _m
Theorem C.3. Definition C.2 is Parametric Linear Relaxation for the Tanh layer.
25

---

Proof. As seen in Definition C.2 Tanh (y.. is linear formula. Let m be the number of input dimensions of Tanh. E Erana V. x) has 4m linear constraints over 4m variables ( E R X, X) is poly-size linear formula, whose size is polynomial in the number of input dimensions of the Tanh layer.
X E I E Rd and y E I)",, Hence, Taa (y.y, Vyy,
Now goal is to prove that Tranh yy X) defined in Definition C.2 implies
vx E
X y S Tanh(x) y
We will discuss the upper and lower bounds separately.
For the upper bound constraint Tranh (f.x) der y Tanh(x") y a + b". for the case when & S. x we have y; 2 tamh(x;)) tam)(x;) because tanh is monotonically increasing. For the case when &; x We have y, a, + b 2 tanh(x;) because f(x) a + by tangent to the concave piece of tanh in Prant (y.x) defined in Definition C.2 implies that Vx E [. Tanh(x) sy.
oo). and tanh is monotonically increasing in [x] OJ. Therefore,
For the lower bound constraint LTant (y, < Txnh(x') A y S a'x b', for the case when X; 2 x we have y, I tanh(x() I tanh(x;) because tanh is monotonically increasing. For the case when &; < x we have y S a + bj. z Lanh(x;) because f(xx = a/x + by is tangent to the convex piece of tanh in [-o0,0] 0j. and tanh is monotonically increasing in x0,x]]. Therefore, Lranh (F)
defined in Definition C.2 implies that vx E X y Tanh(x).
C.2 Parametric Linear Relaxation for Sigmoid layers
Definition C.4. y deff Sigmoid(x) with input x e R and output y R" is defined as y; def
T+e
Definition C.5. For Sigmoid layer with variable input bounds [ x), its Parametric Linear Relaxation is defined as P Sigaoiia (
def
Psigmosa (XX) L Signoid
where:
P Psigmoid (X
def y Sigmoid(x") y a "x b
(22)
Lsignoid x
Sigmoid(x')
a'x b'
where x E IRm a E RT, b" E R are constants that satisfy the following two conditions: i) let f(x)= = a, x + by. the line defined by function f(x) is tangent to the concave piece of sigmoid at some x 2 0; ii) a axx" + bb convex piece of sigmoid x," where x 0.
sigmoid(x"):: viz., the line defined by function f(x) intersects with
Similarly, x' E Ihm a² E Rmm" b' E Ih' are constants that satisfy the following two conditions: i) let f(x) a/ + by. the line defined by function f(x) tangent the convex piece of sigmoid at some x 0; ii) a'x' b' Sigmoid(x')) viz., the line defined by function f(z) intersects with concave piece of sigmoid at x where x 2 0.
Theorem C.6. Definition C.5 is Parametric Linear Relaxation for the Sigmoid layer.
Proof. As seen in Definition of input dimensions of Sigmoid. Esignoia y x.
P gioid ( x)) is a linear formula. Let be the number X) has 4m linear constraints over 4m variables & E RT IRT y R and ý ".. Hence, Esignoid {, is a poly-size linear formula, whose size is polynomial in the number of input dimensions of the Sigmoid layer.
C.5
Now our goal is to prove that 7
Esignosa
Y. X.X
X) defined in Definition
C.5 implies
Vx
x y < Sigmoid(x) $
We will discuss the upper and lower bounds separately.
For the upper bound constraint Ssigmoia (y, x) def y 2 Sigmoid(x") A y > a b², for the case when x; S x", we have y, 2 sigmoid(x!)) 2 si sigmoid(x;) because sigmoid is monotoni- cally increasing. For the case when &; > x", we have y, 2 a ".x + by 2 sigmoid(X:) because
26

---

fx) = a + by¹ is tangent to the concave piece of sigmoid in [0, oo), and sigmoid is mono- tonically increasing in [x, O]. Therefore, Pssgnota (y.x) x) defined in Definition C.5 implies that Vx E x]. Sigmoid(x)) y.
S Sigmoid(x') ^ y S a + b'. for the case when x; 2 x we have y, S sigmoid (x)) S (iigmid(X)) because sigmoid is monotonically b - sigmoid(x;) because f(x) a bj is tangent to the convex piece of sigmoid in [-00, 0l, and sigmoid monotonically increasing in [0. x Therefore, Esignoia (y.)) defined in Definition C.5 implies that Vx X x). y Sigmoid(x).
For the lower bound constraint Esignoia ( def
increasing. For the case when x we have S a/ +b;
C.3 Parametric Linear Relaxation for ELU layers
Definition C.7. ELU(x)
with input x E I and output y E R is defined as y; def elu(x,)
where elu(x) def
x
and > 0.
aa(e" 1)
Definition C.8. For ELU layer with variable input bounds [x, x its Parametric Linear Relaxation is
defined F BLD
def
FELU (y, A PELU y
where:
PELD (y,)
def 2
(23)
EEL
x)
def
+b
where a E IR"" b E R are constants such that the line detined by f(x) a, + b; for any i is langent to elu.
Theorem C.9, Definition C.8 is Parametric Linear Relaxation for the ELU layer.
Proof. As seen in Definition C.8 P (y. (. is linear formula. Let m be the number of input dimensions of ELU. PELO ( yx x) has 3m linear constraints over 4m variables (& R X E R
y E RD and y ) Hence, FELU ( y, & x) is poly-size linear formula, whose size is polynomial in the number of imput dimensions of the ELU layer.
Now our goal is to prove that F y. & X) defined in Definition C.8
implies
R X ELU(x) y
We will discuss the upper and lower bounds separately.
For the upper bound constraint FeceeainnFFuurle y tion C.7 we have y, 2 X = elu(X,). For the case x; < O, because elu is monotonically increasing elu(X,). Therefore, PeLu (f, defined in Definition C.8 implies
0, for the when x; 0, by Defini-
and elu that vx
we have y, X. x]. [LU(x) y.
< ax b, because the line defined by f(x) = a, b, is tangent elu and elu a convex function, we have y S a + b; S elu Therefore, Ea (y.x) defined in Definition C.8 imimllss that Vx E [. S ELU(x).
For the lower bound constraint FLL x
D Experiment Details
D.1 Provable fine-tuning PFT(.)
Because there are no efficient prior approaches for provable editing, we implemented provable fine-tuning PFT() baselines that combine prior (noo-bbovbble) DNN editing approaches with verifier in the loop: the editing stops when the verifier confirms that the DNN satisfies the property (Appendix D.1). Specifically: 1) In each epoch, provable fine-tuning first updates the DNN parameters with the DNN editing approach; 2) the editing approach or adversarial attack cannot find any constraint violation, call a verifier to check if all constraints satisfied; 3) If all constraints
27

---

are satisfied, the loop terminates; otherwise the loop continues. According to the DNN architecture and editing property, we use the best verifier from (1) a a.3-CR 466 44]: winner of the VNN Competition VNN-COMP 2021, 2022 and 2023; (2) MN-BaB [ runner-up of VNN-COMP 2022 and 2023; and (3) DeepT state-of-the-an (incomplete) transformer verifier.
In order to improve the performance of provable fine-tuning with non-provable DNN editing approach, viz., preserve the DNN's accuracy, we a) freeze all batch normalization layers, b) only edit the last few layers, c) incorporate changes of parameters as regularization, and d) sample points and incorporate the changes in their outputs as regularization.
D.2 Provable Editing on VNN Competition Benchmarks
In this section we present the further details for S.cttion4.1
Benchmarks. We take 12 out of 15 benchmarks from VNN-COMP'22 29 excluding i) aaarvana_unet.am 2022" and "nn4sys": the support for the sigmoid activation function is not implemented in PREPARED, and is not supported by APRNN. ii) "vggnet16 2022": the bound computation for intermediate layers runs out of CPU and GPU memory using auto LiRPA.
Setup details. For both PFT(DL2) and PFT((PRRI), we use a.,B-CROW, the winner of VNN-COMP, as the verifier. We only call the verifier when DL2 cannot find counterexamples. For all approaches, we edit the last few layers, which differs for different or DeepPoly to compute the constant bounds for the
DL2 find counterexamples to edit, and
DNNs. For PREP ARED, we use input to the first layer to edit.
Hyperparameters for PFT(DL2). SGD optimizer with learning rate of 0.001, DL2 weight of 0.2, batch size of 32 for the single-property setting, and 256 for the all-properties setting.
Hyperparameters for PFT(AP)N)). For different DNNs, APRNN edits from the last six layers to the last layer. we set a bound of [-10, 10] for the change of each parameter. We use DL2 to find counterexamples for APRNN to edit in each epoch, and use the same hyperparameters as the DL2 experiments for the DL2 oracle.
Hyperparameters for PREPARED. For different DNNs, PREPARES edits from the last eight layers to the last layer. We use auto_LiRPA (50] or DeepPoly (39 to compute the input bounds to the first layer to edit. we set bound of [-10, 10] for the change of each parameter.
Results details. In Table we present the number of succeed instances for provably editing single-properties and all-properties instances in each benchmark.
D.3 Local robustness editing for image-recognition DNNs
In this section we present the experiment details for Section
4.2
Property. Given - local robustness perturbation for DNN N and pair of input point x and output label I, the repair specification Vx'. ||x - x' 2/oloo =
arg max = L. other words, for all inputs x' in the 0e ball around x with radius the DNN N should classify them as label
Setup details. The validation set is the same 10% of the training set, randomly selected with seed O. For PFT(DL2), PFT(SABR) and PFT(STAPS), we use MN-BaB, the complete verifier used by SABR and STAPS, as the verifier in the loop. MN-BaB is the runner-up of VNN-COMP. We only call the verifier when DL2, SABR or STAPS cannot find counterexamples. For PREPARED, we use DeepPoly to compute the constant bounds for the input to the first layer to edit.
Hyperparameters for PSA(R)) We take the base hyperparameters from the SABR training script (27). We freeze all batch normalization layers. and search the hyperparameters: i) learn- ing rate (5e-4, 1c-4, 5c-5, 1e-5): ii) batch size in (5, 10, 25}: iii) lambda in {0.1, 0.2,.... ..... 0.9); iv) end epoch_epsssseeeeeeeeeeeeeeeppe in {80, 60, 40, 20}: v) fine-tune the entire DNN, the last three layers, or the last layer to find the edit with the highest efficacy, then the best validation set accuracy. Other hyperparam-
eters are the same as used for training the CIFARIO 10 (s 2/255) and TINYIMAGENET (8 = 1/255) CNN7 in the SABR paper. We use the following early-stopping criteria: i) CIFAR 10: validation accuracy drops below 60%; ii) TINYIMAGNNE::
validation accuracy drops below 20%. The final hyperparameters for CIFAR10 are: Adam optimizer with learning rate of 5e-4, batch size of 5,
28

---

Table 4: Comparison of the number of succeed instances for provably editing single-instances and aal-propesties instances in each benchmark.
(a) Comparison of the number of instances succeeded for provably editing single-instances instances in each
benchmark.
Benchmark
PFT(D12)
PFT(APREM)
PREPARED
Total
acasxu
0
5
47
47
rl benchmarks
103
84
103
103
tllverifybench
20
5
21
cifari00 Lanyimagenet_ressne resnet
29
@ri_reanet_a
8
2
52
52
reanet
8
0
44
44
reach secth__robb__eeeee
0
0
14
14
mnist_fc
1
1
22
22
cifar biasfield
0
4
4
cifar2020
35
0
55
55
collins collins_rul_cee rnn_enn
8
20
27
oval21
0
5
all
185
117
423
423
(b) Comparison of the number of instances succeeded for provably editing all-properties instances in each benchmark.
Benchmark
PFT(DL2)
PFT(APRXX)
PREP ARED
Total
38
40
42
42
rl benchmarks tllverifybench"
0
1
2
3
0
0
0
0
cifar100_tii haaar000__dnyiingeee_eeeeeee
0
0
5
5
sri resnet_a a sri uri_reanet__ reach prop_deesiitt density mnist_fc cifar biasffeldd
0
1
1
1
0
0
2
1
3
2
3
3
0
0
0
0
cifar2020
0
1
3
3
colline_rul_cnn
0
0
0
3
oval21
2
2
2
2
all
45
48
62
66
The DNNs that violate the properties benchmarks only one prop- erty, hence are subsumed in the prior single-property setting and excluded in this all- all-properties setting.
lambda of 0.1, aad__epoch_epp_ of 80, and fine-tune the last three layers. The final hyperparameters for TINYIMAGENET are: Adam optimizer with a learning rate 5e-4, batch size lambda of O. end_epoch_eps of 80, and fine-tune the last three layers.
Hyperparameterss for PFT(STAPS). We take the base hyperparameters from the STAPS training script in the TAPS code 25 We freeze all batch normalization layers, and search the following hyperpa- rameters: i) learning rate (5c-4, le-4, 5c-5, lc-5): batch size {5, 10, 25): : iii) reg lambda in (0.1, 0.2, ... 0.9): iv) and_epoch_eee
in [80, 60, 40, 20). v) fine-tune the entire DNN, the last three layers, or the last layer. to find the edit with the highest efficacy, then the best validation set accuracy.
Other hyperparameters are same as used for training CIFARIO (s = 2/255) and TINYIMAGENE 1/255) CNN7 using STAPS in the TAPS paper We use the following early-stopping criteria: i) CIFAR10: validation accuracy drops below 60%; ii) TINYIMAGENET: validation accuracy drops
29

---

below 20%. The final hyperparameters for CIFARIO are: Adam optimizer with a learning rate of 1e-5, batch size of 10, reg lambda of 0.9, end epoch eps of 80, and fine-tune the last three layers. The final hyperparameters for TINYIMAGENET are: Adam optimizer with a Learning rate of 1e-5, batch size of 10, reg_ lambda of 0.8, end_ aadd_epoch_eps_ of 80, and fine-tune the last three layers.
Hyperparameters for (FT()) We take the base hyperparameters from the RobustnessG training script the DL2 code [.] We freeze all the batch normalization layers, and search for the following hyperparameters: i) learning rate in { {1e-3, 5e-4, le-4, 5e-53; 3; ii) batch size in (5, 10, 25}; iii) fine-tune the entire DNN, the last layer or the last three layers. to find the edit with the highest efficacy, then the best validation set accuracy. We use the following early-stopping criteria: i) CIFAR I0: validation accuracy drops below 70%: ii) TINYIMAGENET: validation accuracy drops below 20%. The final hyperparameters for CIFAR 10 are: SGD optimizer with learning rate of 1c-4, batch size of 10, DL2 weight of 0.2, fine-tune the last three layers. The final hyperparameters for TINYIMAGENET are: SGD optimizer with learning rate of le-4, batch size of 10, DL2 weight of 0.2, fine-tune the last three layers.
Tlyperaarameters for APRNN. We edit up to the fifth last layer, and set a bound [-10, 10] for the change of each DNN parameter. For both CIFARIO and TINYIMAGENET, the final result comes from editing the last layer.
Hyperparameters for PREPARED. We edit up the fifth last layer, and set bound [-10, 10] for the change of each DNN parameter. For both CIFAR 10 and TINYÍMAGENET, the final result comes from editing the last layer.
D.4 Local robustness editing for sentiment classification BERT transformers
In this section we present the experiment details for Section 4.3
Setup details. We use the default validation set used in the DeepT training scripts 3 For PFT(DL2), we use DeepT as the verifier in the loop. We only call the verifier when DL2 cannot find counterexamples. For PREPARED, we use DeepT to compute the constant bounds for the input to the first layer to edit.
Hyperparameters for PFT(D We incorporate the default training script and hyperparameters from DeepT 44. We search the hyperparameters i) fine-tune the last three layers or only the last layer; ii) batch size in {4. 8, 16, 32): iii) learning rate in ( (1e-3, 5e-3, le-4, 5c-4]; J; to find the edit with the best efficacy, then the best validation accuracy. For s=1e-4, the final hyperparameters are: fine-tune the last layer, batch size of 32, Adam optimizer with learning rate of Ic-4, DL2 weight of 0.1 For E=Se-4, the final hyperparameters are: fine-tune the last layer, batch size of 16, Adam optimizer with learning rate of le-4, DL2 weight of 0.1.
Hyperparameters for PAP We edit up to the third last layer, and set a bound [-10, 10] for the change of each DNN parameter. The final result comes from editing the last layer.
Hyperparameters for PREPARED. We edit up to the third last layer, and set a bound [-10, 10] for the change of each DNN parameter. The final result comes from editing the last layer.
D.5 Provable training for physics-plausible DNNs
In this section we present the experiment details for Section 4.4
Hyperparameters for DL2. We search the hyperparameters batch size in {4, 8, 16, 32); ii) lear- ing rate in [le-3, 5e-3, lc-4, 5e-4J; We train 2000 epochs and take the epoch with the highest validation accuracy. The final hyperparameters are: batch size of SGD optimizer with Ir of Ie-3, DL2 weight of 0.2, 1241 epochs.
Hyperparameters for GD. We search the hyperparameters batch size in (4. 8, 16, 32); ii) learning rate in ( 1e-3, 5e-3, le-4, 5e-4]; We train 2000 epochs and take the epoch with the highest validation accuracy. The final hyperparameters are: batch size of 32, SGD optimizer with Ir of 1e-3, 635 epochs.
Hyperparameters for GD(APRNN). We edit up to the first layer, and set a bound [-10, 10] for the change of each DNN parameter. The final result comes from editing the last layer.
30

---

Hyperparameters for (D We edit to the first layer, and set bound [-10, 10] for the change of each DNN parameter. We use DeepPoly compute the input bounds to the first layer to edit. The final result comes from editing the last three layers.
31

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification:
The theoretical claims in the abstract and introduction are proved in Section
as well as Appendix A
The empirical claims in the abstract and introduction are justified
in Section
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No
NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
is fine to include aspirational goals as motivation as long as is clear that these goals not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
Justification:
The limitations are discussed in Section
Guidelines:
The answer NA means that the paper has limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create a separate "Limitations" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (c.g.. independence assumptions, noiseless settings, model sell-speciiiatiinn asymptotic approximations only holding locally). ). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution low or images are taken in low lighting. Or speech-to-tex, system might not be used reliably to provide closed captions for online lectures because it fails handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and faimesss.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community, Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory Assumptions and Proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
32

---

Answer: [Yes]
Justification: The full set of assumptions and informal proof sketch are provided in Section complemented by formal proofs in Appendix A
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced in the statement of any theorems.
The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental Result Reproducibility
Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that affects the main claims and/or conclusions of the paper (regardless whether the code and data are provided or not)?
Question:
Answer: [Yes]
Justification: Section Berioonnoommpg complemented by Appendix fully disclose all information needed to reproduce the techmique, and Section 4 complemented by Appendix D fully disclose all information needed to reproduce the experimental results.
Guidelines:
The answer NA means that the paper does not include experiments. If the paper includes experiments, No answer this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is a novel architecture, describing the architecture fully might suffice, or if the contribution is specific model and empirical evaluation, it may be necessary to either make it possible for others to replicate the model with the same dataset, or provide access the model. In general. releasing code and data is often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how replicate the results, access a hosted model (e.g.. in the case of large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
While NeurIPS does not require releasing code, the conference does require submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) the contribution is primarily a new algorithm, the paper should make clear how reproduce that algorithm. (b) If the contribution is primarily
model architecture, the paper should describe the architecture clearly and fully.
(c) the contribution is a new model (e.g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should possible for other researchers to have some path to reproducing verifying the results.
33

---

5. Open access to data and code
Question: Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, described in supplemental material?
Answer: [No]
open-access benchmarks. We plan to release on acceptance the data we generated for Section 4.4 For the implementation of our tool, could not make the code open access due ongoing IP restrictions.
Justification:
The experiments Section 4.1
4.3
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurlPS code and data submission guidelines (https://nips cc/
for more details.
While we encourage the release of code and data, we understand that this might be possible, so "No" is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurIPS code and data submission guidelines (https
tniiss.cc/uublic//ee
for more details.
The authors should provide instructions data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information as possible in supplemental material (appended to the paper) recommended, but including URLs to data and code is permitted.
6. Experimental Setting/Details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification: The experimental settings presented in Section complemented by further details Appendix D.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the of the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, or as supplemental material.
7. Experiment Statistical Significance
Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Answer: [No]
Justification: Because the proposed algorithm is deterministic, we instead evaluate our approach on wide-variety of benchmarks to demonstrate its efficacy and efficiency.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by enror bars, confi- dence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper.
34

---

The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g.. Normally distributed errors).
It should be clear whether the error bar is the standard deviation the standard error of the mean.
It is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not show in tables figures symmetric error bars that would yield results that are out range (e.g. negative error rates).
error bars are reported in tables or plots, The authors should explain the text how they were calculated and reference the corresponding figures or tables in the text.
8. Experiments Compute Resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed reproduce the experiments?
Question:
Answer: [Yes]
Justification:
The evaluation platform and runtime are provided in Section
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount compute required for each of the individual experimental runs as well estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't make into the paper).
9. Code Of Ethics
Question: Does the research conducted the paper conform, in every respect, with the NeurlPS Code of Ethics https: httee:///eeuuiieee hww.rpsu...../ http://urripss...cccc/////ttttta ctc//ubllc/thiicccuddel.....
Answer: [Yes]
Justification: The research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics.
Guidelines:
The answer NA means that the authors have reviewed the NeurIPS Code of Ethics.
the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (c.g.. there special consid- eration due to laws or regulations in their jurisdiction).
10. Broader Impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [Yes]
Justification: This is discussed in Sections D and
Guidelines:
The answer NA means that there is no societal impact of the work performed.
35

---

If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), faimess considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and tied to particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional unintentional) misuse of the technology.
If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g.. gated release of models, providing defenses in addition attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of ML).
11. Safeguards
Question:
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Answer: [NA]
Justification: This paper proposes an efficient and provable DNN editing approach, which does not involve releasing of data and models that have high risk for misuse.
Guidelines:
The answer NA means that the paper poses no such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [Yes]
Section 4 cites the original papers that produced the baselines, tools, models and benchmarks used in the paper. Appendix D cites commits for open-access code and scripts used in the paper.
Justification:
Guidelines:
The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package dataset.
The authors should state which version of the asset used and, possible, include URL.
The name of the license (c.g., CC-BY 4.0) should be included for each asset.
36

---

For scraped data from a particular source (e.g., website). the copyright and terms of service of that souree should be provided.
assets are released, the license, copyright information, and terms use in the datasets.paperssiii paperswi thcode. www.coo//aaaaa datasets package should be provided. For popular datasets,
has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.
If this information is not available online, the authors are encouraged to reach out to the asset's s creators.
13. New Assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [NA]
Justification:
We do not introduce new assets in the paper.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/code/mmodl as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent obtained from people whose asset is used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsourcing and Research with Human Subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given participants and screenshots, if applicable, as well as details about compensation (if any)?
Answer: [NA]
Justification:
This paper does not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included in the main paper.
According to the NeurlPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional Review Board (IRB) Approvals or Equivalent for Research with Human Subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification:
This paper does involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsoureing nor research with human subjects.
37

---

Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review.
38


Reviews:
[{"review_id": "OAtebXwTC1", "reviewer": "Reviewer_UT9i", "summary": "The paper proposes a novel method for provably editing neural networks using neural network verification techniques. The proposed method is based on a new linear programming formulation of neural networks. Unlike typical neural network verification settings, in the neural network editing settings, the weights are also variables that will multiply to neural network features, and this is challenging to handle. The proposed formulation constructs the lower and upper bounds of each neuron as linear program variables separately, which offers some benefits when dealing with weight variables. Experiments were conducted in multiple settings to demonstrate that the proposed method achieves better efficacy and efficiency compared to existing provable neural network editing methods.", "questions": "Questions:\n\n1. It is unclear how the editing approach was extended to the BERT model. How the editing of the Transformer layer was done? Is DeepT handling it as a blackbox? In addition, you can consider using a better verifier for Transformers such as https://files.sri.inf.ethz.ch/wfvml23/papers/paper_24.pdf\n\n2. The notations are somewhat confusingly differentiated using colors. It will be impossible to read if the paper is printed in black and white. It is better to not solely use colors to distinguish among different letters. It makes the paper less accessible and confusing to understand.", "limitations": "1. Comparisons to provable fine tuning setting is limited, as pointed out above.\n\n2. The approach's scalability is unclear. How large can the network be using the LP formulation?\n\n3. Extensions to other activation functions were discussed conceptually but without formulations and experiements.", "rating": 6, "confidence": 5, "soundness": 4, "presentation": 3, "contribution": 3, "strengths": "1. The paper studies a fundamental problem of how to find neural network weights that guarantee to satisfy output properties. The approach is based on NN verification and has theoretical guarantees unless ordinary gradient-based training is used. The relaxations based on the epigraph and hypograph of nonlinear functions are inspiring and effective in the proposed setting. Based on these contributions, I tend to recommend acceptance of this paper overall, although there are weaknesses and questions I hope the authors address below.\n\n2. Experiments include multiple settings, including standardized benchmarks such as the VNN-COMP 2022 benchmarks, as well as novel settings such as physics-plausible DNNs.", "weaknesses": "Weaknesses:\n\n1. Lack of theoretical discussions on how the proposed relaxations (especially for ReLU) connect to the optimal LP relaxation for ReLU neurons (https://arxiv.org/abs/1902.08722 https://arxiv.org/abs/2006.14076). Note that these relaxations are not the ones presented in Figure 1(a). Since now the pre-activation lower and upper bounds are considered as variables, it can introduce looseness in some situations, for example, for stable neurons. To make the paper more insightful, it will be helpful to discuss when the new formulation which keeps the lower and upper bounds as two separate variables helps.\n\n2. The benefits of the proposed method compared to provable fine-tuning, an important baseline, are not well demonstrated. It is only included in one set of experiments (table 1). Also the setting used in this experiment is strange - the typical perturbation used for CIFAR is 2/255 or 8/255 (0.5/255 is too small). It also looks strange SABR and STAPS achieve very low accuracy (far below the accuracy reported in their papers).", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "> ### Weakness 1\n\nWe will add the theoretical results and proofs related to the precision of our relaxation in the Appendix D of the uploaded PDF to the revision.\n\n#### Regarding [1]\n[1] and our approach both use linear inequalities. The main difference is that they\nrequires a sound input bound for each layer, and uses the convex hull for the layer function within the constant input bound as the convex relaxation; while we uses convex under-approximations of the epigraph and hypograph of the layer function as the convex relaxation, without restricting to a constant input bound.\n\n[1] is used for DNN verification where the parameters are fixed. \nOur method has major advantages in the context of provable editing where the parameters are also variables (Definition 1.1), as discussed below: \n\n##### Relaxation for ReLU layers:\n\n[1] requires constant input bounds for each layer (e.g. to encode the ReLU upper bound). In the context of DNN verification, computing constant input bounds per layer only needs to take into account all inputs to the DNN in the given input polytope. However, for provable editing, the DNN parameters are also variables and can take any value (Definition 1.1). In other words, to ensure that the constant input bounds are sound, [1] would need to account for ***all possible edits to parameters***, which is not optimal. Thus, the only sound constant input bound for the ReLU layer would be [-\\infty, \\infty]. As a consequence, the ReLU relaxation of [1] would be very imprecise in the context of provable editing. \nIn contrast, our work does NOT require constant input bounds for any layer, as illustrated in Figures 1(b),1(c) and 2(b), 2(c) in our paper. \n\nEven if the constant input bounds are provided, their ReLU relaxation (Fig. 2(b) and Eq. 4 in [1]) has a loose upper bound and an exact lower bound, while our relaxation has an exact upper bound and a loose lower bound (Theorem 1).\n\n##### Relaxation for Affine layers:\n\n[1] does not directly address the problem of editing parameters of linear layers (affine and convolutional layers). Figure 2(a) illustrates an approach that adapts ideas from techniques such as [1] to handle editing linear layers. As with ReLU relaxation described above, the linear layer relaxation would need to account for all possible edits to the parameters. Thus relaxations such as [1] would produce a loose bound to take into account all possible edits to the weights of the layer (Figure 2(a)). In contrast, our relaxation has the exact bound which is parametrized by the variable weight (as illustrated in Fig. 2(b) and 2(c) in our paper). This is formalized in Theorems 2 and 3.\n\nRegarding [2]:\n[2] focuses on multi-neuron layerwise approximation for DNN verification, and has drawbacks similar to the ones discussed for [1] above when used for provable editing, while our work focuses on single-neuron layerwise approximation for provable editing. Extending our single-neuron layerwise approximation for provable editing to multi-neuron layerwise approximation is an interesting direction for future work.\n\nWe will include this comparison to the related work section of our revision. \n\n> ### Provable fine-tuning\n\nProvable fine-tuning (PFT) is used as a baseline for all provable editing tasks in the paper (Section 4.1--4.3), where the goal is to edit pre-trained DNNs to satisfy given properties. \nDepending on the task, the most appropriate fine-tuning approach was used. PFT\\<DL2\\> was used in all experiments in Sections 4.1--4.3. PFT\\<SABR\\> and PFT\\<STAPS\\> are the state-of-the-art certified training methods and are used as the baselines for section 4.2; SABR and STAPS cannot handle the benchmarks in Section 4.1 and 4.3. \n\nSection 4.4 deals with provable training where the goal is to train the DNN to satisfy given properties, hence, PFT is not relevant. \n\n> ### Settings for CIFAR10\n\nThe setting for provable editing differs from that used in certified training, which is why we used a different epsilon and why the accuracy for SABR and STAPS is lower than that reported in their papers.\n\n- We are editing the parameters of the pre-trained DNN given an edit set of misclassified corrupted images, which are out of the distribution of the training set. The aim is to also evaluate the generalization of the edit to other corrupted images. Certified training uses images from the training data, while in our provable editing setting, the training data is not available.\n\n- Provable editing has to guarantee that the edited DNN is 𝜖-locally robust for the edit set. Certified training does not provide any such guarantees. \n  \nWe settled on epsilon=0.5/255 based on our preliminary experiments with the provable fine-tuning (PFT) baselines. Using a larger perturbation (𝜖=2/255) in the context of provable editing leads to a large decrease in the accuracy of the edited network for all baselines (PFT\\<DL2\\>, PFT\\<SABR\\>, PFT\\<STAPS\\>).\n\n> ### It is unclear how the editing approach was extended to the BERT model. How the editing of the Transformer layer was done? Is DeepT handling it as a blackbox? \n\nOur approach offers the flexibility to edit the DNN by only editing the last few layers (as described in Appendix B), without editing the transformer layers. HRDNN leverages DeepT to compute a sound input bound to the first edited layer. \n\n> ### [3].\n\nThe implementation of [3] is not publicly available yet. It is easy to replace DeepT in our implementation with this verifier for Transformers. Once it is made public, we could use it in our future work.\n\n#### References:\n1.  \"A convex relaxation barrier to tight robustness verification of neural networks.\"\n   \n2.  \"The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification.\" \n\n3.  \"Formal verification for neural networks with general nonlinearities via branch-and-bound.\" (2023).", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "NKIjeqnVU3", "reviewer": "Reviewer_rPq2", "summary": "This paper proposes a novel approach named HRDNN to provably edit a DNN to satisfy a given property. Concretely, given a DNN, its input domain P, and desired output range Q, HRDNN edits the parameters of the DNN so that for any input in P, the output of the edited DNN falls into Q. The key contribution of this approach is that it uses a novel notion of Parametric Linear relaxation to construct tight output bounds of the DNN. It finally shows the effectiveness and efficiency over a set of benchmarks.", "questions": "* It is weird to use \";\" before \"viz\". Please replace them with \", viz.,\". The same holds for \"; e.g.,\"\n* line 58, \" with defines tight\", typo?\n* The authors distinguish different symbols with different colors. This is good but not friendly to readers with amblyopia. Please consider adding certain marks to colored symbols.\n* Is the scalability of this approach restricted by the ability of LP solvers?", "limitations": "Limitations and social impact are adequately discussed in the paper.", "rating": 7, "confidence": 4, "soundness": 4, "presentation": 3, "contribution": 3, "strengths": "* The paper is well-written and easy to read.\n* It proposes a novel notion of parametric linear relaxation to construct tight parametric bounds of the DNN outputs.\n* The paper provides theoretical proof for the soundness of the proposed notion.\n* The paper shows experimental results that demonstrate the efficacy and efficiency of the proposed method.", "weaknesses": "* The parametric linear relaxation is developed for specific activation functions, like ReLU, Tanh.  It lacks a discussion or summary about a general paradigm to devise parametric bounds for different activation functions.\n* The paper does not discuss the scalability of this approach. It is a white-box method in that the weights of neural networks shall be known in advance.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "> ### The parametric linear relaxation is developed for specific activation functions, like ReLU, Tanh. It lacks a discussion or summary about a general paradigm to devise parametric bounds for different activation functions.\n\nOur implementation and evaluation covers popular activation functions and architectures. \nHowever, in Fig. 4, we just wanted to illustrate that our approach can be extended to other activation functions such as tanh, sigmoid, and elu. We will include a formal description for these activation functions in the appendix of the revision. Providing a generalization to arbitrary activation functions and evaluating these will be interesting future work.\n\n> ### The paper does not discuss the scalability of this approach. It is a white-box method in that the weights of neural networks shall be known in advance.\n\nPlease refer to the general response for a discussion of scalability.\n\n> ### It is weird to use \";\" before \"viz\". Please replace them with \", viz.,\". The same holds for \"; e.g.,\"\n\nWe will make sure that we are using ';' only when 'viz.' is used to introduce a complete sentence or clause, and use ',' in other cases, following the Chicago Manual of Style.\n\n> ### line 58, \" with defines tight\", typo?\n\nIt should be \"which defines tight ...\", we will fix it.\n\n> ### The authors distinguish different symbols with different colors. This is good but not friendly to readers with amblyopia. Please consider adding certain marks to colored symbols.\n\nOnly the notation for LP decision variables solely relies on blue-colored letters. We will improve this notation to make sure it is clear in black and white prints.\n\n> ### Is the scalability of this approach restricted by the ability of LP solvers?\n\nOur approach does not require to encode the entire network as LP for editing, as described in Appendix B. Just like fine-tuning, our approach offers the flexibility to only edit the last few layers (Equation 8, line 849) and calls an off-the-shelf DNN verifier to compute a sound constant bound before the first layer that is edited (Equation 9, line 851). The hyperparameters k (line 847) controls which is the first layer that is edited. \n\nFor the edited layers, here are theorems for the size of the LP formulation for each type of layer. For the freezed layers, its scalability improves as the DNN verifiers improve.\n\nSee Appendix E in the uploaded PDF for theorems for the LP size of the edited layers.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "wcZNuz7tFW", "reviewer": "Reviewer_hnCj", "summary": "This paper addresses the problem of finding a minimal changes to the parameters of a DNN $f(.)$ in order to satisfy pre/post conditions defined as *convex* polytopes, i.e. $\\forall x . (x \\in Pre \\implies f(x) \\in Post ) $.\nThe proposed algorithm is efficient as it considers a Linear Programming (LP) relaxation, while being more general than previous LP-based approaches. The key contribution is a parametric relaxation by defining bound on the affine transformations *in terms of the layers parameters*. The approach is evaluated on multiple benchmarks from the VNN competition and local robustness of classifiers.", "questions": "1) Wouldn't local robustness on the whole test set be a non-convex property (i.e. the union of many $\\epsilon$-balls)? How was this approached in the experimental section? Editing the network independently for each input instance does not guarantee that the constraint holds globally, right (i.e. some fixes might be undone in successive edits)?\n\n\n---\n\n## Minors\n\n\n\n\"This paper presents HRDNN, the first efficient technique for provable editing of DNNs that runs in polynomial time.\"\nPolynomial in..?\n\n---\n\nEq. 1 and 2 both define *the provable editing problem*. In the former, arbitrary convex polytopes are considered, the latter seems restricted to axis-aligned inequalities/halfspaces (or maybe the notation with square brackets misled me?). Which is the correct one? In any case, I would avoid redefining it twice.\n\n---\n\nIn the experiments, I think it would be interesting to read the accuracy of the original (unedited) NNs as a reference.\n\n---\n\nEfficacy means different things in the VNN Comp benchmarks and later benchmarks. I would use a different term.\n\n---\n\nI would define certified accuracy in the text.", "limitations": "The limitations are adequately addressed in my opinion.", "rating": 7, "confidence": 3, "soundness": 3, "presentation": 4, "contribution": 3, "strengths": "- The paper is very well written.\n- Quite extensive evaluation that seems to validate the proposed approach\n- Evaluation of HRDNN both as a post-hoc technique and during training", "weaknesses": "- I think that runtime results for an editing algorithm should always be paired with its impact on predictive performance to be meaningful. I don't understand the role of the VNN Comp benchmark in this sense;\n- Some details of the experimental section are not perfectly unclear.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "> ### I think that runtime results for an editing algorithm should always be paired with its impact on predictive performance to be meaningful. I don't understand the role of the VNN Comp benchmark in this sense\n\nWe used VNNComp to construct a challenging benchmark for evaluating provable editing methods. No prior approaches are able to provably edit properties from VNNComp benchmarks; viz., DL2 does not provide guarantee, and APRNN can not handle universal quantifiers. We propose a novel provable fine-tuning (PFT) framework and use the PFT-enhanced version of prior approaches as our baselines. We demonstrated that our method, HRDNN, is the only one that can effectively and efficiently handle the DNNs and properties in VNNComp.\n\nIn particular, VNNComp is the standard benchmark for evaluating the state-of-the-art DNN verifiers. In our setting, we used these DNNs and properties to construct a difficult benchmark for provable editing: instead of verifying that the DNN satisfies the properties, we have to provably edit the DNN to satisfy the properties. The benchmark demonstrates the efficacy, expressivity, and scalability of our approach compared to the baselines.\n\n- Expressivity: VNNComp demonstrates that our approach can handle a wide range of network architectures and properties that are used in the VNNComp benchmark, e.g. ACAS Xu, reinforcement learning and TinyImageNet ResNet benchmarks, etc. listed in Table 4 of Appendix C.2.\n\n- Efficacy: VNNComp demonstrates that HRDNN is able to find an edit to the DNN that satisfies the given properties. For instance, HRDNN is able to provably edit all 423 single-property editing problems, while PFT\\<DL2\\> is only able to edit 185 problems.\n\n- Scalability: When both HRDNN and the baselines are able to find a provable edit, HRDNN is significantly faster achieving 10x to 100x speedup over PFT\\<DL2\\>.\n\nIn terms of the impact on predictive performance, the experiments in Sections 4.2--4.4 report accuracy after editing. The VNNComp benchmark does not come with such evaluation metrics and data.\n\n> ### Wouldn't local robustness on the whole test set be a non-convex property (i.e. the union of many 𝜖-balls)? How was this approached in the experimental section? Editing the network independently for each input instance does not guarantee that the constraint holds globally, right (i.e. some fixes might be undone in successive edits)?\n\nWe do not edit the network independently for each input. We edit the whole edit set altogether by taking the conjunction of the constraints for each input 𝜖-ball. In other words, we compute the parametric linear relaxation for each input 𝜖-ball independently, conjoin the corresponding constraints, and then solve them altogether. The constraints for each input 𝜖-ball is a convex polytope *in the editable parameter space*, and their conjunction is the convex intersection of those polytopes.\n\nAppendix B.1 (line 854) describes how our approach handles editing multiple properties.\n\n> ### \"This paper presents HRDNN, the first efficient technique for provable editing of DNNs that runs in polynomial time.\" Polynomial in..?\n\nIt is formally defined in Definition 3.3, Line 114-115: \"... is a linear formula whose size is polynomial in the size of the DNN; viz., the number of input dimensions, output dimensions, and parameters of N\".\n\nWe will add a forward reference to the formal definition in the revision.\n\n> ### Q3: Eq. 1 and 2 both define the provable editing problem. In the former, arbitrary convex polytopes are considered, the latter seems restricted to axis-aligned inequalities/halfspaces (or maybe the notation with square brackets misled me?). Which is the correct one? In any case, I would avoid redefining it twice.\n\nEq. 1 (Definition 1.1) is the one that is handled by our actual implementation and is described in Appendix B. Eq. 2 (Definition 3.2) is a simplified version of the provable editing problem that is only used for ease of exposition in Section 3, as stated in Lines 105–106. We will clarify this further in the revision by renaming Definition 3.2. \n\n> ### Q4: In the experiments, I think it would be interesting to read the accuracy of the original (unedited) NNs as a reference.\n\nFor section 4.2, the CIFAR10 CNN7 has 17.2M parameters, 79.24\\% test accuracy and 62.84\\%\ncertified accuracy 75.77\\% (𝜖=0.5/255); the TinyImageNet CNN7 has 51.9M parameters, 28.85\\% test accuracy and 20.46\\% certified accuracy (𝜖=1/255).\n\nFor section 4.3, the test accuracy of this BERT DNN is 84.07\\%.\n\nWe will include the original accuracy in the revision.\n\n> ### Q5: Efficacy means different things in the VNN Comp benchmarks and later benchmarks. I would use a different term.\n\nIn the revision, We will use a different term in Section 4.1 to avoid confusion.\n\n> ### Q6: I would define certified accuracy in the text.\n\nWe will define it in the revision.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "VNY912bna9", "reviewer": "Reviewer_NEaR", "summary": "The authors propose HRDNN, the first efficient technique for provable editing of DNNs.  HRDNN is able to provably edit the DNN to satisfy this property within 45 seconds. HRDNN is efficient because it relaxes the NP-hard provable editing problem to solving a linear program (LP). It enables HRDNN to construct tight bounds of the DNN that are parameterized by the new parameters $\\theta$. The edited models could be vnn-comp22 benchmarks, CIFAR10,tiny imagenet, bert SST dnns.", "questions": "There are many robustness-enhancing  methods. What are the results of comparing HRDNN to verified training(lipschitz-based).\n\n\nOther question can be seen in weakness.\n\nI am happy to reconsider my rating, if the authors address satisfactorily my questions.", "limitations": "What I'm more concerned about: In Table1, the results with <100\\%efficacy are shaded. However, I think APRNN is more effective in terms of ACC. , Cert. and Time. Are these metrics more important than the efficacy, as editing methods are purposed to improve the certified robustness(Cert.)?", "rating": 5, "confidence": 2, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "+Important research topic\n\n+the first verifier-in-the-loop, and the editing stops when the verifier confirms that the DNN satisfies the property\n\n+well writing\n\n+It can apply to many types of networks(sigmoid,tanh,elu DNNs)", "weaknesses": "- In Table1, the generalized accuracy is smaller than PFT<ASBR>. Further, the results in Table 1  are only tested on two models and can not sufficiently demonstrate the effectiveness of HRDNN. \n\n-In Table1, the results with <100\\%efficacy are shaded. However, I think APRNN is more effective in terms of ACC. , Cert. and Time. Are these metrics more important than the efficacy, as editing methods are purposed to improve the certified robustness (Cert.)?\n\n-Unclear metric. Where is the definition of Og. Effic in Table2?", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "> ### the first verifier-in-the-loop, and the editing stops when the verifier confirms that the DNN satisfies the property\n\nWe would like to clarify that our approach, HRDNN, is not a verifier-in-the-loop approach: as proved in Theorem 3.5, any solution to the LP problem constructed via our parametric linear relaxation is guaranteed to satisfy the given properties. Hence, if a solution is found, there is no need to call a verifier to confirm whether the edited DNN satisfies the properties. \n\nHowever, we were the first to evaluate the use of prior fine-tuning approaches in a verifier-in-the-loop framework, which we refer to as provable fine-tuning (PFT) (as stated on lines 182-189).\n\n> ### In Table1, the generalized accuracy is smaller than PFT\\<SABR\\>.\n\nWe would like to clarify the metrics for provable repair. \n\n- Efficacy—the percentage of editing set that have been successfully repaired—is the most critical metric: a provable edit must guarantee 100% efficacy.\n  \n- Standard (and certified) accuracy on the test set is an important metric, a good provable edit should have high accuracy. However, this metric is relevant only if efficacy is 100%.\n\n- The generalization accuracy on the generalization set is a \"bonus\" metric measuring\nhow well the edit generalizes to inputs that are similar to the edit set. However, the generalization accuracy is relevant only if the standard (and certified) accuracy is good; that is, the predictive power of the edited DNN should not be sacrificed for better generalization.\n\nSpecifically in Table 1, although the PFT\\<SABR\\> baseline has a higher generalization accuracy than our approach HRDNN, PFT\\<SABR\\> is *not* better than HRDNN because it has much lower standard and certified accuracy than HRDNN. In other words, PFT\\<SABR\\> sacrificed the more important predictive power (accuracy) to gain slightly higher generalization than HRDNN. Note that the absolute generalization accuracy for HRDNN is still good, demonstrating that HRDNN is able to find a good balance between preserving the predictive power while generalizing to the unseen out-of-distribution corrupted examples.\n\n> ### Further, the results in Table 1 are only tested on two models and can not sufficiently demonstrate the effectiveness of HRDNN.\n\nWe thoroughly evaluated the scalability and expressivity of HRDNN using the VNN-Comp benchmark (Section 4.1), which includes 101 networks and 423 properties spanning a wide-variety of application domains. HRDNN was also evaluated on three other application domains: image recognition, natural language processing to physical-plausible HPC applications in Sections 4.2--4.4.\n\n> ### In Table1, the results with <100% efficacy are shaded. However, I think APRNN is more effective in terms of ACC. , Cert. and Time. Are these metrics more important than the efficacy, as editing methods are purposed to improve the certified robustness (Cert.)?\n\nIn Section 4.2, we are editing the CIFAR10 and TinyImagenet networks to ***guarantee*** that they are locally robust for 50 misclassified corrupted images from CIFAR10-C and TinyImageNet-C, respectively (line 216), which are out of distribution of the training and test sets. The goal is to provably edit the network while ensuring high standard and certified accuracy on the test set (Acc. and Cert.) and generalizing to other corrupted images (Gen.). Thus, the goal is not to increase the certified robustness on the test set as done in the certified training setting.\n\nIn particular, as explained earlier in this response, Acc., Cert. and Time are relevant only if the edited DNN has 100% efficacy on the edit set. APRNN is not more effective than HRDNN because APRNN was unable to provably edit the network to get 100% efficacy. It is not surprising that the Acc, Cert. and Time metrics are better for APRNN considering it did not successfully edit the network to satisfy the given properties. For instance, an approach that does nothing to the given network will outperform all baselines in terms of Acc., Cert. and Time in this experiment, but will get 0% efficacy.\n\n> ### Unclear metric. Where is the definition of Og. Effic in Table2?\n\nOg. Effic is the original certified accuracy on the edit set before editing. We will clarify it in the revision.\n\n> ### There are many robustness-enhancing methods. What are the results of comparing HRDNN to verified training(lipschitz-based).\n\nIn terms of the robustness-enhancing methods, SABR and TAPS are the state-of-the-art method, outperforming the lipschitz-based training methods. Therefore, we chose SABR and TAPS as our baselines.\n\nWe also would like to clarify that our approach is not restricted to robustness-enhancing but is capable of effectively and efficiently handling a variety of applications as demonstrated by our extensive experiments (Section 4.1--4.4).", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:
> #### Scalability

Our approach does not require to encode the entire network as LP for editing, as described in Appendix B. Just like fine-tuning, our approach offers the flexibility to only edit the last few layers (Equation 8, line 849) and calls an off-the-shelf DNN verifier to compute a sound constant input bound to the first edited layer (Equation 9, line 851). The hyperparameters k (line 847) controls which is the first edited layer: the layers N[0:k] are not edited, while N[k:L] are edited. The values of these hyperparameters used for our experiments are described in Appendix C.

See Appendix E in the uploaded PDF for theorems for the LP size of the edited layers.

We have evaluated the scalability and expressivity of our approach using multiple benchmarks such as VNN-Comp, TinyImageNet, BERT used in the DNN verification literature; instead of verifying the properties, we use our approach to provably edit the pre-trained network to guarantee that the network satisfies the properties. To the best of our knowledge, our approach is the first provable editing approach that can handle those benchmarks, and we outperform all the baselines.

> #### Handling other activation functions

Our implementation and evaluation covers popular activation functions and architectures. 
However, in Fig. 4, we just wanted to illustrate that our approach can be extended to other activation functions such as tanh, sigmoid, and elu. We will include a formal description for these activation functions in the appendix of the revision. Providing a generalization to arbitrary activation functions and evaluating these will be interesting future work.

Meta-review: The paper proposed a novel approach to edit the deep neural network to satisfy certain properties, backed by theoretical guarantees and numerical experiments. The reviewers unanimously find the approach sound and useful. After reading the manuscript and discussion, the meta-reviewer agrees with the assessment and recommend the paper by acceptance.
Decision: Accept (poster)