Semidefinite Bound Propagation for Neural Network Verification with General Activations

Linear bound propagation enables scalable neural network verification by propagating linear bounds through activation functions, but these bounds can lose tightness for general activations. The semidefinite bound propagation method SDP-CROWN strengthens these bounds while retaining efficient linear bound propagation, but its construction relies on a quadratic outer approximation derived from ReLU's piecewise linear structure. We extend semidefinite bound propagation to general activations using quadratic outer approximations derived from sector bounds and quadratic bounds. Our construction converts these constraints into optimizable linear bounds over ellipsoidal domains, which we refine recursively using the same semidefinite bound-propagation framework. The resulting linear bounds integrate directly into the standard bound-propagation recursion, enabling scalable verification against both ${\ell }_{\infty }$ and ${\ell }_2$ adversaries. Our experiments demonstrate substantial improvements in verification performance across all benchmarks with general activations. On representative benchmarks, our method improves verified accuracy over GenBaB from 12% to 57% on MNIST under ${\ell }_2$ perturbations and from 23% to 87% on CIFAR-10 under ${\ell }_{\infty }$ perturbations.