Branch and Bound for Relational Verification of Neural Networks

Affiliation: Kyushu University, National Institute of Informatics, UNSW Sydney

The paper addresses the verification of neural networks against relational specifications, particularly global robustness, which is crucial for safety-critical applications of cyber-physical systems (CPS). The authors note that most existing works in neural network verification take local robustness as their target, but local robustness has limited expressivity. For example, a neural network controller for an adaptive cruise control system is expected to be globally robust, i.e., given similar environmental inputs, its control actions should not change drastically.

The paper defines global robustness (Definition 3) as follows: "Given a neural network N: Rn → Rm and parameters (ε, δ), let omega = Q 1≤j≤n [omegaj, omegaj] be an n-dim rectangular input space... N is said to be (ε, δ)-globally robust w.r.t. the l-th dimension, if the following condition holds: ∀y, ŷ ∈ omega, ∥y − ŷ∥∞ ≤ ε =⇒ Nl (y) − Nl (ŷ) ≤ δ."

The authors explain that relational verification requires reasoning about multiple inferences, so most existing approaches solve the problem by producing multiple copies of the network, each processing one inference. Existing approximation approaches, such as RaVeN, suffer from a completeness issue, i.e., they may raise false alarms, reporting violations that do not actually exist.

The paper proposes SABRE (Splitting Approximated Bounds for RElational verification), a novel BaB-based verification framework that:

1. Splits relational neurons rather than individual neurons for problem splitting in branch-and-bound

2. Devises a relational neuron selection strategy based on the dual formulation of the verification problem

The authors state: "our BaB framework features splitting of relational neurons rather than individual neurons as prior works do, and as the core of our technique, we devise a relational neuron selection strategy based on the dual formulation of the verification problem, which allows us to efficiently select the (most likely) optimal relational neuron that maximizes the refinement brought by problem splitting."

The paper introduces the concept of relational neurons: the differences ∆yj between corresponding individual neurons constitute additional symbolic nodes, which we call relational neurons. The authors explain that in relational verification, in addition to individual neurons, relational neurons may also be selected to split.

They demonstrate through Example 1 that splitting individual neurons in relational verification may lead to suboptimal performance, compared to splitting relational neuron. Specifically, they show that by branching on the relational neuron ∆x1, the bound of ∆x2 is refined to be [−0.067, 0.15], which is tighter than the result of splitting individual neurons.

The paper defines relational constraints (Definition 5): Given a pair (i, j), a relational constraint φ w.r.t. (i, j) is a proposition either ∆xj(i) ≤ 0 (written as ∆xj(i)−) or ∆xj(i) ≥ 0 (written as ∆xj(i)+).

The verification problem is generalized (Definition 6): "Given a neural network N, a global robustness property identified by (omega, ε, δ), and a relational constraint sequence Φ, a verification problem is to determine whether N satisfies global robustness under the constraint of Φ."

The paper formulates the verification as an LP problem: min ∆yl(L) s.t. Constinp, Constaffn, ConstReLU, Const∆ReLU, Const∆affn, Φ where:

• Constinp denotes constraints related to the input layer

• Constaffn and Const∆affn denote constraints associated with affine transformations

• ConstReLU denotes constraints for ReLU functions in individual neurons

• Const∆ReLU denotes constraints of ReLU function for relational neurons

The proposed Algorithm 1 (R EL BA B) follows a branch-and-bound workflow:

1. Initialize queue Q with the original problem (⊤)

2. Pop a sub-problem and apply ApxVerRel

3. If the output bound exceeds δ, validate the counterexample by feeding it to the network

4. If the counterexample is spurious, select a relational neuron and split it into two sub-problems (positive and negative cases)

5. Recursively process sub-problems until all are verified

The core technical contribution is the dual formulation for relational verification. The authors state: we extend the neuron selection approach BaBSR in classic verification to the relational settings, based on the dual formulation of the LP program.

The derived dual problem is expressed as:

max [omega]−B(0) − [omega]+B(0) + [omega]−Bb(0) − [omega]+Bb(0) − ε[B∆(0)]− − ε[B∆(0)]+ − ΣL−1 i=0 (A(i+1) + Ab(i+1))T b(i) + ΣL−1 i=1 Σj [µj(i)[Bj(i)]− + µbj(i)[Bbj(i)]− + µj+∆(i)[Bj∆(i)]+ + µj−∆(i)[Bj∆(i)]−]

The dual variables are derived by backpropagation: A(L) = Ab(L) = 0, A∆(L) = −C and B(i) = W(i)T A(i+1), Bb(i) = W(i)T Ab(i+1), B∆(i) = W(i)T A∆(i+1).

The neuron selection strategy estimates the improvement in the bounds of relational neurons in the output layer, resulting from splitting a relational neuron by computing the change in the dual objective function before and after splitting.

The evaluation covers 817 verification problems across:

• ACAS Xu (230 instances, 7-layer FNN, 305 neurons, 420s budget)

• MNIST-F (156 instances, 5-layer FNN, 1,034 neurons, 600s budget)

• MNIST-C (156 instances, CNN with 2 Cnv + 2 Lin, 9,518 neurons, 600s budget)

• CIFAR (158 instances, CNN with 2 Cnv + 2 Lin, 4,862 neurons, 1800/3600/7200s budget)

• GTSRB (117 instances, CNN with 2 Cnv + 2 Lin, 6,287 neurons, 1800/3600/7200s budget)

• RaVeN: A state-of-the-art approximation verifier without abstraction refinement

• ClasIS: A BaB approach based on problem splitting of individual neurons with BaBSR-style selection

• DualIS: Splits individual neurons but relies on our dual formulation

• RandRS: An ablation variant of SABRE that retains the relational splitting framework but substitutes the proposed dual-based selection strategy with a uniform random selection

RQ1 (vs. RaVeN): SABRE significantly improves the verification performance compared to RaVeN in terms of the number of solved instances. SABRE solves 67 vs. 42 on ACAS Xu, 54 vs. 31 on MNIST-F, 27 vs. 23 on MNIST-C, 23 vs. 10 on CIFAR, and 33 vs. 9 on GTSRB.

RQ2 (Relational vs. Individual splitting): SABRE consistently outperforms both ClasIS and DualIS on ACAS Xu, MNIST-F, MNIST-C, and GTSRB in terms of the number of solved instances, the number of sub-problems, and verification time ratio. On ACAS Xu, SABRE solves 67 instances while DualIS and ClasIS solve only 9 and 12, respectively.

However, on CIFAR, individual splitting methods outperform SABRE in both solved instances (31 and 28 vs. 23) and time efficiency. The authors investigate this and find that relational splitting is less effective when the relational bounds are small, and becomes more effective as the propagated relational bounds increase. They note that the CIFAR model contains significantly more unstable ReLU neurons along the reasoning path.

RQ3 (Scalability): SABRE exhibits consistent and evident performance advantages over the baseline approaches across different numbers of input dimensions. For p% = 1.0, SABRE records 24 solved instances against 17 and 15 of DualIS and ClasIS.

RQ4 (Neuron selection): Our selection strategy leads to substantial improvements across all benchmarks compared to random selection. On ACAS Xu, our method solves 67 instances, compared to only 44 solved by random selection. On GTSRB, SABRE achieves 33, which is around 4 times compared to 9 of RandRS.

RQ5 (Maximum verifiable perturbation): SABRE consistently achieves the largest certifiable perturbation region across the majority of instances. The statistical analysis shows SABRE holds a consistent advantage over all baselines, with moderate effect sizes ranging from d = 0.26 to d = 0.38.

The paper concludes: "We presented SABRE, a BaB framework for relational neural network verification that splits relational neurons rather than individual neurons, paired with a neuron selection strategy based on dual problem formulation of the relational neuron propagation."

For future work, the authors plan to investigate more refined splitting strategies to achieve tighter relational bounds and design neuron selection heuristic to further improve the efficiency and scalability of verification. They also note an open question: "our current approach selects relational neurons exclusively without considering individual neurons. While it is possible to consider both individual and relational neurons simultaneously, it introduces a non-trivial question about when we should select individual neurons and when we switch back to relational neurons."

Improvement 1: Relational Branch-and-Bound for Multi-Output Consistency in AI Decision-Making

• What to implement: Integrate SABRE’s relational neuron splitting into AI systems that must satisfy pairwise or group-wise output constraints (e.g., fairness, Lipschitz continuity, or safety margins between multiple outputs). Instead of verifying each output independently, the system will branch on differences between neurons (e.g., Δy j = y j - y k) to prune the search space more efficiently.

• Capability gained: The AI can formally certify that for any two inputs within a bounded region, the difference between any two outputs (e.g., class probabilities, control signals) stays within a specified tolerance. This is critical for systems like multi-agent coordination, ensemble models, or controllers with redundant actuators where relative consistency matters more than absolute accuracy.

Improvement 2: Dual-Formulation-Guided Splitting for Faster Counterexample Validation

• What to implement: Use the dual LP formulation from SABRE to compute, for each candidate relational neuron, an upper bound on the improvement in the objective (output bound) if that neuron were split. The AI system will then prioritize splitting the neuron with the highest estimated improvement, rather than using random or heuristic selection.

• Capability gained: The system can verify or falsify global robustness properties with significantly fewer sub-problems (e.g., 3–4× fewer than random selection, as shown on ACAS Xu). This enables real-time verification of safety properties in adaptive systems (e.g., autonomous driving controllers) where computational budget is tight.

Improvement 3: Hybrid Splitting Strategy (Individual + Relational) with Adaptive Switching

• What to implement: Extend SABRE to dynamically choose between splitting individual neurons (classic BaB) and relational neurons, based on the current bound tightness. Use the observation from CIFAR experiments—where relational splitting underperforms when relational bounds are small—to trigger a switch to individual splitting when the relational bound width falls below a threshold.

• Capability gained: The AI system becomes robust across diverse network architectures (e.g., CNNs with many unstable ReLUs vs. FNNs with few). It can automatically adapt its verification strategy to the model’s internal dynamics, achieving higher solved-instance rates on both dense and sparse activation networks.

Improvement 4: Scalable Verification for High-Dimensional Input Spaces

• What to implement: Adopt SABRE’s relational constraint propagation (Definition 5) to handle input spaces with many dimensions (e.g., images, sensor arrays). The system will maintain relational constraints on input differences (Δx j) and use the dual backpropagation to efficiently compute bounds without enumerating all input pairs.

• Capability gained: The AI can certify global robustness for high-dimensional inputs (e.g., 784-pixel MNIST images) within practical time limits (600s), as demonstrated by solving 54 vs. 31 instances over RaVeN. This enables formal guarantees for perception systems in CPS before deployment.

Improvement 5: Counterexample-Guided Refinement with Relational Constraints

• What to implement: When a spurious counterexample is found (i.e., the LP bound exceeds δ but the actual network output does not), the system will use SABRE’s relational neuron selection to add a constraint (Δx j ≤ 0 or ≥ 0) that most tightly separates the spurious region from the true violation region. This replaces naive bisection or random branching.

• Capability gained: The AI system can iteratively refine its verification until either a true violation is found or the property is proven. This is especially useful for adversarial robustness auditing, where the system must distinguish between actual vulnerabilities and approximation artifacts.

Improvement 6: Certifiable Robustness for Neural Network Ensembles

• What to implement: Apply SABRE’s relational framework to verify that an ensemble of networks (e.g., multiple models voting on a class) produces stable outputs under input perturbations. Treat the ensemble’s outputs as relational neurons (e.g., differences between model votes) and use the dual formulation to bound the ensemble’s decision margin.

• Capability gained: The AI can formally certify that an ensemble’s final decision (e.g., majority vote) remains unchanged for all inputs within an ε-ball, even if individual models disagree. This improves reliability in safety-critical applications like medical diagnosis or autonomous navigation where ensemble methods are common.

Improvement 7: Time-Bounded Verification for Online Monitoring

• What to implement: Use SABRE’s branch-and-bound with a time budget (as in the experiments) to return a partial verification result: either “verified safe,” “violation found,” or “unknown within budget.” The system will prioritize sub-problems most likely to yield a definitive answer, based on the dual-based improvement estimates.

• Capability gained: The AI can provide real-time safety guarantees with a tunable trade-off between completeness and latency. This is essential for runtime monitoring of neural network controllers in drones, robots, or industrial automation where a decision must be made within milliseconds.

Verification of neural networks against relational specifications, such as global robustness, is crucial for safety-critical applications of cyber-physical systems (CPS), given their increasing adoption of AI components. Compared to simple trace properties (e.g., local robustness), verifying relational specifications requires reasoning about the relationship between multiple network inferences, which brings significant technical challenges. Existing research has explored abstraction techniques based on sound and convex over-approximation of neural network outputs; however, since these approaches are inherently incomplete and may raise false alarms, they further underscore the need of effective abstraction refinement. In this paper, we propose a branch-and-bound (BaB) framework to mitigate the issue, which iteratively splits the problem until all sub-problems are verified. Specifically, our BaB framework features splitting of relational neurons rather than individual neurons as prior works do, and as the core of our technique, we devise a relational neuron selection strategy based on the dual formulation of the verification problem, which allows us to efficiently select the (most likely) optimal relational neuron that maximizes the refinement brought by problem splitting. We evaluate SaBRe on 817 verification problems across ACAS Xu, MNIST-F, MNIST-C, CIFAR and GTSRB. The results show that SaBRe outperforms different baseline approaches, in terms of the number of solved instances and verification efficiency, which demonstrates the effectiveness of our proposed techniques.