# LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions

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

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- Builds on 25 of its 47 references that are in the map.
- First posted on arXiv 31 Jan 2022.

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

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Gaussian Error Linear Units (GELUs)](https://mlsanity.com/paper/1606.08415/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Generating Natural Language Adversarial Examples](https://mlsanity.com/paper/1804.07998/) (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)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [A Dual Approach to Scalable Verification of Deep Networks](https://mlsanity.com/paper/1803.06567/) (2018)
- [Measuring Neural Net Robustness with Constraints](https://mlsanity.com/paper/1605.07262/) (2016)
- [Robustness Verification for Transformers](https://mlsanity.com/paper/2002.06622/) (2020)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [CNN-Cert: An Efficient Framework for Certifying Robustness of Convolutional Neural Networks](https://mlsanity.com/paper/1811.12395/) (2018)
- [Geometric robustness of deep networks: analysis and improvement](https://mlsanity.com/paper/1711.09115/) (2017)
- [Reach-SDP: Reachability Analysis of Closed-Loop Systems with Neural Network Controllers via Semidefinite Programming](https://mlsanity.com/paper/2004.07876/) (2020)
- [POPQORN: Quantifying Robustness of Recurrent Neural Networks](https://mlsanity.com/paper/1905.07387/) (2019)
- [ReluDiff: Differential Verification of Deep Neural Networks](https://mlsanity.com/paper/2001.03662/) (2020)
- [Low Curvature Activations Reduce Overfitting in Adversarial Training](https://mlsanity.com/paper/2102.07861/) (2021)
- [NeuroDiff: Scalable Differential Verification of Neural Networks using Fine-Grained Approximation](https://mlsanity.com/paper/2009.09943/) (2020)
- [Scalable Polyhedral Verification of Recurrent Neural Networks](https://mlsanity.com/paper/2005.13300/) (2020)
- [DiffRNN: Differential Verification of Recurrent Neural Networks](https://mlsanity.com/paper/2007.10135/) (2020)
- [Delta-Decision Procedures for Exists-Forall Problems over the Reals](https://mlsanity.com/paper/1807.08137/) (2018)

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

- [Neural Network Verification with Branch-and-Bound for General Nonlinearities](https://mlsanity.com/paper/2405.21063/) (2024)
- [Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks](https://mlsanity.com/paper/2207.00759/) (2022)
- [Reliability Assurance for Deep Neural Network Architectures Against Numerical Defects](https://mlsanity.com/paper/2302.06086/) (2023)
- [A Tale of Two Approximations: Tightening Over-Approximation for DNN Robustness Verification via Under-Approximation](https://mlsanity.com/paper/2305.16998/) (2023)
- [Probabilistically Tightened Linear Relaxation-based Perturbation Analysis for Neural Network Verification](https://mlsanity.com/paper/2507.05405/) (2025)
- [SAIL: Sound Abstract Interpreters with LLMs](https://mlsanity.com/paper/2511.13663/) (2025)
- [Towards Global Neural Network Abstractions with Locally-Exact Reconstruction](https://mlsanity.com/paper/2210.12054/) (2022)
- [DualApp: Tight Over-Approximation for Neural Network Robustness Verification via Under-Approximation](https://mlsanity.com/paper/2211.11186/) (2022)
- [Neural Network Verification using Partial Multi-Neuron Relaxation](https://mlsanity.com/paper/2605.30155/) (2026)
- [Shifting-based Optimizable Linear Relaxations for General Activation Functions](https://mlsanity.com/paper/2606.20292/) (2026)

## Abstract (arXiv)

The most scalable approaches to certifying neural network robustness depend on computing sound linear lower and upper bounds for the network's activation functions. Current approaches are limited in that the linear bounds must be handcrafted by an expert, and can be sub-optimal, especially when the network's architecture composes operations using, for example, multiplication such as in LSTMs and the recently popular Swish activation. The dependence on an expert prevents the application of robustness certification to developments in the state-of-the-art of activation functions, and furthermore the lack of tightness guarantees may give a false sense of insecurity about a particular model. To the best of our knowledge, we are the first to consider the problem of automatically computing tight linear bounds for arbitrary n-dimensional activation functions. We propose LinSyn, the first approach that achieves tight bounds for any arbitrary activation function, while only leveraging the mathematical definition of the activation function itself. Our approach leverages an efficient heuristic approach to synthesize bounds that are tight and usually sound, and then verifies the soundness (and adjusts the bounds if necessary) using the highly optimized branch-and-bound SMT solver, dReal. Even though our approach depends on an SMT solver, we show that the runtime is reasonable in practice, and, compared with state of the art, our approach often achieves 2-5X tighter final output bounds and more than quadruple certified robustness.