Establishing Formal Behavioral Guarantees for Trained Neural Networks

Machine Learning (ML)-based systems, particularly those deploying deep neural networks (DNNs), are widely adopted into real-world applications due to their ability to be trained without being explicitly programmed and high output accuracy. However, despite their high classification accuracy and optimal decision-making in testing scenarios, they are often found to be vulnerable under unseen (but realistic) inputs. This points to the lack of generalization of these data-driven models under unseen input scenarios, hence highlighting the need for behavioral guarantees to ensure their reliable classification and decision-making in the real world. Research efforts constantly provide empirical evidence for the lack of reliable DNN behavior (under seed inputs) for various ML applications. Orthogonally, formal efforts attempt to provide concise formal guarantees for behavioral properties/specifications like robustness and safety to hold for the DNN models. However, due to the scalability challenges associated with formal methods, not only are these efforts often restricted to providing qualitative (binary) guarantees but they also focus only on limited DNN behaviors and verification techniques.To address the aforementioned limitations, this research provides model checking and scalable sampling-based formal frameworks for DNN analysis, focusing on a diverse range of DNN behavioral specifications. These include DNN noise tolerance, input node sensitivity (to noise), node robustness bias, robustness under constrained noise, robustness bias against tail classes and safety under bounded inputs. Realistic noise modeling is proposed for practical DNN analysis, while restraining from the use of unrealistic assumptions during analysis. These lead to formal guarantees that may potentially be leveraged to identify reliable ML systems. The research additionally leverages our DNN analysis to improve training for robust DNNs. The resulting frameworks designed and developed during the research are all accompanied by case studies based on DNNs trained on real-world datasets, hence supporting the efficacy of the research efforts and provide behavioral guarantees essential to ensure more reliable ML systems in practice.