1 Introduction↩︎

Complete neural-network verification requires a decisive answer: either produce an input violating a specification or prove that no such input exists. For piecewise-linear networks, this task underlies SMT, mixed-integer, and branch-and-bound verifiers [1]–[5]. Verification competitions document continuing algorithmic progress together with substantial variation in difficulty across benchmarks [6].

Worst-case hardness does not by itself determine what happens after perturbation. One possible explanation for difficult instances is that they depend on exact algebraic alignments, vanishing activation margins, or synchronized coefficients. Under that explanation, generic parameter noise could remove the relevant structure and make exact verification efficient on every smoothed adversarial instance.

Smoothed analysis formalizes this question. An adversary first chooses an instance; each numerical parameter is then independently perturbed; complexity is averaged only over the perturbation [7]. This framework explains the practical performance of the simplex method and has revealed both positive and negative phenomena in discrete optimization [8]. Neural-network verification adds several requirements: the algorithm must establish a universal inequality over a continuum, it must be correct on every rounded rational instance, and all arithmetic must be charged in the ordinary bit model.

We study the perturb-and-round model in which each network coefficient \(q\) becomes \[\widetilde{q}=\operatorname{clip}_{[-2,2]} \left(2^{-B}\operatorname{round}\bigl(2^B(q+\sigma Z_q)\bigr)\right), \qquad Z_q\sim\mathcal{N}(0,1),\] independently. The input box and output threshold are unchanged. We prove a conditional lower bound against a universal smoothed-polynomial exact verifier under the standard assumption \(\mathrm{NP}\not\subseteq\mathrm{BPP}\).

1.0.0.1 Quantitative step beyond worst-case hardness.

A worst-case reduction is not automatically robust to parameter noise. A constant output gap by itself may be overwhelmed by the aggregate motion of linearly many coefficients. We therefore use a perfect-completeness gap version of E3SAT, obtain a verification margin proportional to the number of clauses, and compare it with the weighted influence of every perturbed parameter. Concentration then gives exponentially small label-change probability at a noise level independent of network size. The argument is a quantitative robustification of gap hardness rather than a claim that the particular clause gadget is the only route to such a result.

1.0.0.2 What is established.

1. An exact continuous extension of E3SAT. A formula with \(m\) clauses is represented by a one-hidden-layer network with four ReLUs per clause. Every fractional point is dominated by its coordinatewise threshold rounding, so the ReLU maximization problem has zero integrality gap and an exact closed form in terms of the minimum number of unsatisfied clauses.

2. A weighted smoothed-transfer theorem. We prove a deterministic bound of the form \[\sup_x |g_{\theta'}(x)-g_\theta(x)| \le \sum_q c_q|\theta'_q-\theta_q|,\] where \(c_q\) is the worst-case influence of coefficient \(q\). Gaussian concentration for the weighted folded-normal sum yields an explicit label-preservation probability. The argument handles clipping, exact dyadic rounding, output-layer perturbations, ReLU boundaries, and the full input box.

3. A fixed-noise hardness consequence in the bit model. With \(\sigma_\star=2^{-11}\), the perturbed instance has the same safe/unsafe answer as the source gap formula with probability at least \(1-e^{-m/8}\). We give a polynomial-bit sampler for the rounded Gaussian law and convert the hypothesized expected running-time bound into a BPP algorithm by Markov truncation.

4. Computational checks and reproducibility. We compare the exact identity with independent MILP optima, globally optimize perturbed three-input networks by activation-arrangement enumeration, cross-check that solver against MILP, and illustrate the different scaling of extensive and one-defect gaps. These computations audit implementation-sensitive claims and visualize the proof mechanism; they do not establish the complexity result.

The transfer mechanism is intentionally general: other bounded-coefficient gap reductions with an extensive margin and linear weighted sensitivity can support analogous analyses. The E3SAT construction is used because it gives an exact identity and transparent coefficient accounting. The theorem does not claim that typical trained networks are usually hard, nor that perturbations cannot help a particular verifier. It rules out a guarantee that exact verification becomes smoothed-polynomial for every adversarial base network under the stated coefficient perturbation.

2 Model and main result↩︎

A feedforward ReLU network is a finite directed acyclic graph. Each hidden node computes \[z_v=b_v+\sum_{u\to v}w_{vu}y_u, \qquad y_v=\operatorname{ReLU}(z_v)=\max\{0,z_v\},\] and the scalar output \(g_N(x)\) is affine in the final hidden layer. All weights, biases, box endpoints, and thresholds are rational.

For a rational box \(X\), define \[\mathrm{\small Exact-ReLU-Verify}(N,X,\tau)=\mathbf{1}\{g_N(x)\le \tau\text{ for every }x\in X\}.\] An unsafe answer therefore needs a witness \(x\) with \(g_N(x)>\tau\); a safe answer establishes the universal weak inequality. The instance size \(s\) is the number of neurons plus the number of nonzero affine coefficients. Its bit complexity \(B\) is the largest binary encoding length of any rational datum. Our construction also works under the narrower convention in which \(B\) is computed only from network coefficients.

Let \(h=2^{-B}\). For every explicitly present network weight or bias \(q\), independently draw \(Z_q\sim\mathcal{N}(0,1)\) and set \[\widetilde{q}=\Pi_{[-2,2]} \left(h\operatorname{round}\left(\frac{q+\sigma Z_q}{h}\right)\right), \label{eq:smoothing}\tag{1}\] where \(\Pi_{[-2,2]}\) is clipping and \(h\le\sigma\le1\). Zero hidden biases and the affine output bias are included as parameter slots. If a convention perturbs fewer slots, every robustness bound below only improves.

The extra hidden ReLU is an inactive precision guard. The semantic SAT construction uses exactly four ReLUs per clause.

3 An exact four-ReLU-per-clause E3SAT embedding↩︎

We use the following standard consequence of Håstad’s optimal E3SAT inapproximability theorem [9]. Choosing approximation parameter \(\epsilon=1/40\), it is NP-hard to distinguish formulas for which all clauses can be satisfied from formulas for which every assignment satisfies at most a \(9/10\) fraction. Equivalently, in the no case every assignment violates at least \[\eta m,\qquad \eta=\frac{1}{10}, \label{eq:eta}\tag{2}\] clauses. Taking 64 disjoint copies is a constant-factor padding that preserves both alternatives and ensures \(m\ge64\).

For a literal \(\lambda\), define its relaxed value \[\ell_\lambda(x)= \begin{cases} x_i,&\lambda=X_i,\\ 1-x_i,&\lambda=\neg X_i. \end{cases}\] For each occurrence \(\lambda_j\) in a clause \(C\), create a literal unit \[h_{C,j}(x)=\operatorname{ReLU}\left(\ell_{\lambda_j}(x)-\frac{1}{2}\right) \quad\text{with output weight }\frac{2}{3}. \label{eq:literal-unit}\tag{3}\] For \(C=(\lambda_1\vee\lambda_2\vee\lambda_3)\), let \[L_C(x)=\frac{\ell_{\lambda_1}(x)+\ell_{\lambda_2}(x)+\ell_{\lambda_3}(x)}{3}\] and create one overflow unit \[r_C(x)=\operatorname{ReLU}\left(L_C(x)-\frac{1}{3}\right) \quad\text{with output weight }-1. \label{eq:overflow-unit}\tag{4}\] The network output is \[g_\Phi(x)=\frac{2}{3}\sum_{C\in\Phi}\sum_{j=1}^3 h_{C,j}(x) -\sum_{C\in\Phi}r_C(x). \label{eq:network}\tag{5}\] Every hidden fan-in is at most three. Literal-unit weights and biases are \(\pm1\) and \(\pm1/2\); overflow weights are integer multiples of \(1/3\) in \([-1,1]\), overflow biases belong to \(\{-1/3,0,1/3,2/3\}\), and output weights are \(2/3\) or \(-1\).

Let \(u(a)\) be the number of clauses false under Boolean assignment \(a\), and let \[u^\star(\Phi)=\min_{a\in\{0,1\}^n}u(a).\]

The exact identity yields an extensive symmetric verification gap. Set \[T=\frac{m}{3}, \qquad \tau=T-\frac{\eta m}{6}=\frac{19m}{60}, \qquad \Gamma=\frac{\eta m}{6}=\frac{m}{60}. \label{eq:threshold-margin}\tag{9}\] If \(\Phi\) is satisfiable, some Boolean input has \(g_\Phi=T=\tau+\Gamma\). In the no case, 2 gives \[\max_xg_\Phi(x)\le T-\frac{\eta m}{3}=\tau-\Gamma.\] The two alternatives are separated from the unchanged threshold by the same margin \(\Gamma\).

4 Weighted robustness under perturbation↩︎

4.1 The precision guard↩︎

The smoothing model requires \(2^{-B}\le\sigma\). To make the fixed \(\sigma_\star\) admissible under any natural convention for \(B\), add one input \(x_0\in[0,1]\) and one hidden unit \[d(x_0)=\operatorname{ReLU}\left(-1+2^{-20}x_0\right) \quad\text{with output weight }1. \label{eq:guard}\tag{10}\] Its base output is identically zero, so it does not change 6 or the threshold gap. Its coefficient \(2^{-20}\) ensures \(B\ge20\) and therefore \[2^{-B}\le2^{-20}<2^{-11}=\sigma_\star.\] The guard’s perturbation is included in all bounds below.

4.2 A deterministic weighted sensitivity inequality↩︎

Let \(\theta\) denote the vector of all network parameter slots, including hidden biases, output weights, and the output bias. For each slot \(q\), define a nonnegative influence coefficient \(c_q\):

Define \[C=\sum_qc_q, \qquad D^2=\sum_qc_q^2, \qquad \mu=\mathbb{E}|Z|=\sqrt{2/\pi}. \label{eq:CD}\tag{12}\] The compact construction admits tight linear bounds. Per clause, the three literal units contribute \(27/2\) to \(C\) and \(99/4\) to \(D^2\); the overflow unit contributes at most \(26/3\) and \(148/9\). The precision guard and output bias add at most \(5\) to \(C\) and \(9\) to \(D^2\). Hence, for \(m\ge64\), \[C\le \frac{133m}{6}+5\le23m, \qquad D^2\le\frac{1483m}{36}+9\le43m. \label{eq:CD-bounds}\tag{13}\]

4.3 A reusable Gaussian transfer theorem↩︎

4.4 Explicit fixed-noise instantiation↩︎

For our reduction, \(\Gamma=m/60\), \(\sigma_\star=2^{-11}\), and \(h\le2^{-20}<\sigma_\star\). Using the coarser but convenient inequality \(h/(2\sigma_\star)\le1/2\), \(\mu<5/6\), and 13 , \[\begin{align} \Lambda &\ge \frac{m/60}{2^{-11}} -\left(\frac{5}{6}+\frac{1}{2}\right)23m\\ &=\frac{512m}{15}-\frac{92m}{3} =\frac{52m}{15}. \label{eq:lambda-lower} \end{align}\tag{17}\] Consequently, \[\frac{\Lambda^2}{2D^2} \ge \frac{(52m/15)^2}{86m} =\frac{2704}{19350}m >\frac{m}{8}. \label{eq:exponent}\tag{18}\]

This is the central smoothed-hardness mechanism. Both the logical margin and the weighted aggregate perturbation scale linearly with \(m\); a sufficiently small constant noise level leaves a positive linear separation, and concentration makes failure exponentially unlikely.

5 From label preservation to a BPP collapse↩︎

We now complete the proof of 1. The construction is polynomial-time and has \(4m+1\) hidden ReLUs. Counting all possible sparse incoming weights, hidden biases, output weights, the precision guard, and the output bias gives at most \[P\le14m+4 \label{eq:param-count}\tag{19}\] perturbed slots. After removing unused variables, \(n\le3m\); under any standard convention counting input and output nodes, the instance size remains \(s=\Theta(m)\). All semantic coefficients have constant bit length, the guard gives \(B\ge20\), and the threshold \(19m/60\) gives \(B=O(\log(m+2))\) if thresholds are included in \(B\).

Assume the verifier \(A\) in 1 exists. Let \[Q(s,B,1/\sigma_\star)\] be a polynomial upper bound on its expected running time under the exact perturbation law, including any internal randomness. The polynomial may be hard-coded into the derived machine because the complexity implication is for the fixed algorithm \(A\). Run \(A\) for at most \(100Q\) bit operations. Markov’s inequality bounds the timeout probability under the exact smoothing distribution by \(1/100\).

A standard probabilistic Turing machine cannot sample an ideal real Gaussian at unit cost. The dyadic rounding makes the required discrete law efficiently approximable. For one coefficient, the support is \[G_B=\{-2,-2+h,\ldots,2-h,2\}, \qquad |G_B|=2^{B+2}+1=\operatorname{poly}(s).\] Each interior atom probability is a difference of normal CDF values, \[p_q(r)= \Phi\left(\frac{r+h/2-q}{\sigma_\star}\right) - \Phi\left(\frac{r-h/2-q}{\sigma_\star}\right), \label{eq:atom}\tag{20}\] with the two endpoint atoms absorbing the tails. The normal CDF is polynomial-time computable to any requested number of bits [12]. Approximating each marginal by a dyadic probability table within total variation \(\epsilon/P\), and sampling that table exactly, produces a joint distribution within \(\epsilon\) of the exact independent product law. Full normalization and bit-complexity details are in 11.

Choose \(\epsilon=1/100\). Total variation cannot increase after applying the verifier, its internal randomness, and the timeout rule. The resulting polynomial-time randomized SAT algorithm can fail only if:

1. the perturbation changes the reduction label, probability at most \(e^{-8}\);

2. the exact verifier exceeds its timeout, probability at most \(1/100\); or

3. approximate sampling changes the final event, probability at most \(1/100\).

The total is below \(1/3\). Accept exactly when \(A\) reports unsafe. A satisfiable source instance maps to an unsafe network, while a no instance maps to a safe network, except on the accounted-for perturbation event. Thus SAT lies in BPP and \(\mathrm{NP}\subseteq\mathrm{BPP}\).

The verifier itself is never allowed to be approximate or wrong: approximation is used only by the outer randomized reduction to sample a distribution close to the exact rounded Gaussian law.

6 Computational checks and numerical illustration↩︎

The theorem is analytic, and experiments cannot establish smoothed complexity. We use computations only to test implementation-sensitive consequences of the proof: the exact continuous-to-Boolean identity, global optimization after perturbation, and the different scaling of extensive and constant gaps. All raw data, fixed seeds, and scripts are included in the reproducibility package.

6.1 Exact identity and exhaustively optimized perturbations↩︎

6.1.0.1 Identity audit.

We generated 18 random E3SAT formulas with 4–7 variables and 18–47 clauses. The minimum number \(u^\star\) of false clauses was found by exhaustive Boolean enumeration. We then built the compact networks, containing 72–188 ReLUs, and independently maximized them with exact logical big-\(M\) formulations using interval-tight preactivation bounds. The prediction \((m-u^\star)/3\) agreed with the reported global MILP optimum to maximum absolute error \(7.11\times10^{-15}\).

6.1.0.2 Three-dimensional exhaustive laboratory.

For perturbation studies we use two eight-clause blocks on three variables. The gap block contains all eight sign patterns and therefore falsifies exactly one clause under every Boolean assignment. The same-size satisfiable block removes the clause false at \(000\) and duplicates one clause true at \(000\). Each compact block contains 32 ReLUs and 112 coefficient slots before the shared output bias.

A shallow ReLU network is affine on every cell of its activation-hyperplane arrangement. In three dimensions, a maximum on a box occurs at an arrangement vertex. For every perturbed block we enumerated all \[\binom{32+6}{3}=8{,}436\] triples of activation planes and box facets, discarded singular or infeasible intersections, and evaluated the network at every retained point. We generated 300 globally optimized blocks of each family at each of ten noise levels from \(0.0015\) through \(0.063\), with \(B=16\). Forty-four independently selected optima were cross-checked against a separate MILP model; the maximum discrepancy was \(7.99\times10^{-15}\).

Disjoint blocks have disjoint inputs and additive outputs, so the product optimum is exactly the sum of the block optima plus one independently perturbed output bias. We formed 50,000 bootstrap products for each noise/size cell and each \(q\in\{1,2,4,8,16,32,64,128\}\), reaching 4,096 ReLUs and \(112q+1=14{,}337\) perturbed slots.

1 (b)–(c) isolates the extensive-gap phenomenon. At intermediate noise, one block is unreliable, yet independent products become highly reliable because their signed margin grows and concentrates linearly. At larger noise, an asymmetric shift in the perturbed optimum can dominate; replication then amplifies the bias. The theorem avoids relying on cancellation or empirical symmetry by using the deterministic sensitivity certificate.

6.2 The deterministic certificate exhibits the predicted scaling↩︎

For a realized perturbation, define the exact certificate quantity \[W(\Delta\theta)=\sum_qc_q|\Delta\theta_q|. \label{eq:certificate}\tag{21}\] By 1, the answer is deterministically preserved whenever \(W(\Delta\theta)<\Gamma\). We compare two block products built from the same parameterized networks:

• in the extensive-gap family, all \(q\) blocks are gap blocks and \(\Gamma=q/6\);

• in the one-defect ablation, only one block carries the logical defect, so \(\Gamma=1/6\) while the number of perturbed parameters still grows with \(q\).

For each \(q\in\{1,4,16,64,128\}\) and 37 logarithmically spaced noise levels, we drew 12,000 exact rounded/clipped single-block perturbations at \(B=24\) and formed 40,000 bootstrap products. The extensive family crosses 50% certificate probability at essentially constant noise, from \(1.154\times10^{-3}\) at \(q=1\) to \(1.132\times10^{-3}\) at \(q=128\). The fitted log–log slope is \(-0.0035\). The one-defect transition falls from \(1.154\times10^{-3}\) to \(8.49\times10^{-6}\), with slope \(-1.014\), matching the predicted \(q^{-1}\) law.

This ablation illustrates the quantitative condition used by the proof. In the present construction, fixed noise is possible because the logical margin and aggregate coefficient influence grow at the same extensive scale.

7 Related work↩︎

7.0.0.1 Exact ReLU verification.

Reluplex and related SMT methods [1], [2], MILP formulations [3], [13], and branch-and-bound methods [4], [5] exploit the piecewise-linear structure of ReLU networks while retaining completeness. Convex relaxations provide scalable bounds but face intrinsic tightness barriers without branching or additional structure [14]. Reachability and verification are NP-hard for highly restricted shallow networks [11], [15]; more recent work gives strong parameterized and approximation hardness for shallow ReLU optimization and verification [16]. Worst-case hardness alone does not rule out smoothed polynomial time, because a hard family may be unstable under the prescribed perturbation.

7.0.0.2 Gap reductions and robustness.

The present proof should be viewed as a quantitative robustification of gap hardness. The weighted transfer theorem applies whenever a reduction supplies a sufficiently large verification margin relative to its aggregate coefficient sensitivity. As noted in 4, cut-based shallow-network constructions provide another natural route. The contribution here is therefore not that the E3SAT gadget is uniquely capable of surviving noise, but that the perturb-and-round model, exact rational correctness, fixed-noise preservation, sampling law, and expected-time conversion are handled together with explicit constants.

7.0.0.3 Smoothed complexity.

Smoothed analysis takes a worst case over base inputs and an average over local perturbations [7]. Integer programming demonstrates that smoothing can improve algorithms without erasing all discrete structure [8]. In the present setting, the source inapproximability gap is converted into an extensive verification margin and compared directly with weighted coefficient motion.

7.0.0.4 Parameter smoothing in neural learning.

[17] study computational hardness of learning neural networks under parameter smoothing. Learning and exact verification differ in their quantifiers, objectives, and correctness requirements. Our result concerns universal exact verification of a supplied rational network, uses a standard NP-hard gap source, and derives the collapse \(\mathrm{NP}\subseteq\mathrm{BPP}\) rather than relying on an average-case conjecture.

8 Limitations and conclusion↩︎

The theorem concerns worst-case base networks in a specific absolute-parameter-noise model. It does not predict verifier runtime on networks trained from a particular data distribution, and it does not preclude polynomial algorithms under monotonicity, fixed input dimension, bounded unstable-neuron count, special architectures, or training-induced margins. The input box and threshold are not perturbed. The explicit constant \(2^{-11}\) is conservative and small relative to the coefficient range, rather than optimized. Similar conclusions may be obtainable from other gap reductions satisfying the transfer theorem’s sensitivity condition.

The computational study uses separable low-dimensional products so that every perturbed block can be globally optimized and independently cross-checked. It is a diagnostic illustration of the proof mechanism, not a benchmark of modern vision-scale verifiers and not evidence that typical trained networks are difficult after perturbation.

Within these limits, the theorem gives a precise negative result for the stated smoothed model: independent parameter noise and generic activation geometry do not by themselves guarantee smoothed-polynomial exact verification for every adversarial base instance. The main technical content is the explicit robust-gap accounting, including exact dyadic rounding, clipping, bit-complexity sampling, and expected-time conversion.

8.0.0.1 Reproducibility.

The accompanying archive contains the full LaTeX source, fixed random seeds, raw CSV files, figure-generation scripts, proof-audit code, and instructions for rerunning the computations. The appendices below record the encoding, concentration, sampling, and bit-complexity details.

Acknowledgments↩︎

The author thanks Prof. Vincent Froese for helpful feedback, in particular for emphasizing the relationship between the smoothed-hardness argument and existing gap reductions for shallow ReLU optimization. Large language-model tools were used substantially for proof exploration, adversarial auditing, experiment design, and manuscript drafting.

9 Full reduction and encoding details↩︎

9.1 Source promise problem and constant padding↩︎

Håstad’s E3SAT theorem implies that for every fixed \(\epsilon>0\), it is NP-hard to distinguish a satisfiable E3SAT formula from one in which no assignment satisfies more than a \(7/8+\epsilon\) fraction of clauses [9]. Set \(\epsilon=1/40\). Then \(7/8+1/40=9/10\), giving 2 . If the resulting formula has \(m_0\) clauses, make 64 disjoint variable-renamed copies. The new formula has \(m=64m_0\ge64\) clauses, remains satisfiable in the yes case, and has the same maximum satisfiable fraction in the no case. This is a fixed constant blowup.

9.2 Coefficient expansion↩︎

For a positive literal, 3 has incoming weight \(1\) and bias \(-1/2\); for a negative literal it has weight \(-1\) and bias \(1/2\). For a clause with \(k\) negative literals, \[L_C(x)-\frac{1}{3} =\sum_{i\in P_C}\frac{x_i}{3} -\sum_{i\in N_C}\frac{x_i}{3} +\frac{k-1}{3}.\] If a variable is repeated, equal-variable coefficients are combined and exact zeros are omitted. The resulting fan-in is at most three, every incoming coefficient lies in \([-1,1]\), and the bias belongs to \(\{-1/3,0,1/3,2/3\}\). The output weights \(2/3\) and \(-1\) also lie in \([-1,1]\).

The precision guard 10 has one weight \(2^{-20}\), bias \(-1\), and output weight \(1\). Its base preactivation is at most \(-1+2^{-20}<0\) on \([0,1]\).

9.3 Counts↩︎

The semantic construction has \(3m\) literal units and \(m\) overflow units. Its parameter slots are bounded by

A parameter slot is counted even when its base value is zero. The instance-size definition counts only nonzero coefficients, so this table is an upper bound for that contribution. There are at most \(3m\) used Boolean variables, and thus the total number of input, hidden, and output nodes plus nonzero coefficients is between constant multiples of \(m\).

All semantic coefficients have constant bit length. The guard gives \(B\ge20\). The threshold \(19m/60\) and the formula encoding have \(O(\log(m+2))\)-bit rational data, so \(B=O(\log(m+2))\) under the broad convention that includes the threshold and box endpoints. Under a network-only convention, \(B\) is a fixed constant at least 20. Both conventions make \(2^{-B}\le2^{-20}<\sigma_\star\) and make the rounded support polynomial in the input length.

9.4 Strict unsafe and weak safe inequalities↩︎

In the satisfiable case the Boolean witness has base output \(\tau+\Gamma\). On the event \[\sup_x|g_{\widetilde{\theta}}(x)-g_\theta(x)|<\Gamma,\] that same witness remains strictly above \(\tau\), as required for an unsafe answer. In the no case every base output is at most \(\tau-\Gamma\), so every perturbed output is strictly below \(\tau\). The safe weak inequality therefore holds. The concentration proof treats every perturbation with uniform displacement at least \(\Gamma\), including equality, as part of the failure event. No correctness claim therefore depends on a tie convention at the output threshold.

10 Full robustness calculations↩︎

10.1 Derivation of the influence norms↩︎

For each literal unit there is one incoming weight, one hidden bias, and one output weight. The incoming parameters have influence 2 and the output parameter has influence \(1/2\). Three literal units per clause therefore contribute \[3\left(2+2+\frac{1}{2}\right)=\frac{27}{2}\] to \(C\), and \[3\left(2^2+2^2+\left(\frac{1}{2}\right)^2\right)=\frac{99}{4}\] to \(D^2\).

An overflow unit has at most three incoming weights, one hidden bias, and one output weight. It contributes at most \[4\cdot2+\frac{2}{3}=\frac{26}{3}\] to \(C\), and \[4\cdot2^2+\left(\frac{2}{3}\right)^2=\frac{148}{9}\] to \(D^2\). Thus the semantic per-clause totals are \[\frac{27}{2}+\frac{26}{3}=\frac{133}{6}, \qquad \frac{99}{4}+\frac{148}{9}=\frac{1483}{36}.\] The guard’s incoming weight and bias contribute 4 to \(C\) and 8 to \(D^2\); its output weight has influence zero because the base activation is identically zero. The output bias contributes 1 to both \(C\) and \(D^2\). This gives the first inequalities in 13 ; \(m\ge64\) yields the simplified bounds.

10.2 Clipping and rounding↩︎

Let \(R_h(t)=h\operatorname{round}(t/h)\). Every nearest-grid rule satisfies \(|R_h(t)-t|\le h/2\). Since \(q\in[-1,1]\subset[-2,2]\) and Euclidean projection onto an interval is nonexpansive relative to a point in that interval, \[|\Pi_{[-2,2]}(R_h(q+\sigma Z))-q| \le |R_h(q+\sigma Z)-q| \le \sigma|Z|+\frac{h}{2}.\] This remains true when the noisy rounded value lies outside the clipping interval.

10.3 Gaussian concentration constants↩︎

The map \(F(z)=\sum_qc_q|z_q|\) is \(D\)-Lipschitz because \[|F(z)-F(z')| \le\sum_qc_q|z_q-z'_q| \le D\|z-z'\|_2.\] Its expectation is \(\mu C\), where \(\mu=\sqrt{2/\pi}<5/6\). The standard Gaussian concentration inequality for Lipschitz functions gives \[\mathbb{P}\{F\ge\mu C+t\}\le e^{-t^2/(2D^2)}.\] At \(\Gamma=m/60\) and \(\sigma_\star=2^{-11}\), and using only \(h\le\sigma_\star\), the rational lower bound 17 follows. The exact Gaussian mean would give the stronger per-clause tail separation \(4.2819\ldots\) and exponent \(0.2132\ldots m\); the paper uses the rational lower bounds \(52m/15\) and \(m/8\).

11 Polynomial-bit sampling of the rounded Gaussian law↩︎

11.1 One marginal↩︎

Fix a base coefficient \(q\), precision \(B\), \(h=2^{-B}\), and fixed rational \(\sigma_\star\). The support after rounding and clipping is \[G_B=\{-2,-2+h,\ldots,2-h,2\}, \qquad M=|G_B|=2^{B+2}+1.\] For an interior point \(r\), the probability is 20 ; the endpoint probabilities aggregate the corresponding half-infinite tails. Every CDF argument is rational with \(O(B)\) bits and lies in a fixed bounded interval depending only on \(\sigma_\star\). The standard normal CDF is polynomial-time computable as a real function [12]; equivalently, one may combine polynomial-time evaluation of \(e^{-x^2/2}\) on a fixed interval with quadrature or power-series approximation and elementary tail bounds. Thus each atom can be approximated to \(R\) binary digits in time \(\operatorname{poly}(B,R)\).

Let the desired marginal total-variation error be \(\varepsilon/P\). Approximate each exact probability \(p_i\) by a rational \(a_i\) satisfying \[|a_i-p_i|\le\delta:=\frac{\varepsilon}{32PM},\] and replace negative approximations by zero. The resulting vector has \(\ell_1\) error at most \(M\delta\), and its sum differs from one by at most the same amount. Normalizing it increases the \(\ell_1\) error by only a constant factor. Next choose a dyadic denominator \(2^R\) with \[2^R\ge\frac{16PM}{\varepsilon},\] round the first \(M-1\) normalized probabilities downward to multiples of \(2^{-R}\), and place the leftover mass on the last atom. This changes the \(\ell_1\) distance by at most \(2M2^{-R}\). With the displayed choices, the final dyadic marginal lies within \(\varepsilon/P\) total variation of the exact marginal. It can be sampled exactly using fair random bits and a cumulative table. All stored integers and all arithmetic have polynomial bit length.

11.2 Independent products↩︎

Let \(D_q\) and \(\widehat D_q\) be the exact and approximate marginal laws. A coordinatewise maximal coupling gives \[d_{\mathrm{TV}}\left(\bigotimes_{q=1}^P D_q, \bigotimes_{q=1}^P\widehat D_q\right) \le\sum_{q=1}^Pd_{\mathrm{TV}}(D_q,\widehat D_q) \le\varepsilon.\] Any randomized verifier together with a timeout rule is a Markov kernel. Total variation contracts under Markov kernels, so replacing the exact perturbation vector by the approximate sampler changes the probability of every final event by at most \(\varepsilon\).

11.3 Expected time and the hard-coded polynomial↩︎

The smoothed polynomial bound for a fixed algorithm \(A\) means that some fixed polynomial \(Q\) upper-bounds its expectation. A machine proving the complexity implication may hard-code \(Q\) and run \(A\) for \(100Q\) steps. This does not require discovering \(Q\) from black-box access to \(A\). Markov’s inequality then gives the \(1/100\) timeout bound used in 5.

12 Experimental methodology↩︎

12.1 MILP formulation↩︎

For each hidden unit \(y=\operatorname{ReLU}(z)\) with exact interval bounds \(L\le z\le U\) on the box, stable units are represented by \(y=z\) if \(L\ge0\) and \(y=0\) if \(U\le0\). For \(L<0<U\), with binary phase variable \(a\), we use \[y\ge0, \qquad y\ge z, \qquad y\le Ua, \qquad y\le z-L(1-a).\] Because the network has one hidden layer, \(L\) and \(U\) are obtained exactly by selecting the appropriate endpoint of each input coefficient. The models were solved through SciPy’s MILP interface [18], backed by HiGHS; relevant dual-simplex implementation details are described by [19]. We required reported optimality and a relative MIP gap of \(10^{-10}\).

12.2 Arrangement enumeration↩︎

For each 32-ReLU block, the solver enumerated all \(\binom{38}{3}=8{,}436\) plane triples by vectorized Cramer’s rule, discarded singular systems and points outside \([0,1]^3\), and evaluated the network at all remaining candidates. Floating-point arithmetic is used only in this numerical study. The independent MILP cross-check covered 44 perturbed networks; maximum and mean absolute discrepancies were \(7.99\times10^{-15}\) and \(3.63\times10^{-16}\).

12.3 Product construction↩︎

If blocks use disjoint inputs and their outputs are added, then \[\max_{x^{(1)},\ldots,x^{(q)}}\sum_{j=1}^qg_j(x^{(j)}) =\sum_{j=1}^q\max_{x^{(j)}}g_j(x^{(j)}).\] For the eight-clause satisfiable block, the base optimum is \(8/3\); for the gap block it is \(7/3\). The midpoint threshold for \(q\) homogeneous blocks is \[\tau_q=\frac{8q}{3}-\frac{q}{6},\] leaving margin \(q/6\) on both sides. The shared output bias is perturbed once per product. The bootstrap experiment used 300 exact block optima per family/noise cell and 50,000 products per product cell.

12.4 Certificate experiment↩︎

For one compact block, the vector of semantic parameters contains 112 slots. Each realized perturbation was scored with the exact weighted sum in 21 ; the output-bias displacement was sampled separately. At each of 37 noise levels, 12,000 single-block weighted sums were generated and then combined into 40,000 products for each \(q\). The 50% transition was estimated by linear interpolation of certificate probability against \(\log\sigma\). Least-squares fits of \(\log\sigma_{1/2}\) against \(\log q\) gave slopes \(-0.003496\) and \(-1.013715\) for extensive and one-defect gaps.

12.5 Figure typography↩︎

All plots were generated with Matplotlib’s PGF backend, \(\texttt{text.usetex=True}\), and a LaTeX preamble containing amsmath and amssymb. Legends were anchored above or outside their axes, so no legend or annotation obscures a data curve. PDF and PGF versions are supplied.

13 Proof-audit checklist↩︎

The following items address common failure modes in smoothed-hardness arguments.

1. Smoothed adversarial, not random-instance, hardness. The formula and base network are worst-case. Probability is only over independent coefficient perturbations.

2. Fractional inputs. 2 proves a global rounding inequality on the entire box; no Boolean-input restriction is assumed.

3. Exact correctness. The hypothetical verifier is exact on every rational input. Approximation is used only to implement the outer reduction’s sampling law in total variation.

4. ReLU boundaries. The sensitivity proof uses only global 1-Lipschitzness and is valid at preactivation zero.

5. No activation independence. No step treats ReLU phases or activation margins as independent random variables.

6. Aggregate perturbation. The proof controls a weighted sum over all coefficients; it does not replace the aggregate by a single-coordinate anti-concentration claim.

7. Clipping and rounding. Both are included explicitly in 16 . Clipping is nonexpansive relative to every base coefficient in \([-1,1]\).

8. Output perturbations. Hidden-to-output weights and the output bias are perturbed and counted. The precision-guard output weight is also perturbed, although its first-order influence coefficient is zero because the base activation is zero.

9. Strict witness. On the preservation event, the satisfiable witness remains strictly above the unchanged threshold.

10. Fixed admissible noise. The guard forces \(B\ge20\) at every size, so \(2^{-B}<2^{-11}\) without asymptotic or finite-prefix assumptions.

11. Expected versus bounded-error time. Markov truncation is applied to the joint expectation over the perturbation and verifier randomness. Total variation is applied only after the timeout makes the final event bounded.

12. Polynomial sampling. The rounded marginal support has polynomial cardinality because \(B=O(\log s)\); Gaussian atom probabilities are approximated and normalized in polynomial bit time.

The supplied proof_checks.py performs additional redundant diagnostics: 64 random exact-identity checks (including repeated and complementary literals), 32 global sensitivity-certificate checks in which the true sup-norm difference is itself solved by MILP, and exact rational verification of every numerical constant. The current audit reports maximum identity error \(9.77\times10^{-15}\), positive sensitivity slack on every test, and status PASS. These computations are diagnostics, not substitutes for the proofs.

References↩︎