Neural Network Verification using Partial Multi-Neuron Relaxation Ido Shmuel[0009−0002−9870−549X] and Guy Katz[0000−0001−5292−801X]
arXiv:2605.30155v1 [cs.LO] 28 May 2026
The Hebrew University of Jerusalem, Jerusalem, Israel {ido.shmuel, g.katz}@mail.huji.ac.il
Abstract. The increasing integration of deep neural networks in critical systems has spawned a theoretical and practical interest in formally guaranteeing safety properties about their behavior. To achieve this, contemporary verification algorithms rely on computing linear relaxations for a network’s non-linear activation functions. Existing approaches for linear relaxations typically fall into one of two categories: single-neuron relaxation, in which each activation neuron is bounded in terms of its sources; and multi-neuron relaxation, in which linear bounds involving multiple activation neurons and their sources are calculated. However, existing methods might fail to balance tightness and scalability, as single-neuron bounds might not derive sufficiently tight bounds necessary for verification to complete, whereas generating multi-neuron relaxation for all activation neurons is computationally expensive. In this paper, we present a middle-ground approach featuring partial multi-neuron relaxation, in which we generate multi-neuron bounds for only a small, heuristically selected subset of neurons. To achieve this, we build upon existing branching heuristics for selecting neurons and for optimizing bounding hyperplanes for multi-neuron bounds. We integrated our proposed method within the Marabou verifier, and obtained favorable results in comparison to existing bound tightening methods. Our experiments showcase the potential of our technique for neural network verification.
1
Introduction
Deep neural networks [13] (DNNs) are increasingly being adopted as key components in mission-critical systems. They have been achieving unprecedented performance in diverse domains such as natural language processing [12], protein structure prediction [21, 29], image recognition [39], medical analysis [6], aircraft collision avoidance [22], self-driving [3], and task scheduling [34], often greatly improving upon the results of algorithms crafted by human experts. However, despite their immense success, the opacity of DNNs raises new concerns regarding their stability and reliability. Unlike classical, human-crafted algorithms, DNNs are perceived as black-boxes, making it troublesome to correctly reason about their decision making [5]. Moreover, DNNs are known to be susceptible to adversarial perturbations [7,14,42], where low-magnitude changes to their inputs result in incorrect outputs. The absence of a formal proof of
correctness of DNNs might raise doubts about the robustness of existing applications of DNNs and potentially slow down their adoption. In order to address these issues, diverse strategies have been suggested to feasibly solve the problem of formal verification of DNNs [28]. Despite recent advances [25], these methods have limited scalability, in light of the fact DNN verification has been proven to be NP-complete for DNNs with piecewise-linear activation functions [23]. A major component in existing methods for DNN verification is the branchand-bound (BaB) paradigm [4]. Due to the non-linear nature of activation functions, DNN verification often necessitates performing recursive case splitting, resulting in a large search space whose size grows exponentially as a function of the number of activation neurons. Under the BaB paradigm, prior to splitting the original verification problem to sub-problems, verifiers take advantage of bound tightening tactics to deduce upper and lower bounds on the values of the networks’ neurons. This often results in a major size reduction of the search space, facilitating verification. In order to derive bounds on a DNN’s neurons, solvers leverage linear relaxations of a network’s non-linear activation functions. By calculating linear over-approximations on activation neurons as a function of their sources, solvers may leverage technique featuring symbolic bound propagation [41,46] and Linear Programming (LP) [36, 45] to quickly gather bounds on the network’s neurons. Existing methods typically fall into one of two categories: single-neuron relaxation [41, 55], in which each of the calculated linear over-approximations involve a single activation neuron; and multi-neuron relaxation, which features linear bounds consisting of multiple activation neurons [11, 26, 32, 40]. Although the former strategy is highly scalable, it might result in insufficiently tight overapproximations, due to the convex relaxation barrier [36]. In contrast, the latter approach results in tighter bounds while incurring a higher computational toll. In this paper, we present a novel approach to bound tightening, which seeks a better balance between scalability and tightness. We propose a general framework for performing partial multi-neuron relaxation (PMNR), namely, generating multi-neuron over- approximations for only a heuristically selected subset of neurons, while using tunable single-neuron bounds for the remainder of the network. Our approach can be instantiated with various heuristics for selecting neurons and hyper-planes for multi-neuron relaxations, and we demonstrate that multiple existing branching heuristics can be used for this purpose. Whereas in the BaB paradigm, branching heuristics indicate a single neuron whose bounds may be improved by first performing a case-split, in our approach we use these heuristics to identify cases where it is beneficial to infer a multi-neuron bound. We implemented PMNR within the popular Marabou verification tool [24,50]. We evaluated our implementation on local robustness queries with fully connected DNNs, trained on the MNIST dataset [27]; and compared it to other tightening algorithms implemented in Marabou. We discovered that the PMNRenhanced Marabou solved 49% more queries than base Marabou, with a runtime reduction of 17% on our benchmarks. Our experiments demonstrate the signifi-
cant potential of the PMNR approach for bound tightening. Our implementation is available online [38]. The rest of the paper is organized as follows. In Section 2 we provide the necessary background on DNNs, their verification, and linear relaxations of activation functions. Next, in Section 3 we describe our general technique for verifying DNNs using partial multi-neuron relaxations, before instantiating it with specific heuristics in Section 4. Next, we evaluate the performance of our approach in Section 5. We cover related work in Section 6, and conclude with ideas for future research in Section 7.
2
Background
2.1
Deep Neural Networks and their Verification
Deep Neural Networks. A deep neural network (DNN) N : Rn0 → RnL contains an input layer, L − 1 hidden layers, and an output layer. The ith layer of the network is a real-valued vector of size ni . We denote the ith layer as (i) x̂(i) and its j th neuron as x̂j . For 0 < i < L, the DNN’s hidden layers are iteratively computed given the recursion formula x̂(i) = σi (W (i) x̂(i−1) + b(i) ), and the output layer is defined as x(L) = W (L) x̂(L−1) + b(L) . For each i, W (i) is a weight matrix, b(i) is a bias vector, and σi : Rni → Rni is a (usually non-linear) activation function. Note that N ’s output N (x̂(0) ) = x(L) does not contain post-activation values, which could be modeled as setting σL to be the identity function. We also define pre-activation values with the relation x(i) = W (i) x̂(i−1) + b(i) . Since the activations σi are modeled as arbitrary multivariate functions, our formulation generalizes to several common DNN architectures (e.g. fully-connected, convolutional, residual) equipped with arbitrary activation functions. Example Network. Consider the DNN in Fig. 1 with input x̂(0) ∈ [−1, 1]2 , one hidden layer containing Abs(x) = |x| (absolute value) activations with preactivation x(1) and post-activation x̂(1) , another hidden layer containing two ReLU(x) = max(0, x) activations with pre-activation x(2) and post-activation (3) (1) (2) (3) x̂(2) , and a single output x0 . Neurons x̂1 , x̂1 , x̂0 have bias values of 1, 2, −26 respectively, and all other neurons have a bias of 0. The piecewise-linear functions Abs and ReLU are applied element-wise for multi-dimensional inputs. The network’s neurons are computed recursively: 1 0 1 x(1) = 2 −3 x̂(0) + 0 , x̂(1) = Abs(x(1) ). 0 1 0 1 1 −1 (1) 0 x(2) = x̂ + , x̂(2) = ReLU(x(2) ). 1 −1 −5 2 x(3) = −1 −3 x̂(2) + 26.
[0, 2] (1)
x̂0 [−1, 1]
1
1 1 -1
(0)
x̂0
[0, 5] 2
[0, 4] (2)
x̂0
-1 0
1
[12.1, 26.1]
(1)
(3)
x̂1 [−1, 1]
-3
0
x0 1
[0, 6]
(0)
-3
26.1
(2)
x̂1
x̂1
-1 [0, 1] 1
-5
2
(1) x̂2
0 Fig. 1. An example neural network.
Given input x̂(0) = (0.4, −0.6)⊤ , N ’s hidden neurons have these values: x̂(1) = (Abs(1.4), Abs(2.6), Abs(−0.6))⊤ = (1.4, 2.6, 0.6)⊤ . x̂(2) = (ReLU(3.4), ReLU(0.2))⊤ = (3.4, 0.2)⊤ . The output of the network is N (x̂(0) ) = x(3) = 22.1. Neural Network Verification. Neural network verification [20] is the process of soundly deciding whether a safety property holds in a neural network’s output given known bounds on its inputs. Formally, a verification query is a triple Q = (N, Din , Dout ), consisting of a DNN N , an input domain Din ⊂ Rn0 and an output domain Dout ⊂ RnL , which typically represents an unsafe behavior of N . DNN verification is framed as a satisfiability problem: Q is satisfiable (SAT) if there exists x for which the predicate x ∈ Din ∧ N (x) ∈ Dout holds (i.e. N demonstrates undesirable behavior Dout ); otherwise, it is considered unsatisfiable (UNSAT). Any common verification query could be easily rewritten [9, 19] into a query with a single-output DNN whose output domain is Dout = (0, ∞). We will therefore assume for the remainder of this paper that all queries are of this simplified form unless indicated otherwise. As an example, consider the verification query composed of the DNN in Fig. 1, the input domain [−1, 1]2 and the output domain (0, ∞). The input x̂(0) = (0.4, −0.6)⊤ satisfies it because N (x̂(0) ) = 22.1 > 0. Hence, (0.4, −0.6)⊤ is considered a satisfying assignment for this query, and no sound verifier would consider it unsatisfiable.
2.2
Branch and Bound (BaB)
Branch-and-bound (BaB) is a key technique, applied by various neural network verifiers [4, 11, 47]. It is formed by interleaving calls to a bound tightening algo(i)
rithm which calculates concrete bounds ℓ̂ ≤ x̂(i) ≤ û(i) , ℓ(i) ≤ x(i) ≤ u(i) for a DNN’s neurons, and a branching method which recursively splits the verification problem into smaller, easier-to-solve sub-problems, giving rise to a search tree of an exponentially increasing size. The original problem is determined to be satisfiable if and only if at least one sub-problem is declared SAT by the verifier. Bound tightening is invoked post-splitting to limit the growth rate of the search tree. In order to generate sub-problems, verifiers commonly use case splitting on activation neurons [47]. Case splitting is typically applied for piecewise-linear activation neurons, which are then split into a collection of linear constraints, one for each linear segment; though it has been applied successfully for general activation functions as well [37]. Given the massive scale of branching trees in practice, verifiers heavily leverage heuristics and other techniques to prune infeasible sub-problems and limit the number of sub-problems that are generated as a result of case splitting. 2.3
Single-Neuron Relaxation
Linear Over-Approximations. Contemporary bound tightening algorithms reason about a DNN’s general non-linearities by replacing them with linear overapproximations [28, 41, 55]. Namely, a DNN’s sound single-neuron relaxation is a collection of linear bounds of the form: Wℓ (i) x(i) + bℓ (i) ≤ σi (x(i) ) = x̂(i) ≤ Wu (i) x(i) + bu (i) These bounds are sound if they hold whenever ℓ(i) ≤ x(i) ≤ u(i) . The symbolic weight matrices Wℓ (i) , Wu (i) and symbolic bias vectors bℓ (i) , bu (i) are chosen as a function of σi , ℓ(i) , u(i) to guarantee soundness using known methods [33, 41, 51]. They may depend on an external, tunable parameter α [51]. For example, consider again the ReLU, Abs activation functions from the network in Fig. 1, which are piecewise-linear with two linear phases. Given known (i) (i) (i) (i) (i) bounds xj ∈ [ℓj , uj ], sound linear bounds on ReLU(xj ), Abs(xj ) are: (i) (i) 0 ≤ ReLU(xj ) ≤ 0 if uj ≤ 0 (i) (i) (i) (i) xj ≤ ReLU(xj ) ≤ xj if ℓj ≥ 0 (i) (i) (i) j −ℓj ) αx(i) ≤ ReLU(x(i) ) ≤ uj (x otherwise, for any α ∈ [0, 1] (i) (i) j j uj +ℓj (i) (i) (i) (i) if uj ≤ 0 −xj ≤ Abs(xj ) ≤ −xj (i) (i) (i) (i) xj ≤ Abs(xj ) ≤ xj if ℓj ≥ 0 (i) (i) (i) (i) αxj ≤ Abs(xj ) ≤ max(ℓj , uj ) otherwise, for any α ∈ [−1, 1]
In the first two cases of the inequalities above, the two activation functions (i) (i) (i) are known to have a fixed phase in the domain xj ∈ [ℓj , uj ], and their linear bounds are identical to their respective linear phases. Else, they are said to have an unfixed phase in the given domain, and they are relaxed into a pair of linear constraints. The linear relaxations in the unfixed case are illustrated in Fig. 2. (i)
(i)
Abs(xj )
ReLU(xj ) (i)
uj
(i)
(i)
(i)
uj
(i)
uj (xj −ℓj ) (i)
(i)
(i)
max(ℓj , uj )
(i)
uj +ℓj
(i)
αxj
(i)
(i)
xj
xj 0
(i) ℓj
(i) uj
0
(i) ℓj
(i)
(i) uj
(i)
ℓj
ℓj
(i)
αxj
Fig. 2. An illustration of linear bounds on the ReLU and Abs functions over x ∈ (i) (i) (i) (i) (i) (i) [ℓj , uj ] where ℓj < 0 < uj . αxj is a sound linear lower bound on ReLU(xj ) for (i)
α ∈ [0, 1], and it is a sound linear lower bound on Abs(xj ) for α ∈ [−1, 1].
Symbolic Bound Tightening (SBT). Symbolic Bound Tightening is a common, light-weight tightening method requiring linear over-approximations on a DNN’s non-linear activations. In this method, linear bounds of every neuron in the network as a function the previous layer’s neurons are computed iteratively using back-substitution and concretization. Two noteworthy variations of SBT are Symbolic Intervals [46] and DeepPoly [41]. Linear Programming (LP). Alternative approaches to bound tightening reduce the DNN verification query Q to a linear program. The existence a of positive solution to the following LP establishes the satisfiability of Q: min
α,x∈Din
s.t.
N (x) = x̂(L) x(i) = W (i) x̂(i−1) + b(i) x̂(i) ≥ Wℓ (i) x(i) + bℓ (i) x̂(i) ≤ Wu (i) x(i) + bu (i)
This LP is typically dispatched by an LP solver or duality-based strategies [8, 36]. Alternately, the problem might be transformed into a Mixed-Integer LP (MILP) instance, and then solved by invoking a MILP solver [44].
2.4
Multi-Neuron Relaxation
Although single-neuron relaxation allows for scalable bound tightening, its precision is inherently limited by the convex relaxation barrier, even for simple ReLU activations [36]. A multi-neuron bound is a linear bound involving multiple activations and their associated pre-activation values. Formally, given activation (i ) (i ) neurons Neurons = {x̂j11 , . . . x̂jdd }, multi-neuron linear bounds are a boundPd (k) (ik ) ing polyhedron of the form x̂jk − C (k) x(ik ) ) ≤ d. The technique k=1 (c of multi-neuron relaxation bypasses the convex barrier by incorporating multineuron linear bounds. Some existing verification tools apply this technique, and are able to learn stronger bounds by calculating multi-neuron bounds for all neurons [11, 32, 40].
3
Partial Multi-Neuron Relaxation Paradigm
While the technique of Multi-Neuron relaxation produces tighter bounds compared to Single-Neuron Tightening, it incurs a significant runtime overhead. Current methods [32, 40] either require calculating multi-neuron bounds for every activation neuron in a given DNN, solving MILPs [54], or having already performed branching [57]. The first two might not scale well for larger networks, and the third does not apply for initial (pre-branching) bound tightening. In order to achieve more accurate bounds compared to Single-Neuron Tightening, while avoiding the higher cost of Multi-Neuron Tightening, we propose to extend single-neuron relaxation by heuristically selecting a small subset of neurons and generating multi-neuron bounds only for these neurons. This allows to circumvent the convex relaxation barrier without needing to calculate multi-neuron bounds for all activation neurons. Though it is difficult to know a priori which subset of neurons will yield the tightest bounds, we argue that existing branching heuristics might be suitable for the task of neuron selection. The motivation is that these heuristics are already designed to identify neurons for which Single-Neuron Relaxation fails to produce sufficiently tight bounds, so that branching can be performed on them. Here, instead of performing branching, we propose to tighten these neurons’ bounds by incorporating them in multi-neuron bound calculation. In this section, we introduce the concept of lemmas, and outline our Partial Multi-Neuron Relaxation (PMNR) bound tightening framework — the pseudocode of which appears in Algorithm 1. Next, we describe each step in greater detail and prove soundness properties. Derived Lemmas. For the purpose of defining soundness, we introduce the following definitions pertaining to lemmas inferred from a verification query or from other lemmas. Definition 1. The set of constraints C on x̂(i) , x(i) is a lemma derived from verification query Q if x̂(0) ∈ Din ∧ N (x̂(0) ) ∈ Dout implies x̂(i) , x(i) satisfy all the constraints in C, and we denote Q ⇒ C.
Definition 2. For two sets C1 , C2 of constraints on x̂(i) , x(i) , C2 is a lemma derived from C1 if any x̂(i) , x(i) which satisfy C1 ’s constraints also satisfy C2 ’s, and we denote C1 ⇒ C2 . As a corollary of Definition 1, if Q ⇒ C and for no choice of x̂(0) ∈ Rn0 do x̂ , x(i) satisfy C’s constraints, Q is necessarily unsatisfiable. (i)
Single-Neuron Relaxation. Our framework uses as a backend a single-neuron relaxation-based bound tightening method. Any number of existing methods can be plugged in for this purpose, and we invoke them through a call to the abstract SingleNeuronTightening method — which returns concrete bounds ConcreteB, single-neuron relaxation SingleB and a optimizable parameter αinitial . Here, SingleB is a set of linear over-approximations (as in Subsection 2.3) which depend on an optimizable parameter α, and SingleB(α) is the resulting linear over-approximations by substituting a value of α. Our framework requires ConcreteB and SingleB(α) returned by SingleNeuronTightening are lemmas learned from Q for all values of α. Partial Multi-Neuron Relaxation. In the case ConcreteB does not contain any constraint which is a contradiction (which we denote by ⊥), we proceed to calculating multi-neuron bounds for a heuristically selected subset of neurons. The process is repeated until StopCondition becomes true or ConcreteB contains a contradiction ⊥. First, at line 6 of Algorithm 1, the optimizable parameter selection heuristic PickAlphas outputs optimizable parameters αselect , αgener , αfinal to be used in the next stages of the PMNR paradigm. Then, at line 7, SelectNeurons (i ) (i ) outputs a set of activation neurons Neurons = {x̂j11 , . . . x̂jdd }. Afterwards, at line 8, GeneratePMNR returns a set of multi-neuron bounds MultiB which is Pd (i ) a polyhedron k=1 (c(k) x̂jkk − C (k) x(ik ) ) ≤ d, Finally, at line 9, PostTighten returns updated bounds ConcreteB′ . For soundness, our framework requires that MultiB is a lemma learned from ConcreteB ∪ SingleB(αgener ), ConcreteB′ is a lemma learned from ConcreteB ∪ SingleB(αfinal ) ∪ MultiB, and it holds true that ConcreteB′ ⇒ ConcreteB (i.e. ConcreteB′ is stronger than ConcreteB). Soundness. It is straightforward to prove by induction that the returned concrete bounds from Pmnr are sound and are no less precise than those inferred by SingleNeuronTightening if Pmnr’s soundness requirements hold. Formally: Theorem 1. If Pmnr’s requirements hold and ConcreteBsingle , ConcreteBPmnr are the concrete bounds yielded by SingleNeuronTightening and Algorithm 1 respectively, then Q ⇒ ConcreteBPmnr and ConcreteBPmnr ⇒ ConcreteBsingle .
4
Instantiating PMNR
In Section 3, we described our approach for performing partial multi-neuron tightening and proved soundness properties. Here, we list specific heuristics we
Algorithm 1 Pmnr(N, Din , Dout ) 1: while ¬StopCondition() do 2: ConcreteB, SingleB, αinitial ← SingleNeuronTightening(N, Din , Dout ) 3: if ⊥ ∈ ConcreteB then 4: break 5: end if 6: αselect , αgener , αfinal ← PickAlphas(N, ConcreteB, SingleB, αinitial ) 7: Neurons ← SelectNeurons(N, ConcreteB, SingleB, αselect ) 8: MultiB ← GeneratePMNR(N, ConcreteB, SingleB, αgener , Neurons) 9: ConcreteB ← PostTighten(N, Din , Dout , ConcreteB, SingleB, αfinal , MultiB) 10: end while 11: if ⊥ ∈ ConcreteB then 12: break 13: end if 14: return ConcreteB
used to instantiate the PMNR paradigm in our experiments. Our suggested heuristics build on contemporary branching heuristics and bound tightening algorithms which tolerate general non-linearities, and are therefore generally applicable to multiple kinds of DNNs and activations.
4.1
Neuron Selection
Neuron Selection with Symbolic Expressions (NSSE). The novel NSSE heuristic presented here, designed for neuron selection from DNNs with arbitrary activation functions, is reworked from the Bound Propagation with Shortcuts (BBPS) branching heuristic [37]. BBPS, which supports arbitrary non-linearities, estimates the lower bound on a DNN’s output neuron for all potential branchings and selects the neuron which is projected to yield the maximal improvement. One major alteration between BBPS and NSSE is that BBPS assigns a score for every pair of neuron and possible branch, while NSSE assigns a score for every unfixed-phase neuron. Calculating BBPS Scores. To calculate the BBPS score for the k th phase of (i) neuron xj , the single-neuron relaxation-based tightening method is augmented (i)
to calculate linear lower over-approximations on x(L) in terms of x̂j , as well (i)
(i)
as linear bounds on x̂j in terms of x(i) , which are sound when xj is in its k th phase. By substituting the concrete bounds on x(i) in these linear overapproximations, a concrete linear bound for the output layer is calculated. This (i) lower bound is defined to be the BBPS score of k th phase of neuron xj , and it serves as a cheap approximation on the post-branching lower bounds on the output. The BBPS heuristic prioritizes neurons with the highest score, in an attempt to prove the output domain (0, ∞) is satisfiable.
(i)
Calculating NSSE Scores. To calculate the NSSE score of a neuron xj , we derive linear upper and lower bounds on the output neuron x(L) as a function (i) (i) of a chosen source neuron xj ′ which are sound when xj is in its k th phase, in a similar fashion to the calculation routine of the BBPS heuristic. Then, we separately aggregate the linear upper and lower over-approximations over all (i) branches, producing two symbolic expressions of xj ′ . and the post-concretization (i)
average range of these symbolic expressions is xj ’s NSSE score. Our heuristic picks the d highest-score unfixed-phase neurons from the layer ℓ with highest score-sum layer, unlike BBPS which picks the highest-score neuron and branch. 4.2
PMNR Generation
We will break down the novel Bounding hyper-planes via Splitting and Optimization (BHSO) paradigm for generating bounding hyper-planes, described in Algorithm 2, and apply it to PMNR generation. BHSO features elements from the Branch-and-Bound paradigm [4, 37] and preimage over-approximation [26], and applies them to the problem of inferring bounding hyper-planes. Initial hyper-planes. Though BHSO applies to general bounding hyper-planes PL−1 (i) (i) PL + i=1 C (i) x(i) ≤ d, we focused in our evaluation on inferring i=0 Ĉ x̂ multi-neuron bounds of the form (similarly to [40]): X k∈[d]
(ℓ) (ℓ) ϵ(k) x̂jk − Wu jk : x(ℓ) ≤ d,
X
(ℓ) (ℓ) ϵ(k) x̂jk − Wℓ jk : x(ℓ) ≤ d.
k∈[d]
To avoid re-optimizing ConcreteB or SingleB with OptimizePMNR, we limited ourselves to vectors ϵ ∈ {−1, 0, 1}d with more than one non-zero entry. The number of such vectors equals 3d − 2d − 1, which grows exponentially with d: For d values of 2, 3, 4, the quantity of bounding hyper-planes to be generated would be 4, 20 and 72 respectively. We limit ourselves to d ∈ {2, 3} selected neurons in order to ensure Pmnr remains computationally affordable within our experiments. Optimizing hyper-planes. BHSO employs OptimizePMNR to refine the bias of all hyper-planes defined above. In the case of ReLU networks, the INVPROP algorithm [26] might be used to instantiate it. To support general networks, we employ a generalized version of [26, Theorem 2, Appendix C], which applies to general activations σi and input domains Din and allows to optimize current hyper-planes depending on previous ones. See Appendix B for details on the generalized theorem, and Appendix C for proof. We utilize this theorem to optimize multi-neuron bounds sequentially given ConcreteB, SingleB and previously optimized multi-neuron bounds MultiB with PGD. Optimizing Further with General Branching. BHSO incorporates branching in order to learn more precise bounds from OptimizePMNR. Like NSSE, it assumes all chosen neurons could be partitioned into several branches, for
instance, via ReLU splitting or GenBaB [37]. OptimizePMNR operates several times per hyper-plane, with each run superseding a pre-activation value’s bounds with those of the current branch combinations, and substituting the neurons’ linear over-approximations with the corresponding, more accurate ones. The hyper-plane’s new bias d(k) is the weakest bound among all branch combinations, thereby ensuring the soundness of BHSO is not impaired by the existence of infeasible branch combinations (for which the dual problem solved by INVPROP or Theorem 2 is unbounded). As an illustration, here are the main steps that the BHSO paradigm might (2) (2) perform to deduce a hyper-plane involving the ReLU neurons x̂0 , x̂1 from the example network in Fig. 1. An initial hyper-plane would be directly derived via OptimizePMNR, leveraging the neurons’ unfixed-phase linear bounds. To tighten it further, OptimizePMNR will be called four additional times, per (2) (2) (2) (2) each combination of the neurons being in their active x0 ≤ x̂0 ≤ x0 , x1 ≤ (2) (2) (2) (2) x̂1 ≤ x0 or inactive phase 0 ≤ x̂0 ≤ 0, 0 ≤ x̂1 ≤ 0, while superseding the neurons’ unfixed-phase linear bounds with precise per-branch bounds. Ultimately, BHSO will choose the loosest bound found. Infeasible Branches Detection. It is possible to identify some branch combinations which are infeasible by calculating an upper bound for the bounding hyper-planes (e.g. with simple concretization) and comparing it to the bias resulted by invoking OptimizePMNR. These findings might be integrated with the next steps of the larger Branch-and-Bound paradigm, though we have not explored this direction yet. 4.3
Other Heuristics
In this subsection we describe other heuristics employed in our evaluation. Single-Neuron Tightening and Stopping Criteria. We instantiated the method SingleNeuronTightening with DeepPoly [41], which rapidly gathers concrete bounds by propagating single-neuron bounds across a DNN via concretization and back-substitution. If the ⊥ becomes an element of ConcreteB during at any point during Algorithm 1, then Pmnr terminates as the verification query Q is proven to be unsatisfiable. The stopping criterion StopCondition, which controls the execution of the main loop of Pmnr, holds when any of these conditions is met: (i) the main loop of Algorithm 1 has completed n iterations, where n is a user-defined budget parameter; or (ii) the operation of PostTighten at line 9 of Algorithm 1 has not resulted in any revision to ConcreteB. Optimizable Parameters. Among the algorithm four tunable parameters, the first three αinitial = αselect = αgener are chosen as detailed at [45], whilst αfinal is defined as such: Linear over-approximations of N ’s output layer in terms of its input layer are produced through Symbolic Intervals [46], following which local optimization [56, Section 4.2, Appendix F.] is applied to select αfinal which minimizes the volume of the input-space polytope created by them.
Algorithm 2 GeneratePMNR(N, ConcreteB, SingleB, αgener , Neurons) 1: BranchPoints, BranchB ← Branches(N, ConcreteB, SingleB, αselect ) 2: InfeasibleBranches ← ∅ 3: MultiB ← ∅ (i) 4: m, C (i) , Ĉ , d(i) , dFeasible(i) ← (i) initialPMNR(N, ConcreteB, SingleB, αgener , C (i) , Ĉ ) 5: for k ∈ 1, . . . m do 6: dOptimized(k) ← (i) OptimizePMNR(N, ConcreteB, SingleB, αgener , C (i) , Ĉ , d(i) , MultiB) 7: dBranch(k) ← −∞ 8: for branchCombination in BranchCombinations(Neurons, BranchB) do 9: dBranch(k) ← (i) OptimizePMNR(N, ConcreteB, SingleB, αgener , C (i) , Ĉ , d(i) , MultiB) 10: if dBranch(k) > dFeasible(k) then 11: InfeasibleBranches ← InfeasibleBranches ∪ {branchCombination} 12: end if 13: dOptimized(k) ← min(dOptimized(k) , dBranch(k) ) 14: end for 15: d(k) ← max(d(k) , dOptimized(k) ) P P (i) (i) (i) (i) 16: MultiB ← MultiB ∪ { L−1 + L ≤ d(k) } i=0 Ĉ :k x̂ i=1 C :k x 17: end for 18: return MultiB
Final Tightening. To further tighten ConcreteB given multi-neuron bounds, PostTighten capitalizes on a modified version of the LP-based Forward- Backward Abstract Interpretation [49] framework. It consists of a forward pass, during which only the subset of linear bounds from Din ∪ Dout ∪ ConcreteB ∪ SingleB ∪ MultiB containing neurons from current or preceding layers are counted among the constraints of the LPs solved, as well as a backward pass, in which only those containing neurons from current or subsequent layers are included. 4.4
Heuristics For PMNR-ALL
For the purpose of fairly comparing PMNR instantiated with the heuristics described in previous subsections to existing Multi Neuron Relaxation approaches, we introduce another instantiation of the PMNR paradigm called PmnrAll. It generates multi-neuron bounds for nearly all activation neurons from all layers using the same heuristics in Subsections 4.2 and 4.3, although it differs from our main instantiation of Pmnr in regard to neuron selection. While Pmnr chooses d neurons from a single layer with the NSSE heuristic, PmnrAll selects a set containing all groups of d consecutive unfixed-phase activation neurons from all layers. Following neuron selection, both instantiations produce hyper-planes involving each group of d neurons separately, via BHSO. Pmnr constitutes a middle-ground between SingleNeuronTightening and PmnrAll in regard to performance and tightness. Pmnr improves on
SingleNeuronTightening by producing hyper-planes only involving d heuristically selected neurons, whereas PmnrAll does so by by generating multineuron bounds for nearly all neurons. Notably, in PmnrAll the number of hyper-planes to be calculated scales linearly in the size of the DNN, while in Pmnr it would be constant. Combined with the fact that the computational resources necessary to generate a single hyper-plane also grows with the DNN’s size, it follows that the bounds discovered by PmnrAll are likely to be stronger than these deduced by Pmnr, though they are more computationally expensive to obtain. 4.5
Running Example
Here is a demonstration of Pmnr on an example query Q, featuring the network depicted in Fig. 1. DeepPoly Fails to Verify Q. Consider once more the neural network N from Fig. 1, and domains Din = [−1, 1]2 and Dout = (−∞, 0). Executing DeepPoly (as the instantiation of SingleNeuronTightening) yields the bounds depicted in Appendix D. DeepPoly does not manage to prove that the verification query (3) Q = (N, Din , Dout ) is UNSAT, because the computed output layer’s bounds x0 ∈ [−0.15, 40.1] are not adequately strong. Thus, we progress to the ensuing stages of the PMNR paradigm. Running Example Heuristics. For the running example, we employed simplified tunable parameters and neuron selection heuristics to demonstrate Pmnr. (i) (i) (i) First, ReLU(xj ) ≥ xj and Abs(xj ) ≥ 0 are the linear lower bounds of our choice for unfixed-phase ReLU neurons and Abs neurons, respectively. Moreover, rather than computing NSSE scores for all unfixed-phase activation neurons, we (i) use the span of each neuron’s concrete bounds as its score: i.e., scorej = (i)
(i)
(i)
uj − ℓj is the score of neuron x̂j . Multi-Neuron Relaxation Solves Q. We first demonstrate how Q is solved with PmnrAll, a Multi-Neuron Relaxation-based approach; and then proceed to show that PMNR likewise solves it while requiring less computational effort. (1) (1) (2) (2) PMNR-ALL selects all unfixed-phase neurons in N : x̂1 , x̂2 , x̂0 , x̂1 . It applies multi-neuron bound generation with BHSO, and, given the linear overapproximations discovered by DeepPoly, it produces 12 multi-neuron bounds of (2) (1) (2) (2) (2) (1) the form ϵ(1) x̂0 + ϵ(2) x̂1 ≤ t, ϵ(1) (x̂0 − x0 ) + ϵ(2) (x̂1 − x1 ) ≤ t and (2) (2) (2) (2) 7 x1 ) ≤ t for ϵ ∈ {−1, 1}2 (see Appendix D for ϵ(1) (x̂0 − 87 x0 ) + ϵ(2) (x̂1 − 12 the resulting hyper-planes). (2) (2) Applying PostTighten results in these concrete bounds: ℓ̂0 ← 0, ℓ̂1 ← (3) (3) 0, ℓ̂0 ← 0.1, û0 ← 26.1. Augmenting DeepPoly with partial multi-neuron (3) relaxation yielded the tightened output layer’s bounds x0 ∈ [0.1, 26.1], which, when intersected with the output domain Dout = (−∞, 0), results in empty concrete bounds Q ⇒ ⊥. The stronger relaxations learned by PMNR-ALL thus allowed proving that Q is UNSAT.
PMNR Solves Q more Quickly. The unfixed-phase neurons of N are (1) (1) (2) (2) (1) (1) x̂1 , x̂2 , x̂0 , x̂1 , with associated scores score1 = 10, score2 = 2, (2) (2) score0 = 8, score1 = 12. Because x̂(2) is the layer with greatest neuron score (2) (2) sum, the d = 2 highest-score neurons from it (namely, x̂0 and x̂1 ) are chosen per our BHSO paradigm. PMNR produces eight multi-neuron bounds of the form (2) (2) (2) (2) (2) (2) (2) 7 (2) x1 ) ≤ t ϵ(1) (x̂0 − x0 ) + ϵ(2) (x̂1 − x1 ) ≤ t, ϵ(1) (x̂0 − 78 x0 ) + ϵ(2) (x̂1 − 12 for ϵ ∈ {−1, 1}2 , which are listed in Appendix D. Applying PostTighten yields the same bounds computed by PMNRALL, proving Q is UNSAT. Thus, despite having calculated fewer hyper-planes via BHSO than PMNR-ALL, PMNR manages to solve Q. The ratio between the number of hyper-planes produced by the Multi-Neuron Relaxation-based PMNR-ALL versus PMNR scales linearly with N ’s size, implying that PMNR’s advantage over PMNR-ALL should become even clearer for larger DNNs.
5
Experiments and Evaluation
5.1
Implementation
For our evaluation, we implemented the PMNR paradigm with the heuristics defined in Subsections 4.1–4.3 within the SMT-based Marabou verification tool [24], and compared it to the DeepPoly [41] Symbolic Bound Tightening framework. In addition, we implemented PMNR-ALL defined in Subsection 4.4 as a representative multi-neuron relaxation method, and compared it to our approach. See Appendix E for a more detailed description of our findings. We evaluated our approach on ℓ∞ -local robustness queries with fullyconnected FFNNs, trained on the MNIST dataset [27], including both piecewiselinear (PL) and non-piecewise-linear (NPL) activations. Local robustness verification pertains to the robustness of a DNN to small perturbations around a given input. Formally, given a DNN N , an input x0 and positive reals ε, δ, ℓ∞ local robustness queries have Din = {x : ∥x − x0 ∥∞ ≤ ε} and Dout = {x : ∥N (x) − N (x0 )∥∞ ≤ δ}. Marabou’s SMT Solver is interleaved with calls to bound tightening procedures (by default, DeepPoly) [50]. In our implementation, the initial bound tightening algorithm is replaced by our implementation of PMNR or PMNRALL, while DeepPoly is called for subsequent bound tightening. We have opted to employ DeepPoly for subsequent tightening since invoking PMNR repeatedly would incur an intolerable computational toll. This experimental setup guarantees the only difference between base Marabou, PMNR-enhanced and PMNRALL-enhanced Marabou results from augmenting the first run of DeepPoly with PMNR or PMNR-ALL, with the aim of discovering stronger bounds. We evaluated Marabou with DeepPoly, Pmnr and PmnrAll as the initial bound tightening method on 344 local robustness queries overall, including 272 queries for PL networks and 72 queries for NPL networks. The architectures of all the FFNNs in our evaluation are specified in Appendix A.
The external LP solver Gurobi [15] served to assist the PMNR paradigm’s final bound tightening method PostTighten. For our experiments in this section, we set n = 10 for the stopping condition for PMNR and PMNR-ALL. All experiments were conducted on dual-core machines with 4GB of memory, running Debian 12, with a timeout of T = 14100 seconds (235 minutes). 5.2
PL FFNNs
For our benchmarks on DNNs with piecewise-linear activations, we experimented on fully-connected networks featuring the ReLU, LeakyReLU, Max (Max Pool) [41] and Sign [1] activations. We trained the ReluSignMax and LeakyRelu 14 × 28 FFNNs ourselves using the PyTorch library [43], and verified local robustness for the first image in the MNIST test set with arbitrarily selected ε values of 0.02, 0.04, 0.06, 0.08, thereby producing 36 queries per DNN. As for the remaining two FFNNs, we used the two benchmarks denoted as MNIST1 , MNIST2 in [49], which consist of verifying local robustness around the first 100 MNIST test images with ε = 0.02. The results of our experiments on PL networks is summarized at Table 1. The “Verified” column represents the number of robustness queries which Marabou verified as either satisfiable or unsatisfiable within the time frame of 14100 seconds, and the “Time” column represents the average time required to verify a query (in seconds), computed over the queries that the solver successfully verified. These results highlight the superiority of our approach over both SingleNeuron Relaxation and Multi-Neuron Relaxation: thanks to the tighter hyperplanes discovered by PMNR, PMNR-enhanced Marabou has verified 245 queries out of 272, a 40% improvement over base Marabou which verified only 156 queries, and a 612% improvement over PMNR-ALL which verified merely 40 queries within the time limit due to its higher runtime overhead. Table 1. Comparing Pmnr to DeepPoly and PmnrAll on piecewise-linear networks. Model
Queries
LeakyRelu5 × 100 LeakyRelu8 × 100 LeakyRelu14 × 28 ReluSignMax Total
100 100 36 36 272
5.3
Pmnr DeepPoly PmnrAll Solved ↑ Time ↓ Solved ↑ Time ↓ Solved ↑ Time ↓ 100 67 97 129 40 5003 98 294 33 501 0 ∞ 29 1321 26 16 0 ∞ 18 6138 18 6742 0 ∞ 245 752 174 866 40 5003
NPL Activations FFNNs
For evaluation on non-piecewise-linear activations, we used the PyTorch library to train MNIST classifiers containing the Sigmoid [41], Bilinear (Multiplica-
tion) [37] and Softmax [48] activations. We executed Marabou on 36 local robustness queries per network, characterized in the same way as the LeakyRelu 14 × 28 benchmarks. Summary statistics for our experiments on NPL networks are visible at Table 2. Notably, PMNR-enhanced Marabou verified 56 queries out of 72, an 100% increase over base Marabou (28 verified) and a 3% increase over PMNR-ALL-enhanced Marabou (54 verified). Overall, out of the 344 robustness queries tested, PMNR-enhanced Marabou successfully solved 301 queries, an 49% improvement over base Marabou which solved 202 queries; and a 220% improvement over PMNR-ALL-enhanced Marabou which solved 94. Employing PMNR within Marabou resulted in an average time requirement for verification of 619 seconds, which is 17% faster than DeepPoly (751 seconds) and 86% faster than PMNR-ALL (4622 seconds). Table 2. Comparing Pmnr to DeepPoly and PmnrAll on NPL FFNNs. Model
Queries
ReluBilinearSoftmax LeakyReluSigmoid Total
36 36 72
Pmnr DeepPoly PmnrAll Solved ↑ Time ↓ Solved ↑ Time ↓ Solved ↑ Time ↓ 29 54 10 46 36 6485 27 22 18 19 18 50 56 38 28 28 54 4340
Fig. 4 compares the runtime of PMNR-enhanced Marabou to base Marabou and PMNR-ALL-enhanced Marabou for both classes of benchmarks, while Fig. 3 displays the cumulative runtime of Marabou for every model. Both figures show that, for all models beside ReluBilinearSoftmax, PMNR-enhanced Marabou solved all queries more rapidly compared to PMNR-ALL-enhanced Marabou — due to the latter’s higher associated computational complexity. Further, the figures show that for all models beside LeakyReluSigmoid there exist several dozens of easier queries, which are solved quickly by both methods and for which base Marabou runs faster than PMNR-enhanced Marabou — since the tighter concrete bounds discovered by augmenting DeepPoly with PMNR cause an unnecessary overhead. Nonetheless, the tighter bounds revealed by PMNR assist Marabou in solving the remaining instances that base Marabou would take longer to verify, or fail to verify within the timeout. This is readily apparent in Fig. 3, as the graph of the cumulative number of instances PMNR-enhanced Marabou solved “catches up” to the graph of base Marabou and surpasses it.
6
Related Work
Bound Tightening for DNN Verification. The problem of DNN verification has been thoroughly studied in recent years, bringing about various approaches to tackle this problem, including BaB-based [4, 11, 47] and SMT-based techniques [23, 24, 50], abstraction-refinement [9], techniques featuring LP [8], MILP solvers [44, 53], Lipschitz bounds [42] and other approaches [28].
Performance (5x100)
Verified Instances
100
Peformance (8x100)
100
Peformance (14x28) 200
80
80
60
60
40
40
100
20
20
50
0 10 1
Verified Instances
DeepPoly PMNR PMNR-ALL
100
101
102
103
Performance (ReluSignMax)
20
104
0 10 1
40
100
101
102
Time (seconds)
103
10
20
5
10 100
101
102
103
0 104 10 1
104
Peformance (ReluBilinearSoftmax)
30
15
0 10 1
150
0 10 1
100
101
102
103
104
DeepPoly PMNR PMNR-ALL
30
Peformance (LeakyReluSigmoid)
20 10 100
101
102
Time (seconds)
103
0 104 10 1
100
101
102
103
104
Fig. 3. Cumulative instances verified vs. time (seconds, log scale) for LeakyReLU FFNNs (Top) and other activations FFNNs (bottom).
Our work focuses on bound tightening, which is a key element in many DNN verification techniques. Since symbolic bound tightening methods were first introduced [41,45,46], various techniques have been devised to improve upon them — for instance, by forward-backward abstract interpretation [49], derivation of over-approximations on the inputs with dual optimization [26] or with optimizable parameters [51,56], reducing errors in symbolic bound propagation [53], spurious region-guided refinement [52], inferring multi-neuron bounds from MILP coefficients [54] or from prior branching performed [57], and producing multineuron bounds for all neurons [32, 40]. Building on this large body of existing work, our Partial Multi-Neuron Relaxation (PMNR) approach heuristically selects neurons and generates multi-neuron constraints only involving them and their source neurons. Our framework is general, and is novel in the sense that it allows selecting neurons arbitrarily, without needing to perform actual branching, calculating MILP coefficients, or generating multi-neuron bounds for all neurons. Dual Optimization of Multi-Neuron Bounds. The INVPROP algorithm [26] receives concrete bounds and single-neuron bounds for a ReLU DNN, and uses them to learn bounding hyper-planes using dual linear optimization. INVPROP can be used for generating multi-neuron bounds for ReLU networks, and it inspired our generalized dual optimization method (see Appendices B and C) — which played a key part in our heuristic for generating multi-neuron
104
Performance of PMNR versus DeepPoly
103
DeepPoly
PMNR-ALL
103
Performance of PMNR versus PMNR-ALL
104
102
102
101
101
100 0 10
101
102 PMNR
103
104
100 0 10
101
102 PMNR
103
104
Fig. 4. Comparing the runtimes (seconds, logscale) of PMNR-enhanced Marabou to base Marabou (Left) and to PMNR-ALL-enhanced Marabou (right).
bounds for general activations, as detailed in Subsection 4.2. We further integrated the GenBaB branch-and-bound method for arbitrary non-linearities [37] in our BHSO framework to further optimize hyper-planes. Finally, the dual optimization technique β-CROWN [47], which encodes split-neuron constraints using optimizable parameters, has been successfully applied to obtain multi-neuron bounds for ReLU networks [54], and integrating it with Generalized INVPROP while supporting arbitrary activation functions would be an interesting direction for future work. Other Verification-Related Tasks. The Marabou verifier and other verification tools have been successfully applied to a wide array of tasks, including verification of binarized [1], quantized [16] and recurrent [20] neural networks, verification of aerospace controllers [31] and reinforcement-learning systems [30], proof production and minimization [10, 17, 18], ensemble selection [2] and multilayer modification [35]. Our proposed approach for extending bound tightening could benefit these tasks.
7
Conclusion and Future Work
We presented our approach to augment existing Single Neuron Relaxation-based bound tightening methods by learning multi-neuron bounds featuring only a heuristically selected subset of all neurons. We achieved this by designing new heuristics for neuron selection (NSSE) and multi-neuron bound generation by altering contemporary branching heuristics and bound tightening algorithms. Implementing PMNR in Marabou has successfully resulted in the derivation of tighter bounds at the cost of a runtime overhead for simpler queries, and we seek to explore directions to improve it further. Some of our directions for future
work include: Evaluating our approach over non-MNIST benchmarks and comparing it to, and consider synergies with, other related approaches, including PRIMA [32], k-ReLU [40] or β-CROWN [47]; adding support for GPU-based parallelization; improving our NSSE and BHSO methods, by integrating the resulting multi-neuron bounds and BHSO-inferred infeasible branch combinations with search-based techniques; combining our approach with automatic inferring of single-neuron linear over-approximations [33] to support arbitrary black-box activations, without expert-designed linear bounds. Acknowledgments. This research was partially supported by a grant from the Israeli Science Foundation (grant number 558/24). In addition, this work was partially funded by the European Union (ERC, VeriDeL, 101112713). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council Executive Agency. Neither the European Union nor the granting authority can be held responsible for them.
References 1. G. Amir, H. Wu, C. Barrett, and G. Katz. An SMT-Based Approach for Verifying Binarized Neural Networks. In Proc. 27th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 203–222, 2021. 2. G. Amir, T. Zelazny, G. Katz, and M. Schapira. Verification-Aided Deep Ensemble Selection. In Proc. 22nd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pages 27–37, 2022. 3. M. Bojarski, D. Del Testa, D. Dworakowski, B. Firner, B. Flepp, P. Goyal, L. Jackel, M. Monfort, U. Muller, J. Zhang, X. Zhang, J. Zhao, and K. Zieba. End to End Learning for Self-Driving Cars, 2016. Technical Report. https: //arxiv.org/abs/1604.07316. 4. R. Bunel, J. Lu, I. Turkaslan, P. H. S. Torr, P. Kohli, and M. P. Kumar. Branch and Bound for Piecewise Linear Neural Network Verification, 2025. Technical Report. https://arxiv.org/abs/1909.06588. 5. N. Burkart and M. F. Huber. A Survey on the Explainability of Supervised Machine Learning. Journal of Artificial Intelligence Research, 70:245–317, 2021. 6. H. Cao, Y. Wang, J. Chen, D. Jiang, X. Zhang, Q. Tian, and M. Wang. Swin-Unet: Unet-Like Pure Transformer for Medical Image Segmentation. In Proc. European Conf. on Computer Vision (ECCV), pages 205–218, 2023. 7. N. Carlini and D. Wagner. Towards Evaluating the Robustness of Neural Networks. In Proc. IEEE Symposium on Security and Privacy (S&P), pages 39–57, 2017. 8. R. Ehlers. Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks. In Proc. 15th Int. Symp. on Automated Technology for Verification and Analysis (ATVA), pages 269–286, 2017. 9. Y. Y. Elboher, J. Gottschlich, and G. Katz. An Abstraction-Based Framework for Neural Network Verification. In Proc. 32nd Int. Conf. on Computer Aided Verification (CAV), pages 43–65, 2020. 10. Y. Y. Elboher, O. Isac, G. Katz, T. Ladner, and H. Wu. Abstraction-Based Proof Production in Formal Verification of Neural Networks. In Proc. 8th Int. Symposium on AI Verification (SAIV), pages 203–220, 2025.
11. C. Ferrari, M. N. Muller, N. Jovanovic, and M. Vechev. Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound, 2022. Technical Report. https://arxiv.org/abs/2205.00263. 12. Gemini Team Google. Gemini: A Family of Highly Capable Multimodal Models, 2025. Technical Report. https://arxiv.org/abs/2312.11805. 13. I. Goodfellow, Y. Bengio, and A. Courville. Deep Learning. MIT Press, 2016. https://www.deeplearningbook.org. 14. I. J. Goodfellow, J. Shlens, and C. Szegedy. Explaining and Harnessing Adversarial Examples. In Proc. Int. Conf. on Learning Representations (ICLR), 2015. 15. Gurobi Optimizer Reference Manual. Gurobi Optimization, LLC, 2026. https://www.gurobi.com. 16. P. Huang, H. Wu, Y. Yang, I. Daukantas, M. Wu, Y. Zhang, and C. Barrett. Towards Efficient Verification of Quantized Neural Networks. In Proc. AAAI Conf. on Artificial Intelligence, pages 21152–21160, 2024. 17. O. Isac, C. Barrett, M. Zhang, and G. Katz. Neural Network Verification with Proof Production. In Proc. 22nd Int. Conf. on Formal Methods in ComputerAided Design (FMCAD), pages 38–48, 2022. 18. O. Isac, I. Refaeli, H. Wu, C. Barrett, and G. Katz. Proof Minimization in Neural Network Verification. In Proc. 27th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI), pages 99–124, 2026. 19. O. Isac, Y. Zohar, C. Barrett, and G. Katz. DNN Verification, Reachability, and the Exponential Function Problem. In Proc. 34th Int. Conf. on Concurrency Theory (CONCUR), pages 26:1–26:18, 2023. 20. Y. Jacoby, C. Barrett, and G. Katz. Verifying Recurrent Neural Networks using Invariant Inference. In Proc. 18th Int. Symposium on Automated Technology for Verification and Analysis (ATVA), pages 57–74, 2020. 21. J. John, E. Richard, P. Alexander, G. Tim, F. Michael, R. Olaf, T. Kathryn, B. Russ, Žı́dek Augustin, P. Anna, B. Alex, M. Clemens, K. S. A. A., B. A. J., C. Andrew, R.-P. Bernardino, N. Stanislav, J. Rishub, A. Jonas, B. Trevor, P. Stig, R. David, C. Ellen, Z. Michal, S. Martin, P. Michalina, B. Tamas, B. Sebastian, S. David, V. Oriol, S. A. W., K. Koray, K. Pushmeet, and H. Demis. Highly Accurate Protein Structure Prediction with AlphaFold. Nature, 596:583–589, 2021. 22. K. D. Julian, J. Lopez, J. S. Brush, M. P. Owen, and M. J. Kochenderfer. Policy Compression for Aircraft Collision Avoidance Systems. In Proc. 35th IEEE/AIAA Digital Avionics Systems Conference (DASC), pages 1–10, 2016. 23. G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In Proc. 29th Int. Conf. on Computer Aided Verification (CAV), pages 97–117, 2017. 24. G. Katz, D. Huang, D. Ibeling, K. Julian, C. Lazarus, R. Lim, P. Shah, S. Thakoor, H. Wu, A. Zeljić, D. Dill, M. Kochenderfer, and C. Barrett. The Marabou Framework for Verification and Analysis of Deep Neural Networks. In Proc. 31st Int. Conf. on Computer Aided Verification (CAV), pages 443–452, 2019. 25. K. Kaulen, T. Ladner, S. Bak, C. Brix, H. Duong, T. Flinkow, T. T. Johnson, L. Koller, E. Manino, T. H. Nguyen, and H. Wu. The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results, 2025. Technical Report. https://arxiv.org/abs/2512.19007. 26. S. Kotha, C. Brix, J. Z. Kolter, K. Dvijotham, and H. Zhang. Provably Bounding Neural Network Preimages. In Proc. 37th Conf. on Neural Information Processing Systems (NeurIPS), pages 80270–80290, 2023. 27. Y. Lecun, L. Bottou, Y. Bengio, and P. Haffner. Gradient-based learning applied to document recognition. Proc. of the IEEE, 86(11):2278–2324, 1998.
28. L. Li, T. Xie, and B. Li. SoK: Certified Robustness for Deep Neural Networks. In 2023 IEEE Symposium on Security and Privacy (SP), pages 1289–1310, 2023. 29. Z. Lin, H. Akin, R. Rao, B. Hie, Z. Zhu, W. Lu, N. Smetanin, R. Verkuil, O. Kabeli, Y. Shmueli, A. dos Santos Costa, M. Fazel-Zarandi, T. Sercu, S. Candido, and A. Rives. Evolutionary-scale prediction of atomic-level protein structure with a language model. Science, 379(6637):1123–1130, 2023. 30. U. Mandal, G. Amir, H. Wu, I. Daukantas, F. L. Newell, R. U., B. Meng, M. Durling, M. Ganai, T. Shim, G. Katz, and C. Barrett. Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates. In Proc. 24th Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pages 95–106, 2024. 31. U. Mandal, G. Amir, H. Wu, I. Daukantas, F. L. Newell, R. U., B. Meng, M. Durling, K. Hobbs, M. Ganai, T. Shim, G. Katz, and C. Barrett. Safe and Reliable Training of Learning-Based Aerospace Controllers. In 43rd AIAA DATC/IEEE Digital Avionics Systems Conference (DASC), pages 1–10, 2024. 32. M. N. Müller, G. Makarchuk, G. Singh, M. Püschel, and M. Vechev. PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations. Proc. ACM Program. Lang., 6(POPL):1–33, 2022. 33. B. Paulsen and C. Wang. LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions. In Proc. 28th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 357–376, 2022. 34. Y. Peng, Y. Bao, Y. Chen, C. Wu, C. Meng, and W. Lin. DL2: A Deep Learningdriven Scheduler for Deep Learning Clusters, 2019. Technical Report. https: //arxiv.org/abs/1909.06040. 35. I. Refaeli and G. Katz. Minimal Multi-Layer Modifications of Deep Neural Networks. In 5th International Workshop on Software Verification and Formal Methods for ML-Enables Autonomous Systems (FoMLAS), pages 46–66, 2022. 36. H. Salman, G. Yang, H. Zhang, C. Hsieh, and P. Zhang. A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks. In Proc. 33rd Conf. on Neural Information Processing Systems (NeurIPS), pages 9835–9846, 2019. 37. Z. Shi, Q. Jin, Z. Kolter, S. Jana, C. Hsieh, and H. Zhang. Neural Network Verification with Branch-and-Bound for General Nonlinearities, 2025. Technical Report. https://arxiv.org/abs/2405.21063. 38. I. Shmuel and G. Katz. Neural Network Verification using Partial Multi-Neuron Relaxation (Code), 2026. https://github.com/ido-shm-uel/PMNR-Code. 39. K. Simonyan and A. Zisserman. Very Deep Convolutional Networks for Large-Scale Image Recognition, 2014. Technical Report. https://arxiv.org/abs/1409.1556. 40. G. Singh, R. Ganvir, M. Puschel, and M. Vechev. Beyond the Single Neuron Convex Barrier for Neural Network Certification. In Proc. 33rd Conf. on Neural Information Processing Systems (NeurIPS), pages 15098–15109, 2019. 41. G. Singh, T. Gehr, M. Puschel, and M. Vechev. An abstract Domain for Certifying Neural Networks. In Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2019. 42. C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, I. Goodfellow, and R. Fergus. Intriguing Properties of Neural Networks, 2013. Technical Report. https://arxiv.org/abs/1312.6199. 43. The PyTorch Team. PyTorch 2: Faster Machine Learning Through Dynamic Python Bytecode Transformation and Graph Compilation. In Proc. of the 29th ACM Int. Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 929–947, 2024.
44. V. Tjeng, K. Xiao, and R. Tedrake. Evaluating Robustness of Neural Networks with Mixed Integer Programming, 2017. Technical Report. https://arxiv.org/ abs/1711.07356. 45. K. Wang, S. Pei, J. Whitehouse, J. Yang, and S. Jana. Efficient Formal Safety Analysis of Neural Networks. In Proc. 32nd Conf. on Neural Information Processing Systems (NeurIPS), pages 6369–6379, 2018. 46. S. Wang, K. Pei, J. Whitehouse, J. Yang, and S. Jana. Formal Security Analysis of Neural Networks using Symbolic Intervals. In Proc. 27th USENIX Security Symposium, pages 1599–1614, 2018. 47. S. Wang, H. Zhang, K. Xu, X. Lin, S. Jana, C. Hsieh, and Z. Kolter. Beta-CROWN: Efficient Bound Propagation with Per-Neuron Split Constraints for Neural Network Robustness Verification. In Proc. 35th Conf. on Neural Information Processing Systems (NeurIPS), pages 29909–29921, 2021. 48. D. Wei, H. Wu, M. Wu, P. Chen, C. Barrett, and E. Farchi. Convex Bounds on the Softmax Function with Applications to Robustness Verification. In Proc. 26th Int. Conf. on Artificial Intelligence and Statistics (AISTATS), pages 6853–6878, 2023. 49. H. Wu, C. Barrett, M. Sharif, N. Narodytska, and G. Singh. Scalable Verification of GNN-Based Job Schedulers. Proc. ACM Program. Lang., 6(OOPSLA2):1036– 1065, 2022. 50. H. Wu, O. Isac, A. Zeljić, T. Tagomori, M. Daggitt, W. Kokke, I. Refaeli, G. Amir, K. Julian, S. Bassan, P. Huang, O. Lahav, M. Wu, M. Zhang, E. Komendantskaya, G. Katz, and C. Barrett. Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. In Proc. 36th Int. Conf. on Computer Aided Verification (CAV), pages 249–264, 2024. 51. K. Xu, H. Zhang, S. Wang, Y. Wang, S. Jana, X. Lin, and C.-J. Hsieh. Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers, 2020. Technical Report. https://arxiv. org/abs/2011.13824. 52. P. Yang, R. Li, , J. Li, C. Huang, J. Wang, J. Sun, B. Xue, and L. Zhang. Improving Neural Network Verification through Spurious Region Guided Refinement. In Proc. 27th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 389–408, 2021. 53. T. Zelazny, H. Wu, C. Barrett, and G. Katz. On Optimizing Back-Substitution Methods for Neural Network Verification. In Proc. 22nd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pages 17–26, 2022. 54. H. Zhang, S. Wang, K. Xu, L. Li, B. Li, S. Jana, C. Hsieh, and J. Z. Kolter. General Cutting Planes for Bound-Propagation-Based Neural Network Verification. In Proc. 36th Conf. on Neural Information Processing Systems (NeurIPS), pages 1656–1670, 2022. 55. H. Zhang, T. Weng, P. Chen, C. Hsieh, and L. Daniel. Efficient Neural Network Robustness Certification with General Activation Functions. In Proc. 32nd Conf. on Neural Information Processing Systems (NeurIPS), pages 4944–4953, 2018. 56. X. Zhang, B. Wang, and M. Kwiatkowska. Provable Preimage UnderApproximation for Neural Networks (Full Version), 2024. Technical Report. https://arxiv.org/abs/2305.03686. 57. D. Zhou, C. Brix, G. A. Hanasusanto, and H. Zhang. Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes. In Proc. 38nd Conf. on Neural Information Processing Systems (NeurIPS), pages 29324–29353, 2024.
Appendix A
Experimental Details
Network Architectures. The architectures of all six MNIST Classifiers which were included in our local robustness benchmarks throughout this paper are shown in Table 3. The last two neural networks, ReluBilinearSoftmax and LeakyReluSigmoid, feature non-piecewise-linear activations; whereas the first four consist entirely of piecewise-linear ones. Table 3. The FFNNs used in our experiments. Hidden Hidden Activations Neurons Layers LeakyRelu5 × 100 500 5 LeakyReLU × 5 LeakyRelu8 × 100 800 8 LeakyReLU × 8 LeakyRelu14 × 28 392 14 LeakyReLU × 14 MNIST ReluSignMax 511 6 ReLU × 4, Sign, Max ReluBilinearSoftmax 586 9 ReLU, Bilinear, Softmax LeakyReLU × 6, LeakyReluSigmoid 280 10 Sigmoid × 3, ReLU Dataset Model
B
Generalized INVPROP
In this section we present a general formulation of Theorem 2 from [26, Appendix C], which served as a key building block for the INVPROP algorithm for hyperplane optimization. Our theorem supports optimizing hyper-planes based on previously derived hyper-planes, and it tolerates more general input domains Din and activation functions σi . Theorem. Given constant P vectors ĉ(i) , c(i) , we to optimize the bias t of the Pseek L−1 L bounding hyper-plane {x | i=0 ĉ(i)⊤ x̂(i) + i=1 c(i)⊤ x(i) ≥ t} by solving the dual of the following LP: min x,x̂
s.t.
L−1 X
ĉ(i)⊤ x̂(i) +
i=0
Ĉ
(i)
x̂
x̂(i) +
i=0
x
(i)
c(i)⊤ x(i)
i=1 (0)
x ∈ Din ; L−1 X
L X
=W
(i)
x̂
=x L X
i=1 (i−1)
C (i) x(i) + d ≤ 0
+ b(i)
Wℓ (i) x(i) + bℓ (i) ≤ x̂(i) ≤ Wu (i) x(i) + bu (i)
Theorem 2 lists a lower bound for this linear program. Theorem 2. For any α, γ ≥ 0, g(α, γ) is a lower bound to the above linear program where g is defined via g(α, γ) = inf
x∈Din
−
L X i=1
ĉ(0) − ν (1)⊤ W (1) + γ ⊤ Ĉ
ν (i)⊤ b(i) −
L−1 X
(0) ⊤
x
[ν̂ (i)⊤ ]+ bu (i) − [ν̂ (i)⊤ ]− bℓ (i) + γ ⊤ d
i=1
where the terms ν (i) , ν̂ (i) could be computed recursively with ν (L) = −c(L)⊤ − γ ⊤ C (L) ν̂ (i) = ν (i+1)⊤ W (i+1) − γ ⊤ Ĉ
(i)
− ĉ(i)⊤ , i ∈ [L − 1]
ν (i)⊤ = [ν̂ (i)⊤ ]+ Wu (i) − [ν̂ (i)⊤ ]− Wℓ (i) − γ ⊤ C (i) − c(i)⊤ , i ∈ [L − 1]
Global Bounds for Common Domains. Here are multiple approaches to (0) ⊤ solving the infimum inf x∈Din ĉ(0) − ν (1)⊤ W (1) + γ ⊤ Ĉ x for common input domains Din . – When Din is the hyper-rectangle ℓ(0) ≤ x ≤ u(0) , concretization results in h i⊤ h i⊤ the minimum value c(0) − ν (1)⊤ W (1) u(0) − c(0) − ν (1)⊤ W (1) ℓ(0) . +
−
– When Din is the ℓp -ball ∥x − x′ ∥p ≤ ε for ε > 0, p ∈ [1, ∞), x′ ∈ Rn0 then, ⊤ by duality [55], −ε∥c(0) −ν (1)⊤ W (1) ∥q + c(0) − ν (1)⊤ W (1) x′ is no larger than the infimum, where p1 + 1q = 1. – When Din is a polyhedron Ax + b ≤ 0 then the infimum might be calculated by solving the corresponding LP in the input space. Between Theorem 2 and INVPROP. Our theorem is a general version of Theorem 2 from [26, Appendix C]. A ReLU’s triangular linear relaxation [51] is replaced by the relaxations Wℓ (i) x(i) + bℓ (i) ≤ x̂(i) ≤ Wu (i) x(i) + bu (i) , the output constraint x(L) ≤ 0 is superseded by the general bounding polyhedron PL−1 (i) (i) PL (i) + i=1 Ĉ x̂(i) + d ≤ 0, and the first global lower bound is i=0 C x replaced by an infimum expression. The reader may verify that, by substituting back all these in Theorem 2, then the linear program, lower bound g(α, γ) and recursion formula for ν, ν̂ evaluate to those of Theorem 2 in [26, Appendix C].
C
Proof of Theorem 2
Let us establish the correctness of our generalized theorem using a close argument to [26, Appendix D.]. We’ll start off by taking the Lagrange of a majority of the LP’s constraints. min
L−1 X
max
x,x̂ ν,τ ,π,γ,α
ĉ(i)⊤ x̂(i) +
i=0
+γ
L X
c(i)⊤ x(i)
i=1 L−1 X
⊤
Ĉ
(i)
x̂
(i)
+
i=0
+
L X
L X
! C
(i)
(i)
x
+d
i=1
ν (i)⊤ x(i) − W (i) x̂(i−1) − b(i)
i=1
+
L−1 X
π (i)⊤ x̂(i) − Wu (i) x(i) − bu (i)
i=1
−
L−1 X
τ (i)⊤ x̂(i) − Wℓ (i) x(i) − bℓ (i)
i=1
ℓ(0) ≤ x̂(0) ≤ u(0) ;
s.t.
τ ≥ 0;
π ≥ 0;
γ≥0
According to the Strong Duality Theorem, Reversing the optimization order and re-arranging results in the following equivalent LP: max
min
ν,τ ,π,γ,α x,x̂
c(L)⊤ + ν (L)⊤ + γ ⊤ C (L) x(L)
(0) ⊤ (0) + ĉ(0) − ν (1)⊤ W (1) + γ ⊤ Ĉ x̂ +
L−1 X
c(i)⊤ + ν (i)⊤ − π (i)⊤ Wu (i) + τ (i)⊤ Wℓ (i) + γ ⊤ C (i) x(i)
i=1
+
L−1 X
ĉ(i)⊤ − ν (i+1)⊤ W (i+1) + π (i)⊤ − τ (i)⊤ + γ ⊤ Ĉ
(i)
x̂(i)
i=1
− s.t.
ℓ
L X
i=1 (0)
ν (i)⊤ b(i) −
L−1 X
π (i)⊤ bu (i) − τ (i)⊤ bℓ (i) + γ ⊤ d
i=1 (0)
≤ x̂
(0)
≤u
;
τ ≥ 0;
π ≥ 0;
γ≥0
To solve the inner optimization, notice the variables x(i) , x̂(i) are unconstrained, meaning that their coefficients must equal zero else the outer optimization’s objective would be unbounded. Eliminating the inner optimization
variables x(i) , x̂(i) results in this LP: max
ν,τ ,π,γ,α
inf
x∈Din
−
L X
ĉ(0) − ν (1)⊤ W (1) + γ ⊤ Ĉ
ν (i)⊤ b(i) −
L−1 X
i=1
s.t.
ν
(L)
(0) ⊤
x
π (i)⊤ bu (i) − τ (i)⊤ bℓ (i) + γ ⊤ d
i=1 (L)⊤
= −c
− γ ⊤ C (L)
ν (i)⊤ = π (i)⊤ Wu (i) − τ (i)⊤ Wℓ (i) − c(i)⊤ − γ ⊤ C (i) , i ∈ [L − 1] (i)
ν (i+1)⊤ W (i+1) − γ ⊤ Ĉ τ ≥ 0;
π ≥ 0;
− ĉ(i)⊤ = π (i)⊤ − τ (i)⊤ , i ∈ [L − 1]
γ≥0
Denote ν̂ (i) = ν (i+1)⊤ W (i+1) − γ ⊤ Ĉ (i+1)
(i)
− ĉ(i)⊤ . The constraints π ≥ 0, τ ≥ 0
(i)
and ν (i+1)⊤ W − γ ⊤ Ĉ = π (i)⊤ − τ (i)⊤ imply setting the values of π (i) and τ (i) to be π (i) = [ν̂ (i) ]+ and τ (i) = [ν̂ (i) ]− yields a valid lower bound for the optimization. Combined with the two other equality constraints of the linear program, we arrive at the following recursive relation for ν (i) , ν̂ (i) : ν (L) = −c(L)⊤ − γ ⊤ C (L) ν̂ (i) = ν (i+1)⊤ W (i+1) − γ ⊤ Ĉ
(i)
− ĉ(i)⊤ , i ∈ [L − 1]
ν (i)⊤ = [ν̂ (i)⊤ ]+ Wu (i) − [ν̂ (i)⊤ ]− Wℓ (i) − γ ⊤ C (i) − c(i)⊤ , i ∈ [L − 1] Overall, we have that the optimal value for the original linear program is no smaller than the solution of this LP: (0) ⊤ max inf ĉ(0) − ν (1)⊤ W (1) + γ ⊤ Ĉ x γ,α
x∈Din
−
L X i=1
s.t.
ν (i)⊤ b(i) −
L−1 X
[ν̂ (i)⊤ ]+ bu (i) − [ν̂ (i)⊤ ]− bℓ (i) + γ ⊤ d
i=1
γ≥0
Consequently, g(α, γ) is a lower bound to the original LP’s solution for every choice of γ ≥ 0 and α, where g is the objective function of the above optimization problem.
D
Running Example Details
In this section we include additional computations regarding the running example in Subsection 4.5. DeepPoly Outputs. Fig. 5 shows the linear over-approximations and concrete bounds produced by the Single-Neuron Relaxation-based DeepPoly.
[0, 2] (1)
x̂0 1
[−1, 1]
1
[0, 4]
1 -1
(0)
x̂0
[0, 5] 2
(2)
x̂0
-1
[12.1, 26.1]
0
1
(1)
(3)
x̂1 -3
[−1, 1]
0
x0 1
[0, 6]
(0)
26.1
-3
(2)
x̂1
x̂1
-1 [0, 1] 1
2
-5 (1) x̂2
0 (0)
(2)
(1)
(2)
(2)
(1)
(1)
(3)
x1 = 2x̂0 − 3x̂1 (1) x1 ∈ [−5, 5]
(0)
0 ≤ x̂1 ≤ 5 (1) x̂1 ∈ [0, 5]
x0 = x̂0 + 1 (1) x0 ∈ [0, 2]
(0)
x2 = x̂1 (1) x2 ∈ [−1, 1]
x1 = 2 − x̂0 + x̂1 − 5x̂2 (2) x1 ∈ [−5, 7]
(1)
0 ≤ x̂2 ≤ 1 (1) x̂2 ∈ [0, 1]
(1)
7 x1 ≤ x̂1 ≤ 12 x1 + 35 12 (2) x̂1 ∈ [−5, 7]
−1 ≤ x̂1 ≤ 1 (0) x̂1 ∈ [−1, 1] (1)
(1)
(1)
x0 ≤ x̂0 ≤ x0 (1) x̂0 ∈ [0, 2]
(1)
(0)
(0)
−1 ≤ x̂0 ≤ 1 (0) x̂0 ∈ [−1, 1]
(1)
(0)
(1)
x0 = x̂0 + x̂1 − x̂2 (2) x0 ∈ [−1, 7] (2)
x0 ≤ x̂0 ≤ 87 x0 + 78 (2) x̂0 ∈ [−1, 7] (1)
(2)
(2)
(2)
(1)
(2)
x0 = −x̂0 (2) −3x̂1 + 26.1 (3) x0 ∈ [−0.15, 40.1] (1)
(2)
Fig. 5. The DNN shown in Fig. 1 and DeepPoly bounds for it given Din = [−1, 1]2 .
Hyper-planes learned by PMNR-ALL. Here are the 12 hyper-planes generated by PmnrAll (in an arbitrary order) by invoking BHSO and PGD for
optimization of the lower bound listed in Theorem 2: (1)
(1)
(1)
(1)
(1)
(1)
(1)
(1)
(2)
(2)
x̂1 + x̂2 ≤ 6, −x̂1 − x̂2 ≤ 0, −x̂1 + x̂2 ≤ 1, x̂1 − x̂2 ≤ 5, (2)
(2)
(x̂0 − x0 ) + (x̂1 − x1 ) ≤ 5, (2)
(2)
(2)
(2)
7 x1 ) ≤ 1.96, −(x̂0 − 87 x0 ) − (x̂1 − 12 (2)
(2)
(2)
(2)
−(x̂0 − x0 ) + (x̂1 − x1 ) ≤ 5, (2)
(2)
(2)
(2)
7 (x̂0 − 87 x0 ) − (x̂1 − 12 x1 ) ≤ 2.96, (2)
(2)
(2)
(2)
(x̂0 − x0 ) − (x̂1 − x1 ) ≤ 1, (2)
(2)
(2)
(2)
7 (x̂0 − 87 x0 ) + (x̂1 − 12 x1 ) ≤ 3.04, (2)
(2)
(2)
(2)
−(x̂0 − x0 ) − (x̂1 − x1 ) ≤ 0, (2)
(2)
(2)
(2)
7 (x̂0 − 87 x0 ) + (x̂1 − 12 x1 ) ≤ 3.54
Hyper-planes learned by PMNR. Below are the 8 multi-neuron bounds Pmnr inferred in an identical manner to PMNR-ALL. They are slightly looser than the relaxations produced by PMNR-ALL. (2)
(2)
(2)
(2)
(x̂0 − x0 ) + (x̂1 − x1 ) ≤ 20, (2)
(2)
(2)
(2)
7 −(x̂0 − 87 x0 ) − (x̂1 − 12 x1 ) ≤ 2.46, (2)
(2)
(2)
(2)
−(x̂0 − x0 ) + (x̂1 − x1 ) ≤ 5.14, (2)
(2)
(2)
(2)
7 (x̂0 − 87 x0 ) − (x̂1 − 12 x1 ) ≤ 2.99, (2)
(2)
(2)
(2)
(x̂0 − x0 ) − (x̂1 − x1 ) ≤ 1.02, (2)
(2)
(2)
(2)
7 (x̂0 − 87 x0 ) + (x̂1 − 12 x1 ) ≤ 3.07, (2)
(2)
(2)
(2)
−(x̂0 − x0 ) − (x̂1 − x1 ) ≤ 0, (2)
(2)
(2)
(2)
7 (x̂0 − 87 x0 ) + (x̂1 − 12 x1 ) ≤ 3.54
E
Evaluation Within Marabou
E.1
Neuron Selection Heuristic
To quantify the impact of our proposed NSSE heuristic, we implemented another instantiation of the PMNR, named PMNR-Random, which only differs from the main instantiation Pmnr in terms of its neuron selection heuristic. As opposed to Pmnr which chooses neurons with maximal NSSE score, PMNR-Random picks a layer ℓ uniformly at random, then proceeds to selects d unfixed-phase neurons from it. In an identical fashion to our experiments in Section 5, we replaced the initial bound tightening algorithm of Marabou with PMNR-Random and compared it to PMNR-enhanced Marabou on 344 local robustness queries. Aggregate results are shown at Table 4 and Marabou’s cumulative runtime per model is depicted in Fig. 6. Overall, leveraging the NSSE heuristic within PMNR-enhanced Marabou resulted in 301 queries being verified out of 344, an 10% improvement over random neuron selection (273 verified). The largest gains were noted for the piecewise-linear ReluSignMax and the non-piecewise-linear ReluBilinearSoftmax DNNs, for which NSSE-based neuron selection has led to a ×2-2.9 more verified queries (27 and 29 solved queries with NSSE, in contrast to 9 and 10 solved queries without NSSE, respectively). Table 4. Comparing NSSE-based to random neuron selection in Pmnr.
E.2
Model
Queries
LeakyRelu5 × 100 LeakyRelu8 × 100 LeakyRelu14 × 28 ReluSignMax ReluBilinearSoftmax LeakyReluSigmoid Total
100 100 36 36 36 36 344
Pmnr (NSSE) Pmnr (Random) Solved ↑ Time ↓ Solved ↑ Time ↓ 100 67 100 68 98 294 98 305 29 1321 29 1147 18 6138 9 34 29 54 10 69 27 22 27 21 301 619 273 261
Stop Condition
Here we assess the costs and benefits of different n values for the stop condition in Subsection 4.3. Deciding on a value for n presents a dilemma between tightness and accuracy, since the more iterations the main loop of Algorithm 1 completes, the bounds returned from it are tighter, at the cost of a requiring greater computational resources to derive. We evaluated the performance of PMNR-enhanced Marabou with n = 1 and compared it to the n = 10, the latter being the setting of choice for all our other experiments in this paper. Aggregate results are shown at Table 5 and Marabou’s cumulative runtime per model is depicted in Fig. 7. Overall, our default choice of n = 10 has led
Performance (5x100)
Verified Instances
100
80
60
60
40
40
20
20
0 10 1
100
101
102
103
Performance (ReluSignMax) Verified Instances
Peformance (14x28) 30 25 20 15 10 5
0 10 1
104
100
101
102
Time (seconds)
103
104
Peformance (ReluBilinearSoftmax) 30
20
102
103
104
0 10 1
103
104
PMNR PMNR-Random
30
Peformance (LeakyReluSigmoid)
5
5 101
102
10
10 100
101
15
15
5
100
20
20
10
0 10 1
25
25
15
0 10 1
Peformance (8x100)
100
80
PMNR PMNR-Random
100
101
102
Time (seconds)
103
104
0 10 1
100
101
102
103
104
Fig. 6. Cumulative instances verified with PMNR-enhanced Marabou and PMNRRandom-enhanced Marabou, versus time (seconds, log scale) required for verification, for every benchmark class.
to three additional queries being verified (301 versus 298, a 1% gain), albeit with a runtime overhead of 37% (619 versus 451 seconds). The stronger hyperplanes inferred by PMNR using n = 10 has only impacted the final number of solved queries for the two piecewise-linear benchmarks LeakyRelu8 × 100, LeakyRelu14 × 28, and the remaining four models have seen no change in the number of verified queries.
E.3
Comparing PMNR to Forward-Backward Abstract Interpretation
In order to further highlight the advantage of the PMNR paradigm over SingleNeuron Relaxation, we have elected to implement the F+BC configuration of Forward-Backward Abstract Interpretation [49], using the stop condition laid out in Subsection 4.3. We replaced PMNR with F+BC as Marabou’s initial bound tightening method and analyzed the results. Summary statistics are specified at Table 6 and Marabou’s cumulative runtime is displayed in Fig. 8. These results demonstrate the benefits provided by the tighter bound inferred by PMNR, as using Pmnr over F+BC for initial bound derivation caused a 55% ( 301 194 ) rise in the number of solved instances, at the cost of a ×3.21 slower runtime (619 versus 193 seconds).
Table 5. Comparing maximum main loop iteration values of n = 1 and n = 10 for Pmnr. Model
Queries
LeakyRelu5 × 100 LeakyRelu8 × 100 LeakyRelu14 × 28 ReluSignMax ReluBilinearSoftmax LeakyReluSigmoid Total
100 100 36 36 36 36 344
Pmnr (n=10) Pmnr (n=1) Solved ↑ Time ↓ Solved ↑ Time ↓ 100 67 100 49 98 294 97 234 29 1321 27 137 18 6138 18 5607 29 54 29 57 27 22 27 28 301 619 298 451
Identically to the comparison between DeepPoly and PMNR in Section 5, for all models except LeakyReluSigmoid it holds that the Single-Neuron Relaxation-based F+BC successfully solves a portion of all queries faster than PMNR does (due to the additional computing power needed for multi-neuron bounds), yet PMNR solves the remaining instances more rapidly compared to F+BC thanks to the tighter relaxations derived. This is illustrated clearly in Fig. 8, where PMNR’s cumulative runtime graph eventually surpasses and towers over F+BC’s graph. Table 6. Comparing Pmnr to the F+BC configuration of Forward-Backward Abstract Interpretation. Model
Queries
LeakyRelu5 × 100 LeakyRelu8 × 100 LeakyRelu14 × 28 ReluSignMax ReluBilinearSoftmax LeakyReluSigmoid Total
100 100 36 36 36 36 344
Pmnr F+BC Solved ↑ Time ↓ Solved ↑ Time ↓ 100 67 97 137 98 294 33 530 29 1321 27 54 18 6138 9 2 29 54 10 38 27 22 18 5 301 619 194 168
Performance (5x100)
Verified Instances
100
Peformance (8x100)
100
Peformance (14x28) 200
80
80
60
60
40
40
100
20
20
50
0 10 1
100
101
102
103
104
100
101
102
Time (seconds)
103
104
Peformance (ReluBilinearSoftmax)
30
103
104
Peformance (LeakyReluSigmoid)
5
5 102
103
10
10 101
102
15
15
100
101
20
20
5
100
25
25
10
0 10 1
PMNR PMNR-Once
30
15
0 10 1
150
0 10 1
Performance (ReluSignMax) 20
Verified Instances
PMNR PMNR-Once
0 104 10 1
100
101
102
Time (seconds)
103
0 104 10 1
100
101
102
103
104
Fig. 7. Cumulative instances solved by PMNR-enhanced Marabou (for n values of 1 and 10) versus time requirements (seconds, log scale).
Performance (5x100)
Verified Instances
100 80
80
60
60
40
40
20
20
0 10 1
100
101
102
103
Performance (ReluSignMax) Verified Instances
Peformance (14x28) 30 25 20 15 10 5
0 10 1
104
100
101
102
Time (seconds)
103
104
Peformance (ReluBilinearSoftmax) 30
20
102
103
104
0 10 1
103
104 PMNR F+BC
30
Peformance (LeakyReluSigmoid)
5
5 101
102
10
10 100
101
15
15
5
100
20
20
10
0 10 1
25
25
15
0 10 1
Peformance (8x100)
100
PMNR F+BC
100
101
102
Time (seconds)
103
104
0 10 1
100
101
102
103
104
Fig. 8. Cumulative instances solved by PMNR-enhanced and Forward-BackwardAnalysis-enhanced Marabou versus time costs (seconds, log scale).