Tighter Abstract Queries in Neural Network Verification
Tighter Abstract Queries in Neural Network Verification
复制标题
DOI：
10.48550/arxiv.2210.12871
复制
发表时间：
2022-10
期刊：
影响因子：
--
通讯作者：
Elazar Cohen;Y. Elboher;Clark W. Barrett;Guy Katz
中科院分区：
文献类型：
--
作者：
Elazar Cohen;Y. Elboher;Clark W. Barrett;Guy Katz
神经网络已经成为计算机科学各个领域中反应系统的关键组成部分。尽管它们表现出色，但使用神经网络会带来许多风险，这些风险源于我们缺乏理解和推理它们行为的能力。由于这些风险，已经提出了各种形式化的方法来验证神经网络;但不幸的是，这些方法通常会遇到可扩展性障碍。最近的尝试表明，抽象-细化方法可以在减轻这些限制方面发挥重要作用;但这些方法通常会产生非常抽象的网络，以至于它们变得不适合验证。为了解决这个问题，我们提出了CEGARETTE，一种新的验证机制，系统和属性同时被抽象和细化。我们观察到，这种方法使我们能够生成既小又足够准确的抽象网络，从而允许快速验证时间，同时避免大量的细化步骤。为了评估的目的，我们实现了CEGARETTE作为最近提出的CEGAR-NN框架的扩展。我们的结果非常有希望，并在多个基准测试中表现出显着的性能改善。
Neural networks have become critical components of reactive systems in various do- mains within computer science. Despite their excellent performance, using neural networks entails numerous risks that stem from our lack of ability to understand and reason about their behavior. Due to these risks, various formal methods have been proposed for verify- ing neural networks; but unfortunately, these typically struggle with scalability barriers. Recent attempts have demonstrated that abstraction-refinement approaches could play a significant role in mitigating these limitations; but these approaches can often produce net- works that are so abstract, that they become unsuitable for verification. To deal with this issue, we present CEGARETTE, a novel verification mechanism where both the system and the property are abstracted and refined simultaneously. We observe that this approach allows us to produce abstract networks which are both small and sufficiently accurate, allowing for quick verification times while avoiding a large number of refinement steps. For evaluation purposes, we implemented CEGARETTE as an extension to the recently proposed CEGAR-NN framework. Our results are highly promising, and demonstrate a significant improvement in performance over multiple benchmarks.