Tutorial: Safe, Secure, and Trustworthy Artificial Intelligence (AI) via Formal Verification of Neural Networks and Autonomous Cyber-Physical Systems (CPS) with NNV

Ensuring safe, secure, and trustworthy artificial intelligence (AI), particularly within safety-critical systems like autonomous cyber-physical stems (CPS), is of paramount importance and of crucial urgency for dependability research. One approach to establishing such desiderata of AI is through formal verification, particularly in machine learning (ML) components like neural networks, to establish they meet certain formal specifications. The Neural Network Verification (NNV) software tool implements automated formal methods for this purpose, specifically reachability analysis, and this interactive tutorial will demonstrate these to formally verify specifications in neural networks, as well as in closed-loop CPS. The tutorial begins with a lecture on the emerging research area of neural network verification, followed by interactive demos of these methods implemented in NNV. Examples will be shown from the security, medicine, and CPS domains.