Random Parameter Noise Does Not Make Exact ReLU Verification Easy
arXiv:2607.14375
The paper proves that exact verification of ReLU neural networks remains computationally hard even when all weights and biases are independently perturbed by Gaussian noise and rounded, showing no polynomial‑time verifier exists under the standard NP ⊄ BPP assumption.
Abstract
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 , and rounded to the exact dyadic grid determined by the input bit complexity. We show that, under the standard assumption , 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 for one-hidden-layer networks over a unit box, with hidden fan-in at most three and base coefficients in . The proof combines an exact gap embedding with a quantitative robustness argument. For every E3SAT formula with clauses, a four-ReLU-per-clause construction satisfies , and coordinatewise threshold rounding never decreases the objective. A weighted parameter-sensitivity inequality and Gaussian concentration then show that a verification gap linear in survives the aggregate perturbation of all coefficients with probability at least . 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.
16 pages, 2 figures. Includes full bit-complexity details and computational checks. Reproducibility code and data are included as ancillary files