The uninterpretability of DNNs hinders their deployment to safety-critical applications. Recent works have shown that Abstract-Interpretation-based formal certification techniques provide promising avenues for building trust in DNNs to some extent. The intricate mathematical background of Abstract Interpretation poses two challenges: (i) easily designing the algorithms that capture the intricate DNN behavior by balancing cost vs. precision tradeoff, and (ii) maintaining the over-approximation-based soundness of these certifiers. General-purpose programming languages like C++ provide extensive functionality, however, verifying the soundness of the algorithms written in them can be impractical. The most commonly used DNN certification libraries like auto_LiRPA and ERAN prove the correctness of their analyses. However, they consist of only a few hard-coded abstract domains and abstract transformers (or transfer functions) and do not allow the user to define new analyses. Further, these libraries can handle only specific DNN architectures. To address these issues, we develop a declarative DSL -- ConstraintFlow -- that can be used to specify Abstract Interpretation-based DNN certifiers. In ConstraintFlow, 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 also provide lightweight automatic verification, which can be used to ensure the over-approximation-based soundness of the certifier code written in ConstraintFlow 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. We prove the soundness of our verification procedure and the completeness of a subset of ConstraintFlow.

翻译：深度神经网络的不可解释性阻碍了其在安全攸关应用中的部署。近期研究表明，基于抽象诠释的形式化验证技术在一定程度上为建立对DNN的信任提供了有前景的途径。然而，抽象诠释深厚的数学背景带来了两大挑战：（i）通过权衡成本与精度，便捷地设计捕捉DNN复杂行为的算法；（ii）维持这些验证器基于过近似的可靠性。通用编程语言（如C++）虽提供了丰富的功能，但验证用其编写的算法的可靠性往往不切实际。当下最常用的DNN验证库（如auto_LiRPA和ERAN）虽然证明了其分析的正确性，但仅包含少数硬编码的抽象域和抽象转移函数，且不允许用户定义新的分析方法；此外，这些库仅能处理特定架构的DNN。为解决上述问题，我们开发了一种声明式领域特定语言——ConstraintFlow——用于指定基于抽象诠释的DNN验证器。借助ConstraintFlow，程序员可轻松定义各类现有及新型抽象域与转换器，且仅需数十行代码即可完成（传统库则需数千行代码）。我们还提供轻量级自动验证机制，可确保用ConstraintFlow编写的验证器代码在任意（有界）DNN架构下均满足基于过近似的可靠性。通过这一自动验证流程，我们首次得以在数分钟内验证任意DNN架构下最先进DNN验证器的可靠性。我们证明了该验证流程的可靠性以及ConstraintFlow子集的完备性。