# Random Parameter Noise Does Not Make Exact ReLU Verification Easy

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 27 references that are in the map.
- First posted on arXiv 15 Jul 2026.

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

- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [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)
- [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)
- [Parallelizing the dual revised simplex method](https://mlsanity.com/paper/1503.01889/) (2015)
- [Reachability Is NP-Complete Even for the Simplest Neural Networks](https://mlsanity.com/paper/2108.13179/) (2021)
- [The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results](https://mlsanity.com/paper/2512.19007/) (2025)
- [Computational Complexity of Learning Neural Networks: Smoothness and Degeneracy](https://mlsanity.com/paper/2302.07426/) (2023)
- [Parameterized Hardness of Zonotope Containment and Neural Network Verification](https://mlsanity.com/paper/2509.22849/) (2025)

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

- [Security Properties of Neural Networks as Decision Problems](https://mlsanity.com/paper/2609.39768/) (2026)

## Abstract (arXiv)

We study exact verification of ReLU networks in an adversarial smoothed model. Every network weight and bias is independently perturbed by Gaussian noise, clipped to [-2,2], and rounded to the exact dyadic grid determined by the input bit complexity. We show that, under the standard assumption NPnotsubseteqBPP, there is no sound and complete verifier whose expected running time is polynomial in network size, bit complexity, and inverse noise level for every base instance. The conclusion already holds at the fixed noise level σ_star=2-11 for one-hidden-layer networks over a unit box, with hidden fan-in at most three and base coefficients in [-1,1]. The proof combines an exact gap embedding with a quantitative robustness argument. For every E3SAT formula Phi with m clauses, a four-ReLU-per-clause construction satisfies maxx∈[0,1]n g_Phi(x)=(m-operatornameunsat(Phi))/3, and coordinatewise threshold rounding never decreases the objective. A weighted parameter-sensitivity inequality and Gaussian concentration then show that a verification gap linear in m survives the aggregate perturbation of all coefficients with probability at least 1-e-m/8. The proof includes clipping, exact dyadic rounding, output-layer perturbations, polynomial-bit sampling of the rounded Gaussian law, and the conversion from expected smoothed running time to a BPP algorithm. Computational checks test the exact identity and illustrate the different scaling of extensive and constant gaps; they are diagnostics rather than evidence for the complexity theorem. The result concerns worst-case base networks in the stated absolute-noise model, but it shows that parameter nondegeneracy alone does not yield a universal smoothed-polynomial guarantee for exact verification.