Having reliable specifications is an unavoidable challenge in achieving verifiable correctness, robustness, and interpretability of AI systems. Existing specifications for neural networks are in the paradigm of data as specification. That is, the local neighborhood centering around a reference input is considered to be correct (or robust). While existing specifications contribute to verifying adversarial robustness, a significant problem in many research domains, our empirical study shows that those verified regions are somewhat tight, and thus fail to allow verification of test set inputs, making them impractical for some real-world applications. To this end, we propose a new family of specifications called neural representation as specification, which uses the intrinsic information of neural networks - neural activation patterns (NAPs), rather than input data to specify the correctness and/or robustness of neural network predictions. We present a simple statistical approach to mining neural activation patterns. To show the effectiveness of discovered NAPs, we formally verify several important properties, such as various types of misclassifications will never happen for a given NAP, and there is no ambiguity between different NAPs. We show that by using NAP, we can verify a significant region of the input space, while still recalling 84% of the data on MNIST. Moreover, we can push the verifiable bound to 10 times larger on the CIFAR10 benchmark. Thus, we argue that NAPs can potentially be used as a more reliable and extensible specification for neural network verification.

翻译：拥有可靠的规范是实现AI系统可验证正确性、鲁棒性和可解释性过程中不可回避的挑战。现有神经网络的规范遵循"数据即规范"的范式，即认为以参考输入为中心的局部邻域是正确的（或鲁棒的）。虽然现有规范有助于验证对抗性鲁棒性（这在许多研究领域都是一个重要问题），但我们的实证研究表明，这些已验证区域较为狭窄，无法涵盖测试集输入的验证需求，因而在部分实际应用中缺乏实用性。为此，我们提出一类新型规范——"神经表征即规范"，它利用神经网络的内在信息——神经激活模式（NAPs），而非输入数据来界定神经网络预测的正确性和/或鲁棒性。我们提出了一种简洁的统计方法来挖掘神经激活模式。为验证所发现NAPs的有效性，我们正式证明了若干重要性质，例如：特定NAP下绝不会发生各类错误分类，且不同NAPs之间不存在歧义。研究表明，使用NAP可验证输入空间的显著区域，同时仍能覆盖MNIST数据集84%的数据。此外，在CIFAR10基准测试中，我们可将可验证边界扩展到原来的10倍。因此，我们认为NAPs有望作为更可靠、更具扩展性的规范用于神经网络验证。