# Solution-aware vs global ReLU selection: partial MILP strikes back for DNN verification

arXiv: https://arxiv.org/abs/2507.23197 · HTML: https://mlsanity.com/paper/2507.23197/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 26 references that are in the map.
- First posted on arXiv 31 Jul 2025.

## Builds on (most cited first, 14 of 14)

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming](https://mlsanity.com/paper/2010.11645/) (2020)
- [The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification](https://mlsanity.com/paper/2006.14076/) (2020)
- [Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition](https://mlsanity.com/paper/2104.06718/) (2021)
- [Efficient Global Robustness Certification of Neural Networks via Interleaving Twin-Network Encoding](https://mlsanity.com/paper/2203.14141/) (2022)

## Built on by (most cited first, 1 of 1)

- [Fast SDP certification of neural networks : towards large multi-class datasets](https://mlsanity.com/paper/2607.03232/) (2026)

## Abstract (arXiv)

To handle complex instances, we revisit a divide-and-conquer approach to break down the complexity: instead of few complex BaB calls, we rely on many small em partial MILP calls. The crucial step is to select very few but very important ReLUs to treat using (costly) binary variables. The previous attempts were suboptimal in that respect. To select these important ReLU variables, we propose a novel em solution-aware ReLU scoring (sf SAS), as well as adapt the BaB-SR and BaB-FSB branching functions as em global ReLU scoring (sf GS) functions. We compare them theoretically as well as experimentally, and sf SAS is more efficient at selecting a set of variables to open using binary variables. Compared with previous attempts, SAS reduces the number of binary variables by around 6 times, while maintaining the same level of accuracy. Implemented in em Hybrid MILP, calling first α,β-CROWN with a short time-out to solve easier instances, and then partial MILP, produces a very accurate yet efficient verifier, reducing by up to 40% the number of undecided instances to low levels (8-15%), while keeping a reasonable runtime (46s-417s on average per instance), even for fairly large CNNs with 2 million parameters.