Abstract Interpretation-Based Certification of Hyperproperties for High-Stakes Machine Learning Software

Abstract

The tutorial will guide participants through the use of abstract interpretation-based static analysis for the certification of hyperproperties of machine learning models. A neural network surrogate from a real-world avionics use case will serve as a running example throughout the session. The design of the static analysis will proceed systematically, beginning from the formal semantics definitions tailored to the property of interest, an instance of abstract non-interference. We will then overview various existing (combinations of) abstractions, exemplifying some of their lesser-known characteristics. Finally, we will address practical implementation challenges, ensuring a comprehensive demonstration that abstract interpretation can effectively be used to certify critical properties of high-stakes machine learning applications.