Research map / Learning theory and algorithms / Combinatorial and search optimization

Dynamic Algorithm Termination for Branch-and-Bound-based Neural Network Verification

AAAI 2025 · Learning theory and algorithms › Combinatorial and search optimization · approach: Semidefinite relaxations for verification · 3 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Predicts, via random forest timeout classifiers on static and dynamic BaB features, which neural network verification runs will time out, and terminates them early to save compute.

Problem

Branch-and-bound neural network robustness verification is computationally expensive, and it is unknown a priori which instances can be solved within a time budget, leading to wasted compute on unsolvable instances.

Approach

Running time (timeout) prediction with cheaply computable static and dynamic BaB features, with a classifier per checkpoint that dynamically terminates runs predicted to exceed the cutoff, controlled by a confidence threshold θ.

Key results

• Dynamic termination reduces total running time to 36% of the standard procedure on average (a 64% reduction) while solving a comparable number of instances.
• Timeout classifiers averaged 84% TPR and 5% FPR across verifiers and benchmarks at θ=0.99 (per-verifier averages in Table 2).
• The largest acceleration occurred on the Marabou benchmark, where up to 95% of standard running time could be saved.

Measured effects reported in the paper

Surprising findings

• Solved-instance loss is small but nonzero: e.g., Conv Small with αβ-CROWN loses 10 solved instances while saving 20% running time relative to standard (Table 3 shows 969 vs 979 solved).

Limitations

• Lower TPR on Conv Big and Conv Small due to few timeouts and little training data for the timeout class.
• Higher FPR on Marabou benchmark due to few queries solved after the first checkpoint.
• Evaluated only on αβ-CROWN, VeriNet and Oval; MN-BaB was excluded.

Experimental setup

Datasets: MNIST CIFAR-10 CIFAR-100 Tiny ImageNet VNN-COMP benchmarks ERAN benchmarks

Benchmarks: 5 100 8 100 Conv Big Conv Small ResNet 2B Marabou Oval21 ViT SRI ResNet A CIFAR-100 Tiny ImageNet

Metrics: accuracy true positive rate false positive rate running time (GPU hours) number of solved instances

Baselines: standard verification procedure (no termination) αβ-CROWN VeriNet Oval

Builds on: Empirical hardness models (Hutter et al. 2014) branch and bound verification CROWN auto-sklearn

Closest papers by meaning

• Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification (NeurIPS 2025 · similarity 0.86)
• Solving Probabilistic Verification Problems of Neural Networks using Branch and Bound (ICML 2025 · similarity 0.85)
• Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes (NeurIPS 2024 · similarity 0.85)
• Stress-Testing Neural Network Verifiers with Provably Robust Instances (NeurIPS 2026 · similarity 0.85)
• Dynamic Back-Substitution in Bound-Propagation-Based Neural Network Verification (AAAI 2025 · similarity 0.85)
• VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees (ICML 2024 · similarity 0.85)