SMLE: Safe Machine Learning via Embedded Overapproximation
This work is significant for developers and regulators of safety-critical AI systems, as it provides a method to formally guarantee model behavior, which is a crucial requirement for adoption in regulated scenarios.
This paper addresses the challenge of training differentiable machine learning models with formal guarantees on their behavior, specifically satisfying designer-chosen input-output properties. The authors developed a framework that scales well to practical applications and produces models with full property satisfaction guarantees, achieving competitive performance against baselines that enforce properties during preprocessing and postprocessing.
Despite the extent of recent advances in Machine Learning (ML) and Neural Networks, providing formal guarantees on the behavior of these systems is still an open problem, and a crucial requirement for their adoption in regulated or safety-critical scenarios. We consider the task of training differentiable ML models guaranteed to satisfy designer-chosen properties, stated as input-output implications. This is very challenging, due to the computational complexity of rigorously verifying and enforcing compliance in modern neural models. We provide an innovative approach based on three components: 1) a general, simple architecture enabling efficient verification with a conservative semantic; 2) a rigorous training algorithm based on the Projected Gradient Method; 3) a formulation of the problem of searching for strong counterexamples. The proposed framework, being only marginally affected by model complexity, scales well to practical applications, and produces models that provide full property satisfaction guarantees. We evaluate our approach on properties defined by linear inequalities in regression, and on mutually exclusive classes in multilabel classification. Our approach is competitive with a baseline that includes property enforcement during preprocessing, i.e. on the training data, as well as during postprocessing, i.e. on the model predictions. Finally, our contributions establish a framework that opens up multiple research directions and potential improvements.