ConstraintFlow: A Declarative DSL for Certified Artificial Intelligence
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.