Faster Verified Explanations for Neural Networks

TL;DR

FaVeX is a new algorithm that significantly speeds up verified explanations for neural networks by combining batch and sequential processing and reusing previous information, enabling explanations for large networks.

Contribution

The paper introduces FaVeX, a novel scalable algorithm for verified explanations, and a hierarchical definition of verifier-optimal explanations that accounts for verifier limitations.

Findings

FaVeX outperforms existing methods in scalability.

It enables formal explanations for networks with hundreds of thousands of activations.

Verifier-optimal explanations improve explanation quality considering verifier limitations.

Abstract

Verified explanations are a principled way to explain the decisions taken by neural networks, which are otherwise black-box in nature. However, these techniques face significant scalability challenges, as they require multiple calls to neural network verifiers, each of them with an exponential worst-case complexity. We present FaVeX, a novel algorithm to compute verified explanations. FaVeX accelerates the computation by dynamically combining batch and sequential processing of input features, and by reusing information from previous queries, both when proving invariances with respect to certain input features, and when searching for feature assignments altering the prediction. Furthermore, we present a novel and hierarchical definition of verified explanations, termed verifieroptimal robust explanations, that explicitly factors the incompleteness of network verifiers within the explanation. Our comprehensive experimental evaluation demonstrates the superior scalability of both FaVeX, and of verifier-optimal robust explanations, which together can produce meaningful formal explanation on networks with hundreds of thousands of non-linear activations.