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.

翻译：神经网络已成为现代软件系统中不可或缺的组成部分。然而，它们仍面临各种问题，尤其是对对抗性攻击的脆弱性。本文提出了一种新颖的神经网络验证程序推理框架，我们称之为符号推理。该框架的核心组件是符号域和二次关系的使用。符号域具有非常灵活的语义，而二次关系则具有相当强的表达能力。这两者使我们能够将许多神经网络验证问题编码为二次规划。随后，我们的方案将二次规划松弛为可高效求解的半定规划。该框架使我们能够在不同场景下验证神经网络的各种属性，尤其是那些对非符号域而言具有挑战性的属性。此外，它为验证任务引入了新的表示方式和视角。我们相信，该框架能为神经网络的验证问题带来新的理论见解和实用工具。