Coursera Spring Sale
40% Off Coursera Plus Annual!
Grab it
Explore a 14-minute conference presentation from OOPSLA 2025 that introduces ProveSound, a groundbreaking automated verification procedure for ensuring the soundness of Deep Neural Network (DNN) certifiers. Learn how researchers from the University of Illinois at Urbana-Champaign address the critical challenge of verifying DNN certifiers used in safety-critical applications, where unsoundness in mathematical logic can lead to incorrect and potentially dangerous results. Discover the innovative concept of symbolic DNNs that enables ProveSound to transform complex universal quantification problems over arbitrary DNN architectures into tractable symbolic representations verifiable by standard SMT solvers. Understand how the formalization of ConstraintFlow, a domain-specific language for specifying certifiers, allows for efficient verification of both existing and newly developed certifiers across diverse DNN architectures. Gain insights into how this automated approach overcomes the limitations of manual, expert-driven proofs that previously hindered the rapid development of new DNN certifiers, and examine the practical implications for building trust in deep learning systems deployed in safety-critical environments.
