CS Compiler Seminar: Avaljot Singh, "Automated Verification of Soundness of DNN Certifiers."

Event Type

Seminar/Symposium

Sponsor

CS 591 ACT

Location

3102 Siebel Center

Virtual

Join online

Date

Oct 9, 2025   4:00 - 5:00 pm  

Speaker

Avaljot Singh

Contact

Allison Mette

E-Mail

agk@illinois.edu

Views

4

Originating Calendar

Siebel School Speakers Calendar

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 the development of 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.

Bio: Avaljot Singh is a CS Ph.D. student at the University of Illinois Urbana-Champaign (UIUC), advised by Prof. Gagandeep Singh and Prof. Charith Mendis. He works at the intersection of Artificial Intelligence and Formal Methods. His current research focusses on ConstraintFlow, a DSL for DNN certifiers that enables high-level declarative specifications to be verified for soundness and compiled into executables. He is also currently exploring how LLMs can support program analysis and theorem proving, with a broader interest in advancing the synergy between AI and Formal Methods to build efficient and trustworthy systems.