# PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations

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

## Key facts

- Cited by 77 papers in the map (data through 14 Oct 2026).
- Builds on 30 of its 74 references that are in the map.
- First posted on arXiv 5 Mar 2021.

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

- [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)
- [Certified Adversarial Robustness via Randomized Smoothing](https://mlsanity.com/paper/1902.02918/) (2019)
- [End to End Learning for Self-Driving Cars](https://mlsanity.com/paper/1604.07316/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Certified Robustness to Adversarial Examples with Differential Privacy](https://mlsanity.com/paper/1802.03471/) (2018)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Provably Robust Deep Learning via Adversarially Trained Smoothed Classifiers](https://mlsanity.com/paper/1906.04584/) (2019)
- [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)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Semidefinite relaxations for certifying robustness to adversarial examples](https://mlsanity.com/paper/1811.01057/) (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)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks](https://mlsanity.com/paper/1902.08722/) (2019)
- [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)
- [Learning Certified Individually Fair Representations](https://mlsanity.com/paper/2002.10312/) (2020)
- [Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming](https://mlsanity.com/paper/2010.11645/) (2020)
- [CNN-Cert: An Efficient Framework for Certifying Robustness of Convolutional Neural Networks](https://mlsanity.com/paper/1811.12395/) (2018)
- [The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification](https://mlsanity.com/paper/2006.14076/) (2020)
- [Neural Network Branching for Neural Network Verification](https://mlsanity.com/paper/1912.01329/) (2019)
- [Scaling Polyhedral Neural Network Verification on GPUs](https://mlsanity.com/paper/2007.10868/) (2020)
- [Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness](https://mlsanity.com/paper/1904.09959/) (2019)
- [Fastened CROWN: Tightened Neural Network Robustness Certificates](https://mlsanity.com/paper/1912.00574/) (2019)
- [Efficient Certification of Spatial Robustness](https://mlsanity.com/paper/2009.09318/) (2020)
- [An efficient nonconvex reformulation of stagewise convex optimization problems](https://mlsanity.com/paper/2010.14322/) (2020)
- [Computing the Approximate Convex Hull in High Dimensions](https://mlsanity.com/paper/1603.04422/) (2016)

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

- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Certified Training: Small Boxes are All You Need](https://mlsanity.com/paper/2210.04871/) (2022)
- [Neural Network Verification with Branch-and-Bound for General Nonlinearities](https://mlsanity.com/paper/2405.21063/) (2024)
- [Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes](https://mlsanity.com/paper/2501.00200/) (2024)
- [VeriX: Towards Verified Explainability of Deep Neural Networks](https://mlsanity.com/paper/2212.01051/) (2022)
- [Understanding Certified Training with Interval Bound Propagation](https://mlsanity.com/paper/2306.10426/) (2023)
- [A DPLL(T) Framework for Verifying Deep Neural Networks](https://mlsanity.com/paper/2307.10266/) (2023)
- [Formally Explaining Neural Networks within Reactive Systems](https://mlsanity.com/paper/2308.00143/) (2023)
- [Expressive Losses for Verified Robustness via Convex Combinations](https://mlsanity.com/paper/2305.13991/) (2023)
- [Neural Network Verification with Proof Production](https://mlsanity.com/paper/2206.00512/) (2022)
- [IBP Regularization for Verified Adversarial Robustness via Branch-and-Bound](https://mlsanity.com/paper/2206.14772/) (2022)
- [Toward Certified Robustness Against Real-World Distribution Shifts](https://mlsanity.com/paper/2206.03669/) (2022)
- [NLP Verification: Towards a General Methodology for Certifying Robustness](https://mlsanity.com/paper/2403.10144/) (2024)
- [From Robustness to Explainability and Back Again](https://mlsanity.com/paper/2306.03048/) (2023)
- [Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs](https://mlsanity.com/paper/2401.06379/) (2024)
- [Architecture-Preserving Provable Repair of Deep Neural Networks](https://mlsanity.com/paper/2304.03496/) (2023)
- [TAPS: Connecting Certified and Adversarial Training](https://mlsanity.com/paper/2305.04574/) (2023)
- [Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees](https://mlsanity.com/paper/2602.16823/) (2026)
- [Verifying message-passing neural networks via topology-based bounds tightening](https://mlsanity.com/paper/2402.13937/) (2024)
- [Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification](https://mlsanity.com/paper/2512.11087/) (2025)
- [Tighter Abstract Queries in Neural Network Verification](https://mlsanity.com/paper/2210.12871/) (2022)
- [Expressivity of ReLU-Networks under Convex Relaxations](https://mlsanity.com/paper/2311.04015/) (2023)
- [Robustness Assessment of a Runway Object Classifier for Safe Aircraft Taxiing](https://mlsanity.com/paper/2402.00035/) (2024)
- [Formal Verification of Graph Convolutional Networks with Uncertain Node Features and Uncertain Graph Structure](https://mlsanity.com/paper/2404.15065/) (2024)
- [On Optimizing Back-Substitution Methods for Neural Network Verification](https://mlsanity.com/paper/2208.07669/) (2022)
- [Optimization and Optimizers for Adversarial Robustness](https://mlsanity.com/paper/2303.13401/) (2023)
- [Fully Automatic Neural Network Reduction for Formal Verification](https://mlsanity.com/paper/2305.01932/) (2023)
- [Set-Based Training for Neural Network Verification](https://mlsanity.com/paper/2401.14961/) (2024)
- [DeepCDCL: An CDCL-based Neural Network Verification Framework](https://mlsanity.com/paper/2403.07956/) (2024)

## Abstract (arXiv)

Formal verification of neural networks is critical for their safe adoption in real-world applications. However, designing a precise and scalable verifier which can handle different activation functions, realistic network architectures and relevant specifications remains an open and difficult challenge. In this paper, we take a major step forward in addressing this challenge and present a new verification framework, called PRIMA. PRIMA is both (i) general: it handles any non-linear activation function, and (ii) precise: it computes precise convex abstractions involving multiple neurons via novel convex hull approximation algorithms that leverage concepts from computational geometry. The algorithms have polynomial complexity, yield fewer constraints, and minimize precision loss. We evaluate the effectiveness of PRIMA on a variety of challenging tasks from prior work. Our results show that PRIMA is significantly more precise than the state-of-the-art, verifying robustness to input perturbations for up to 20%, 30%, and 34% more images than existing work on ReLU-, Sigmoid-, and Tanh-based networks, respectively. Further, PRIMA enables, for the first time, the precise verification of a realistic neural network for autonomous driving within a few minutes.