Formal Reasoning About Confidence and Automated Verification of Neural Networks

TL;DR

This paper introduces a unified framework for verifying neural networks' robustness and confidence, using a new grammar and verification technique that enhances existing tools and scales to large networks.

Contribution

It presents a novel, expressive grammar for confidence-based specifications and a unified verification method that integrates with existing neural network verification tools.

Findings

Outperforms ad-hoc encoding approaches significantly

Successfully verifies large networks with up to 138 million parameters

Demonstrates scalability and effectiveness on extensive benchmarks

Abstract

In the last decade, a large body of work has emerged on robustness of neural networks, i.e., checking if the decision remains unchanged when the input is slightly perturbed. However, most of these approaches ignore the confidence of a neural network on its output. In this work, we aim to develop a generalized framework for formally reasoning about the confidence along with robustness in neural networks. We propose a simple yet expressive grammar that captures various confidence-based specifications. We develop a novel and unified technique to verify all instances of the grammar in a homogeneous way, viz., by adding a few additional layers to the neural network, which enables the use any state-of-the-art neural network verification tool. We perform an extensive experimental evaluation over a large suite of 8870 benchmarks, where the largest network has 138M parameters, and show that this outperforms ad-hoc encoding approaches by a significant margin.