  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.
