Neuro-Symbolic Verification of Deep Neural Networks
This addresses the problem of verifying safety-critical properties in deep neural networks for applications such as autonomous systems, representing a novel extension rather than an incremental improvement.
The paper tackles the limitation of current neural network verification tools, which only handle first-order constraints, by introducing a neuro-symbolic verification framework that enables verification of complex real-world properties like autonomous vehicle safety, and demonstrates its implementation on existing infrastructure.
Formal verification has emerged as a powerful approach to ensure the safety and reliability of deep neural networks. However, current verification tools are limited to only a handful of properties that can be expressed as first-order constraints over the inputs and output of a network. While adversarial robustness and fairness fall under this category, many real-world properties (e.g., "an autonomous vehicle has to stop in front of a stop sign") remain outside the scope of existing verification technology. To mitigate this severe practical restriction, we introduce a novel framework for verifying neural networks, named neuro-symbolic verification. The key idea is to use neural networks as part of the otherwise logical specification, enabling the verification of a wide variety of complex, real-world properties, including the one above. Moreover, we demonstrate how neuro-symbolic verification can be implemented on top of existing verification infrastructure for neural networks, making our framework easily accessible to researchers and practitioners alike.