Input-Relational Verification of Deep Neural Networks

Explore a 17-minute video presentation from PLDI 2024 on input-relational verification of deep neural networks. Delve into the novel concept of difference tracking introduced by researchers from the University of Illinois at Urbana-Champaign and VMware Research. Learn about the DiffPoly abstract domain designed for efficient difference tracking in large DNNs, and discover how it enables precise linear cross-execution constraints. Examine the implementation of RaVeN, an input-relational verifier for DNNs that utilizes DiffPoly and linear program formulations to handle various input-relational properties. Gain insights into experimental results demonstrating RaVeN's superior precision over baselines across multiple datasets, networks, and input-relational properties. Access supplementary materials, including the article, archive, and web page for further exploration of this innovative approach to DNN verification.

[PLDI24] Input-Relational Verification of Deep Neural Networks