# Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks

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

## Key facts

- Cited by 242 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 3 May 2017.

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

- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Orthogonalizing Convolutional Layers with the Cayley Transform](https://mlsanity.com/paper/2104.07167/) (2021)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Boosting Randomized Smoothing with Variance Reduced Classifiers](https://mlsanity.com/paper/2106.06946/) (2021)
- [Causality-based Neural Network Repair](https://mlsanity.com/paper/2204.09274/) (2022)
- [Certified Patch Robustness via Smoothed Vision Transformers](https://mlsanity.com/paper/2110.07719/) (2021)
- [Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition](https://mlsanity.com/paper/2104.06718/) (2021)
- [Provable Repair of Deep Neural Networks](https://mlsanity.com/paper/2104.04413/) (2021)
- [CROP: Certifying Robust Policies for Reinforcement Learning through Functional Smoothing](https://mlsanity.com/paper/2106.09292/) (2021)
- [Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective](https://mlsanity.com/paper/2206.12227/) (2022)
- [Reachability Analysis of Neural Feedback Loops](https://mlsanity.com/paper/2108.04140/) (2021)
- [Partition-based formulations for mixed-integer optimization of trained ReLU neural networks](https://mlsanity.com/paper/2102.04373/) (2021)
- [How to Robustify Black-Box ML Models? A Zeroth-Order Optimization Perspective](https://mlsanity.com/paper/2203.14195/) (2022)
- [When Deep Learning Meets Polyhedral Theory: A Survey](https://mlsanity.com/paper/2305.00241/) (2023)
- [Don't Lie to Me! Robust and Efficient Explainability with Verified Perturbation Analysis](https://mlsanity.com/paper/2202.07728/) (2022)
- [Scalable Certified Segmentation via Randomized Smoothing](https://mlsanity.com/paper/2107.00228/) (2021)
- [A Review of Formal Methods applied to Machine Learning](https://mlsanity.com/paper/2104.02466/) (2021)
- [Verifying Learning-Based Robotic Navigation Systems](https://mlsanity.com/paper/2205.13536/) (2022)
- [Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes](https://mlsanity.com/paper/2501.00200/) (2024)
- [HardNet: Hard-Constrained Neural Networks with Universal Approximation Guarantees](https://mlsanity.com/paper/2410.10807/) (2024)
- [VeriX: Towards Verified Explainability of Deep Neural Networks](https://mlsanity.com/paper/2212.01051/) (2022)
- [Low Curvature Activations Reduce Overfitting in Adversarial Training](https://mlsanity.com/paper/2102.07861/) (2021)
- [Provably Bounding Neural Network Preimages](https://mlsanity.com/paper/2302.01404/) (2023)
- [Reachability Is NP-Complete Even for the Simplest Neural Networks](https://mlsanity.com/paper/2108.13179/) (2021)
- [Bayesian Inference with Certifiable Adversarial Robustness](https://mlsanity.com/paper/2102.05289/) (2021)
- [An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks](https://mlsanity.com/paper/2201.01978/) (2022)
- [Efficient Neural Network Analysis with Sum-of-Infeasibilities](https://mlsanity.com/paper/2203.11201/) (2022)

## Abstract (arXiv)

We present an approach for the verification of feed-forward neural networks in which all nodes have a piece-wise linear activation function. Such networks are often used in deep learning and have been shown to be hard to verify for modern satisfiability modulo theory (SMT) and integer linear programming (ILP) solvers. The starting point of our approach is the addition of a global linear approximation of the overall network behavior to the verification problem that helps with SMT-like reasoning over the network behavior. We present a specialized verification algorithm that employs this approximation in a search process in which it infers additional node phases for the non-linear nodes in the network from partial node phase assignments, similar to unit propagation in classical SAT solving. We also show how to infer additional conflict clauses and safe node fixtures from the results of the analysis steps performed during the search. The resulting approach is evaluated on collision avoidance and handwritten digit recognition case studies.