# Property Inference for Deep Neural Networks

## TL;DR

This paper introduces methods to automatically infer formal properties of feed-forward neural networks by analyzing neuron activation patterns, aiding in explanation, robustness, and simplification tasks.

## Contribution

It proposes novel techniques to extract input and layer properties from neural networks based on neuron decision patterns, enhancing interpretability and robustness analysis.

## Key findings

- Effective property extraction for MNIST and ACASXU networks
- Improved explanation and robustness guarantees
- Simplified proofs and network distillation

## Abstract

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.