Click here to flash read.
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.
