一句话：提出 ProveSound，通过符号化 DNN 将 DNN 认证器的健全性验证归约为 SMT 可处理问题，实现任意架构认证器的自动验证。
DNN 难以解释，限制其在安全关键场景中的应用；基于抽象解释的 DNN 认证器可提升可信度，但其数学逻辑若不健全会产生错误结论。目前保证健全性依赖专家手工证明，开发新认证器缓慢。本文提出 ProveSound，自动验证任意 DNN 架构下认证器的健全性。核心是符号 DNN 概念：它将“对所有 DNN 成立”的健全性性质归约为可处理的符号表示，从而用标准 SMT 求解器验证。作者还形式化了 ConstraintFlow（一种指定认证器的 DSL）的语法与操作语义，使 ProveSound 能高效验证已有和新的认证器。代码已开源。
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
@article{paperbot3175,
title = {Automated Verification of Soundness of DNN Certifiers},
author = {Avaljot Singh and Yasmin Chandini Sarita and Charith Mendis and Gagandeep Singh},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720509}
}