# Achieving the Tightest Relaxation of Sigmoids for Formal Verification

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 17 of its 25 references that are in the map.
- First posted on arXiv 20 Aug 2024.

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

- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [TrustLLM: Trustworthiness in Large Language Models](https://mlsanity.com/paper/2401.05561/) (2024)
- [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)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks](https://mlsanity.com/paper/1902.08722/) (2019)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Neural Network Verification with Branch-and-Bound for General Nonlinearities](https://mlsanity.com/paper/2405.21063/) (2024)
- [Fastened CROWN: Tightened Neural Network Robustness Certificates](https://mlsanity.com/paper/1912.00574/) (2019)
- [The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results](https://mlsanity.com/paper/2312.16760/) (2023)
- [From Self-Attention to Markov Models: Unveiling the Dynamics of Generative Transformers](https://mlsanity.com/paper/2402.13512/) (2024)
- [A Review of Formal Methods applied to Machine Learning](https://mlsanity.com/paper/2104.02466/) (2021)
- [Convex Bounds on the Softmax Function with Applications to Robustness Verification](https://mlsanity.com/paper/2303.01713/) (2023)
- [Toward Certified Robustness Against Real-World Distribution Shifts](https://mlsanity.com/paper/2206.03669/) (2022)
- [Neural Network Verification in Control](https://mlsanity.com/paper/2110.01388/) (2021)
- [Provably Tightest Linear Approximation for Robustness Verification of Sigmoid-like Neural Networks](https://mlsanity.com/paper/2208.09872/) (2022)
- [Global Performance Guarantees for Neural Network Models of AC Power Flow](https://mlsanity.com/paper/2211.07125/) (2022)
- [GPU-Accelerated Verification of Machine Learning Models for Power Systems](https://mlsanity.com/paper/2306.10617/) (2023)

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

- [Beyond Statistical Learning: Exact Learning Is Essential for General Intelligence](https://mlsanity.com/paper/2506.23908/) (2025)
- [Efficient Preimage Approximation for Neural Network Certification](https://mlsanity.com/paper/2505.22798/) (2025)

## Abstract (arXiv)

In the field of formal verification, Neural Networks (NNs) are typically reformulated into equivalent mathematical programs which are optimized over. To overcome the inherent non-convexity of these reformulations, convex relaxations of nonlinear activation functions are typically utilized. Common relaxations (i.e., static linear cuts) of "S-shaped" activation functions, however, can be overly loose, slowing down the overall verification process. In this paper, we derive tuneable hyperplanes which upper and lower bound the sigmoid activation function. When tuned in the dual space, these affine bounds smoothly rotate around the nonlinear manifold of the sigmoid activation function. This approach, termed α-sig, allows us to tractably incorporate the tightest possible, element-wise convex relaxation of the sigmoid activation function into a formal verification framework. We embed these relaxations inside of large verification tasks and compare their performance to LiRPA and α-CROWN, a state-of-the-art verification duo.