Property Inference for Deep Neural Networks
This work addresses the need for interpretability and verification in deep learning, particularly for safety-critical domains, but it is incremental as it builds on existing property inference methods.
The paper tackles the problem of automatically inferring formal properties of feed-forward neural networks by extracting patterns based on neuron activation status, and it demonstrates the techniques on MNIST and ACASXU applications for tasks like explaining predictions and providing robustness guarantees.
We present techniques for automatically inferring formal properties of feed-forward neural networks. We observe that a significant part (if not all) of the logic of feed forward networks is captured in the activation status ('on' or 'off') of its neurons. We propose to extract patterns based on neuron decisions as preconditions that imply certain desirable output property e.g., the prediction being a certain class. We present techniques to extract input properties, encoding convex predicates on the input space that imply given output properties and layer properties, representing network properties captured in the hidden layers that imply the desired output behavior. We apply our techniques on networks for the MNIST and ACASXU applications. Our experiments highlight the use of the inferred properties in a variety of tasks, such as explaining predictions, providing robustness guarantees, simplifying proofs, and network distillation.