Motivated by the need to reliably characterize the robustness of deep neural networks, researchers have developed neural network verification algorithms. The verifiers aspire to answer whether certain properties are guaranteed with respect to all inputs in a space for a neural network. However, many verifiers inaccurately model floating point arithmetic but do not fully discuss the consequences.

We show that the negligence of floating point error leads to unsound verification that can be systematically exploited in practice. For a pretrained neural network, we present a method that efficiently searches inputs as witnesses for the incorrectness of robustness claims made by a complete verifier. We also present a method to construct neural network architectures and weights that induce wrong results of an incomplete verifier. Our results highlight that, to achieve practically reliable verification of neural networks, any verification system must accurately (or conservatively) model the effects of any floating point computations in the network inference or verification system.