Mon 19 Jun 2023 17:20 - 17:40 at Royal - PLDI: Machine Learning Chair(s): Yaniv David

Complete verification of deep neural networks (DNNs) can exactly determine whether the DNN satisfies a desired trustworthy property (e.g., robustness, fairness) on an infinite set of inputs or not. Despite the tremendous progress to improve the scalability of complete verifiers over the years on individual DNNs, they are inherently inefficient when a deployed DNN is updated to improve its inference speed or accuracy. The inefficiency is because the expensive verifier needs to be run from scratch on the updated DNN. To improve efficiency, we propose a new, general framework for incremental and complete DNN verification based on the design of novel theory, data structure, and algorithms. Our contributions implemented in a tool named IVAN yield an overall geometric mean speedup of 2.4x for verifying challenging MNIST and CIFAR10 classifiers and a geometric mean speedup of 3.8x for the ACAS-XU classifiers over the state-of-the-art baselines.

Mon 19 Jun

Displayed time zone: Eastern Time (US & Canada) change

16:00 - 18:00
PLDI: Machine LearningPLDI Research Papers at Royal
Chair(s): Yaniv David Columbia University

#pldi-mon-1600-ml-royal Discord icon small YouTube icon small

16:00
20m
Talk
Scallop: A Language for Neurosymbolic Programming
PLDI Research Papers
Ziyang Li UPenn, Jiani Huang UPenn, Mayur Naik University of Pennsylvania
DOI
16:20
20m
Talk
Abstract Interpretation of Fixpoint Iterators with Applications to Neural Networks
PLDI Research Papers
Mark Niklas Müller ETH Zurich, Marc Fischer ETH Zurich, Robin Staab ETH Zurich, Martin Vechev ETH Zurich
DOI
16:40
20m
Talk
Register Tiling for Unstructured Sparsity in Neural Network Inference
PLDI Research Papers
Lucas Wilkinson University of Toronto, Kazem Cheshmi McMaster University, Maryam Mehri Dehnavi University of Toronto
DOI
17:00
20m
Talk
Architecture-Preserving Provable Repair of Deep Neural Networks
PLDI Research Papers
Zhe Tao University of California, Davis, Stephanie Nawas University of California, Davis, Jacqueline Mitchell University of California, Davis, Aditya V. Thakur University of California at Davis
DOI Pre-print
17:20
20m
Talk
Incremental Verification of Neural Networks
PLDI Research Papers
Shubham Ugare University of Illinois at Urbana-Champaign, Debangshu Banerjee UIUC, Sasa Misailovic University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign
DOI
17:40
20m
Talk
Prompting Is Programming: A Query Language for Large Language Models
PLDI Research Papers
Luca Beurer-Kellner ETH Zurich, Marc Fischer ETH Zurich, Martin Vechev ETH Zurich
DOI