Paper deep dive
Learning Lookahead Lemmas for Neural Network Verification
Liam Davis, Haoze Wu
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 87%
Last extracted: 8/3/2026, 2:31:41 AM
Summary
The paper introduces an inprocessing framework for neural network verification that utilizes a lookahead procedure to derive lemmas regarding the phases of unstable ReLUs. These lemmas are collected into an implication graph, which is then used to prune the search space and vivify boolean cuts. The framework is instantiated in two state-of-the-art verifiers, Marabou and α-β-CROWN, demonstrating improved performance by proving up to 34% more instances unsatisfiable.
Entities (10)
Relation Signals (9)
Lookahead Procedure → derives → Implication Graph
confidence 90% · lookahead derives new lemmas over the phases of unstable ReLUs, which are collected into an implication graph
Implication Graph → usedby → Marabou
confidence 90% · We instantiate the framework in two state-of-the-art verifiers, Marabou... and demonstrate that it improves performance
Implication Graph → usedby → α-β-CROWN
confidence 90% · We instantiate the framework in two state-of-the-art verifiers... α-β-CROWN, and demonstrate that it improves performance
Lookahead Procedure → prunes → Search Space
confidence 85% · implication graph that is used to prune the search space
Lookahead Procedure → vivifies → Boolean Cuts
confidence 85% · implication graph that is used to ... vivify boolean cuts
Marabou → uses → PICID
confidence 80% · PICID is used in Marabou
α-β-CROWN → uses → BICCOS
confidence 80% · α-β-CROWN uses BICCOS cuts
Marabou → uses → DeepPoly
confidence 80% · Marabou tightens with DeepPoly
α-β-CROWN → uses →
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:State-of-the-art neural network verifiers use the branch-and-bound procedure as their core solving mechanism. We introduce an inprocessing framework for neural network verification driven by the lookahead procedure. Under this framework, lookahead derives new lemmas over the phases of unstable ReLUs, which are collected into an implication graph that is used to prune the search space and vivify boolean cuts. We instantiate the framework in two state-of-the-art verifiers, Marabou and $\alpha$-$\beta$-CROWN, and demonstrate that it improves performance in both, proving up to 34% more instances unsatisfiable.
Tags
Links
- Source: https://arxiv.org/abs/2607.29051v1
- Canonical: https://arxiv.org/abs/2607.29051v1
Trouble viewing inline? Open PDF directly →
Full Text
49,673 characters extracted from source content.
Expand or collapse full text
Learning Lookahead Lemmas for Neural Network Verification Liam Davis, Haoze Wu Amherst College Abstract State-of-the-art neural network verifiers use the branch-and- bound procedure as their core solving mechanism. We intro- duce an inprocessing framework for neural network verifica- tion driven by the lookahead procedure. Under this framework, lookahead derives new lemmas over the phases of unstable ReLUs, which are collected into an implication graph that is used to prune the search space and vivify boolean cuts. We instantiate the framework in two state-of-the-art verifiers, Marabou and α-β-CROWN, and demonstrate that it improves performance in both, proving up to 34% more instances un- satisfiable. 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). Despite this, their internal structure is opaque or unintelligible, which makes it difficult to under- stand their behavior and trust their predictions. To ensure the safe deployment of DNNs in safety-critical domains, there has been substantial effort from the formal methods and machine learning communities on developing scalable formal verification techniques (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 the branch- and-bound (BaB) procedure, which involves performing case splitting on non-linear activation functions, such as ReLUs, and analyzing the resulting subproblems with an incomplete verifier. If the analysis is inconclusive, further case splits are performed recursively. Recent efforts to accelerate the BaB search procedure fall broadly into two families. The first family focuses on im- proving the branching heuristic, or the strategy used to select what ReLU to perform a case split on. Heuristics such as BaBSR (Bunel et al. 2020) and pseudo-impact (Wu et al. 2022) attempt to get the most out of the information already available about the state of the search. Lookahead branch- ing (Davis et al. 2026) extends this idea into a general proce- dure that simulates several candidate splits and evaluates the subproblems each one produces. The second family is deriv- ing information from subproblems proven to be infeasible, usually in the form of boolean cuts like BICCOS (Zhou et al. 2024) and PICID (Isac et al. 2026). Both of these families are reactive, in that they exploit information the search has already paid to obtain. Lookahead branching (Davis et al. 2026) comes closest to escaping this, as simulating a can- didate split can fix the phase of an unstable ReLU (active or inactive) globally, but this is a consequence of the pro- cedure rather than its primary purpose, which remains to select the best ReLU to split on. Compare this to modern SAT solvers, which not only derive information reactively via conflict clauses, but also proactively through inprocess- ing (Järvisalo, Heule, and Biere 2012), where the search is periodically paused to conduct exploration intended to de- rive new information. Neural network verification has no analogue, and this is the gap we seek to fill. In this work, we explore the idea of inprocessing in neural network verification in full, treating the derivation of new information as a part of the solve procedure rather than as a consequence of the branching heuristic. Specifically, we construct a variation of the lookahead procedure to derive lemmas about the phases of unstable ReLUs. Each lemma states either that a phase is infeasible outright or that fixing one phase forces another, and we collect them into an implica- tion graph. The graph is not a fixed set of facts but a structure the solver reasons over, and we develop three techniques that do so. SAT closure treats the graph as a propositional formula and closes it under its logical consequences, so that a sub- problem can be pruned whenever the phase fixes are jointly unsatisfiable. Reprobing reruns the lookahead procedure as the search establishes new phases, refreshing the graph with implications that hold only once bounds have tightened. Cut vivification uses the graph to extract an unsatisfiable core of a boolean cut, shortening the cut to the phase fixes responsible for the infeasibility so that it prunes more subproblems. To- gether, these compound into an inprocessing framework for neural network verification. We implement the framework in two state-of-the-art verifiers, Marabou (Katz et al. 2019; Wu et al. 2024) and α-β-CROWN (Zhang et al. 2018; Xu et al. 2020, 2021; Wang et al. 2021; Zhang et al. 2022a,b; Kotha et al. 2023; Shi et al. 2025; Zhou et al. 2025), and show that the framework yields improved performance in both verifiers. The rest of the paper is organized as follows: Section 2 reviews related work. Section 3 provides background infor- mation on neural network verification. Section 4 presents the construction of the implication graph with the lookahead procedure, as well as how the graph is used to prune the arXiv:2607.29051v1 [cs.LG] 31 Jul 2026 search space and strengthen boolean cuts. Section 5 provides an evaluation of the inprocessing framework, comparing it to the current version of both Marabou and α-β-CROWN. Fi- nally, we conclude and discuss future directions in Section 6. 2 Related Work Early efforts for complete neural network verification used SMT and MILP solvers to enumerate activation pat- terns (Katz et al. 2017). The first unified instantiation of BaB was presented by Bunel et al. (2020). State-of-the- art complete neural network verifiers include SMT-based solvers (Katz et al. 2019; Wu et al. 2024) and GPU- accelerated bound propagation-based verifiers (Wang et al. 2021; Shi et al. 2025). Inprocessing techniques have been widely used in both SAT and SMT solving, including variable and clause elimi- nation (Eén and Biere 2005), probing-based simplifications such as failed literal detection, hyper-binary resolution and equality reduction (Bacchus and Winter 2003), and simpli- fications derived from the binary implication graph (Heule, Järvisalo, and Biere 2011). Biere, Järvisalo, and Kiesl (2021) provides a survey of such techniques. While these techniques were first applied as preprocessing, Järvisalo, Heule, and Biere (2012) formalized the rules under which they can be interleaved with the search itself while preserving satisfia- bility. Clause vivification was likewise introduced as a pre- processing step (Piette, Hamadi, and Saïs 2008) and later applied to learnt clauses during the search (Luo et al. 2017; Li et al. 2020). Lookahead has also been used to derive in- formation rather than only to branch, most notably in cube- and-conquer (Heule et al. 2011). Our contributions draw conceptually from this line of work. The implication graph is inspired by the binary impli- cation graph, reprobing by periodic re-simplification, and cut vivification by clause vivification. We depart from it in how the information is obtained, taking inspiration from looka- head branching (Davis et al. 2026) and using a variant of the lookahead procedure as the probe, which lets the frame- work reason about ReLU phases with the bound propagation machinery a verifier already has. 3 Background 3.1 Neural Network Verification For a trained deep neural network N :R n →R m with an input x ∈R n and output y ∈R m , 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). As the property φ(y) is a safety property, SAT denotes that an adversarial example violates the safety property and is referred to as unsafe, while UNSAT denotes a satisfied property and is referred to as safe. In this paper, we will use the terms SAT and UNSAT. 3.2 Branch-and-Bound The branch-and-bound (BaB) framework, illustrated by Fig- ure 1, is an efficient approach to neural network verification. r 1 r 2 r 3 ✓ r 4 r 5 r 6 ✓ ¬ r 1 r 1 ¬ r 2 r 2 ¬ r 3 r 3 ¬ r 4 r 4 ¬ r 5 r 5 ¬ r 6 r 6 Figure 1: Each node represents a subproblem from BaB by splitting unstable ReLUs. Green nodes are verified, blue nodes require further splitting. BaB systematically tightens the bounds of a neural network by splitting on unstable ReLU neurons. When an unstable ReLU is split, the problem is divided into two subproblems, one where the ReLU is active and one where the ReLU is inactive. After bound propagations, this turns a large prob- lem into two more manageable problems. To verify with BaB, ReLU splits are repeatedly applied until each resulting subproblem can be classified as either SAT or UNSAT. 3.3 Boolean Cuts in Branch-and-Bound In the BaB framework, a cut is a global infeasibility that can be used to determine that a subproblem is UNSAT, without requiring further ReLU splits. Boolean cuts are collections of ReLU phase fixes that are globally infeasible. In neural network verification, there are two predominant boolean cuts: BICCOS (Zhou et al. 2024) and PICID (Isac et al. 2026). α-β-CROWN uses BICCOS cuts, which are in- feasibilities mined from the BaB search procedure. Formally, let R + and R − denote the sets of neurons restricted to the active (r i = 1) and inactive (r i = 0) regimes, respectively, along a branch proven UNSAT. BICCOS introduces the cut X i∈R + r i − X i∈R − r i ≤|R + |− 1,(1) where r i ∈ [0, 1] is the relaxed ReLU indicator for neu- ron i. This inequality is violated exactly by the assignment r i = 1 ∀i ∈ R + and r i = 0 ∀i ∈ R − , so it excludes that phase combination everywhere in the search tree, even in subdomains where those neurons have not yet been split. PICID is used in Marabou, and derives a similar boolean cut through a different mechanism. Whenever a subproblem is proven UNSAT, PICID uses the Farkas lemma to derive an infeasibility certificate that isolates the branching decisions responsible for the contradiction. Formally, letR denote a set of ReLU phase fixes that jointly derive infeasibility. PICID defines the cut as the conjunction over R: i∈R r i .(2) r 1 ¬r 1 r 2 ¬r 2 r 3 ¬r 3 r 4 ¬r 4 Figure 2: Implication graph over four unstable ReLUs. Solid edges are binary implications; dashed edges are their contra- positives. r 4 is a unit lemma. Both cuts are applied the same way during the BaB search procedure. When a subproblem is proven UNSAT, the cut is added to the global problem and if violated elsewhere, that subproblem is immediately deemed UNSAT without further ReLU splits. This way, cuts can be used to prune the search tree and accelerate the verification process. 3.4 Lookahead Branching Lookahead Branching (Davis et al. 2026) is a branching heuristic for BaB that selects which unstable ReLU to split at a given subproblem. The heuristic simulates several splits prior to committing to one, making more informed decisions than heuristics that rely solely on local information. Notably, it can also fix the phases of certain unstable ReLUs. In this work, we extend this direction and instead of using lookahead as a branching heuristic, we use it solely to de- rive new information, integrating it with the boolean cuts in Section 3.3 into our framework. 4 Methodology Recall that a phase fix pins an unstable ReLU to its active or inactive state. Denote r i for a phase fix of ReLU i in the active phase and¬r i for the complementary phase fix in the inactive phase. Definition 1 (Binary Implication). Let r 1 and r 2 be phase fixes of unstable ReLUs. We say r 1 implies r 2 , written r 1 → r 2 , if the phase fixesr 1 ,¬r 2 are globally infeasible. Binary implications are the natural unit of information here, as pinning one neuron shows what that one fix forces, whereas obtaining larger implications would require probing sets of fixes. Definition 2 (Unit Lemma). Let r be a phase fix of an un- stable ReLU. We say r is a unit lemma if the phase fix¬r is globally infeasible on its own, i.e., r is entailed uncondi- tionally. Definition 3 (Implication Graph). The implication graph is the directed graph G = (V,E), where V = r i ,¬r i : i is an unstable ReLU is the set of phase fixes and E = (r,r ′ )∈ V ×V : r → r ′ is the set of binary implications. A unit lemma is represented in the implication graph as an edge from a phase fix to its complement. Applying Def- inition 1 to the two phase fixes of the same ReLU reduces exactly to¬r being globally infeasible, so a unit lemma r contributes the edge¬r → r to E. Algorithm 1: Lookahead Procedure for Constructing the Im- plication Graph Require: unstable ReLUs 1,...,n Ensure: implication graph G = (V,E) 1: V ←r i ,¬r i : i = 1,...,n; E ←∅ 2: for each unstable ReLU i and phase fix r ∈ r i ,¬r i do 3: tighten bounds under r with a restricted oracle 4: if r is infeasible then 5:record¬r as a unit lemma 6: else 7:for each unstable ReLU j ̸= i do 8:if the tightened bounds force j to a single phase r ′ j then 9:E ← E∪(r,r ′ j ) 10:end if 11:end for 12: end if 13: end for 14: return G = (V,E) Figure 2 illustrates an example implication graph over four unstable ReLUs. An implication graph can be used to derive new information during the BaB search procedure, but the implication graph must be constructed first. The next sections describe how to construct the implication graph, then how to use it to derive new information. 4.1 Constructing the Implication Graph Algorithm 1 shows the lookahead procedure used to con- struct the implication graph. Each unstable ReLU is fixed to both the active and inactive phases. After each phase fix, the bounds are tightened, but not with the full verification ma- chinery. Unlike lookahead branching, which commits to each simulated split using the full bound propagation procedure, constructing the implication graph only requires a restricted, budgeted tightening pass per phase fix. A restricted pass keeps each probe cheap enough to afford a probe over every unstable neuron. Marabou tightens with DeepPoly (Singh et al. 2019), plus a pivot-capped simplex feasibility check rather than an exact LP. α-β-CROWN tightens with a single α-CROWN (Xu et al. 2021) pass reusing build-time alphas rather than the full optimization loop. This restriction is what makes lookahead as inprocessing cheap in comparison to the branching heuristic. After tightening, the bounds are checked for infeasibility. If the phase fix is infeasible, then we can record the comple- mentary phase fix as a unit lemma. Otherwise, the previously unstable neurons are checked to see if any have been forced to a single phase. Each newly-fixed neuron is assigned a new binary implication, where the source is the phase fix that forced it and the target is the newly-fixed neuron. Theorem 1 formalizes the soundness of the implication graph. Theorem 1 (Soundness of Construction). If the tightening oracle (CROWN / DeepPoly) is sound, then every unit lemma and every edge of the resulting implication graph G satisfies Definition 2 and Definition 1, respectively. Proof is deferred to Appendix A. Through the lookahead procedure, we can also derive tighter bounds on all ReLUs. When we look ahead on both phases of a neuron, each phase fix outputs its own per-neuron bounds. Since every point satisfies one of the two phases, the hull of the two bounds is sound and can be tighter than the bounds at the root. The following theorem formalizes this bound. Theorem 2 (Hull Bound). For each unstable ReLU i and neuron k, let [lb r i k , ub r i k ] and [lb ¬r i k , ub ¬r i k ] be the bounds computed under r i and ¬r i . The hull [min(lb r i k , lb ¬r i k ), max(ub r i k , ub ¬r i k )] is sound for k without assuming either phase of ReLU i. Proof is deferred to Appendix A. With the implication graph, we can also use the SAT closure of the graph to derive new information. 4.2 SAT Closure of the Implication Graph The implication graph is built from binary implications and unit lemmas of ReLU phase fixes, which are boolean vari- ables. Thus, the implication graph can be represented as a SAT formula Σ, where each unit lemmar becomes the clause (r), and each edge (r,r ′ )∈ E becomes the clause (¬r∨r ′ ). At each BaB node, let R be the phase fixes already com- mitted along the path from the root to that node. Checking Σ∪ R with a SAT solver is free relative to the tightening oracle; if it is unsatisfiable, the node is infeasible and can be pruned without any further splitting. Theorem 3 formalizes the soundness of the closure. Theorem 3 (Soundness of SAT-Closure Pruning). Let R be the phase fixes fixed at a BaB node and Σ the implication graph’s clauses. If Σ∪ R is unsatisfiable, the subproblem is UNSAT. Proof is deferred to Appendix A. Σ∪ R only checks the clauses the graph already has, computed against Q alone at the root. Deeper in the tree, R has already tightened the problem substantially, and a pin that did not refute at the root may refute now, or force a phase it did not force before. Catching that requires rerunning the lookahead procedure itself, not just recombining existing clauses. 4.3 Reprobing to Update the Implication Graph The implication graph was built once, before any splits were made, so its facts only reflect what is true at the root. By the time BaB reaches a deeper node, several ReLUs have already been fixed, and those fixes narrow the space of remaining inputs. A phase fix that looked possible at the root may now be provably impossible once the earlier fixes are accounted for, or it may now force some other neuron’s phase where it could not before. Reprobing catches these newly-provable facts by simply rerunning the lookahead procedure at the current node instead of at the root. Formally, let Q denote the original verification query. Let Q R := Q∧ r∈R r denote the query restricted to the current node’s fixed phases. Reprobing is Algorithm 1 rerun against Q R instead of Q, restricted to the ReLUs still unstable at the node: each still- unstable neuron is branched on its active and inactive phase, the tightening oracle is rerun underQ R together with that pin, and any resulting infeasibility or forced phase is recorded as a unit lemma or edge, exactly as before. By Theorem 1 with Q replaced by Q R , the new units and edges hold in every model of Q R . The trigger condition below ensures every fix in R is entailed by Q, so Q R has the same models as Q and the new facts enter Σ as root-global facts. This keeps the implication graph up to date with the present subproblem. Reprobing is not run at every node. A pass sweeps every unstable neuron in both phases, so it costs on the order of the initial construction, and running one per node would dominate the search. Instead a reprobe is triggered when two conditions hold. First, the search must be at a point where no branching decisions are in force, so that the facts derived are conditioned only on phases already established globally rather than on a path that is about to be undone. Second, the set of established phases must have grown since the last pass, since Q R is otherwise unchanged and a repeat sweep would rederive exactly what is already in Σ. 4.4 Cut Vivification With the implication graph, beyond using it to directly de- termine infeasibility, we can use it to vivify boolean cuts. Recall that a boolean cut is a collection of ReLU phase fixes that are globally infeasible. The process of vivifying a cut is to remove phase fixes from the collection, creating a smaller set of phase fixes and a stronger cut. The implication graph provides the machinery to vivify cuts. Concretely, both BICCOS and PICID cuts are mined from subproblems determined infeasible, coming directly from the BaB search procedure. All of the phase fixes are used to derive the cut in some form, but in most cases, not all of them are necessary. The implication graph records which phase fixes are consequences of each other, so naturally, we can use the implication graph to determine which phase fixes in the cut are consequences of others. Algorithm 2 shows the cut vivification procedure. The first observation is that if a phase fix in a cut is implied in the implication graph by the other phase fixes in the cut, then the phase fix is redundant and can be removed. The following theorem formalizes this observation. Theorem 4 (Redundant Phase Fixes). Let S be a cut, let r ∈ S, and write S ′ = S\r. If Σ∧ r ′ ∈S ′ r ′ |= r, then S ′ is itself a cut. Proof is deferred to Appendix A. The next observation is that if a cut is unsatisfiable against the SAT closure of the implication graph, then a subset of its phase fixes is already infeasible and that subset is a stronger cut. That subset is read directly off the implication graph. As- sume every phase fix of the cut and propagate through the graph. Each newly derived phase fix is forced by a single edge, so it can be traced backwards along that edge to the fix that forced it, and that fix in turn to the one before it, until the Algorithm 2: Cut Vivification Require: cut S, clause formula Σ, query Q Ensure: vivified cut S ′ ⊆ S 1: for each r ∈ S do 2: if Σ∪ (S\r) propagates r then 3: S ← S\r 4: end if 5: end for 6: propagate S through Σ 7: if propagation derives both r and¬r then 8: return the roots of the antecedent chains of r and¬r 9: end if 10: if Σ is unsatisfiable under the assumptions S then 11: return the failed assumptions S ′ ⊆ S 12: end if 13: order S as r (1) ,...,r (n) , most tightening first 14: P ←∅ 15: for j = 1,...,n do 16: P ← P ∪r (j) 17: P ← P ∪r ′ : Σ∪ P propagates r ′ 18: if propagation yields a conflict then 19:return r (1) ,...,r (j) 20: end if 21: tighten bounds under P with a restricted oracle 22: if P is infeasible then 23:return r (1) ,...,r (j) 24: end if 25: end for 26: return S chain ends at either a phase fix of the cut or a unit lemma. A conflict occurs when some phase fix and its complement are both derived. Tracing each of the two back to where its chain began identifies exactly the phase fixes of the cut that participated in the refutation, and that set is the unsatisfiable core. Since every derived fix has exactly one antecedent, each chain has a single root, so a conflict found this way rests on at most two phase fixes of the cut. A cut of any length therefore collapses in one step to a cut of size two, or to a single phase fix when one of the two chains begins at a unit lemma. In practice this trace is not performed by hand. The graph is already maintained as the formula Σ, so the phase fixes of the cut are handed to the SAT solver as assumptions and the solver is asked whether Σ survives them. When it does not, the solver reports which of the assumptions its refutation used, and that set of failed assumptions is the core. Conflict analysis performs the same backward trace, over a resolution derivation rather than over a single chain of edges, which is what allows the procedure to keep working once Σ holds clauses that are not binary, such as previously vivified cuts. For those, propagation alone may no longer find the con- flict and the core may be larger than two, but the interface is unchanged. The solve is conflict bounded, so its cost re- mains negligible against a single call to the tightening oracle. Lemma 5 formalizes the core extraction. Lemma 5 (Core from the Implication Graph). Suppose prop- agating S through the binary fragment of Σ, its unit and binary clauses, derives both r and¬r, and let a 1 and a 2 be the roots of their antecedent chains. Then S ′ =a 1 ,a 2 ∩S satisfies|S ′ |≤ 2 and Σ∪ S ′ is unsatisfiable. Proof is deferred to Appendix A. The intersection with S covers the case where a chain begins at a unit lemma rather than at the cut, as such a root holds under Σ alone and contributes nothing to S ′ . When both chains begin at unit lemmas, S ′ =∅ and Σ is unsatisfiable on its own, which by Theorem 3 with R =∅ means the query itself is UNSAT and the search can stop. Corollary 6 formalizes this fact. Corollary 6 (Refutation by the Implication Graph). Let S be a cut and let S ′ ⊆ S be an unsatisfiable core of Σ under the assumptions S. Then S ′ is itself a cut. This is Theorem 3 applied with R = S ′ , where a set of phase fixes that cannot be extended to a model of Σ cannot be extended to a model of Q either. Together with Lemma 5 it licenses returning the core in place of the cut. Using exclu- sively the implication graph has one drawback: it sees only binary implications and unit lemmas, so the first two steps add negligible overhead but cannot act on combinations of phase fixes. For that we turn to the tightening oracle, using a variant of the lookahead procedure. Algorithm 1 pins one phase fix and asks whether the query survives it, but nothing in the procedure requires the pin to be a single fix. Pinning several at once and running the same restricted tightening oracle asks the same question of a set, and the answer is what the criterion for vivification needs. The remaining phase fixes of the cut are therefore added to a pin set one at a time, and after each addition the bounds are tightened. If the pin set becomes infeasible after j additions, those j phase fixes are a cut on their own and replace S. This is the only stage that consults the network rather than the graph, and it is the only one that can act on combinations of phase fixes, because a combination is precisely what it pins. Since the fixes are added in order, the procedure can only return a prefix of the order it was given. We sort the fixes by the tightening each one produced when it was probed during the construction of the implication graph, most tight- ening first, breaking ties by the instability of the neuron under the refined bounds. Both quantities are by-products of Algorithm 1 and are already stored, so the ordering costs nothing, and placing the most constraining fixes first makes an infeasibility surface at the smallest j. The two boolean stages continue to pay off inside this one. After each fix is pinned, the phase fixes it implies in Σ are added to the pin set as well. These additions are free and can only help the oracle, and if propagation conflicts outright, the prefix is returned without invoking the oracle at all. This is sound because each added fix is entailed by Σ together with the prefix, so the pin set and the prefix have the same models by the argument of Theorem 4. Theorem 7 formalizes the soundness of this. Theorem 7 (Soundness of the Descent). Let P j = r (1) ,...,r (j) and let ˆ P j denote its closure under prop- agation in Σ. If the tightening oracle finds Q ∧ V r∈ ˆ P j r infeasible, then P j is a cut. This is a consequence of the previous theorems, as an Lookahead Probe Implication Graph Σ BaB Subproblem Mined Cut Vivification Reprobe units, edges, hull prune / clamp UNSAT shortened cut fixed set grew facts under Q R Figure 3: Inprocessing over the course of a solve. Lookahead probe constructs the implication graph; cuts mined from UN- SAT subproblems are vivified back into the graph; new phase fixes trigger reprobing. empty bound implies infeasibility by Theorem 1, and the propagated fixes may be discarded from ˆ P j by Theorem 4. A cut that reaches the end of the descent unchanged is certified minimal with respect to the tightening oracle. 4.5 Inprocessing Framework with Lookahead Figure 3 shows how the pieces fit together over the course of a solve. Before the search begins, the lookahead procedure probes every unstable ReLU in both phases, and its results seed three channels at once. Unit lemmas and binary impli- cations become the clauses of Σ, and the hull of each pair of probes tightens the root bounds. The search then proceeds as usual, with two additions at each subproblem. On entering a subproblem with committed phase fixesR, the solver first checks Σ∪R. If it is unsatisfiable the subproblem is infeasible by Theorem 3 and is discarded before any bound computation. Otherwise the phase fixes that Σ propagates from R are clamped into the subproblem’s bounds. Both are propagation over the clause database, so their cost is negligible. When a subproblem is proven UNSAT, the underlying cut mechanism mines a cut from it as before, but the cut is now vivified by Algorithm 2 before it is installed. The shortened cut goes into the cut pool and into Σ, where it strengthens every subsequent check, and any cut that vivification reduces to a single phase fix is a unit lemma and enters the implication graph as a node fact. Cuts are added to Σ only after their own vivification attempt, since a cut already present in Σ refutes its own assumptions and the resulting core is the cut itself. Those unit lemmas grow the set of established phases, which is the condition under which reprobing runs. When the search next reaches a point with no branching decisions in force, the lookahead procedure is rerun against Q R over the still-unstable neurons, and whatever it derives returns to Σ as root-global facts. The result is a loop rather than a pipeline: the graph informs the search, the search produces cuts, vivification turns those cuts back into graph facts, and those facts trigger the probing that grows the graph further. 5 Evaluation To evaluate the effectiveness of our proposed inprocessing framework, we implemented the framework in two state-of- the-art BaB-based verifiers in Marabou and α-β-CROWN. These two solvers represent two different solver paradigms: Marabou (Wu et al. 2024) is a CPU-based verifier that em- ploys an SMT-based search procedure and PICID, while α-β-CROWN (Wang et al. 2021) uses GPU-accelerated bound propagation and BICCOS. We evaluate our framework against the most recent versions of these verifiers, which in- clude both PICID and BICCOS respectively. 5.1 Case Study on Marabou Experimental Setup For experimentation on Marabou, we evaluated our framework on several standard bench- marks from recent literature using Marabou, including the ACASXu, MNIST and SafeNLP benchmarks. The ACASXu benchmark (Julian et al. 2016; Katz et al. 2017) is a set of neural networks for airborne collision avoidance systems, and has been widely used to evaluate different verifiers. The MNIST dataset (LeCun et al. 1998) includes various feed- forward neural networks for handwritten digit recognition. SafeNLP is a set of neural networks for natural language processing tasks and has been a staple benchmark in the most recent editions of the VNN-COMP (Brix et al. 2023, 2024; Kaulen et al. 2025). CaDiCaL (Biere et al. 2024) was used as the SAT solver for the implication graph, and the tightening oracle included one DeepPoly (Singh et al. 2019) pass and a simplex feasibility check capped at 400 pivots. 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 20 minute time limit and a 32 GB memory limit. Results Table 1 shows the results of the inprocessing framework on Marabou. In total, the framework leads to fewer timeouts on every benchmark. It solves substantially more UNSAT instances on every benchmark, and on SAT instances it matches PICID on ACASXu, solves two more on MNIST, and solves fewer only on SafeNLP. The SafeNLP regression reflects an asymmetry between deducing UNSAT versus SAT. Proving unsatisfiability is a universal claim, re- quiring every subdomain to be proven UNSAT. Proving sat- isfiability requires only one counterexample, which is why attack algorithms as shown in Section 5.2 are usually more effective at deducing SAT than BaB. Inprocessing slightly changes the order in which domains are explored, which by chance can leave a domain with a counterexample explored later. Cactus plots for both runtime and visited states on the Marabou benchmarks are presented in Appendix C. Table 2 shows the overhead of the lookahead probing and reprobing phases on Marabou. On SafeNLP probing takes up less than 0.1% of the total wall clock time, and on ACASXu 2.6%. On MNIST it accounts for 19.2%, though the gap between the median and mean per-instance probing times shows this is driven by a few outliers, and inprocessing still solves 35 more UNSAT instances there. Appendix B reports how often each component fires and succeeds. InstancesAvg. time (s) Avg. states Configuration UNSAT SAT T/O UNSAT SAT UNSAT SAT ACASXu PICID99 24 40 142.2 53.2 1724.1 502.9 + inprocessing124 24 15 75.6 115.5 795.1 993.5 MNIST PICID102 27 122 12.8 172.0 16.0 3041.1 + inprocessing137 29 85 37.7 185.2 13.3 2685.2 SafeNLP PICID242 596 238 42.5 1.2 3982.7 84.5 + inprocessing266 575 235 25.9 1.7 2308.8 134.2 Table 1: Results on Marabou. Probing time (s) Benchmark MedianMeanMax Wall clock (%) ACASXu3.835.4313.852.6 MNIST38.42 135.31 491.7319.2 SafeNLP0.240.240.41<0.1 Table 2: Overhead of inprocessing on Marabou. 5.2 Case Study on α-β-CROWN Experimental Setup For experimentation on α-β- CROWN, we evaluated our framework on the CIFAR and TinyImageNet benchmarks drawn from recent literature us- ing α-β-CROWN (Zhou et al. 2024, 2025). These consist of CNNs for image classification ranging from 14.4 million to 31.6 million parameters. The CIFAR benchmarks include adversarially trained networks, making them challenging ver- ification tasks. CaDiCaL (Biere et al. 2024) was used as the SAT solver for the implication graph through the PySAT Python API, with the tightening oracle implemented as a single α-CROWN bound propagation pass. The experiments were run on a server with 2.6-GHz AMD CPUs and NVIDIA A100 GPUs, with 96 CPU cores and one A100 GPU allocated per bench- mark. Each benchmark was given a 128 GB memory limit. Results Table 3 presents the results of the inprocessing framework.α-β-CROWN first runs PGD attack to find coun- terexamples, so on all four benchmarks all the SAT instances are solved without entering BaB. On UNSAT instances, the inprocessing framework solves more instances and reduces the average time on all four benchmarks. Cactus plots for both runtime and visited states are presented in Appendix C. Table 4 shows the overhead of the probing of the inpro- cessing framework. Overall, lookahead takes between 0.2% and 6% of the total wall clock time. Appendix B reports how often each component fires and succeeds. 6 Conclusion In this paper, we introduced an inprocessing framework for BaB-based neural network verification. The framework lever- ages the lookahead procedure to construct an implication InstancesAvg. time (s)Avg. Configuration UNSAT SAT T/O UNSAT SAT states CIFAR CNN-A-Adv BICCOS91 10095.1 0.1 2446.6 + inprocessing92 10084.3 0.1 1583.3 CIFAR CNN-A-Mix BICCOS88 94 1813.3 0.0 4434.0 + inprocessing90 94 1610.1 0.0 2712.8 CIFAR CNN-B-Adv BICCOS95 70 3517.9 0.1 9095.9 + inprocessing97 70 3316.1 0.0 2652.3 TinyImageNet BICCOS131 43 2631.0 2.4 1683.5 + inprocessing135 43 2230.0 1.0 1762.7 Table 3: Results onα-β-CROWN. Time limits: CIFAR CNN- A-Adv and CIFAR CNN-A-Mix: 200s, CIFAR CNN-B-Adv: 350s, TinyImageNet: 360s. Probing time (s) BenchmarkMedian Mean Max Wall clock (%) CIFAR CNN-A-Adv0.18 0.18 0.300.2 CIFAR CNN-A-Mix0.29 0.29 0.440.4 CIFAR CNN-B-Adv4.12 4.14 7.332.0 TinyImageNet2.39 2.86 5.816.0 Table 4: Overhead of inprocessing on α-β-CROWN. graph of ReLU phases, which is then used to prune subprob- lems and vivify boolean cuts. We implemented the frame- work in two state-of-the-art BaB-based verifiers, Marabou and α-β-CROWN, and evaluated it on several benchmarks. Our results show that the inprocessing framework improves the performance of both verifiers. This work suggests several directions for future work. The implication graph is currently exploited through its SAT clo- sure, which captures only the lemmas entailed over binary implications. Propagation redundant (PR) clauses only need to leave satisfiability intact (Heule, Kiesl, and Biere 2017), and harvesting them from the graph, as SDCL does (Heule, Kiesl, and Biere 2019), would derive lemmas no closure can produce. A second direction is to lift inprocessing above the propositional abstraction, reasoning about linear constraints rather than boolean phase variables to prune subproblems and vivify cuts the boolean abstraction cannot. Finally, our lemmas are facts about a network under an input domain, not about the query that produced them. Elsaleh et al. (2026) show such conflicts survive query refinement, so carrying the graph across queries would improve incremental verification. References Bacchus, F.; and Winter, J. 2003. Effective Preprocessing with Hyper-Resolution and Equality Reduction. In Theory and Applications of Satisfiability Testing (SAT), 341–355. Springer. Biere, A.; Faller, T.; Fazekas, K.; Fleury, M.; Froleyks, N.; and Pollitt, F. 2024. CaDiCaL 2.0. In Gurfinkel, A.; and Ganesh, V., eds., Computer Aided Verification - 36th Inter- national Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, volume 14681 of Lecture Notes in Computer Science, 133–152. Springer. Biere, A.; Järvisalo, M.; and Kiesl, B. 2021. Preprocessing in SAT Solving. In Handbook of Satisfiability, chapter 9. IOS Press, 2 edition. Brix, C.; Bak, S.; Johnson, T. T.; and Wu, H. 2024. The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results. arXiv:2412.19985. Brix, C.; Bak, S.; Liu, C.; and Johnson, T. T. 2023. The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results. arXiv:2312.16760. Bunel, R.; Lu, J.; Turkaslan, I.; Torr, P. H.; Kohli, P.; and Kumar, M. P. 2020. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 21(42): 1–39. Davis, L.; Zhou, D.; Zhang, H.; Katz, G.; Barrett, C.; and Wu, H. 2026. Lookahead Branching for Neural Network Verification. arXiv:2607.17290. Eén, N.; and Biere, A. 2005. Effective Preprocessing in SAT Through Variable and Clause Elimination. In Theory and Applications of Satisfiability Testing (SAT), 61–75. Springer. Elsaleh, R.; Davis, L.; Wu, H.; and Katz, G. 2026. Incre- mental Neural Network Verification via Learned Conflicts. arXiv:2603.12232. He, K.; Zhang, X.; Ren, S.; and Sun, J. 2015. Delving deep into rectifiers: Surpassing human-level performance on ima- genet classification. In Proceedings of the IEEE international conference on computer vision, 1026–1034. Heule, M. J. H.; Järvisalo, M.; and Biere, A. 2011. Efficient CNF Simplification Based on Binary Implication Graphs. In Theory and Applications of Satisfiability Testing (SAT), 201–215. Springer. Heule, M. J. H.; Kiesl, B.; and Biere, A. 2017. Short Proofs Without New Variables. In International Conference on Au- tomated Deduction (CADE), 130–147. Springer. Heule, M. J. H.; Kiesl, B.; and Biere, A. 2019. Encoding Redundancy for Satisfaction-Driven Clause Learning. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer. Heule, M. J. H.; Kullmann, O.; Wieringa, S.; and Biere, A. 2011. Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads. In Haifa Verification Conference (HVC), 50– 65. Springer. Isac, O.; Refaeli, I.; Wu, H.; Barrett, C.; and Katz, G. 2026. PICID: Proof-Driven Clause Learning in Neural Network Verification. arXiv:2503.12083. Järvisalo, M.; Heule, M. J. H.; and Biere, A. 2012. Inpro- cessing Rules. In Automated Reasoning (IJCAR), 355–370. Springer. Julian, K. D.; Lopez, J.; Brush, J. S.; Owen, M. P.; and Kochenderfer, M. J. 2016. Policy Compression for Aircraft Collision Avoidance Systems. In 2016 IEEE/AIAA 35th Dig- ital Avionics Systems Conference (DASC), 1–10. Katz, G.; Barrett, C.; Dill, D. L.; Julian, K.; and Kochen- derfer, M. J. 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In International Confer- ence on Computer Aided Verification, 97–117. Katz, G.; Huang, D. A.; Ibeling, D.; Julian, K.; Lazarus, C.; Lim, R.; Shah, P.; Thakoor, S.; Wu, H.; Zeljić, A.; Dill, D. L.; Kochenderfer, M. J.; and Barrett, C. 2019. The Marabou Framework for Verification and Analysis of Deep Neural Networks. In International Conference on Computer Aided Verification, 443–452. Kaulen, K.; Ladner, T.; Bak, S.; Brix, C.; Duong, H.; Flinkow, T.; Johnson, T. T.; Koller, L.; Manino, E.; Nguyen, T. H.; and Wu, H. 2025. The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results. arXiv:2512.19007. Kotha, S.; Brix, C.; Kolter, J. Z.; Dvijotham, K.; and Zhang, H. 2023. Provably Bounding Neural Network Preimages. In Oh, A.; Neumann, T.; Globerson, A.; Saenko, K.; Hardt, M.; and Levine, S., eds., Advances in Neural Information Processing Systems, volume 36, 80270–80290. Curran As- sociates, Inc. LeCun, Y.; Bottou, L.; Bengio, Y.; and Haffner, P. 1998. Gradient-Based Learning Applied to Document Recognition. Proceedings of the IEEE, 86(11): 2278–2324. Li, C.-M.; Xiao, F.; Luo, M.; Manyà, F.; Lü, Z.; and Li, Y. 2020. Clause Vivification by Unit Propagation in CDCL SAT Solvers. Artificial Intelligence, 279: 103197. Luo, M.; Li, C.-M.; Xiao, F.; Manyà, F.; and Lü, Z. 2017. An Effective Learnt Clause Minimization Approach for CDCL SAT Solvers. In International Joint Conference on Artificial Intelligence (IJCAI). Mnih, V.; Kavukcuoglu, K.; Silver, D.; Graves, A.; Antonoglou, I.; Wierstra, D.; and Riedmiller, M. 2013. Play- ing atari with deep reinforcement learning. arXiv preprint arXiv:1312.5602. Piette, C.; Hamadi, Y.; and Saïs, L. 2008. Vivifying Propo- sitional Clausal Formulae. In European Conference on Arti- ficial Intelligence (ECAI). Sallab, A. E.; Abdou, M.; Perot, E.; and Yogamani, S. 2017. Deep reinforcement learning framework for autonomous driving. arXiv preprint arXiv:1704.02532. Shi, Z.; Jin, Q.; Kolter, Z.; Jana, S.; Hsieh, C.-J.; and Zhang, H. 2025. Neural Network Verification with Branch-and- Bound for General Nonlinearities. In International Con- ference on Tools and Algorithms for the Construction and Analysis of Systems, 315–335. Springer. Singh, G.; Gehr, T.; Püschel, M.; and Vechev, M. 2019. An Abstract Domain for Certifying Neural Networks. Proceed- ings of the ACM on Programming Languages, 3(POPL): 1– 30. Wang, S.; Zhang, H.; Xu, K.; Lin, X.; Jana, S.; Hsieh, C.- J.; and Kolter, J. Z. 2021. Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. Advances in Neural Information Processing Systems, 34. 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.; and Barrett, C. 2024. Marabou 2.0: A Versa- tile Formal Analyzer of Neural Networks. In International Conference on Computer Aided Verification, 249–264. Wu, H.; Zeljić, A.; Katz, G.; and Barrett, C. 2022. Effi- cient neural network analysis with sum-of-infeasibilities. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 143–163. Springer. Xu, K.; Shi, Z.; Zhang, H.; Wang, Y.; Chang, K.-W.; Huang, M.; Kailkhura, B.; Lin, X.; and Hsieh, C.-J. 2020. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems, 33. Xu, K.; Zhang, H.; Wang, S.; Wang, Y.; Jana, S.; Lin, X.; and Hsieh, C.-J. 2021. Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Par- allel Incomplete Verifiers. In International Conference on Learning Representations. Zhang, H.; Wang, S.; Xu, K.; Li, L.; Li, B.; Jana, S.; Hsieh, C.- J.; and Kolter, J. Z. 2022a. General Cutting Planes for Bound- Propagation-Based Neural Network Verification. Advances in Neural Information Processing Systems. Zhang, H.; Wang, S.; Xu, K.; Wang, Y.; Jana, S.; Hsieh, C.- J.; and Kolter, Z. 2022b. A Branch and Bound Framework for Stronger Adversarial Attacks of ReLU Networks. In Pro- ceedings of the 39th International Conference on Machine Learning, volume 162, 26591–26604. Zhang, H.; Weng, T.-W.; Chen, P.-Y.; Hsieh, C.-J.; and Daniel, L. 2018. Efficient Neural Network Robustness Cer- tification with General Activation Functions. Advances in Neural Information Processing Systems, 31: 4939–4948. Zhou, D.; Brix, C.; Hanasusanto, G. A.; and Zhang, H. 2024. Scalable Neural Network Verification with Branch- and-bound Inferred Cutting Planes. In The Thirty-eighth Annual Conference on Neural Information Processing Sys- tems. Zhou, D.; Chavez, J.; Chen, H.; Hanasusanto, G. A.; and Zhang, H. 2025. Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verifi- cation. In The Thirty-ninth Annual Conference on Neural Information Processing Systems. A Proofs Proof of Theorem 1. Suppose the oracle computes bound [lb k , ub k ] for neuron k under phase fixes R, and let r ′ be a further fix inconsistent with [lb k , ub k ]. Any point satisfying R ′ = R∪r ′ satisfies R, so its pre-activation k lies in [lb k , ub k ], contradicting r ′ ; thus R ′ is infeasible. Unit lemmas. The algorithm records¬r as a unit lemma ex- actly when the oracle finds r itself infeasible, i.e., the bounds computed under r are already empty. By the argument above,r is globally infeasible. Binary implications. The algorithm adds the edge (r,r ′ j ) exactly when the bounds computed underr already confine ReLU j to phase r ′ j , i.e., every point satisfying Q∧r satisfies r ′ j . The complementary fix¬r ′ j requires j to be in the other phase, which no such point can satisfy, thus Q∧r∧¬r ′ j has no solution. Proof of Theorem 2. r i and¬r i are complementary, so every point of the input domain satisfies one of them, and thus lies in [lb r i k , ub r i k ] or [lb ¬r i k , ub ¬r i k ] for neuron k. Their hull therefore contains every such point. Proof of Theorem 3. Every clause of Σ holds in every model of Q by Theorem 1, and every r ∈ R holds at the node by construction, so a model of Q∧ V r∈R r would satisfy Σ∪R. Since Σ∪ R has no satisfying assignment, no such model exists. Proof of Theorem 4. Since S ′ ⊆ S, every point satisfying Q∧ V r ′ ∈S r ′ satisfiesQ∧ V r ′ ∈S ′ r ′ . Conversely, every clause of Σ holds in every model of Q by Theorem 1, so a point satisfying Q∧ V r ′ ∈S ′ r ′ satisfies Σ∧ V r ′ ∈S ′ r ′ and satisfies r as well. Therefore, it satisfies Q∧ V r ′ ∈S r ′ . The two have the same models, so S ′ is infeasible whenever S is. Proof of Lemma 5. |S ′ | ≤ 2 is immediate, as S ′ is a subset ofa 1 ,a 2 . Consider any assignment satisfying Σ∪S ′ . Each root a i holds under it, either a i ∈ S ′ and it is assumed, or a i is a unit lemma and its clause lies in Σ. The antecedent chain from a i is a sequence of phase fixes in which each is forced by the previous one through an edge of the implication graph, and each such edge contributes the clause (¬r∨ r ′ ) to Σ. Following the chain from a 1 , the assignment therefore satisfies r, and following the chain from a 2 it satisfies ¬r. No assignment does both, so Σ∪ S ′ is unsatisfiable. B Contribution of Each Component Table 5 shows how many times each component of the in- processing framework attempted to fire, how many times it succeeded, and the average number of attempts and successes per benchmark. Table 6 shows the same for α-β-CROWN. Vivification fired nearly every time on Marabou, and some of the time on α-β-CROWN. SAT closure pruned only a small percentage of the subproblems attempted, but this is expected as SAT closure is attempted every search state. For hull bounds, an attempt is an unstable neuron probed and a success is a bound tightening it produced, so the ratio ex- ceeds one where a single neuron tightens several bounds. Overall, on Marabou with the exception of SafeNLP the hull ComponentActive Avg. att. Avg. succ. Succ./att. ACASXu Vivification2718.517.70.96 SAT closure147728.78.00.01 Hull bounds147182.3733.24.02 MNIST Vivification1615.514.40.93 SAT closure160854.06.70.01 Hull bounds160352.71021.92.90 SafeNLP Vivification6127.326.30.96 SAT closure365210.81.50.01 Hull bounds365104.63.00.03 Table 5: Per-component yield on Marabou. ComponentActive Avg. att. Avg. succ. Succ./att. CIFAR CNN-A-Adv Vivification20364.181.10.22 SAT closure27796.346.60.06 Hull bounds27862.6214.10.25 CIFAR CNN-A-Mix Vivification43293.285.90.29 SAT closure551672.563.50.04 Hull bounds551238.5320.60.26 CIFAR CNN-B-Adv Vivification74324.650.50.16 SAT closure845278.988.50.02 Hull bounds842286.1721.30.32 TinyImageNet Vivification84271.2128.10.47 SAT closure1171039.769.40.07 Hull bounds1171700.2589.60.35 Table 6: Per-component yield on α-β-CROWN. bound tightens each unstable neuron multiple times. On α- β-CROWN, the hull bound tightens between 25% and 35% of the unstable neurons. C Additional Cactus Plots Figures 4 through 7 report runtime and domains visited on the Marabou benchmarks, and figures 8 and 9 report the same for α-β-CROWN. Forα-β-CROWN, only UNSAT instances are shown, as its PGD attack solves every SAT instance without entering BaB. Legends report the number of instances solved by each configuration. Figure 4: Cactus plots of runtime on the UNSAT instances of the Marabou benchmarks. Figure 5: Cactus plots of runtime on the SAT instances of the Marabou benchmarks. Figure 6: Cactus plots of domains visited on the UNSAT instances of the Marabou benchmarks. Figure 7: Cactus plots of domains visited on the SAT in- stances of the Marabou benchmarks. Figure 8: Cactus plots of runtime on the UNSAT instances of the α-β-CROWN benchmarks. Figure 9: Cactus plots of domains visited on the UNSAT instances of the α-β-CROWN benchmarks.