一句话：提出自动推断前馈神经网络形式化属性的技术，从神经元激活模式中提取蕴含期望输出性质的输入与层属性。
针对神经网络缺乏可理解形式化属性这一问题，论文观察到前馈网络的逻辑在很大程度上体现于神经元激活状态（开或关），因而提出从神经元决策中提取模式作为前提条件，用以蕴含期望的输出性质（如预测为某一类别）。作者给出两类技术：一是提取输入属性，即输入空间上蕴含给定输出属性的凸谓词；二是提取层属性，即隐藏层中捕获的、蕴含期望输出行为的网络性质。方法在面向 MNIST 与 ACASXU 应用的网络上进行了评估，实验表明所推断的属性可用于多种任务，包括解释预测、提供鲁棒性保证、简化证明以及网络蒸馏。
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.