Mon 19 Jun 2023 18:15 - 18:22 at Cypress 1 - SRC: Poster Session

Growing concerns about the trustworthiness of state-of-the-art Artificial Intelligence (AI) systems hinder their deployment in safety-critical domains such as autonomous driving and healthcare. To tackle this, the field of Certified AI aims to formally certify the trustworthiness of Deep Neural Networks (DNNs). Formal guarantees provide a more reliable metric for assessing the suitability of a DNN for real-world deployment than standard test-set accuracy. Unfortunately, existing certifiers are severely limited in the types of models, properties, and hardware that they can handle. Extending these works to new cases is often error-prone and requires substantial manual effort and expertise, limiting their accessibility to the general users of deep learning frameworks who may not have the necessary background to develop a DNN certifier. To overcome these barriers, we envision a compiler framework that can automatically generate precise, scalable, fast, and memory-efficient code for certifying properties for arbitrary DNNs, optimized for different hardware. As the first step, we propose a DSL called ConstraintFlow to specify DNN certifiers with minimal high-level description. For example, we can specify thousands of lines of intricate C-code of DeepPoly in just 16 lines of ConstraintFlow. The certifier specifications in ConstraintFlow are functional, declarative, and pointer-free making it suitable for advanced compiler optimizations. Further, we also support automatic verification for the correctness of the certifier code to eliminate any algorithmic or implementation errors early in the development process.

Mon 19 Jun

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

18:00 - 19:30
SRC: Poster SessionSRC at Cypress 1
18:00
7m
Poster
An Eager SMT Solver for Algebraic Data Type Queries
SRC
File Attached
18:07
7m
Poster
A Synchronization Mechanism for an Accelerator Design IR
SRC
Pai Li Cornell University, USA
Media Attached
18:15
7m
Poster
ConstraintFlow: A Declarative DSL for Certified Artificial Intelligence
SRC
Media Attached
18:22
7m
Poster
Distributions for Compositionally Differentiating Parametric Discontinuities
SRC
Jesse Michel Massachusetts Institute of Technology
Media Attached
18:30
7m
Poster
Formal Verification of a MIR-to-MIR optimisation
SRC
Media Attached
18:37
7m
Poster
Formal verification of approximate differential privacy via the characteristic function
SRC
Media Attached
18:45
7m
Poster
Leveraging Far Memory for Data-Intensive Processing: A Hotness-Segregated Heap Approach
SRC
Dat Nguyen Texas A & M University
File Attached
18:52
7m
Poster
On lightweight Hoare logic of probabilistic programs: a bound tighter than the union bound
SRC
Xingyu Xie Tsinghua University
Media Attached
19:00
7m
Poster
Prettybird: A DSL for Programmatic Font Compilation
SRC
Charles Averill University of Texas at Dallas
Media Attached
19:07
7m
Poster
Quantum Simulation using Context-Free-Language Ordered Binary Decision Diagrams
SRC
Media Attached
19:15
7m
Poster
Resource Sharing through Control-Flow Based Optimizations
SRC
Media Attached
19:22
7m
Poster
Scaling Decision-Theoretic Probabilistic Programs Through Factorization
SRC
Minsung Cho Northeastern University
Media Attached