ConstraintFlow: A DSL for Specification and Verification of Neural Network Analyses

TL;DR

ConstraintFlow is a declarative domain-specific language that simplifies the specification and automatic verification of neural network certifiers, enabling rapid soundness checks for diverse architectures.

Contribution

It introduces a lightweight DSL for defining and verifying abstract interpretation-based DNN certifiers, significantly reducing code complexity and enabling automated soundness verification.

Findings

Automated verification ensures soundness of DNN certifiers within minutes.

DSL simplifies the development of new and existing certifiers.

First-time verification of certifier soundness for arbitrary DNN architectures.

Abstract

We develop a declarative DSL - \cf - that can be used to specify Abstract Interpretation-based DNN certifiers. In \cf, programmers can easily define various existing and new abstract domains and transformers, all within just a few 10s of Lines of Code as opposed to 1000s of LOCs of existing libraries. We provide lightweight automatic verification, which can be used to ensure the over-approximation-based soundness of the certifier code written in \cf for arbitrary (but bounded) DNN architectures. Using this automated verification procedure, for the first time, we can verify the soundness of state-of-the-art DNN certifiers for arbitrary DNN architectures, all within a few minutes.