# A Review of Formal Methods applied to Machine Learning

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

## Key facts

- Cited by 33 papers in the map (data through 14 Oct 2026).
- Builds on 58 of its 173 references that are in the map.
- First posted on arXiv 6 Apr 2021.

## Builds on (most cited first, 30 of 58)

- [Very Deep Convolutional Networks for Large-Scale Image Recognition](https://mlsanity.com/paper/1409.1556/) (2014)
- [ImageNet Large Scale Visual Recognition Challenge](https://mlsanity.com/paper/1409.0575/) (2014)
- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Fashion-MNIST: a Novel Image Dataset for Benchmarking Machine Learning Algorithms](https://mlsanity.com/paper/1708.07747/) (2017)
- [Learning Phrase Representations using RNN Encoder-Decoder for Statistical Machine Translation](https://mlsanity.com/paper/1406.1078/) (2014)
- [Towards Evaluating the Robustness of Neural Networks](https://mlsanity.com/paper/1608.04644/) (2016)
- [DeepFool: a simple and accurate method to fool deep neural networks](https://mlsanity.com/paper/1511.04599/) (2015)
- [End to End Learning for Self-Driving Cars](https://mlsanity.com/paper/1604.07316/) (2016)
- [Adversarial Machine Learning at Scale](https://mlsanity.com/paper/1611.01236/) (2016)
- [Robustness May Be at Odds with Accuracy](https://mlsanity.com/paper/1805.12152/) (2018)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [On the Number of Linear Regions of Deep Neural Networks](https://mlsanity.com/paper/1402.1869/) (2014)
- [Certified Defenses against Adversarial Examples](https://mlsanity.com/paper/1801.09344/) (2018)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Towards Stable and Efficient Training of Verifiably Robust Neural Networks](https://mlsanity.com/paper/1906.06316/) (2019)
- [Formal Guarantees on the Robustness of a Classifier against Adversarial Manipulation](https://mlsanity.com/paper/1705.08475/) (2017)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Verifiable Reinforcement Learning via Policy Extraction](https://mlsanity.com/paper/1805.08328/) (2018)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [Scaling provable adversarial defenses](https://mlsanity.com/paper/1805.12514/) (2018)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Fairness Testing: Testing Software for Discrimination](https://mlsanity.com/paper/1709.03221/) (2017)
- [A Dual Approach to Scalable Verification of Deep Networks](https://mlsanity.com/paper/1803.06567/) (2018)
- [Maximum Resilience of Artificial Neural Networks](https://mlsanity.com/paper/1705.01040/) (2017)

## Built on by (most cited first, 30 of 33)

- [Trustworthy AI: From Principles to Practices](https://mlsanity.com/paper/2110.01167/) (2021)
- [The Role of Explainability in Assuring Safety of Machine Learning in Healthcare](https://mlsanity.com/paper/2109.00520/) (2021)
- [A DPLL(T) Framework for Verifying Deep Neural Networks](https://mlsanity.com/paper/2307.10266/) (2023)
- [Neural Network Repair with Reachability Analysis](https://mlsanity.com/paper/2108.04214/) (2021)
- [AgentGuard: Runtime Verification of AI Agents](https://mlsanity.com/paper/2509.23864/) (2025)
- [Incremental Verification of Neural Networks](https://mlsanity.com/paper/2304.01874/) (2023)
- [Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks](https://mlsanity.com/paper/2207.00759/) (2022)
- [CAISAR: A platform for Characterizing Artificial Intelligence Safety and Robustness](https://mlsanity.com/paper/2206.03044/) (2022)
- [Neural Network Verification with PyRAT](https://mlsanity.com/paper/2410.23903/) (2024)
- [Machine Learning Robustness: A Primer](https://mlsanity.com/paper/2404.00897/) (2024)
- [Verifying Low-dimensional Input Neural Networks via Input Quantization](https://mlsanity.com/paper/2108.07961/) (2021)
- [Never trust, always verify : a roadmap for Trustworthy AI?](https://mlsanity.com/paper/2206.11981/) (2022)
- [Faster Verified Explanations for Neural Networks](https://mlsanity.com/paper/2512.00164/) (2025)
- [Checking Trustworthiness of Probabilistic Computations in a Typed Natural Deduction System](https://mlsanity.com/paper/2206.12934/) (2022)
- [Verifiable Obstacle Detection](https://mlsanity.com/paper/2208.14403/) (2022)
- [VerifIoU -- Robustness of Object Detection to Perturbations](https://mlsanity.com/paper/2403.08788/) (2024)
- [LipShiFT: A Certifiably Robust Shift-based Vision Transformer](https://mlsanity.com/paper/2503.14751/) (2025)
- [FAME: Formal Abstract Minimal Explanation for Neural Networks](https://mlsanity.com/paper/2603.10661/) (2026)
- [Achieving the Tightest Relaxation of Sigmoids for Formal Verification](https://mlsanity.com/paper/2408.10491/) (2024)
- [Assessing Code Understanding in LLMs](https://mlsanity.com/paper/2504.00065/) (2025)
- [BEAVER: An Efficient Deterministic LLM Verifier](https://mlsanity.com/paper/2512.05439/) (2025)
- [Fixed-Point Code Synthesis For Neural Networks](https://mlsanity.com/paper/2202.02095/) (2022)
- [Verifying Attention Robustness of Deep Neural Networks against Semantic Perturbations](https://mlsanity.com/paper/2207.05902/) (2022)
- [A General Framework for Property-Driven Machine Learning](https://mlsanity.com/paper/2505.00466/) (2025)
- [On AI Verification in Open RAN](https://mlsanity.com/paper/2510.18417/) (2025)
- [An Empirical Analysis of the Use of Real-Time Reachability for the Safety Assurance of Autonomous Vehicles](https://mlsanity.com/paper/2205.01419/) (2022)
- [Abstract Interpretation-Based Feature Importance for SVMs](https://mlsanity.com/paper/2210.12456/) (2022)
- [A SAT-based approach to rigorous verification of Bayesian networks](https://mlsanity.com/paper/2408.00986/) (2024)
- [The CAISAR Platform: Extending the Reach of Machine Learning Specification and Verification](https://mlsanity.com/paper/2506.12084/) (2025)
- [A Cycle-Consistency Constrained Framework for Dynamic Solution Space Reduction in Noninjective Regression](https://mlsanity.com/paper/2507.04659/) (2025)

## Abstract (arXiv)

We review state-of-the-art formal methods applied to the emerging field of the verification of machine learning systems. Formal methods can provide rigorous correctness guarantees on hardware and software systems. Thanks to the availability of mature tools, their use is well established in the industry, and in particular to check safety-critical applications as they undergo a stringent certification process. As machine learning is becoming more popular, machine-learned components are now considered for inclusion in critical systems. This raises the question of their safety and their verification. Yet, established formal methods are limited to classic, i.e. non machine-learned software. Applying formal methods to verify systems that include machine learning has only been considered recently and poses novel challenges in soundness, precision, and scalability. We first recall established formal methods and their current use in an exemplar safety-critical field, avionic software, with a focus on abstract interpretation based techniques as they provide a high level of scalability. This provides a golden standard and sets high expectations for machine learning verification. We then provide a comprehensive and detailed review of the formal methods developed so far for machine learning, highlighting their strengths and limitations. The large majority of them verify trained neural networks and employ either SMT, optimization, or abstract interpretation techniques. We also discuss methods for support vector machines and decision tree ensembles, as well as methods targeting training and data preparation, which are critical but often neglected aspects of machine learning. Finally, we offer perspectives for future research directions towards the formal verification of machine learning systems.