The Power of Typed Affine Decision Structures: A Case Study

Abstract

TADS are a novel, concise white-box representation of neural networks. In this paper, we apply TADS to the problem of neural network verification, using them to generate either proofs or concise error characterizations for desirable neural network properties. In a case study, we consider the robustness of neural networks to adversarial attacks, i.e., small changes to an input that drastically change a neural networks perception, and show that TADS can be used to provide precise diagnostics on how and where robustness errors a occur. We achieve these results by introducing Precondition Projection, a technique that yields a TADS describing network behavior precisely on a given subset of its input space, and combining it with PCA, a traditional, well-understood dimensionality reduction technique. We show that PCA is easily compatible with TADS. All analyses can be implemented in a straightforward fashion using the rich algebraic properties of TADS, demonstrating the utility of the TADS framework for neural network explainability and verification. While TADS do not yet scale as efficiently as state-of-the-art neural network verifiers, we show that, using PCA-based simplifications, they can still scale to mediumsized problems and yield concise explanations for potential errors that can be used for other purposes such as debugging a network or generating new training samples.

References in corpus (10)

• Adam: A Method for Stochastic Optimization
• Explaining and Harnessing Adversarial Examples
• Explaining Machine Learning Classifiers through Diverse Counterfactual Explanations
• Deep ReLU Networks Have Surprisingly Few Activation Patterns
• An Abstraction-Based Framework for Neural Network Verification
• Automated Verification of Neural Networks: Advances, Challenges and Perspectives
• The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results
• Empirical Studies on the Properties of Linear Regions in Deep Neural Networks
• Exact and Consistent Interpretation for Piecewise Linear Neural Networks: A Closed Form Solution
• MixTrain: Scalable Training of Verifiably Robust Neural Networks