No Soundness in the Real World: On the Challenges of the Verification of Deployed Neural Networks

The ultimate goal of verification is to guarantee the safety of deployed neural networks. Here, we claim that all the state-of-the-art verifiers we are aware of fail to reach this goal. Our key insight is that theoretical soundness (bounding the full-precision output while computing with floating point) does not imply practical soundness (bounding the floating point output in a potentially stochastic environment). We prove this observation for the approaches that are currently used to achieve provable theoretical soundness, such as interval analysis and its variants. We also argue that achieving practical soundness is significantly harder computationally. We support our claims empirically as well by evaluating several well-known verification methods. To mislead the verifiers, we create adversarial networks that detect and exploit features of the deployment environment, such as the order and precision of floating point operations. We demonstrate that all the tested verifiers are vulnerable to our new deployment-specific attacks, which proves that they are not practically sound.

AI algorithms that can recognize the content of an image can often be very easily misled by a skilled attacker. Such an attacker can design invisible modifications of the image so that the algorithm makes a mistake. For this reason, it is important to carefully examine AI algorithms and prove that they cannot be attacked this way. This is called formal verification.In our work, we argue that formal verification becomes much harder if one considers the technical details of how the computations of an AI algorithm are implemented in the real world, where they run on multiple complex GPUs simultaneously, using non-exact arithmetic. This means that the result of the algorithm might be different every time it is run, even if the input is the same.We show that the formal verification methods that have been proposed up to now all fail in the real world. This is because they focus on an idealized theoretical model of the algorithms. We demonstrate this by designing AI algorithms that are reported to be safe by all the known formal verifiers, yet the algorithms might act maliciously in practice.