Lookahead Branching for Neural Network Verification

1 Introduction

Deep neural networks (DNNs) have become state-of-the-art solutions in various domains [Sallab et al., 2017; Mnih et al., 2013; He et al., 2015]. To ensure the deployment of DNNbased systems in safety critical domains, there has been significant effort from the formal methods and machine learning communities on developing scalable formal verification techniques that can reason about the behaviors of a neural network [Katz et al., 2017; Singh et al., 2019; Zhang et al., 2018; Wang et al., 2021]. State-of-the-art complete neural network verifiers are based on branch-and-bound (BaB), which involves performing case splitting on non-linear activation functions (e.g., ReLU) and analyzing the cases using an incomplete verifier; if the analysis is inconclusive, further case splits are recursively performed.

The branching heuristic, the strategy to choose which case to split on, has a significant impact on verification efficiency. Ideally, the branching heuristic should lead to easier subproblems. Failing to do so, especially at the top of the search tree, can result in duplicated verification efforts and increased verification time. A number of branching heuristics have been developed for neural network verification [Katz et al., 2017; Wu et al., 2020; Bunel et al., 2020; De Palma et al., 2021;

Wu et al., 2022]. Most heuristics aim to make a decision quickly by leveraging local information (e.g., variable bounds) gathered during the solving process. This increases the risk of ineffective branching, as decisions are made without evaluating the long-term impact of splits. Recent heuristics have shown it is beneficial to spend more effort making a branching decision by simulating branching on candidate neurons and evaluating its effect [De Palma et al., 2021]. This approach has culminated in Filtered Smart Branching (FSB), the standard branching heuristic in recent work.

Motivated by the success of FSB, we systematically study a general branching strategy that spends significant effort making branching decisions. We adopt the terminology in formal methods and call this approach lookahead [Heule and van Maaren, 2009]. Lookahead involves simulating potential branching decisions by performing multiple splits to measure downstream effects. By analyzing the impact of each simulated branch, lookahead uses more information to make branching decisions. We present lookahead as a template algorithm with several tunable parameters such as the preselect strategy, lookahead depth, and evaluation metric that can be instantiated in a solver-specific manner. We discuss the choices for these parameters and how FSB can be viewed as a special instantiation of the lookahead procedure. In addition to informing the branching decision, lookahead might also discover new information, such as tightened variable bounds. We show this information can be used to derive valid lemmas and potentially prune the search space. We instantiate lookahead in two distinct BaB-verifiers, Marabou [Katz et al., 2019; Wu et al., 2024] and α-β-CROWN [Wang et al., 2021; Xu et al., 2020; Zhang et al., 2022a; Zhou et al., 2024], and demonstrate that lookahead can improve both tools.

An overview of the lookahead workflow is presented in Figure 1. At a given search state when branching is required, a set of split candidates is pre-selected and lookahead simulates branching on each candidate up to a certain depth. The outcome of each simulation is a score along with a number of tightened bounds, which might entail that certain unstable neurons are fixed to particular activation phases. In the end, lookahead outputs the next neuron to split on and a set of lemmas discovered during the lookahead simulations.

The rest of the paper is organized as follows: Section 2 reviews related work. Section 3 provides background on neural network verification. Section 4 presents the general lookahead approach and concrete instantiations in Marabou and α-β-CROWN. Section 5 provides an evaluation of lookahead branching, comparing it to existing heuristics in Marabou and α-β-CROWN. Finally, we conclude and discuss future directions in Section 6.

2 RelatedWork

Early efforts for complete verification of neural networks employed SMT and MILP solvers that enumerate activation patterns [Katz et al., 2017]. A unified BaB view of verification was presented by [Bunel et al., 2020]. State-of-the-art complete verification tools including the SMT-based solvers [Katz et al., 2019; Wu et al., 2024] and GPU-accelerated boundpropagation-based tools [Wang et al., 2021; Xu et al., 2020; Zhang et al., 2022a; Zhou et al., 2024; Shi et al., 2025] can be viewed as instantiations of BaB. Branching heuristics have a significant impact on the runtime of complete verification tools. BABSR introduced a "strong-branching" style score that solves a cheap surrogate relaxation for each candidate and became the default in many verifiers [Bunel et al., 2020]. FSB (Filtered Smart Branching) refines this idea by first filtering candidates with BaBSR and then re-running a tighter bound computation on the shortlist [De Palma et al., 2021]. There has also been work on using Graph Neural Networks to train a policy for selecting splitting neurons [Lu and Kumar, 2019], but such approaches require offline training and are typically tied to the distribution of training data, making them less directly comparable to general-purpose heuristics like ours. Our framework is complementary with learning-based heuristics, which could in principle be used as a preselect strategy within the lookahead template. Our work is inspired by lookahead search in SAT and SMT solvers [Heule and van Maaren, 2009] as well as MILP solvers [Glankwamdee and Linderoth, 2006], and we extend similar ideas to neural network verification.

3 Background

3.1 Neural Network Verification

For a trained deep neural network N : Rn → Rm with an input x ∈ Rn and output y = N(x) ∈ Rm, the general DNN verification problem is whether or not there exists an input x that produces an output y that satisfies a property ϕ(y). If there exists an input x that leads to an output y that satisfies the property ϕ(y), then the problem is satisfiable (SAT); otherwise it is unsatisfiable (UNSAT).

3.2 Bound Propagation

To refine the search space of a neural network verification problem, bound propagation [Singh et al., 2019] estimates activation ranges at each layer, defining upper and lower bounds for each neuron. The Rectified Linear Unit (ReLU) activation function is defined as ReLU(x) = max(0, x). A ReLU neuron is considered active if its lower bound is strictly greater than zero (z(l) > 0), meaning its output will always be its input. Conversely, a ReLU neuron is inactive if its upper bound is less than or equal to zero (z(l) ≤ 0), meaning its output will always be zero. Otherwise, the activation status is not yet known and the ReLU in unstable. If a ReLU's bounds can guarantee the neuron is always active or inactive, unnecessary computations can be eliminated. Through this iterative process, the bounds on neuron activations are progressively tightened, leading the solver closer to a solution.

3.3 Branch-and-bound

The branch-and-bound (BaB) framework, illustrated by Figure 2, is an efficient approach to neural network verification. BaB systematically tightens the bounds of a neural network by splitting on unstable ReLU neurons. When an unstable ReLU is split, the problem is turned into two problems, one where the ReLU is active and one where the ReLU is inactive. To verify with BaB, ReLU splits are repeatedly applied until each subproblem can be definitively classified as either satisfying the property (SAT) or not satisfying it (UNSAT).

The choice of ReLU to split on is imperative for the efficiency of BaB, as it determines how fast a solver converges to a solution; well-selected splits make significantly more progress to a solution than poorly-chosen splits. Thus, branching heuristics are essential to efficient verification.

3.4 Branching Heuristics

Several branching heuristics have been developed for BaBbased neural network verification. BABSR is a deterministic heuristic that computes a surrogate relaxation of each neuron with the upper and lower bounds, and the biases of previous layers [2020]. The unstable neuron with the highest score is then branched on. PSEUDO-IMPACT BRANCHING is a branching heuristic specific to Marabou. It estimates the impact a ReLU has on the Sum-of-Infeasibilities (SoI) of the network, calculated during Marabou's DeepSoI procedure [Wu et al., 2022]. The ReLU with the greatest estimated impact on the SoI is branched on. Pseudo-impact is presently the state-of-the-art heuristic implemented in Marabou. FSB pre-selects candidate ReLUs with BaBSR scores, and simulates one level of branching on each candidate before making a branching decision, and can be seen as a special instantiation of lookahead branching. FSB is presently the state-ofthe-art heuristic implemented in α-β-CROWN. We will discuss how lookahead extends FSB in section 4.

4 Methodology

In this section, we first present lookahead as a template algorithm and discuss its properties. We then discuss concrete strategies for instantiating the lookahead procedure. The algorithm begins by identifying a set of unstable neurons to simulate splits on. Given that performing a lookahead simulation on every unstable ReLU is computationally expensive, a preselect strategy is employed to shrink the candidate set. The preselect strategy differs based on implementation as detailed in Section 4.1.

For each preselected candidate, the SIMULATESPLIT subroutine simulates a case split on the neuron, creating one branch for each activation phase. For the ReLU activation function, there would be two phases (active and inactive). The algorithm then recursively explores the next level of the search tree by selecting another neuron to split on, using the BASESELECT heuristic. This process continues until a specified lookahead depth (d) is reached. The goal of performing additional splits is to explore the cascading effects of each candidate split. After each split is simulated, the solver performs bound propagation. When the lookahead depth is

Algorithm 1 Lookahead Branching

• 1: Input: Set of unstable neurons N at the current search level 2: Output: ⟨n∗ ,L, U⟩ where n∗ is the neuron to split, L and U are sound lower and upper bounds 3: Parameters: lookahead depth k, preselect strategy P, heuristic B, scoring function E, aggregate strategy C 4: N ′ ← P(N); agScores ← {}; L, U ← [ ], [ ] 5: for each n ∈ N ′ do 6: scores′ , ℓ, u ←CaseSplit(n, k,N \ {n}) 7: agScores[n] ← C(scores′ ); L.append(ℓ); U .append(u) 8: end for 9: return argmax(agScores), 10: elementwise-max(L), elementwise-min(U) 11: Procedure CaseSplit(n, d,N) 12: if d = 0 then 13: score, ℓ, u ←E(); return [score], ℓ, u 14: else 15: storeSolverState(); scores,L,U ← [ ], [ ], [ ] 16: for each p ∈ phases(n) do 17: applySplit(p); propagateBounds() 18: if d = 1 then 19: n′ ← B(N) 20: else 21: n′ ← nil 22: end if 23: scores′ , ℓ, u ← CaseSplit(n′ , d - 1, N \ {n′ }) 24: scores ← scores :: scores′ ; L.append(ℓ); U.append(u); restoreSolverState() 25: end for 26: return scores, 27: elementwise-min(L), elementwise-max(U) 28: end if

reached, the EVALUATESTATE function is called to evaluate the current solver state and collect the current variable bounds. Importantly, the solver state is saved and restored after each simulated split to ensure that the lookahead simulation does not interfere with the actual search process. In the end, the SIMULATESPLIT function returns the score of each simulated leaf, as well as the loosest lower and upper bounds of the variables discovered during the simulation.

The scores from all simulated branches are aggregated using the specified aggregation strategy to produce a single score for each candidate neuron. The neuron with the best score is selected as the next split. Moreover, the tightest lower and upper bounds discovered during lookahead are returned, which can be used to further prune the search space.

In general, lookahead can be computationally expensive, as it requires repeated simulation of the solving process. In practice, it is beneficial to invoke Algorithm 1 at the top of the search tree, before falling back to more efficient heuristics. The key advantage of lookahead is that it considers the cascading effects of a branching decision. A neuron that appears promising based on local information may lead to poor downstream progress, while a seemingly less promising candidate can yield improvements over several branching decisions.

FSB can be viewed as a particular implementation of the lookahead procedure where BaBSR is used as the BASESELECT heuristic, d is 1, and the strategy is applied uniformly at every branching decision. This design prioritizes efficiency by minimizing per-decision overhead. But by simulating only one branching decision, FSB cannot fully capture the cascading effects that propagate through multiple levels of the search tree. Our work explores whether investing additional computation in critical branching decisions can improve verification performance. Specifically, we investigate depth-2 lookahead applied at the top of the search tree, where branching decisions have the largest downstream impact. This design is motivated by the strong branching literature in MILP [Glankwamdee and Linderoth, 2006], which demonstrates that expensive branching heuristics provide the greatest benefit early in search. Additionally, we explore how phase-fixing lemmas discovered during lookahead (Section 4.3) can further prune the search space. Section 5 evaluates whether these design choices yield net performance improvements despite their computational overhead.

4.1 Preselect Strategies

If lookahead were to be performed on every neuron in a large neural network, the computational overhead would outweigh the improvement in branch quality. Thus, it is essential to preselect a subset of neurons on which to run lookahead. Several preselect strategies are possible.

One approach is to use a polarity-based strategy, that uses a heuristic that scores neurons based on the sensitivity of their activation status to changes in their bounds. For example, a score such as max ( ub lb , lb ub ), where ub and lb are the upper and lower bounds of a neuron, can be used to identify neurons whose activation status is most undecided. Neurons with the highest scores are then selected for lookahead. We used this polarity-based preselect strategy in Marabou. Another approach is to use existing branching scores, such as BaBSR scores, to rank neurons. In this case, a fixed number of neurons with the highest scores are chosen for lookahead. This preselect strategy was used in α-β-CROWN. Regardless of the strategy, the preselect method should identify promising candidates using lightweight metrics.

4.2 Scoring Functions

The scoring function is a central component of lookahead branching, as it quantifies the effectiveness of each simulated split and guides the branching decision. Two general classes of scoring metrics are commonly used: neuron-fixing-based metrics and bound-reduction-based metrics.

Neuron-fixing-based metric. This approach evaluates a split by counting how many previously unstable neurons become phase-fixed (i.e., their activation status is determined) after bound propagation in each branch. To encourage both high total progress and balanced outcomes, a balance score is computed for each split. For example, if a split results in a neurons fixed in one branch and b in the other, the score can be defined as a×b a+b+1 . This formula favors splits that both fix many neurons and distribute the fixes evenly between branches. Consider a split that fixes 9 neurons in one branch and 1 in the other. Its score would be 9×1 9+1+1 ≈ 0.8. In contrast, a split that fixes 5 neurons in each branch would yield a score of 5×5 5+5+1 ≈ 2.3. Our metric would then favor the more balanced outcome in case the same number of neurons are fixed. When lookahead is performed to greater depths, the scores are computed recursively: at the leaves, the score is based on the number of phase fixes, and at each internal node, the balance formula is applied to the scores of its child branches, propagating upward to yield a final score. This polarity-based metric was used in Marabou.

Bound-reduction-based metric. This metric is based on the reduction in variable bounds or other continuous measures of progress, such as the width of neuron bounds or their proximity to a decision threshold. For example, a scoring function may combine the width of a neuron's bounds, its distance from zero, and an estimate of its influence on the objective (e.g., via gradient approximation). In a lookahead setting, after simulating a split, the scoring function can aggregate the scores from subsequent branches using a balance formula similar to the neuron-fixing metric. For instance, if S+ and S- are the scores from the two branches after a split, the lookahead score can be defined as S0 + λ · S+×SS++S-+1 , where S0 is the immediate score for the split and λ is a discount factor to control the influence of deeper lookahead. For deeper lookahead, this aggregation is applied recursively as scores are propagated up the lookahead tree. This boundreduction-based metric was used in α-β-CROWN.

Regardless of the specific metric, an effective scoring function should capture both the potential for maximal progress toward a solution and the balance of outcomes across different branches. This ensures that the branching decision not only accelerates convergence but also avoids highly imbalanced splits that may lead to inefficient search.

4.3 Phase Fixing via Lookahead Splits

One significant outcome of the lookahead branching procedure is its ability to refine variable bounds, which can lead to phase fixing of previously unstable neurons. Specifically, during the lookahead process, bound propagation is applied after simulating splits, and the resulting bounds can sometimes determine that a neuron is stable (i.e., its phase is fixed). The following theorem formalizes this effect:

Theorem 1 (Phase Fixing via Lookahead). Let z = ReLU(y) be an unstable ReLU, i.e., ℓy < 0 < uy. Suppose we simulate a split on another unstable ReLU zr = ReLU(yr), generating two subproblems corresponding to the inactive (yr ≤ 0) and active (yr ≥ 0) cases.

Let ℓinact y and ℓact y be the lower bounds on y obtained in each subproblem. Then the refined lower bound ℓnew y := min(ℓinact y , ℓact y ) satisfies ℓnew y ≥ ℓy. Similarly, the refined upper bound unew y :=max(uinact y , uact y ) satisfies unew y ≤ uy. As a consequence: if ℓnew y ≥ 0, the phase of z is fixed to active; if unew y ≤ 0, it is fixed to inactive.

Proof Sketch. Simulating a split on zr refines the input domain into two disjoint subdomains. Bound propagation on each subproblem yields tighter constraints on all dependent variables, including y. Because the union of the subdomains recovers the full feasible region, the maximum lower bound and minimum upper bound across the subproblems provide valid global bounds.

The phase-fixing capability cannot be used when either CROWN or α-CROWN bound propagation is used, as the adaptive ReLU rule means bounds can become looser when pre-activation bounds are tightened. Therefore we used phase-fixing in Marabou but not α-β-CROWN.

5 Evaluation

To evaluate the effectiveness of lookahead branching, we implemented Algorithm 1 in two state-of-the-art BaB-based verification tools Marabou and α-β-CROWN. The two verifiers employ different paradigms: Marabou is a CPU-based verifier that employs an SMT-based incomplete decision procedure, while α-β-CROWN runs GPU-accelerated boundpropagation. We evaluate lookahead branching against the state-of-the-art heuristics in each verifier on various benchmarks, investigating whether lookahead branching can improve the branch-and-bound across distinct solver paradigms.

5.1 Case Study onMarabou

Experimental Setup

For experimentation on Marabou, we compared lookahead branching to BaBSR and pseudo-impact, two of Marabou's existing heuristics. BaBSR is a widely-used deterministic heuristic [Bunel et al., 2020], while pseudo-impact is a dynamic heuristic specific to Marabou [Wu et al., 2022]. We conducted experiments on three different benchmark sets, NAP, NN4Sys, and MNIST. NAP is a benchmark designed to evaluate neural network verifiers on specifications defined by neural activation patterns, which characterize broad, numerically challenging regions of the input space. NN4Sys is a benchmark suite constructed from neural networks used in computer systems, testing real-world verification challenges that have been proven difficult in recent iterations of the VNN Competition. The MNIST dataset includes various feed forward neural networks for handwritten digit recognition. The MNIST network architectures we tested include, in layers by neurons, 20x20, 2x256, 4x256, and 6x256. We implemented lookahead on top of the most recent version of Marabou.

We use the polarity-based pre-selecting strategy as described in Section 4.1 to select 10 candidate neurons. We use a d of 2, and instantiate BASESELECT with two different heuristics, BaBSR and pseudo-impact. In the experiments, we perform lookahead splits on the top five branching levels, and fall back to the base heuristics for the rest of it. We used the neuron-fixed-based metric for evaluating a search state and combining the scores across subproblems 4.2. The experiments were run on a server with 2.6-GHz AMD CPUs, with 4 CPU cores allocated per benchmark. Each benchmark was given a 30 minute time limit and a 32 GB memory limit.

Results

Table 1 presents a comparison of the performance of Marabou with and without lookahead branching across the various benchmarks. The tables report the number of instances solved within the time limit (1800 seconds), along with average run time on solved instances. Overall, lookahead branching results in a substantial increase in the number of solved instances for both BaBSR and pseudo-impact heuristics.

Figure 3 provides cactus plots comparing lookahead against BaBSR and pseudo-impact on the three benchmark sets. Overall, lookahead leads to more solved instances compared to the baseline heuristics, especially at higher time limits. On NAP, overhead makes lookahead slower at low time limits, but branching quality gains dominate overall. On NN4Sys, lookahead yields significantly more solved instances with pseudo-impact and solve time improvements with BaBSR. For MNIST, lookahead solves more instances at higher time limits. Table 2 compares lookahead's overhead an easy and hard instance. On the easy instance, the overhead dominates. On the hard instance, the overhead constitutes a small part of overall runtime and the improved branching yields a substantial speedup.

Ablation Studies on Marabou

We performed additional ablation studies on the NAP and NN4Sys benchmarks by varying the lookahead depth (D), number of preselected candidates (C), and removing phase fixing (PF). All configurations use the polarity-based preselect strategy and BaBSR as the base select heuristic.

On NAP, all lookahead configurations solve between 36 and 47 instances, compared to 30 for BaBSR. On NN4Sys, varying depth and candidate count has minimal effect on performance, with the exception of the D10C10 configuration, where increased branching overhead reduces performance. Comparing lookahead with and without phase fixing shows that phase fixing has no effect on NAP but yields a 33-second improvement on NN4Sys.

5.2 Case Study on α-β-CROWN

Experimental Setup

For experimentation on α-β-CROWN, we compared lookahead branching to its current state-of-the-art heuristic, FSB [De Palma et al., 2021], on seven different convolutional neural networks ranging with various robustness properties for each. The networks came from the CIFAR, MNIST, and TinyImageNet datasets, three computer vision datasets for image and text recognition. The networks from the CIFAR and TinyImageNet datasets range between 14.4 million and 31.6 million parameters, making them challenging verification queries. The MNIST benchmarks were adversarially trained, introducing complexity that makes formal verification particularly challenging. We implemented lookahead in the most recent version of α-β-CROWN [Zhou et al., 2025].

With α-β-CROWN, the solver first attempted to solve the problem with an adversarial attack algorithm [Zhang et al., 2022b], then with incomplete verification using autoLiRPA [Xu et al., 2021] before beginning complete verification with BaB. When BaB is run, the first five BaB rounds are done using lookahead branching with a d of 2, and then FSB branching is used. We use BaBSR as the preselect strategy and select 15 candidate neurons. We used the boundreduction-based metric for the scoring function (Section 4.2) with a discount factor λ of 0.5. We did not implement the phase fixing techniques in α-β-CROWN, as α-β-CROWN leverages α-CROWN for bound propagation and thus phase fixing is not sound. The experiments were run on a server with 2.6-GHz AMD CPUs and A100 GPUs. One A100 GPU and 96 CPU cores were allocated for each experiment, and a 128 GB memory limit was given for each experiment.

Results

Table 4 presents a comprehensive overview of the verification performance on the seven neural network models using both FSB branching and lookahead branching within αβ-CROWN. The table compares the total number of solved instances (including both SAT and UNSAT) and the average runtime on solved instances. To isolate the impact of lookahead branching on the branch-and-bound core of α-β- CROWN, Table 5 presents results filtered to include only instances that required the full BaB procedure. SAT instances solved through adversarial attacks and easier UNSAT instances solved with incomplete verification are excluded. We see that lookahead leads to a consistent speedup in solve time, and contributes two unique solutions.

Ablation Studies on α-β-CROWN

Table 6 presents the performance of α-β-CROWN while varying the number of lookahead branches performed before switching to FSB. Across all hyperparameters tested, lookahead either solves more instances or has faster solve times than FSB. Changing the number of lookahead branches does not change the number of solved instances and changes the solve time minimally.

Overall, we found that lookahead can boost the performance of BaB in two fundamentally different neural network verifiers. This suggests that lookahead branching can be a generally applicable strategy for enhancing the performance of complete neural network verification.

6 Conclusion

In this paper, we introduced a general lookahead branching strategy for neural network verification. The key idea is to simulate candidate splits to make more informed branching decisions. We discussed design choices of lookahead and instantiated lookahead branching for two distinct complete verifiers, Marabou and α-β-CROWN. Our results show that using lookahead branching results in substantial performance gains in both solvers across a wide range of benchmarks.

Limitations. As we presented lookahead as a template algorithm, its design space is massive. While we considered two instantiations in Marabou and one in α-β-CROWN, it would be interesting to evaluate more variants of lookahead. In particular, we plan to investigate deeper lookahead simulations or periodically invoking lookahead later in the search. In addition, while we explored leveraging lookahead to fix unstable neurons, it might be interesting to leverage other information, such as dependencies between neurons, which might result in additional pruning of the search space.

Acknowledgments

This work made use of high-performance computing equipment funded by the National Science Foundation under Grant #2117377. Wu's work is supported by a gift from VMware University Research Fund. Additional support was provided by the Stanford Center for Automated Reasoning (Centaur). Huan Zhang acknowledges the support from the Schmidt Sciences AI2050 program and the National Science Foundation under Grant #2331967.