How to verify neural networks without checking every neuron?

Verifying that neural networks behave safely requires computing tight linear bounds around their nonlinear operations. Current methods either bound each neuron individually (fast but loose) or all neurons together (tight but slow). This work picks a strategic subset of neurons for joint analysis, balancing precision and speed. Integrated into Marabou, the approach outperforms existing bound-tightening methods without the full computational cost.