# SMLE: Safe Machine Learning via Embedded Overapproximation

arXiv: https://arxiv.org/abs/2409.20517 · HTML: https://mlsanity.com/paper/2409.20517/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 24 of its 43 references that are in the map.
- First posted on arXiv 30 Sep 2024.

## Builds on (most cited first, 24 of 24)

- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Certified Adversarial Robustness via Randomized Smoothing](https://mlsanity.com/paper/1902.02918/) (2019)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Fast is better than free: Revisiting adversarial training](https://mlsanity.com/paper/2001.03994/) (2020)
- [Feature Squeezing: Detecting Adversarial Examples in Deep Neural Networks](https://mlsanity.com/paper/1704.01155/) (2017)
- [Defense-GAN: Protecting Classifiers Against Adversarial Attacks Using Generative Models](https://mlsanity.com/paper/1805.06605/) (2018)
- [Recent Advances in Adversarial Training for Adversarial Robustness](https://mlsanity.com/paper/2102.01356/) (2021)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Attacks Which Do Not Kill Training Make Adversarial Learning Stronger](https://mlsanity.com/paper/2002.11242/) (2020)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [On Detecting Adversarial Perturbations](https://mlsanity.com/paper/1702.04267/) (2017)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [You Only Propagate Once: Accelerating Adversarial Training via Maximal Principle](https://mlsanity.com/paper/1905.00877/) (2019)
- [Stochastic Activation Pruning for Robust Adversarial Defense](https://mlsanity.com/paper/1803.01442/) (2018)
- [A predictive safety filter for learning-based control of constrained nonlinear dynamical systems](https://mlsanity.com/paper/1812.05506/) (2018)
- [Strong mixed-integer programming formulations for trained neural networks](https://mlsanity.com/paper/1811.08359/) (2018)
- [Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks](https://mlsanity.com/paper/1708.03322/) (2017)
- [Understanding Catastrophic Overfitting in Single-step Adversarial Training](https://mlsanity.com/paper/2010.01799/) (2020)
- [ME-Net: Towards Effective Adversarial Robustness with Matrix Estimation](https://mlsanity.com/paper/1905.11971/) (2019)
- [Partition-based formulations for mixed-integer optimization of trained ReLU neural networks](https://mlsanity.com/paper/2102.04373/) (2021)
- [The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results](https://mlsanity.com/paper/2312.16760/) (2023)
- [Towards Safe Reinforcement Learning with a Safety Editor Policy](https://mlsanity.com/paper/2201.12427/) (2022)
- [Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification](https://mlsanity.com/paper/1902.09866/) (2019)
- [Can Go AIs be adversarially robust?](https://mlsanity.com/paper/2406.12843/) (2024)

## Built on by (most cited first, 1 of 1)

- [SMiLE: Provably Enforcing Global Relational Properties in Neural Networks](https://mlsanity.com/paper/2511.07208/) (2025)

## Abstract (arXiv)

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.