A Formally Verified Robustness Certifier for Neural Networks (Extended Version)

TL;DR

The paper tackles the challenge of giving formal, code-level guarantees for certified robustness of neural networks by implementing a two-stage robustness certifier in Dafny: offline, sound Lipschitz upper bounds are pre-computed and cached, then used at inference to verifiably certify each output against perturbations. It adopts a globally robust framework that computes margin Lipschitz bounds $L_{i,j}$ for output-dimension pairs and tests robustness by ensuring $N(v)[j]-N(v)[i] > \varepsilon L_{i,j}$. The authors identify and address critical vulnerabilities in prior implementations—incorrect Lipschitz estimation, flawed certification, and floating-point imprecision—by using sound operator-norm derivations via Gram iteration and exact rational arithmetic, ultimately delivering a verifiable, executable certifier with practical results on MNIST, Fashion-MNIST, and CIFAR-10. They demonstrate near-parallel performance to unverified baselines while providing formal guarantees, highlighting the method’s value for safety- and security-critical deployments. The work also discusses limitations (dense ReLU models, lack of biases, and floating-point gaps) and outlines future extensions to broader architectures and floating-point bounding techniques.

Abstract

Neural networks are often susceptible to minor perturbations in input that cause them to misclassify. A recent solution to this problem is the use of globally-robust neural networks, which employ a function to certify that the classification of an input cannot be altered by such a perturbation. Outputs that pass this test are called certified robust. However, to the authors' knowledge, these certification functions have not yet been verified at the implementation level. We demonstrate how previous unverified implementations are exploitably unsound in certain circumstances. Moreover, they often rely on approximation-based algorithms, such as power iteration, that (perhaps surprisingly) do not guarantee soundness. To provide assurance that a given output is robust, we implemented and formally verified a certification function for globally-robust neural networks in Dafny. We describe the program, its specifications, and the important design decisions taken for its implementation and verification, as well as our experience applying it in practice.

Figures (8)

• Figure 1: An overview of the Dafny program. Lipschitz bounds are pre-computed and then reused as each model output is certified against a given perturbation bound.
• Figure 2: Generating margin Lipschitz bounds in Dafny.
• Figure 3: Lemmas used to prove \ref{['fig:dafny-GenerateLipschitzBound']}.
• Figure 4: Certification procedure implemented in Dafny.
• Figure 5: Defining operator norms in Dafny.