Scalable Neural Network Verification against Geometric  Perturbations via Hölder Optimisation
Yanghao Zhang, Panagiotis Kouvaros, Alessio Lomuscio
Neural Network (NN) verification methods provide local robustnessguarantees for a NN in the dense perturbation space of an input point.A key challenge in this area lies in the scalability of the resultingproblem, leading to large models of interest in applications not beingaddressable by the methods.In this paper we introduce HOVer, a method for the verificationof NNs against geometric perturbations, that uniquely employs a Hilbertspace-filling construction to reduce multidimensional problems tosingle-dimensional ones. The underlying Hölder optimisation, which alsoiteratively refines the estimation for the Hölder constant for constructing the lower bound, theoretically it may converge to a localminimum, thereby resulting in arobustness result being incorrect. However, we show experimentally that thisrisk can be contained in practice by appropriately devised heuristicsin the global optimisation setup. Indeed, unlike recently reportederrors from theoretically sound implementations, we found no incorrectresult by running the technique on a large set of benchmarks fromSoundnessBench and VNN-COMP.To validate the scalability of the approach, we report on extensiveexperiments on large NNs ranging from Resnet34 to Resnet152 and ViTs.These demonstrate the SoA performance of the approach in evaluating withhigh reliability the local robustness of large NNs against geometric perturbations on theImageNet dataset.Beyond image tasks, we show that the method's scalabilityenables  for the first time  robustness assessments for large-scale 3D-NNs in video classification tasks against geometricperturbations for long-sequence input frames on Kinetics/UCF101 datasets.