Automated Verification of Soundness of DNN Certifiers

TL;DR

This work tackles the problem of ensuring soundness in DNN certifiers used for safety-critical systems, addressing the bottleneck of manual proofs. It introduces ProveSound, a bounded automated verifier that reduces universal soundness conditions to tractable SMT queries via symbolic DNNs and a formal constraint DSL, ConstraintFlow. The authors formalize ConstraintFlow’s syntax, type system, and operational/symbolic semantics, and prove type-soundness and verification soundness/completeness properties. Their evaluation demonstrates automatic soundness verification across existing and novel certifiers, including variants that balance efficiency and precision or introduce new abstract domains and operations. The approach enables rigorous, scalable verification of DNN certifiers across arbitrary architectures, with practical implications for safer AI systems and accelerated certifier development.

Abstract

The uninterpretability of Deep Neural Networks (DNNs) hinders their use in safety-critical applications. Abstract Interpretation-based DNN certifiers provide promising avenues for building trust in DNNs. Unsoundness in the mathematical logic of these certifiers can lead to incorrect results. However, current approaches to ensure their soundness rely on manual, expert-driven proofs that are tedious to develop, limiting the speed of developing new certifiers. Automating the verification process is challenging due to the complexity of verifying certifiers for arbitrary DNN architectures and handling diverse abstract analyses. We introduce ProveSound, a novel verification procedure that automates the soundness verification of DNN certifiers for arbitrary DNN architectures. Our core contribution is the novel concept of a symbolic DNN, using which, ProveSound reduces the soundness property, a universal quantification over arbitrary DNNs, to a tractable symbolic representation, enabling verification with standard SMT solvers. By formalizing the syntax and operational semantics of ConstraintFlow, a DSL for specifying certifiers, ProveSound efficiently verifies both existing and new certifiers, handling arbitrary DNN architectures. Our code is available at https://github.com/uiuc-focal-lab/constraintflow.git

Figures (16)

• Figure 1: DeepPoly specification in ConstraintFlow
• Figure 2: Symbolic DNN creation and expansion for DeepPoly. $\mathcal{P}(n) \equiv (l \leq n \leq u) \wedge (L \leq n \leq U)$
• Figure 3: Soundness of $f^\sharp$ w.r.t. $f$
• Figure 4: SMT query for Soundness of $f^\sharp$ w.r.t. $f$
• Figure 5: A part of the BNF grammar for ConstraintFlow. The complete grammar can be found in Appendix A

Theorems & Definitions (23)

• Definition 2.1
• Lemma 4.1
• Lemma 4.2
• theorem 1
• Definition 5.1
• Definition 5.2
• theorem 2: Soundness
• theorem 3: Completeness
• Lemma \ref{lemma:optype-checking}
• Lemma \ref{lemma:statementtype-checking}