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.

翻译：本文提出一种代数方法，用于对整流神经网络（分段线性神经网络（PLNNs）的子类，即语义上表示分段仿射函数的网络）进行精确且全局的验证与解释。该方法的核心是对这些网络进行符号执行，从而构建语义等价的类型化仿射决策结构（TADS）。由于TADS具有确定性和序列性，类似于决策树，可被视为白箱模型，因此能够为模型与结果解释问题提供精确解决方案。TADS是线性代数结构，可优雅地比较整流神经网络的等价性或相似性（在失败时提供精确诊断信息），并通过精确刻画特定分类的输入集或两个基于网络的分类器存在差异的输入集来表征其分类潜力。所有现象均通过一个最小化且具说明性的示例——连续XOR函数——的详细讨论进行阐释。