  In this paper we present an algebraic approach to the precise and global
verification and explanation of Rectifier Neural Networks, a subclass of
Piece-wise Linear Neural Networks (PLNNs), i.e., networks that semantically
represent piece-wise affine functions. Key to our approach is the symbolic
execution of these networks that allows the construction of semantically
equivalent Typed Affine Decision Structures (TADS). Due to their deterministic
and sequential nature, TADS can, similarly to decision trees, be considered as
white-box models and therefore as precise solutions to the model and outcome
explanation problem. TADS are linear algebras which allows one to elegantly
compare Rectifier Networks for equivalence or similarity, both with precise
diagnostic information in case of failure, and to characterize their
classification potential by precisely characterizing the set of inputs that are
specifically classified or the set of inputs where two network-based
classifiers differ. All phenomena are illustrated along a detailed discussion
of a minimal, illustrative example: the continuous XOR function.
