Research map / Learning theory and algorithms / Combinatorial and search optimization
Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes
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.
Proposes BICCOS, which infers cutting planes from UNSAT subproblems during branch-and-bound, strengthens them by dropping split neurons, and uses multi-tree search to scale neural network verification without MIP solvers.
Problem
Neural network verification with branch-and-bound is slow; existing cutting-plane methods (GCP-CROWN) rely on generic MIP-solver cuts that do not scale to large networks.
Approach
Derive problem-specific cuts from verified (UNSAT) BaB subproblems that forbid infeasible combinations of ReLU states, strengthen them by removing unnecessary split neurons using influence scores and dual variables, and share them across the search tree, with a BFS-based multi-tree presolving step to find more cuts.
Key results
- On cifar100-2024 BICCOS verifies 125 instances vs 119 for β-CROWN and 119 for GCP-CROWN (MIP cuts), which cannot scale to these models.
- On SDP-FO CNN-B-Adv (CIFAR, ε=2/255), BICCOS (auto) reaches 54.5% verified accuracy vs 47.5% for β-CROWN and 49.0% for GCP-CROWN with MIP cuts.
- On oval22 BICCOS verifies 26 of 27 upper-bound instances, and on tinyimagenet-2024 it verifies 140 vs 135 for β-CROWN.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use BICCOS instead of β-CROWN | Neural network verification · oval22 | # verified: 20 -> 26 | Helped |
| Use BICCOS instead of β-CROWN | Neural network verification · cifar100-tinyimagenet-2022 | # verified: 69 -> 72 | Helped |
| Use BICCOS instead of β-CROWN | Neural network verification · cifar100-2024 | # verified: 119 -> 125 | Helped |
| Use BICCOS instead of β-CROWN | Neural network verification · tinyimagenet-2024 | # verified: 135 -> 140 | Helped |
| Add multi-tree search to base BICCOS (ablation) | BICCOS · CIFAR CNN-B-Adv | Ver.%: 52.0 -> 52.5 | Helped |
| Add multi-tree search to base BICCOS (ablation) | BICCOS · cifar100-2024 | Ver.%: 62.5 -> 61.5 | Hurt |
| Add multi-tree search to base BICCOS (ablation) | BICCOS · tinyimagenet-2024 | Ver.%: 70.0 -> 70.0 | No clear effect |
| Enable adaptive configuration (MTS and/or MIP cuts) rather than base BICCOS (ablation) | BICCOS · CIFAR CNN-B-Adv | Ver.%: 52.0 -> 54.5 | Helped |
| Enable adaptive configuration (MTS and/or MIP cuts) rather than base BICCOS (ablation) | BICCOS · cifar100-2024 | Ver.%: 62.5 -> 62.5 | No clear effect |
| Enable adaptive configuration (MTS and/or MIP cuts) rather than base BICCOS (ablation) | BICCOS · tinyimagenet-2024 | Ver.%: 70.0 -> 70.0 | No clear effect |
Surprising findings
- BICCOS with BaB-inferred cuts alone is not beneficial unless constraints are strengthened, since naive inferred cuts from the regular BaB process do not tighten other subproblems.
- CPLEX could not solve the initial LP relaxation within 200s on CIFAR100 and Tiny-ImageNet models, so MIP-based cut generation never starts for these networks.
Limitations
- Applies only to piecewise linear ReLU networks; extension to other architectures needs further work.
- Effectiveness of cuts varies with network structure and complexity; some benchmarks show little gain.
- Overhead from multi-tree search and strengthening can slow easy instances under short timeouts.
Experimental setup
Datasets: MNIST CIFAR-10 VNN-COMP benchmarks (oval22, cifar100-tinyimagenet-2022, cifar100-2024, tinyimagenet-2024) SDP-FO benchmark models
Benchmarks: VNN-COMP oval22 cifar100-tinyimagenet-2022 cifar100-2024 tinyimagenet-2024 SDP-FO MNIST/CIFAR models
Metrics: number of verified instances verified accuracy average verification time number of cuts domains visited
Baselines: β-CROWN GCP-CROWN with MIP cuts Venus2 MN-BaB PRIMA VeriNet PyRAT Marabou nnenum ERAN OVAL
Builds on: GCP-CROWN β-CROWN α,β-CROWN Planet relaxation filtered smart branching
Closest papers by meaning
- Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification (NeurIPS 2025 · similarity 0.91)
- SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming (ICML 2025 · similarity 0.89)
- Learning Cut Generating Functions for Integer Programming (NeurIPS 2024 · similarity 0.87)
- Dynamic Back-Substitution in Bound-Propagation-Based Neural Network Verification (AAAI 2025 · similarity 0.86)
- Rethinking the Capacity of Graph Neural Networks for Branching Strategy (NeurIPS 2024 · similarity 0.86)
- Dynamic Algorithm Termination for Branch-and-Bound-based Neural Network Verification (AAAI 2025 · similarity 0.85)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.