The neural network has become an integral part of modern software systems. However, they still suffer from various problems, in particular, vulnerability to adversarial attacks. In this work, we present a novel program reasoning framework for neural-network verification, which we refer to as symbolic reasoning. The key components of our framework are the use of the symbolic domain and the quadratic relation. The symbolic domain has very flexible semantics, and the quadratic relation is quite expressive. They allow us to encode many verification problems for neural networks as quadratic programs. Our scheme then relaxes the quadratic programs to semidefinite programs, which can be efficiently solved. This framework allows us to verify various neural-network properties under different scenarios, especially those that appear challenging for non-symbolic domains. Moreover, it introduces new representations and perspectives for the verification tasks. We believe that our framework can bring new theoretical insights and practical tools to verification problems for neural networks.
翻译:神经网络已成为现代软件系统不可或缺的一部分。然而,它们仍然存在各种问题,尤其是对对抗攻击的脆弱性。在这项工作中,我们提出了一种新颖的神经网络验证程序推理框架,我们称之为符号推理。我们框架的关键组成部分是使用符号域和二次关系。符号域具有非常灵活的语义,二次关系非常表达式强。它们允许我们将许多神经网络验证问题编码为二次规划问题。然后,我们的方案将二次规划问题松弛为半定规划问题,这些问题可以被有效地解决。该框架允许我们在不同情况下验证各种神经网络属性,尤其是对于非符号域来说可能具有挑战性的属性。此外,它为验证任务引入了新的表示和视角。我们相信,我们的框架可以为神经网络的验证问题带来新的理论见解和实用工具。