发表机构
University of Illinois Chicago（伊利诺伊大学芝加哥分校）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
研究对抗性平滑模型中ReLU网络精确验证，表明在NP⊈BPP假设下，不存在预期运行时间为多项式的可靠完备验证器，通过结合精确间隙嵌入等方法证明，指出参数非退化不能为精确验证提供通用平滑多项式保证。
AI 中文摘要
我们研究对抗性平滑模型中ReLU网络的精确验证。每个网络权重和偏差都受到高斯噪声的独立扰动，裁剪到[-2,2]，并舍入到由输入比特复杂度确定的精确二进制网格。我们表明，在标准假设NP⊈BPP下，不存在一个可靠且完备的验证器，其预期运行时间在网络规模、比特复杂度和每个基本实例的逆噪声水平上是多项式的。对于单位盒上的单隐藏层网络，在固定噪声水平σ★=2^-11时，该结论就已成立，隐藏扇入最多为3，基本系数在[-1,1]内。证明结合了精确间隙嵌入和定量鲁棒性论证。对于每个有m个子句的E3SAT公式Φ，每个子句由四个ReLU组成的构造满足max_{x∈[0,1]^n} g_Φ(x)=(m - unsat(Φ))/3，并且逐坐标阈值舍入不会降低目标值。加权参数敏感性不等式和高斯集中性表明，在所有系数的总体扰动下，以至少1 - e^-m/8的概率存在与m成线性关系的验证间隙。证明包括裁剪、精确二进制舍入、输出层扰动、舍入高斯定律的多项式比特采样，以及从预期平滑运行时间到BPP算法的转换。计算检查测试精确恒等式，并说明了广泛间隙和恒定间隙的不同缩放；它们是复杂性定理的诊断而非证据。结果涉及所述绝对噪声模型中的最坏情况基本网络，但表明仅参数非退化并不能为精确验证提供通用的平滑多项式保证。
英文摘要
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 $\mathrm{NP}\not\subseteq\mathrm{BPP}$, 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 $Φ$ with $m$ clauses, a four-ReLU-per-clause construction satisfies $\max_{x\in[0,1]^n} g_Φ(x)=(m-\operatorname{unsat}(Φ))/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.
Comments16 pages, 2 figures. Includes full bit-complexity details and computational checks. Reproducibility code and data are included as ancillary files
