Mining Verdict Boundaries for Neural Network Verification Jiawei Ren1
, Guanqin Zhang1
, Zhenya Zhang2,3
, and Yulei Sui1
University of New South Wales, Sydney, Australia {jiawei.ren, guanqin.zhang, y.sui}@unsw.edu.au 2 Kyushu University, Fukuoka, Japan [email protected] 3 National Institute of Informatics, Tokyo, Japan
arXiv:2607.28954v1 [cs.LG] 31 Jul 2026
1
Abstract. Branch and Bound (BaB) aims to achieve complete verification of neural networks by adaptively partitioning the problem and applying off-the-shelf verifiers to subproblems. Its problem-splitting history can be represented as a tree, where each subproblem corresponds to a child node. A key problem of BaB lies in searching for the verdict boundaries across all the paths that divide the verified and unverified subproblems. We observe that the existing BaB approach tackles this problem by solving each expensive subproblem sequentially along the tree path as its depth increases, requiring costly bounds propagation at every visited BaB tree node (i.e., subproblem), which is inefficient. To address this issue, we propose effective search approaches that leverage the monotonicity of each path to efficiently and precisely locate the verdict boundary by simultaneously splitting multiple activation functions (e.g., ReLU), rather than processing them one at a time as in the classical approach. Our approach performs an effective exponential search along each path, allowing us to skip many boundary-unrelated subproblems when identifying the verdict boundary. The enhanced version further improves this process by estimating the boundary’s position using quantitative information obtained from subproblem solving. We perform experimental evaluation on commonly-used benchmarks to assess our proposed techniques, and compare them with recent BaB-based approaches.
1
Introduction
The rapid adoption of neural networks in safety-critical settings, such as autonomous driving, makes unexpected model failures potentially severe. Their susceptibility to adversarial perturbations [12, 22] underscores the need for rigorous assurance. Neural network verification offers provable guarantees of safety and robustness under specified input conditions [15, 21, 23] and has therefore become a rapidly growing area within formal verification research. Existing Efforts. Typical neural network verification approaches include completeness-driven constraint solving with a timeout budget [19, 31] and approximation-based methods [28, 29, 32]. While the former aims to compute exact bounds, the latter trades precision for efficiency. To mitigate the incompleteness of approximation-based methods, Branch and Bound (BaB) [5] has
This version of the contribution has been accepted for publication, after peer review, but is not the Version of Record and does not reflect post-acceptance improvements or corrections. The Version of Record is available online at: https://doi.org/10.1007/978-3-032-26204-2_4.
2
J. Ren et al.
emerged as the state-of-the-art abstraction refinement approach. Given a specification, BaB employs an efficient approximation-based verifier to compute a distance p̂ that signifies how much the network satisfies the specification; if p̂ is negative, it splits the problem into subproblems (e.g., on input intervals [33] or ReLU phases [4]). It repeats this process on each subproblem, which can yield a tighter approximation and hence a greater p̂, for each subproblem, until all the subproblems are verified (i.e., p̂ > 0) [34]. Motivation and Insights. In BaB, the iterative problem splitting process can be structured as a tree, where each node identifies a subproblem. The objective is to confirm that each tree path ends with a verified node, which is a necessary condition to verify the original problem. Moreover, since problem splitting reduces approximation error, p̂, which measures how much the over-approximation satisfies the specification (p̂ > 0 implies satisfaction), often exhibits a high degree of monotonicity along each path as the node depth increases. We empirically confirm this behavior using a state-of-the-art BaB approach [34]. Because of this, there must exist a boundary point (regardless of special cases, such as when the problem is verified at the root) in each path that divides the verified nodes and the unverified nodes, which require no further problem splitting. BaB essentially needs to find such a verdict boundary for each path of the tree. However, existing BaB approaches, e.g., [5, 34], identify the verdict boundary in each path by calling an approximated verifier on each node one by one along the path, to locate the boundary point. Since each visit of a node involves a non-trivial problem-solving process by approximated verifiers, this introduces significant time costs. On the other hand, due to the monotonicity of p̂ in each path, the problem of finding the boundary point in each path boils down to a search problem for a value in a nearly sorted array. To this end, we can devise more efficient approaches to find the verdict boundary. Our Solution. In this paper, we propose a new verification approach, BMiner, which performs efficient per-path boundary mining within the BaB tree. By exploiting the monotonicity of p̂ in each tree path, BMiner formulates the location of the verdict boundary as a search problem in a nearly sorted array and thereby devises two efficient search approaches that, instead of visiting each tree node one-by-one, skip significant node visits in each tree path. The first approach BMinerE adapts the classic exponential search [1]. Given a path, BMinerE involves two phases to locate the boundary point: first, it identifies a range that contains the verdict boundary point, by progressively sliding and expanding the range with an exponentially increasing size; after fixing such a range, it locates the exact boundary point position by binary search. While BMinerE can reduce the number of node visits compared to classic BaB, it may still need too many node visits to identify the range that contains the boundary point in a path. To further improve this, we devise BMinerG , which leverages the quantitative p̂ of nodes to estimate its gradient (more precisely, its changing rate) in a path, by which it predicts the position of the boundary point. While the prediction may not be precise, by checking the node at the predicted
Mining Verdict Boundaries for Neural Network Verification
3
position, we can efficiently update the gradient information and continue our search until we find the boundary point. We compare with two state-of-the-art tools as our baselines, on 500 verification problem instances from the widely used MNIST and CIFAR-10 datasets. The evaluation results demonstrate that our proposed approach can reduce the average verification time cost by 17% – 30%, with a maximum reduction of 44.7% across five neural networks.
2
Preliminaries
2.1
Neural Network Verification Problem
We define feed-forward neural networks following standard literature [5, 19, 29]. Definition 1 (Neural networks). A (feed-forward) neural network N : Rn → Rm consists of alternating affine transformations and nonlinear activations σ. Let x0 be the input. For each layer i (i ∈ {1, . . . , L}), xi = σ(Wi xi−1 + Bi ), where Wi , Bi are the weights and biases. The dimension of xi equals the number of neurons in layer i. Following established works [20], we adopt ReLU in our neural networks, defined as ReLU(x) = max(0, x). Specifications are used to formalize desired properties of neural networks. We adopt the notation in Def. 2 as our specification formalism, which is sufficiently expressive for commonly-used properties, such as local robustness [12]. Definition 2 (Specification). We define a specification for a neural network as a pair (Φ, Ψ) that includes an input specification Φ and an output specification Ψ. The input specification Φ is a predicate over the input region, and the output specification Ψ is a predicate over the output of the neural network. Specifically, we represent the output specification Ψ as f (N (x)) > 0, where f : Rm → R is a function that maps an m-dimensional vector to a real number. Definition 3 (Verification problem). Given a neural network N and a specification (Φ, Ψ), a verification problem aims to answer the question whether Ψ(N (x)) holds, for any input x that holds Φ(x). A verifier is a tool designed to solve this problem. It either returns true, certifying that N satisfies the specification, or returns false with a counterexample. We now demonstrate how our notations formalize a verification problem as in Def. 3 against local robustness, a property frequently studied in image classification. Local robustness requires that a neural network classifier consistently assigns the same label to two images, x and x0 , where x is derived from x0 by applying small perturbations. Formally, given a reference input x0 , the input specification Φ(x) enforces that x should hold that ∥x − x0 ∥∞ ≤ ϵ, where ∥ · ∥∞ is the ℓ∞ -norm distance metric, and ϵ is a small positive real. The output specification Ψ(N (x)) requires that min1≤i≤m,i̸=i0 (N (x)i0 − N (x)i ) > 0 where N (x)i denotes the i-th component of the output vector N (x), and i0 is the label assigned to x0 by the neural network, i.e., i0 = arg max 1≤i≤m N (x0 )i .
4
2.2
J. Ren et al.
Verification by Branch-and-Bound (BaB)
BaB [5] serves as the backbone for sevAlgorithm 1 Branch and Bound [5] eral advanced verification tools, such as αβ-Crown [34]. Essentially, it is Require: A neural network N , an input specification Φ, an output specification a “divide-and-conquer” strategy that Ψ, an approximated verifier AppVer(·), adaptively splits a verification proband a ReLU selection heuristic H(·). lem into its subproblems and lever- Ensure: A verdict ∈ {true, false}. ages off-the-shelf approximated veri- 1: Q ← {⊤} , T ← ∅ fiers to tackle the resulting subprob- 2: BaB(Q) lems. Since approximated verifiers can 3: function BaB(Q) yield tighter over-approximations on 4: if Empty(Q) then return true subproblems, BaB mitigates their com- 5: Γ ← Pop(Q) pleteness limitations when applied di- 6: 7: p̂ ← AppVer(N, Φ, Ψ, Γ) rectly to the original problem. 8: T ← T ∪ {⟨Γ, p̂⟩} Approximated verifiers. Various 9: if p̂ < 0 then techniques have been proposed to con- 10: if |Γ| = K then struct over-approximation, e.g., lin- 11: return false ear relaxation by DeepPoly [29] that 12: else uses linear constraints to bound each 13: {ri+ , ri− } ← H(Γ) ReLU’s output (see Fig. 1). Notably, 14: for a ∈ {ri+ , ri− } do 15: Q ← Q ∪ {Γ ∧ a} BaB is orthogonal to these approaches, i.e., it works with any of the selected 16: return BaB(Q) ones. For a verification problem, an approximated verifier AppVer returns a quantity p̂ ∈ R called a verifier assessment [41], computed by p̂ = miny∈Ω̂ f (y),
where Ω̂ is the over-approximated region of the neural network output, and f is the function in output specification as defined in Def. 2. Here p̂ indicates how much the over-approximation satisfies the specification: If p̂ is positive, the original output satisfies the specification, thereby certifying the neural network.
Definition 4 (ReLU specification). Let N be a neural network with K neurons, and x̂i ∈ R (i ∈ {1, . . . , K}) be the input for the ReLU function in the i-th neuron. Introduce two literals ri+ := (x̂i ≥ 0), ri− := (x̂i < 0). A ReLU specification is a conjunction of literals thatVfixes the activation sign of a (possibly empty) set of distinct neurons: Γ = i∈I ℓi , where I ⊆ {1, . . . , K} and ℓi ∈ { ri+ , ri− }. The length of the specification is defined as |Γ| = |I|. When I = ∅, we write Γ = ⊤ and call it an empty specification. Given a neuron i, w.r.t the sign of its prey x (x − x ) ReLU(x) ≤ x −x activation value, ri+ and ri− can be derived to split the ReLU function into two linear functions. By adding each proposition as an additional conReLU(x) ≥ αx x L U straint, the verification problem can be divided into x x two subproblems. If both subproblems are verified, Fig. 1: Linear relaxation of since ri+ and ri− cover all possible cases of the ReLU ReLU function. input, the original problem is also verified. U
L
U
L
Mining Verdict Boundaries for Neural Network Verification
5
The BaB algorithm is presented in Alg. 1. In addition to input/output specification, we allow AppVer to take an additional argument, i.e., a ReLU specification Γ, which identifies a subproblem obtained by adding Γ (i.e., the conjunction of a number of propositions about ReLU inputs) as a constraint to the original problem. Alg. 1 uses a queue Q to maintain the (sub)problems to be solved, which is initialized as a set that contains only ⊤, i.e., the original problem. The algorithm starts with a call of function BaB with the initial Q (Line 2). i) First, BaB applies AppVer to the original problem (Line 7): if AppVer returns a positive p̂, it implies that the original problem is verified and so the verification can be terminated with true returned; ii) In the case the problem cannot be verified (i.e., p̂ < 0), it splits the problem into two subproblems. This is achieved by selecting a ReLU in the neural network according to a pre-defined ReLU selection heuristic H that returns two propositions {ri+ , ri− } about the input of the selected ReLU, based on a given ReLU specification Γ (Line 13; details are introduced later). The selected ReLU i derives two subproblems, identified by Γ ∧ ri+ and Γ ∧ ri− respectively, which are pushed into Q; iii) Then, the function BaB is called recursively with the updated Q (Line 16), so it can apply AppVer to the new subproblems. For each subproblem, it goes through a similar process with the original problem: the subproblem can be verified if p̂ > 0; otherwise, it needs to be further split; iv) The original problem (identified by ⊤) can be verified if all of the subproblems are verified, in which case Q will be empty (Line 5). BaB needs a ReLU selection heuristic H that orders neurons and selects the next ReLU according to the specification. Existing strategies such as DeepSplit [14] and FSB [8] can be integrated, as our method is orthogonal to them. Following an existing neural network verification approach [34], we adopt and extend the state-of-the-art ReLU selection strategy [8] (detailed in §5).
3
Verdict Boundary Insight and Formulation
We introduce a formulation that models BaB-based verification as a search problem. Strictly, this formulation should be on the premise of the near-monotonicity of p̂ when problem splitting happens, but this may not always hold for some recent implementations of BaB, such as αβ-Crown [34]. Our empirical study shows that such non-monotonic splitting is rare, and even when it occurs, it is typically local and does not change the overall monotonic trend of p̂; thus, it does not affect the effectiveness of our approach, as confirmed experimentally. 3.1
Near-Monotonic Behaviour in BaB Tree Paths
The BaB approach (Alg. 1) produces a binary tree, called the BaB tree. Definition 5 (BaB tree). In BaB, a binary tree T , called a BaB tree, is used to record the (sub)problems produced during the execution of BaB. Each node is denoted as a tuple ⟨Γ, p̂⟩, which consists of a ReLU specification Γ that identifies
6
J. Ren et al.
a (sub)problem, and a verifier assessment p̂ that indicates the verification result of the (sub)problem by applying AppVer. In general, as a divide-and-conquer approach, BaB aims to continuously refine the approximation to increase p̂, i.e., the distance between the over-approximated output region Ω̂ and the negation of the specification, via a sequence of problem splitting in different paths. In other words, during a sequence of problem splitting, p̂ is expected to keep monotonically increasing until it becomes positive at some point, which signifies a successful verification of the subproblem. However, problem splitting may not always produce an increased p̂, depending on the adopted approximated verifier. For example, BaB with Planet [9] as the verifier, holds such monotonicity, because every problem splitting can lead the over-approximation Ω̂ to a subset Ω̂ † ⊆ Ω̂. In recent approaches, e.g., αβCrown [34], this monotonicity may be broken. Instead of using a fixed linear bound for ReLU, they search for an optimal lower bound by varying α (i.e., the slope of the linear constraints in Fig. 1). This may lead to the situation where the over-approximation Ω̂ † after problem splitting is not necessarily a subset of Ω̂ before the splitting. Consequently, p̂ may decrease. To understand how frequently this can happen, we perform an empirical study for αβ-Crown. Empirical evidence on αβCrown. We adopt the same set of benchmarks used in our experimental evaluation (see Table 2). We apply αβ-Crown to solve each problem, and record the resulting BaB tree. Fig. 2 shows a box plot of the distribution of the ratio of the monotonic paths over all Fig. 2: Distribution of ratio of monotone paths the paths in each BaB tree. By a monotonic path, we mean the paths in which p̂ never decreases in a node against its parent. We annotate the relevant statistical data, including the average ratio and the number of trees whose ratio is below 95%. By Fig. 2, we can find that, for many BaB trees, all their paths are monotonic, as evidenced by the very narrow distance between the lower and upper quartiles. Even if there are some trees in which non-monotonic paths exist, the number of such trees is not very large in most models. The notable exception is MNISTL4 , for which there is a considerable number of trees whose monotonic path ratio is relatively low. This could be attributed to our way of counting, i.e., as long as there exists a non-monotonic node, we count the path as non-monotonic; because of this, if a non-monotonic node occurs at a location close to the root, it affects all the paths in its sub-trees, so it can make the ratio very low. Note that the metric used in Fig. 2, i.e., the ratio of monotonic paths, is relatively strong, because monotonicity of the whole path requires that there does not exist even a single pair of nodes that breaks the monotonicity. Therefore, the metric used in Fig. 2 is a relatively strong one, and is subject to the positions
Mining Verdict Boundaries for Neural Network Verification
7
of such non-monotonic pairs of tree nodes. In Table 1, we further analyze the impact of these pairs on the whole paths. • First, the column “Pathmono ” shows the overall ratio of the monotonic paths over all the paths of all the trees in the tasks of each model. This confirms that most of the paths hold monotonicity; • Second, the column “Pairmono ” shows how many pairs are non-monotonic, over all the pairs in the trees. We find that, the ratios are all greater than those in “Pathmono ”, showing that mostly the non-monotonicity of paths happens, due to some individual pairs in the paths; • Third, the column “Triplemono ” records that, among the non-monotonic pairs in “Pairmono ”, how many of them hold that, p̂ in the subsequent node after the pair is increased compared to the first node in the pair; namely, this metric implies that how many non-monotonic pairs only happen locally and do not have a significant impact on the whole paths. The results indicate that, while Table 1: Monotonicity Statistics. some BaB implementations may not Tree size Pathmono Pairmono Triplemono hold monotonicity, such violations do Model 163 98.1% 99.8% 69.1% not happen frequently. Moreover, the MNISTL2 2535 72.3% 96.6% 74.7% impact on the whole path mostly re- MNISTL4 OVAL21 896 97.4% 99.7% 95.8% mains local. By this, we proceed to OVAL21BASE 366 98.3% 99.8% 97.3% DEEP our formulation that deems BaB veri- OVAL21WIDE 877 98.8% 99.9% 99.7% fication as a search problem. 3.2
Verdict Boundary
We first introduce the notion of verdict boundary in Def. 6. Later, we show the connection between this notion and the objective of BaB-based verification. Definition 6 (Verdict boundary). Given a BaB tree that has n paths, a verdict boundary is an n-tuple ⟨b1 , . . . , bn ⟩, where each bi ∈ N≥0 (i ∈ {1, . . . , n}) is called a boundary point such that, for each node ⟨Γ, p̂⟩ in the i-th path, if |Γ| ≥ bi , then p̂ ≥ 0; otherwise if |Γ| < bi , then p̂ < 0. Specifically, bi = 0 if the root node of the BaB tree is verified; bi = K + 1 (K is the total number of ReLUs) if none of the nodes is verified in the i-th path. Intuitively, each element bi in a verdict boundary is a position in a tree path that divides the nodes respectively decided as verified and unverified by approximated verifiers. As p̂ is mostly monotonic in each path, the nodes preceding bi are most likely to be unverified, and the nodes succeeding (including) bi are most likely to be verified. Example 1 visualizes a verdict boundary in a BaB tree. Example 1. Fig. 3a depicts a BaB tree, in which the verifier assessment p̂ of each node is annotated in each node. In this example, the BaB algorithm finally verifies the problem because all the subproblems are verified (i.e., p̂ > 0 for all the leaf nodes). We depict the verdict boundary in this BaB tree, which is ⟨3, 3, 2, 3, 3, 2⟩, as illustrated by the blue line.
8
J. Ren et al.
Sk ip
Li
ne
ar
Se
arc
h
Recall the objective of -4.3 -4.3 BaB in §2.2. To verify a -1 -2.7 -1 problem, it needs to ex-2 0.3 -0.8 0.5 haustively check all the Verdict -2 0.3 -0.8 0.5 Boundary paths in a BaB tree, until it 0.3 0.1 0.2 0.1 0.3 0.1 0.2 0.1 finds that every path ends with a verified leaf node (in (a) BaB Tree. (b) Our idea. which case, the queue Q Fig. 3: Verdict boundary and our idea. used in Alg. 1 will be empty so it can return true in Line 5). As shown in Fig. 3a, this is equivalent to finding the verdict boundary in a BaB tree, because 1) the verdict boundary covers all the paths; 2) the verdict boundary signifies the shifts from unverified nodes to verified ones, and due to the monotonicity of p̂ in each path, the nodes succeeding the boundary point are all verified. Therefore, for verification, the objective of BaB can be deemed to be deciding the verdict boundary in the tree. Motivation and benefits for fast boundary mining. We first look at how existing BaB (Alg. 1) finds the verdict boundary. It essentially performs a linear search in each path, i.e., it checks each node one by one along a path, as visualized in Fig. 3a. Note that this way of checking is independent of how Q in Alg. 1 works. Specifically, regardless of whether Q is first-in-first-out or first-in-last-out, for a given path, the existing BaB checks the nodes one by one. On the other hand, due to the trend of p̂ in each path, we can treat each path as a nearly sorted array, in which each element (i.e., each node) has a value p̂, and consequently, the problem of deciding the boundary point for a given path can be translated to a search problem for the position of the first positive value in the array. Note that, to deal with such a problem, linear search, as classic BaB does, is often known as inefficient. Instead, thanks to nearly monotonic trend of p̂, we do not need to check the node one by one. For example, Fig. 3b shows how to locate the boundary point by skipping the second node. We can devise more efficient approaches that reduce the number of node visits, hence significantly reducing the number of calls to approximate verifiers for bounds propagation.
4
Our Proposed Approaches
Taking the insights from §3, in this section, we propose two novel approaches that tackle the problem of deciding the verdict boundary in a BaB tree. 4.1
Exponential Search Approach for Verdict Boundaries
As mentioned in §3.2, the BaB-based verification can be considered as a problem that aims to find the verdict boundary, and in each path of a BaB tree, finding the boundary point involves a search problem for the position of a specific value 0 in a nearly ascending array. While existing BaB adopts linear search (see Fig. 3a), there are some other methods, such as exponential search [1], that are known to be more efficient than linear search in handling this problem. In this section, we present our proposed approach based on exponential search.
Mining Verdict Boundaries for Neural Network Verification
9
Algorithm 2 Our proposed exponential search approach Require: A neural network N with K neurons, an input specification Φ, an output specification Ψ, an approximated verifier AppVer(·), a ReLU selection heuristic H(·). Ensure: A verdict ∈ {true, false}. 1: Q ← {⊤} ▷ initialize Q with the original problem 2: ExpSearchBaB(Q) ▷ start the process 3: function ExpSearchBaB(Q) 4: if Empty(Q) then 5: return true ▷ manage to verify the problem 6: Γ ← Pop(Q) 7: il ← |Γ|, ir ← K ▷ initialize search range [il , ir ] 8: for l ∈ {0, 20 , . . . , 2⌊log (K−|Γ|)⌋ , K−|Γ|} do ▷ exponentially select nodes 9: p̂ ← AppVer(N, Φ, Ψ, Γ ∧ a0 ∧ . . . ∧ al ) where a0 ≡ ⊤, aj ∈ H(Γ ∧ a0 ∧ . . . ∧ aj−1 ) for j ∈ {1, . . . , l} 10: if p̂(< 0 then ▷ the subproblem is not verified return false if l+|Γ| = K 11: ▷ update il or return false il ← l+|Γ| otherwise 12: else 13: ir ← l+|Γ| ▷ update ir 14: break ▷ the range [il , ir ] is decided 15: ir ← BinarySearch(Γ, il , ir ) 16: for k ∈ {1, . . . , ir −|Γ|} do 17: Q ← Q ∪ {Γ ∧ a0 ∧ . . . ∧ ak−1 ∧ ¬ak } ▷ add unsolved paths to Q 18: return ExpSearchBaB(Q) ▷ recursive call with updated Q 19: function BinarySearch(Γ, il , ir ) 20: while ir − il > 1 do r 21: m ← ⌈ il +i ⌉ 2 22: p̂ ← AppVer(N, Φ, Ψ, Γ ∧ a0 ∧ . . . ∧ am−|Γ| ) ( il ← m if p̂ < 0 23: ir ← m otherwise 24: return ir
▷ take the mid of [il , ir ] ▷ obtain p̂ ▷ update il or ir accordingly
Exponential search, originally proposed in [1], is an algorithm that tackles the search problem in a sorted array. Compared to other search methods, such as binary search, it can outperform if the search target is relatively close to the beginning of the array. In our case, as neural networks typically consist of a large number of neurons, as long as the position of the boundary point is not too deep in a path, this method should be suited for our purpose. Algorithm details. Our proposed algorithm is presented in Alg. 2. It consists of two phases to decide the boundary point for each path: first, it identifies a range that contains the boundary point, by progressively sliding and expanding the range whose size increases exponentially; given such a range, it searches for the exact position of the boundary point by a binary search.
10
J. Ren et al.
Alg. 2 uses a queue Q to maintain the paths to be checked, which is initialized to contain Γ only, i.e., the original verification problem. The algorithm starts with a call of the function ExpSearchBaB with the initial Q (Line 2), and then in function ExpSearchBaB, with a ReLU specification Γ (i.e., a node) popped from Q (Line 6), it goes through the two phases of exponential search: • The first phase (Line 7 – Line 14) aims to identify a range [il , ir ] that contains the boundary point, which is initialized to be [|Γ|, K] in Line 7. To achieve high efficiency, unlike existing BaB that checks the nodes sequentially, it skips nodes with an exponentially increasing step size (Line 8). For each selected node Γ ∧ a0 ∧ a1 ∧ . . . ∧ al , it applies AppVer to obtain p̂ of the node (Line 9): if p̂ < 0 (i.e., the node is not verified), the lower bound il of the range is updated to be the current l (Line 11) and the search proceeds to the next l; otherwise, the upper bound ir is updated (Line 13), and this phase can be terminated (Line 14), because at this point, il identifies an unverified node and ir identifies a verified node, so the boundary point must be within [il , ir ]. • The second phase (Line 19 – Line 24) performs a binary search to exactly find the boundary point. Here, it iteratively checks the node in the middle of [il , ir ] (Line 21, 22) to obtain p̂, and updates il or ir according to the sign of p̂ to further shrink the range. On the termination of this phase, the node identified by il is unverified and the node identified by ir is verified; by Def. 6, ir can be returned as the boundary point for this path. After finding the boundary point ir , Alg. 2 pushes to Q all the unsolved paths resulted from the path Γ ∧ a0 ∧ a1 ∧ . . . ∧ air −|Γ| that has just been checked. One such unsolved path can be obtained by concatenating a prefix of the checked path with the negation of the last node, i.e., Γ ∧ a0 ∧ a1 ∧ . . . ∧ ak−1 ∧ ¬ak , for each k ∈ {1, . . . , ir − |Γ|}, in Line 17. Then, Alg. 2 recursively calls function ExpSearchBaB with the updated Q to process the subsequent unsolved paths. Alg. 2 can be terminated if Q is empty (Line 4), in which case the verdict boundary for each path of the BaB tree has been found, and so Alg. 2 can return true, signifying that the problem can be verified (Line 5). 4.2
Gradient-Based Approach for Verdict Boundaries
The exponential search approach in §4.1 allows skipping boundary-unrelated subproblems (hence avoid redundant calling to approximated verifiers) compared to linear search in classic BaB, however, it may still require a large number of visits of tree nodes before identifying the range that contains the boundary point, as it ignores the quantitative information about the change of p̂ of the nodes in a path. To bridge this gap, we propose a gradient-based search approach that leverages quantitative information about the ascending rate of nodes, allowing us to identify the verdict boundary with much fewer node visits. In this approach, by treating the absolute value |p̂| of p̂ of each node in a path as the objective function, we can transform the problem of deciding the verdict boundary in that path, into an optimization problem that minimizes |p̂|. Specifically, the optimization problem aims to identify the local minimum, namely, the position of the node for which |p̂| = 0.
Mining Verdict Boundaries for Neural Network Verification
11
To solve this problem, our approach iteratively estimates the position of the local minimum, by leveraging the “gradient” of the nodes in the path. The gradient can be estimated by exploiting the quantitative p̂ of the nodes that have been vis- (a) Estimate boundary (b) Update il when p̂ < 0 at estimated t. ited, i.e., given two nodes Γ1 and by observed nodes. Fig. 4: Gradient-based search approach. Γ2 with verifier assessments p̂1 p̂2 −p̂1 and p̂2 respectively, we can estimate the gradient by |Γ2 |−|Γ1 | . While this may not be precise and so our estimated local optimum can be deviated, we continue our search using the updated gradient information obtained by checking the node in the estimated position, until we find the verdict boundary. Algorithm details. Our proposed algorithm is presented in Alg. 3. Similarly to exponential search, Alg. 3 also consists of two phases to identify the boundary point. First, it identifies a range [il , ir ] that contains the boundary point by leveraging the gradient information; after having such a range, the second phase applies binary search to exactly locate the boundary point, similarly to Alg. 2. Alg. 3 uses a queue Q to maintain the paths to be checked. At the beginning of Alg. 3, it checks the original problem by applying AppVer and obtains its verifier assessment p̂∗ (Line 1). If this node is not verified, Alg. 3 pushes its children into Q (Line 5), and then calls GradSearchBaB with Q to search for the verdict boundary in the BaB tree (Line 6). The function GradSearchBaB includes the two phases of searching for the boundary point in a specific path. We first elaborate on the first phase (Line 11 – Line 21). This phase involves two while loops which iteratively update the upper bound ir and the lower bound il of the range [il , ir ] that contains the boundary point, by iteratively checking the position where p̂ is estimated to be 0. This process is visualized in Fig. 4, and described as follows: • In the first loop, t is the estimated position ∗of boundary point, which is computed by taking the minimum between ⌈ p̂t·∗p̂−p̂ ⌉ and K (Line 15), as shown in Fig. 4a. This loop applies AppVer to check the p̂ of the node at t (Line 16), and if p̂ is negative, it updates the lower bound il to be t (Line 14), and reestimates t based on the updated p̂ of the node at t (Line 15). The loop is terminated if p̂ is positive at the estimated position, signifying that il cannot be further refined to a greater position where p̂ is still negative; • The second loop is similar to the first loop, but the purpose is to refine ir to be a smaller position where p̂ is still positive. It uses a similar method to estimate ∗ the boundary point position t, by taking the maximum between ⌈ p̂t·∗p̂−p̂ ⌉ and il (Line 19), as shown in Fig. 4b. This loop applies AppVer to check the p̂ of the node at t (Line 20), and if p̂ is positive, it updates the upper bound ir to be t (Line 18), and re-estimates t based on the updated p̂ of the node at t (Line 19). The loop is terminated if p̂ is negative at the estimated position, signifying that ir cannot be further refined to be a smaller position.
12
J. Ren et al.
Algorithm 3 Our proposed gradient-based search approach Require: A neural network N with K neurons, an input specification Φ, an output specification Ψ, an approximated verifier AppVer(·), a ReLU selection heuristic H(·). Ensure: A verdict ∈ {true, false}. 1: p̂∗ ← AppVer(N, Φ, Ψ, ⊤) ▷ check the original problem and record p̂∗ 2: if p̂ > 0 then 3: return true ▷ verify the problem if p̂ > 0 4: else 5: Q ← Q ∪ {a}, for a ∈ H(⊤) ▷ add children to Q 6: GradSearchBaB(Q) ▷ start the search process 7: function GradSearchBaB(Q) 8: if Empty(Q) then 9: return true 10: Γ ← Pop(Q) 11: il ← |Γ|, ir ← K, t ← |Γ| 12: p̂ ← AppVer(N, Φ, Ψ, Γ) 13: while ( p̂ < 0 do return false if t = K 14: il ← t otherwise t·p̂∗ 15: t ← min ⌈ p̂∗ −p̂ ⌉, K 16:
17: 18: 19: 20: 21: 22: 23: 24: 25:
▷ manage to verify the problem ▷ initialize [il , ir ] and estimation t ▷ check the node Γ ▷ update il or return false ▷ estimate t based on updated information
p̂ ← AppVer(N, Φ, Ψ, Γ ∧ a0 ∧ . . . ∧ at−|Γ| ) ▷ check node at t where a0 ≡ ⊤, aj ∈ H(Γ ∧ a0 ∧ . . . ∧ aj−1 ), for j ∈ {1, . . . , t − |Γ|} while p̂ > 0 do ir ← t ▷ update ir if p̂ > 0 at t t·p̂∗ t ← max ⌈ p̂∗ −p̂ ⌉, il ▷ estimate t based on updated information p̂ ← AppVer(N, Φ, Ψ, Γ ∧ a0 ∧ . . . ∧ at−|Γ| ) il ← t ir ← BinarySearch(Γ, il , ir ) for k ∈ {1, . . . , ir −|Γ|} do Q ← Q ∪ {Γ ∧ a0 ∧ . . . ∧ ak−1 ∧ ¬ak } return GradSearchBaB(Q)
▷ check node t ▷ update il if t < il ▷ collect unsolved paths ▷ recursive call with updated Q
Note that, during the loop, it is possible to encounter the situation that p̂ does not monotonically increase as discussed in §3.1; in this case, as we show that such monotonicity often happens locally, we just skip such a non-monotonic node and use the next one. After the loop, if t is greater than il , il will be updated to be t to further shrink the range (Line 21). This range [il , ir ] then serves as the inputs of the binary search (Line 19) of Alg. 2 in the second phase to exactly locate the boundary point. While the second phase (Line 22) of Alg. 3 also uses binary search, its input range [il , ir ] can be much narrower than in Alg. 2. This is because the exponential search in Alg. 2 expands the range exponentially, whereas our loops can produce
Mining Verdict Boundaries for Neural Network Verification
13
a relatively smaller range. The binary search in Alg. 3 can be more efficient to locate the boundary.
5
Experimental Evaluation
We present the experimental setup, results, and analysis. Our implementation and data are available at [26]. Benchmarks. We adopt widelyTable 2: Benchmark details. used benchmarks from the neural #Problem Network Architecture Dataset #ReLU network verification community [3] 100 MNISTL2 2 × 256 linear MNIST 512 and five neural network models 100 MNISTL4 4 × 256 linear MNIST 1024 relevant to two common datasets 100 OVAL21BASE 2 Conv, 2 linear CIFAR-10 3172 100 OVAL21WIDE 2 Conv, 2 linear CIFAR-10 6244 MNIST and CIFAR-10 adopted in 100 OVAL21DEEP 4 Conv, 2 linear CIFAR-10 6756 VNN-COMP series [3]. • For MNIST, we use two fully connected networks, MNISTL2 and MNISTL4 . • For CIFAR-10, we adopt OVAL21BASE , OVAL21WIDE and OVAL21DEEP . We call each pair that consists of a neural network and a specification to be a verification problem. As shown in Table 2, we have a total of 500 problems that concern the five neural networks and different specifications. Baseline. To assess BMiner, we compare with existing tools as our baselines: • αβ-Crown [34] is the winner of VNN-COMP [3] that adopts classic BaB with an approximated verifier that is not monotonic under problem splitting; • Oliva [41] is a meta-heuristic BaB falsifier that aggressively guides the tree search toward rejecting unsafe verification instances as fast as possible. Extension of ReLU Selection Strategy. Our approaches adopt the same ReLU selection strategy as baselines to ensure the fairness of comparison. As the ReLU selection strategy is not the primary focus of this work, we make an extension of existing methods to integrate into our framework. Commonly used ReLU selection strategies, such as DeepSplit [14], BaBSR [5] and FSB [8], generally follow a two-step procedure: (1) each neuron is assigned a score based on its potential abstraction–refinement gain and its estimated impact on the final network output (2) the neuron with the highest score (Top-1) is selected for splitting. In our approach, we adopt and extend the state-of-the-art ReLU selection strategy [8]. While Step (1) remains unchanged, we extend Step (2) by selecting the Top-k neurons to split simultaneously, where k corresponds to the number of neurons skipped by our method. This extension allows our verification approach to retain compatibility with existing selection heuristics while improving efficiency through parallel refinement of multiple high-impact neurons. This extension further inspires the development of novel ReLU selection heuristics incorporating abstraction–refinement prediction mechanisms, which could better complement our BMiner. As designing such strategies is nontrivial, we leave this as future work. Evaluation metrics. In our experiments, to compare the performances of different approaches, we apply both the baseline approaches and our proposed
14
J. Ren et al.
Table 4: RQ1 – Average, best, and worst-case time comparison w.r.t. αβ-Crown. Model
BMinerE BMinerG AVG BC WC AVG BC WC MNISTL2 -4.5% -12.9% +5.6% -29.2% -44.7% +13.0% MNISTL4 -4.7% -11.5% +5.1% -17.9% -34.2% +16.7% OVAL21BASE -4.0% -13.8% +4.1% -17.9% -35.8% +8.4% OVAL21DEEP -3.9% -13.2% +5.8% -18.1% -34.5% +8.4% OVAL21WIDE -4.5% -10.5% +3.0% -17.0% -26.9% +5.8%
approaches BMinerE , BMinerG , to all the verification problems. For each problem, we set 1,000 seconds as the timeout. We adopt the following metrics: • Verification result: It indicates whether an approach can solve a problem (i.e., it returns either true or false for the problem) within the given time budget; • Time cost: In this case, if an approach successfully solves a problem, we record the time taken as an indicator of its efficiency. Experiment environment. The experiments were conducted on AWS EC2 instance with 32GB memory and 8-core CPUs. 5.1
Evaluation Results
RQ1 Are our proposed approaches more efficient than the baseline approach? Comparison with baselines. Ta- Table 3: RQ1 – Performance comparison ble 3 reports the number of verifica- on certified (C) and falsified (F) counts. tion instances. For certified instances Oliva αβ-Crown BMinerE BMinerG (C), αβ-Crown serves as a strong base- Model C F C F C F C F line, certifying more instances than MNISTL2 72 7 89 4 89 4 89 7 Oliva. Our approaches, BMinerE and MNISTL4 39 10 51 2 51 2 51 2 10 83 0 85 1 85 1 BASE 69 BMinerG , consistently surpass Oliva, OVAL21 OVAL21DEEP 53 8 71 0 71 0 76 1 certifying more instances than it, OVAL21WIDE 51 9 70 1 70 1 72 1 while matching or slightly exceeding αβ-Crown. This demonstrates the strengths of our approaches. On the other hand, Oliva maintains an advantage in falsification (F), consistently identifying more counterexamples due to its design, which focuses on rapid falsification rather than exhaustive proof. Efficiency comparison relative to αβ-Crown. To further highlight the benefits of our approaches, Table 4 reports the relative change in verification time compared to αβ-Crown. Notably, BMinerG achieves substantial time savings, with average reductions of 17.0%–29.2% and up to 44.7% in best-case scenarios, thanks to the gradient-based estimation strategy that skips redundant computations. BMinerE provides a smaller but consistent average improvement of about 4%. In worst-case scenarios, the aggressive search strategy can introduce overhead (up to 16.7%), caused by backtracking when the initial estimation overshoots the verdict boundary (Lines 18–20 in Alg. 3). Overall, these results demonstrate that, compared to αβ-Crown, our approaches bring an evident improvement in terms of verification efficiency.
Mining Verdict Boundaries for Neural Network Verification
15
Impact of non-monotonicity. Since non-monotonicity does not affect the soundness of our approach, we mainly demonstrate our hypothesis that it does not hinder our performance. We present an analysis of the performance comparison of our approaches for monotonic paths and non-monotonic paths, by which we can see that the impact of non-monotonicity is not significant.
(a) MNISTL4
(b) OVAL21BASE
(c) OVAL21WIDE
(d) OVAL21DEEP
Fig. 5: Comparison of time ratios between monotonic and non-monotonic paths for BMinerE and BMinerG .
To evaluate the impact of non-monotonicity on the efficiency of our verification strategies, we compare the runtime performance between monotonic and non-monotonic paths across different benchmark networks. We exclude MNISTL2 from the results because it does not generate a meaningful number of nonmonotonic paths. Specifically, we recorded the execution time and monotonicity status of all analyzed paths. For both monotonic and non-monotonic paths, we computed the time reduction ratio, defined as the running time of linear search divided by the running time of our proposed methods BMinerE and BMinerG , respectively. We further conduct experiments on MNIST and OVAL21 models. The distribution of time ratio (for comparison, we compared each approach with a naive baseline that explores a BaB tree by depth first search (DFS)) in Fig. 5 shows the consistency between monotonic and non-monotonic paths: – Analysis of BMinerE : Comparing on MNISTL4 and OVAL21BASE in Fig. 5a and Fig. 5b, both monotonic and non-monotonic groups exhibit a similar median time ratio, indicating that BMinerE achieves consistent speedup over DFS regardless of path monotonicity. The interquartile range and outliers are slightly smaller in the non-monotonic group, further supporting the robustness of BMinerE in handling non-monotonic paths. – Analysis of BMinerG : Comparing on OVAL21WIDE and OVAL21DEEP in Fig. 5c and Fig. 5d, the median time ratio for both groups is around 1.0, indicating that BMinerG consistently improves efficiency over DFS across
Skipped Visits
16
J. Ren et al.
400
Skipped Visits Boundary Position
600
Skipped Visits Boundary Position
0
23 28 28232425 2423 22 23
Time (sec)
200
2524 23282824 0 1 2 10 10
11 119 9
10 9 10 9 10 9
100
400
200 0 101 102
800
3628 3327
Time (sec)
103
Skipped Visits 200 Boundary Position 1 2 10 10
Time (sec)
Fig. 6: RQ2 – Our performance advantage throughout verification processes. both path types. However, the monotonic group exhibits a wider interquartile range and more high-value outliers (some exceeding 5), whereas the non-monotonic group shows a narrower spread with almost no extreme outliers. This suggests that non-monotonicity does not hinder—and may even contribute to—more stable and predictable performance under BMinerG . In conclusion, this supports our hypothesis that the non-monotonicity of certain paths has little impact on the effectiveness of our techniques. RQ2 Which factors affect the performance of our approaches? We look into the verification processes of our two approaches to understand the reasons behind performance advantages. To that end, we select 3 problems, and show how our performance advantages (in terms of the number of skipped node visits, compared to αβ-Crown) evolve throughout a verification process. Our experimental results are shown in Fig. 6. In each sub-figure, y-axis denotes the number of skipped nodes, compared to the hypothetical number of visits by αβ-Crown for covering the same tree nodes. By the results, in the problems where BMiner outperforms αβ-Crown, the number of skipped node visits keeps increasing in most cases. This result implies that, our strategies are indeed helpful to save subproblem solving/visits in verification. Moreover, we also annotate the position of a boundary point in each path, i.e., the search goal of our approaches. By observing this, we find that our performance advantages stem from the ability of our approach in handling long paths, because when such a long path occurs, the improvement rate will often increase. Over the verification process, there are many paths where the boundary point is small, for which the naive linear search in BaB-baseline can also work well; for this reason, our improvement rate can decrease as the verification process evolves. This can also explain when our approaches cannot perform well, as in the last sub-figure: it happens when there is almost no long path in the BaB tree. RQ3 What causes performance differences between BMinerE and BMinerG ? In this RQ, we compare the search strategies used in BMinerE and BMinerG to locate the boundary point in a path. We select two verification problems for which BMinerG outperforms BMinerE , and we look into the number of node visits consumed by BMinerE and BMinerG for each path during each verification process, to understand the performance advantage of BMinerG . Table 5 shows the total number of visits for paths with different lengths. We find that BMinerG has advantages in handling long paths. For example, in the first problem, for paths with length 16-40, BMinerG takes an average
Mining Verdict Boundaries for Neural Network Verification
17
Table 5: RQ3 – Node visits by BMinerE and BMinerG . # denotes the number of paths with a specific length. Each value shows the average number of visits. len. #
BMinerE
BMinerG
Ph1 Ph2 Total Ph1 Ph2 Total
0-7 70 4.2 1.4 5.6 5.2 1.9 8-15 26 6.0 3.0 9.0 4.5 2.3 16-40 8 7.1 4.1 11.2 3.3 3.0
7.1 6.8 6.3
len.
#
BMinerE
BMinerG
Ph1 Ph2 Total Ph1 Ph2 Total
0-7 1151 3.2 0.5 3.7 5.5 0.6 8-15 441 5.9 2.9 8.8 6.6 0.8 16-40 367 7.0 4.0 11.0 5.3 0.8
6.1 7.4 6.1
of 6.3 visits to locate the boundary, while BMinerE requires 11.2 visits. These results demonstrate the usefulness of our estimation strategy in BMinerG , and explain why BMinerG can outperform BMinerE . Moreover, by observing the detailed node visits for Phase 1 and Phase 2 in each approach, BMinerE in Phase 1 can take fewer visits for shorter paths than BMinerG , but it takes more visits for longer paths. In Phase 2, BMinerG generally requires fewer visits than BMinerE , particularly on long paths (e.g., 16–40 in the second problem), as our effective boundary estimation yields a much narrower search range.
6
Related Work
Neural network verification has been extensively studied [2, 7, 9, 16–20, 24, 25, 27–30, 35–40, 43, 44]. Notably, the combined use of BaB [5] with approximated methods is both efficient and complete, and has been adopted by many advanced tools such as αβ-Crown [34]. There has been a rich body of literature [6, 8, 11, 14, 42] that aims to improve BaB, but mostly they focus on issues such as splitting strategy [33], selection of ReLU functions [8,14], counterexample-guided falsification [10, 13, 41]. In contrast to the classical one-by-one processing, our contribution is a new per-path formulation that jointly splits multiple activation functions to speed up BaB-based certification-centric verification.
7
Conclusion and Future Work
This paper introduces BMiner, which reformulates BaB-based verification as verdict boundary mining via exponential and gradient-based searches. BMiner exploits the near-monotonic nature of verification assessments to skip redundant subproblems computations, which outperforms state-of-the-art verification approaches and reduces the average verification time by 17% to 30%, with a maximum time reduction of 44.7%. As future work, we aim to further improve the efficiency by considering GPU parallelization, meta-heuristic falsification, and the order of checking different paths in verdict boundary mining, which can affect the efficiency of our approaches.
Acknowledgements We thank the anonymous reviewers for their comments and suggestions. This research is supported by the Australian Research Grant DP250101396, the JST BOOST Grant No. JPMJBY24D7 and the JSPS Grant No. JP25K21179.
18
J. Ren et al.
References 1. Bentley, J.L., Yao, A.C.C.: An almost optimal algorithm for unbounded searching. Information processing letters 5(SLAC-PUB-1679) (1976). https://doi.org/10. 1016/0020-0190(76)90071-5 2. Boudardara, F., Boussif, A., Meyer, P.J., Ghazel, M.: A review of abstraction methods toward verifying neural networks. ACM Transactions on Embedded Computing Systems 23(4), 1–19 (2024). https://doi.org/10.1145/3617508 3. Brix, C., Bak, S., Liu, C., Johnson, T.T.: 4th int. verification of neural networks competition (vnn-comp 2023): Summary and results. arXiv preprint arXiv:2312.16760 (2023). https://doi.org/10.48550/arXiv.2312.16760 4. Bunel, R., De Palma, A., Desmaison, A., Dvijotham, K., Kohli, P., Torr, P., Kumar, M.P.: Lagrangian decomposition for neural network verification. In: Conference on Uncertainty in Artificial Intelligence. pp. 370–379. PMLR (2020), http://proceedings.mlr.press/v124/bunel20a.html 5. Bunel, R., Mudigonda, P., Turkaslan, I., Torr, P., Lu, J., Kohli, P.: Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research 21(2020) (2020), https://jmlr.org/papers/v21/19-468.html 6. Cohen, E., Elboher, Y.Y., Barrett, C., Katz, G.: Tighter abstract queries in neural network verification. arXiv preprint arXiv:2210.12871 (2022). https://doi.org/ 10.48550/arXiv.2210.12871 7. Dalrymple, D., Skalse, J., Bengio, Y., Russell, S., Tegmark, M., Seshia, S., Omohundro, S., Szegedy, C., Goldhaber, B., Ammann, N., et al.: Towards guaranteed safe ai: A framework for ensuring robust and reliable ai systems. arXiv preprint arXiv:2405.06624 (2024). https://doi.org/10.48550/arXiv.2405.06624 8. De Palma, A., Bunel, R., Desmaison, A., Dvijotham, K., Kohli, P., Torr, P.H., Kumar, M.P.: Improved branch and bound for neural network verification via lagrangian decomposition. arXiv preprint arXiv:2104.06718 (2021). https://doi. org/10.48550/arXiv.2104.06718 9. Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: Automated Technology for Verification and Analysis: 15th Int. Symp., ATVA 2017, Proceedings 15. pp. 269–286. Springer (Oct 2017). https://doi.org/10. 1007/978-3-319-68167-2_19 10. Fukuda, K., Zhang, G., Zhang, Z., Sui, Y., Zhao, J.: Adaptive branch-and-bound tree exploration for neural network verification. In: 2025 Design, Automation & Test in Europe Conference (DATE). pp. 1–7 (2025). https://doi.org/10.23919/ DATE64628.2025.10992738 11. Geng, C., Le, N., Xu, X., Wang, Z., Gurfinkel, A., Si, X.: Towards reliable neural specifications. In: International Conference on Machine Learning. pp. 11196–11212. PMLR (2023), https://proceedings.mlr.press/v202/geng23a.html 12. Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. In: 3rd Int. Conf. on Learning Representations (ICLR’15). Int. Conf. on Learning Representations, ICLR, San Diego, CA, United States (2015). https: //doi.org/10.48550/arXiv.1412.6572 13. Guo, X., Wan, W., Zhang, Z., Zhang, M., Song, F., Wen, X.: Eager falsification for accelerating robustness verification of deep neural networks. In: 2021 IEEE 32nd Int. Symp. on Software Reliability Engineering (ISSRE). pp. 345–356. IEEE (2021). https://doi.org/10.1109/ISSRE52982.2021.00044 14. Henriksen, P., Lomuscio, A.: Deepsplit: An efficient splitting method for neural network verification via indirect effect analysis. In: IJCAI. pp. 2549–2555 (2021). https://doi.org/10.24963/ijcai.2021/351
Mining Verdict Boundaries for Neural Network Verification
19
15. Henzinger, T.A., Lukina, A., Schilling, C.: Outside the box: Abstraction-based monitoring of neural networks. In: ECAI 2020, pp. 2433–2440. IOS Press (2020). https://doi.org/10.48550/arXiv.1911.09032 16. Huang, P., Wu, H., Yang, Y., Daukantas, I., Wu, M., Zhang, Y., Barrett, C.: Towards efficient verification of quantized neural networks. In: Proceedings of the AAAI Conference on Artificial Intelligence. vol. 38, pp. 21152–21160 (2024). https: //doi.org/10.1609/aaai.v38i19.30108 17. Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Computer Aided Verification: 29th Int. Conf., CAV 2017, Part I 30. pp. 3–29. Springer (July 2017). https://doi.org/10.1007/978-3-319-63387-9_1 18. Isac, O., Zohar, Y., Barrett, C., Katz, G.: Dnn verification, reachability, and the exponential function problem. arXiv preprint arXiv:2305.06064 (2023). https:// doi.org/10.48550/arXiv.2305.06064 19. Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kunčak, V. (eds.) Computer Aided Verification. pp. 97–117. Springer Int. Publishing (2017). https://doi.org/10.1007/978-3-319-63387-9_5 20. Liu, C., Arnon, T., Lazarus, C., Strong, C., Barrett, C., Kochenderfer, M.J., et al.: Algorithms for verifying deep neural networks. Foundations and Trends® in Optimization 4(3-4), 244–404 (2021). https://doi.org/10.1561/2400000035 21. Lukina, A., Schilling, C., Henzinger, T.A.: Into the unknown: Active monitoring of neural networks. In: International Conference on Runtime Verification. pp. 42–61. Springer (2021). https://doi.org/10.1007/978-3-030-88494-9_3 22. Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. In: 6th Int. Conf. on Learning Representations (ICLR’18). Vancouver, Canada (2018). https://doi.org/10.48550/arXiv. 1706.06083 23. Mandal, U., Amir, G., Wu, H., Daukantas, I., Newell, F.L., Ravaioli, U.J., Meng, B., Durling, M., Ganai, M., Shim, T., et al.: Formally verifying deep reinforcement learning controllers with lyapunov barrier certificates. arXiv preprint arXiv:2405.14058 (2024). https://doi.org/10.48550/arXiv.2405.14058 24. Mitra, S., Păsăreanu, C., Prabhakar, P., Seshia, S.A., Mangal, R., Li, Y., Watson, C., Gopinath, D., Yu, H.: Formal verification techniques for vision-based autonomous systems–a survey. In: Principles of Verification: Cycling the Probabilistic Landscape: Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part III, pp. 89–108. Springer (2024). https://doi.org/10.1007/ 978-3-031-75778-5_5 25. Ostrovsky, M., Barrett, C., Katz, G.: An abstraction-refinement approach to verifying convolutional neural networks. In: International Symposium on Automated Technology for Verification and Analysis. pp. 391–396. Springer (2022). https://doi.org/10.1007/978-3-031-19992-9_25 26. Ren, J.: Artifact: "mining verdict boundaries for neural network verification". GitHub (2026), https://github.com/jiawei-95/BMiner 27. Shi, Z., Wang, Y., Zhang, H., Kolter, J.Z., Hsieh, C.J.: Efficiently computing local lipschitz constants of neural networks via bound propagation. Advances in Neural Information Processing Systems 35, 2350– 2364 (2022), http://papers.nips.cc/paper_files/paper/2022/hash/ 0ff54b4ec4f70b3ae12c8621ca8a49f4-Abstract-Conference.html 28. Singh, G., Gehr, T., Mirman, M., Püschel, M., Vechev, M.: Fast and effective robustness certification. In: Advances in Neural Information Processing
20
J. Ren et al.
Systems. vol. 31 (2018), https://proceedings.neurips.cc/paper/2018/hash/ f2f446980d8e971ef3da97af089481c3-Abstract.html 29. Singh, G., Gehr, T., Püschel, M., Vechev, M.: An abstract domain for certifying neural networks. ACM on Programming Languages 3(POPL), 1–30 (2019). https: //doi.org/10.1145/3290354 30. Strong, C.A., Wu, H., Zeljić, A., Julian, K.D., Katz, G., Barrett, C., Kochenderfer, M.J.: Global optimization of objective functions represented by relu networks. Machine Learning 112(10), 3685–3712 (2023). https://doi.org/10.1007/ s10994-021-06050-2 31. Tjeng, V., Xiao, K.Y., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. In: Int. Conf. on Learning Representations (2018), https://openreview.net/forum?id=HyGIdiRqtm 32. Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Efficient formal safety analysis of neural networks. Advances in neural information processing systems 31 (2018), https://proceedings.neurips.cc/paper/2018/hash/ 2ecd2bd94734e5dd392d8678bc64cdab-Abstract.html 33. Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: 27th USENIX Security Symp. (USENIX Security 18). pp. 1599–1614 (2018), https://www.usenix.org/ conference/usenixsecurity18/presentation/wang-shiqi 34. Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S., Hsieh, C.J., Kolter, J.Z.: Betacrown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. Advances in Neural Information Processing Systems 34, 29909–29921 (2021), https://proceedings.neurips.cc/paper/2021/ hash/fac7fead96dafceaf80c1daffeae82a4-Abstract.html 35. Wei, D., Wu, H., Wu, M., Chen, P.Y., Barrett, C., Farchi, E.: Convex bounds on the softmax function with applications to robustness verification. In: International Conference on Artificial Intelligence and Statistics. pp. 6853–6878. PMLR (2023), https://proceedings.mlr.press/v206/wei23c.html 36. Wu, H., Isac, O., Zeljić, A., Tagomori, T., Daggitt, M., Kokke, W., Refaeli, I., Amir, G., Julian, K., Bassan, S., Huang, P., Lahav, O., Wu, M., Zhang, M., Komendantskaya, E., Katz, G., Barrett, C.: Marabou 2.0: A versatile formal analyzer of neural networks. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification. pp. 249–264. Springer Nature Switzerland, Cham (2024). https: //doi.org/10.1007/978-3-031-65630-9_13 37. Wu, H., Tagomori, T., Robey, A., Yang, F., Matni, N., Pappas, G., Hassani, H., Pasareanu, C., Barrett, C.: Toward certified robustness against real-world distribution shifts. In: 2023 IEEE Conference on Secure and Trustworthy Machine Learning (SaTML). pp. 537–553. IEEE (2023). https://doi.org/10.1109/SaTML54575. 2023.00042 38. Wu, M., Wu, H., Barrett, C.: Verix: Towards verified explainability of deep neural networks. Advances in Neural Information Processing Systems 36 (2024), http://papers.nips.cc/paper_files/paper/2023/hash/ 46907c2ff9fafd618095161d76461842-Abstract-Conference.html 39. Xie, X., Kersting, K., Neider, D.: Neuro-symbolic verification of deep neural networks. In: Raedt, L.D. (ed.) Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22. pp. 3622–3628. International Joint Conferences on Artificial Intelligence Organization (7 2022). https://doi.org/10. 24963/ijcai.2022/503, main Track
Mining Verdict Boundaries for Neural Network Verification
21
40. Zelazny, T., Wu, H., Barrett, C., Katz, G.: On optimizing back-substitution methods for neural network verification. In: 2022 Formal Methods in Computer-Aided Design (FMCAD). pp. 17–26. IEEE (2022). https://doi.org/10.34727/2022/ isbn.978-3-85448-053-2_7 41. Zhang, G., Fukuda, K., Zhang, Z., Bandara, H.D., Chen, S., Zhao, J., Sui, Y.: Efficient Neural Network Verification via Order Leading Exploration of Branchand-Bound Trees. In: 39th European Conference on Object-Oriented Programming (ECOOP 2025). vol. 333, pp. 36:1–36:29 (2025). https://doi.org/10.4230/ LIPIcs.ECOOP.2025.36 42. Zhang, H., Shinn, M., Gupta, A., Gurfinkel, A., Le, N., Narodytska, N.: Verification of recurrent neural networks for cognitive tasks via reachability analysis. In: ECAI 2020, pp. 1690–1697. IOS Press (2020). https://doi.org/10.3233/FAIA200281 43. Zhang, R., Sun, J.: Certified robust accuracy of neural networks are bounded due to bayes errors. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification. pp. 352–376. Springer Nature Switzerland, Cham (2024). https://doi.org/10. 1007/978-3-031-65630-9_18 44. Zhang, Y., Chen, G., Song, F., Sun, J., Dong, J.S.: Certified quantization strategy synthesis for neural networks. In: Formal Methods: 26th International Symposium, FM 2024, Milan, Italy, September 9–13, 2024, Proceedings, Part I. pp. 343–362. Springer-Verlag, Berlin, Heidelberg (2024). https://doi.org/10.1007/ 978-3-031-71162-6_18