{"id":"c3c42afe-1bee-49f0-b1dc-29bfe36ab0c7","arxiv_id":"2607.14375","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":3,"one_line_summary":"Exact ReLU verification remains worst-case hard even when every coefficient is independently perturbed by clipped, rounded Gaussian noise, unless NP ⊆ BPP.","lead":"Random noise added to every weight of a ReLU network does not make exact verification of safety properties easy in the worst case. This paper proves a conditional lower bound: if NP is not contained in BPP, no exact verifier can run in expected polynomial time on all perturbed instances, even at a fixed small noise level.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified","rationale":"The paper's central theorem is a conditional hardness result under NP⊄BPP. The proof chain is: (1) Håstad-based gap E3SAT; (2) exact zero-integrality embedding with a linear margin; (3) deterministic weighted sensitivity bound; (4) Gaussian concentration giving 1-e^{-m/8} label preservation; (5) Markov truncation and total-variation sampling to convert expected time into BPP. I checked each step. The exact embedding is correct: the decomposition in (8) and the false-clause deficit argument yield g(x)≤g(a) for threshold rounding; at Boolean points the output is (m-u)/3. The sensitivity lemma correctly charges hidden input/bias perturbations at coefficient 2 because of the clipped output weight bound, and output-weight perturbations at the base activation bound; the per-clause C and D² bounds are accurate. The concentration argument is a direct application of Gaussian Lipschitz concentration. The arithmetic yields Λ≥52m/15 and Λ²/(2D²)≥m/8, so preservation probability ≥1-e^{-m/8}. The BPP conversion is sound: the outer machine runs A for 100Q steps, sampling from a distribution within TV 1/100 of the exact perturbed law; the total error is below 1/3. I found no internal inconsistency or unproven assumption beyond the standard NP⊄BPP hypothesis and the cited Håstad theorem. The paper honestly labels its computations as diagnostics. The only conceivable weak point is Theorem 2; if it had a counterexample, the extensive margin would vanish. But the proof is rigorous and the computational checks support it. Thus I maintain the reader's ACCEPT verdict without changes.","tokens_in":12836,"tokens_out":33230,"duration_ms":286197,"concrete_test":"Enumerate all E3SAT formulas with up to 6 variables and 20 clauses (or all clauses over a 4-variable set) and verify by exact rational arithmetic both the identity max g=(m-u⋆)/3 and the pointwise inequality g(x)≤g(a) for the threshold rounding a, over a dense grid of x; if any violation appears, the margin analysis collapses. A more definitive check would be to formalize Theorem 2 in a proof assistant such as Lean.","verdict_should_be":"UNCHANGED","load_bearing_attack":"I read the proof carefully and could not identify a load-bearing flaw. The exact zero-integrality embedding (Theorem 2) is the linchpin: it provides the extensive margin Γ=m/60 that survives perturbation. I verified the algebra of the threshold-rounding proof; the identity g(x)≤g(a) follows from the decomposition (8), and the false-clause deficit bound is valid. The weighted sensitivity inequality (Lemma 3) and the Gaussian concentration bound (Theorem 4) are correctly applied; the constants check out (C≤23m, D²≤43m, Λ≥52m/15, exponent ≥m/8). The conversion from expected running time to BPP via Markov truncation and total-variation sampling is standard and sound. The main caveat is that the entire proof relies on Theorem 2 being exactly right; any hidden edge case there would shrink the margin. I found none, and the computational audits are consistent.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies exact ReLU network verification under an adversarial smoothed model in which 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. The main result (Theorem 1) is a conditional lower bound: if NP is not contained in BPP, then no sound and complete exact verifier can have expected bit-running time polynomial in network size, bit complexity, and inverse noise level for every adversarial base instance. The proof combines an exact E3SAT embedding (four ReLUs per clause, zero integrality gap, extensive margin m/60), a weighted parameter-sensitivity inequality (Lemma 3), Gaussian concentration (Theorem 4), and a BPP conversion that includes polynomial-bit sampling of the rounded Gaussian law. The conclusion already holds at fixed noise level 2^{-11} for one-hidden-layer networks with bounded fan-in and base coefficients in [-1,1].","tokens_in":13110,"tokens_out":17699,"duration_ms":143677,"significance":"If the result holds, it resolves a natural smoothed-complexity question for exact verification: parameter nondegeneracy alone does not guarantee smoothed-polynomial exact verification for every adversarial base network. The paper is unusually quantitative and self-contained: explicit constants are supplied (sigma_star = 2^{-11}, preservation probability at least 1 - e^{-m/8}), and the proof is built from elementary, checkable steps. The reusable weighted-sensitivity transfer theorem (Theorem 4) is a methodological contribution beyond the specific E3SAT construction. The computational audits of the exact identity and the certificate scaling are clearly labeled as diagnostics rather than evidence, and the reproducibility package is a strength. The proof is internally consistent; my remaining concerns are local typographical issues.","major_comments":[],"minor_comments":[{"comment":"The sentence 'Combining (16) with Theorem 3' should refer to Lemma 3, not Theorem 3. The weighted sensitivity bound used here is Lemma 3; there is no Theorem 3 in the paper.","section":"Section 4.3 (proof of Theorem 4)"},{"comment":"The displayed inequality '1/3 max{0,1-D_C} >= 1-D_C/3' is false as written (e.g., D_C=0 gives 1/3 >= 1). It should read '1/3 max{0,1-D_C} >= 1/3 - D_C/3', or equivalently, for D_C <= 1, '= (1-D_C)/3'. The subsequent derivation uses the corrected form, so the conclusion is unaffected, but the printed inequality must be fixed.","section":"Section 3 (proof of Theorem 2)"},{"comment":"The phrase 'As noted in Theorem 5' should be 'As noted in Remark 5'; there is no Theorem 5. The reference is to the MAX-CUT remark in Remark 5.","section":"Section 7"},{"comment":"The step 'the first two terms in (8) equal -V/3' uses the identity |x_i - 1/2| = 1/2 - delta_i, where delta_i = min{x_i, 1-x_i}. This substitution is not shown and may confuse readers; making it explicit would improve readability.","section":"Section 4.2 / Eq. (8)"}],"recommendation":"minor_revision","confidential_remarks":"I reviewed the proof chain carefully: the exact zero-integrality-gap embedding, the weighted sensitivity Lemma 3, the Gaussian concentration transfer in Theorem 4, and the BPP conversion are all sound. I found no load-bearing flaw. The only issues are typographical, most notably the false displayed inequality in the proof of Theorem 2; this should be corrected before publication. The paper is a solid contribution to smoothed verification complexity."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe short version: this is a solid conditional lower bound. The main theorem—if a sound and complete exact verifier runs in expected time polynomial in size, bit complexity, and 1/σ⋆ for every adversarial base instance with σ⋆ = 2^{-11}, then NP⊆BPP—is proven correctly. The proof's backbone is the exact four-ReLU-per-clause embedding: for any E3SAT formula, the network's continuous maximum over [0,1]^n equals (m−unsat)/3, and threshold rounding never decreases the objective. That step is the linchpin, and I checked the algebra; it's right. The weighted sensitivity lemma and Gaussian concentration transfer are also correct; the constants work out, and the exponential preservation bound e^{−m/8} follows. The conversion from expected time to BPP via Markov truncation and polynomial-bit sampling of the rounded Gaussian law is standard and clean.\n\nWhat's genuinely new is the zero-integrality-gap embedding itself, along with the explicit accounting that lets a fixed noise level preserve an extensive gap. The paper also honestly frames the computational checks as diagnostics, not evidence.\n\nSoft spots, in proportion. Minor: a few typos—'Theorem 3' for Lemma 3, and a missing parenthesis in the false-clause deficit display (it should be (1−D_C)/3, not 1−D_C/3). These don't affect the argument. More substantively, σ⋆ = 2^{-11} is tiny, and the model perturbs every coefficient individually; skeptics may say this is not the smoothed analysis they care about. But the paper's point is exactly that even this small perturbation does not help in the worst case, and the limitations section says that plainly. The result is conditional on NP⊄BPP, which is standard for this kind of hardness.\n\nOverall, the central argument holds up. The stress-test found no load-bearing flaw, and I agree. This is a careful, honest paper that deserves a serious referee. I'd bring it to a reading group on verification or smoothed complexity, and I'd cite it if I worked in either area.\n\nRecommendation: send it out for peer review.","headline":"A correct, careful conditional lower bound showing fixed small Gaussian coefficient noise does not give a universal smoothed-polynomial exact ReLU verifier; the exact E3SAT embedding holds up.","tokens_in":13490,"tokens_out":17394,"would_cite":true,"duration_ms":145647,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q17","68Q15","68T07"],"pacs":[],"model":"deepseek-v4-flash","headline":"Random parameter noise does not make exact ReLU verification computationally easy.","keywords":["ReLU verification","smoothed analysis","NP versus BPP","E3SAT embedding","gap reductions","Gaussian concentration","integrality gap","neural network verification"],"falsifier":"For any E3SAT formula with m clauses, build the four-ReLU-per-clause network and globally maximize it over the unit box using a rigorous MILP or exhaustive arrangement enumeration; if the maximum exceeds (m-unsat(Φ))/3 by any positive amount, Theorem 2 and hence the linear-margin argument fail. Conversely, the complexity theorem itself would be refuted by exhibiting a single sound-and-complete exact verifier whose expected running time is polynomial in s, B, and 1/σ on all instances of the construction at σ = 2^-11.","tokens_in":12803,"feed_emoji":"🎲","tokens_out":5480,"duration_ms":55922,"temperature":0.7,"pith_summary":"The paper asks whether adding small Gaussian noise to every weight and bias of a ReLU network can guarantee that exact verification becomes easy on average. It answers negatively, conditionally: if NP is not contained in BPP, no sound and complete algorithm can verify every adversarially chosen base network in expected polynomial time, even when the noise level is fixed at 2^-11 and the network is a tiny one-hidden-layer net with fan-in at most three. The proof works by encoding E3SAT so that the maximum network output exactly equals (m-unsat(Φ))/3, giving a verification gap that grows linearly with the number of clauses, and then showing that this gap survives the aggregate perturbation of all coefficients with probability at least 1-e^{-m/8}. The upshot is that generic parameter nondegeneracy is not enough to make exact ReLU verification smoothed-polynomial in the worst case.","feed_headline":"Random noise does not make exact ReLU verification easy","feed_subtitle":"A fixed noise level 2^-11 still leaves verification super-polynomial unless NP is in BPP.","key_machinery":"The carrying object is the compact E3SAT embedding: three ReLU literal units per occurrence with weight ±1, bias ∓1/2, and output weight 2/3, plus one overflow unit with bias -1/3 and output weight -1. The exact identity max g_Φ = (m-unsat)/3, together with the threshold-rounding domination property, turns the NP-hard gap of E3SAT into a verification margin Γ = m/60 that is extensive (linear in m). The robustness transfer is a deterministic weighted Lipschitz inequality, sup_x |g_{θ'}(x) - g_θ(x)| ≤ Σ_q c_q|θ'_q - θ_q|, combined with Gaussian concentration for the D-Lipschitz function F(Z) = Σ c_q|Z_q|; at σ⋆ = 2^-11 this yields preservation probability at least 1-e^{-m/8}.","core_discovery":"The central claim is Theorem 1: if there existed a sound and complete exact algorithm whose expected bit-running time is polynomial in network size, bit complexity, and inverse noise level for every adversarial base instance with 2^{-B} ≤ σ, then NP ⊆ BPP. Equivalently, under NP not in BPP, no such verifier exists. The result already holds for one-hidden-layer ReLU networks on the unit box, hidden fan-in at most three, base coefficients in [-1,1], 4m+1 hidden units, and fixed noise σ⋆ = 2^{-11}. The engine is an exact gap embedding: every E3SAT formula Φ with m clauses maps to a network satisfying max_{x∈[0,1]^n} g_Φ(x) = (m-unsat(Φ))/3, and coordinatewise threshold rounding never decreases","pith_inferences":["Because the transfer theorem is stated generally, similar fixed-noise lower bounds may be derivable from other gap-hard continuous optimization problems, such as MaxCut on unweighted graphs, offering a template for smoothed hardness more broadly.","The extensive-margin mechanism suggests that the decisive quantity is the ratio of logical gap to aggregate coefficient sensitivity, so verifier difficulty likely tracks how margins scale with network size rather than the raw noise level.","Since the input box and threshold are unperturbed and the noise is absolute and small, the result says little about trained networks with data-dependent margins; a natural empirical test is to measure label-change probabilities on real trained networks at σ≈2^-11 and compare them with the e^{-m/8} bound.","The fixed constant 2^-11 is conservative; the rational lower-bound calculations suggest the preservation exponent could be as large as 0.21m, so the qualitative statement is likely robust to significant constant improvements."],"forward_implications":["Under NP not in BPP, there is no universal smoothed-polynomial exact verifier for ReLU networks in the stated perturb-and-round model, even at fixed noise 2^-11.","The hardness already occurs for one-hidden-layer networks with fan-in at most three and only 4m+1 ReLU units, so the obstruction is not architectural complexity.","Exact verification remains hard despite clipping, dyadic rounding, and independent perturbation of every parameter, including output-layer weights and biases.","A corollary of the proof is that any sound-and-complete polynomial expected-time verifier would put SAT in BPP, a concrete collapse that most complexity theorists disbelieve.","The result refutes the idea that generic parameter noise alone, without data-distribution or architectural assumptions, can guarantee smoothed-polynomial verification."],"fun_headline_variants":["Random noise can't make exact ReLU verification easy","Even Gaussian noise fails to simplify ReLU verification","Smoothing ReLU nets doesn't ease exact verification","Exact ReLU verification remains hard under noise","At noise 2^-11, exact ReLU verification stays hard"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The entire argument rests on the exact identity max_x g_Φ(x) = (m-unsat(Φ))/3 and on the fact that threshold-rounding never decreases the objective: if even a small fractional gap existed, the linear verification margin Γ = m/60 would shrink and the fixed-noise preservation bound e^{-m/8} would no longer follow.","fun_headline_variants_meta":{"raw":{"variants":["Random noise can't make exact ReLU verification easy","Even Gaussian noise fails to simplify ReLU verification","Smoothing ReLU nets doesn't ease exact verification","Exact ReLU verification remains hard under noise","At noise 2^-11, exact ReLU verification stays hard"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000795,"raw_usage":{"total_tokens":3414,"prompt_tokens":897,"completion_tokens":2517,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":641,"completion_tokens_details":{"reasoning_tokens":2439}},"tokens_in":641,"tokens_out":2517,"duration_ms":19244,"temperature":1.0,"reasoning_tokens":2439,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-02T02:18:10.765992+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"For any E3SAT formula with m clauses, build the four-ReLU-per-clause network and globally maximize it over the unit box using a rigorous MILP or exhaustive arrangement enumeration; if the maximum exceeds (m-unsat(Φ))/3 by any positive amount, Theorem 2 and hence the linear-margin argument fail. Conversely, the complexity theorem itself would be refuted by exhibiting a single sound-and-complete exact verifier whose expected running time is polynomial in s, B, and 1/σ on all instances of the construction at σ = 2^-11.","supporting_citations":[],"review_version":1}