Neural networks have become critical components of reactive systems in various domains 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 verifying 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 networks 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 very promising, and demonstrate a significant improvement in performance over multiple benchmarks.

翻译：神经网络已成为计算机科学各领域中反应式系统的关键组件。尽管性能卓越，但由于我们缺乏理解和推理其行为的能力，使用神经网络会带来诸多风险。针对这些风险，研究者已提出多种形式化方法用于神经网络验证；但遗憾的是，这些方法通常受限于可扩展性瓶颈。近期尝试表明，抽象精炼方法在缓解这些局限方面可发挥重要作用；然而这类方法生成的网络往往过于抽象，以致不再适用于验证。为应对此问题，我们提出CEGARETTE——一种新颖的验证机制，其中系统和属性同时被抽象和精炼。我们观察到，该方法能够生成既精简又足够精确的抽象网络，从而在实现快速验证的同时避免大量精炼步骤。为进行评估，我们将CEGARETTE作为扩展模块集成到近期提出的CEGAR-NN框架中。实验结果令人振奋，多项基准测试表明该方法在性能上实现了显著提升。