论文标题
深神经网络的神经符号验证
Neuro-Symbolic Verification of Deep Neural Networks
论文作者
论文摘要
正式验证已成为确保深神经网络的安全性和可靠性的强大方法。但是，当前的验证工具仅限于少数属性，这些属性可以作为网络输入和输出的一阶约束表示。尽管对抗性的鲁棒性和公平性属于这一类别，但许多现实世界的属性（例如，“自动驾驶汽车必须停在停车标志前”）仍然超出了现有验证技术的范围。为了减轻这种严重的实际限制，我们引入了一个新的框架，用于验证神经网络，名为Neuro-Symbolic验证。关键思想是将神经网络用作原本逻辑规范的一部分，以验证各种复杂的现实世界属性，包括上述属性。此外，我们证明了如何在现有的神经网络验证基础架构上实施神经符号验证，使研究人员和从业人员都可以轻松访问我们的框架。
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.
