SMLE: Safe Machine Learning via Embedded Overapproximation

TL;DR

This paper introduces SMLE, a novel framework for training neural networks with formal guarantees of property satisfaction, enabling safe and reliable machine learning in critical applications.

Contribution

It proposes a scalable, efficient method combining a simple architecture, a rigorous training algorithm, and counterexample search to ensure property compliance in neural networks.

Findings

Models satisfy properties with guarantees

Approach scales well to complex models

Competitive with existing property enforcement methods

Abstract

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.