{"id":"7d717f9b-253a-4f2c-b613-c2b6e3cac2fd","arxiv_id":"2607.05251","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":8.0,"correctness_risk":"unknown","formal_verification":"none","parameter_count":3,"one_line_summary":"SecureCROWN enables privacy-preserving neural network robustness verification via secure two-party computation, eliminating data-dependent branching using ReLU arithmetic and Newton-Raphson refinement.","lead":"This paper presents SecureCROWN, a framework that lets two parties jointly verify a neural network's robustness without revealing the model's parameters or the input data to each other. A smart business person might read this because it could enable third-party safety audits of proprietary AI models in regulated domains like healthcare.","discovery_kind":"unclear","skeptic_critique":{"model":"glm-5.2","headline":"The ε_s stability constant (Eq. 12) makes the perturbed upper relaxation an invalid bound for ReLU, creating a real soundness gap the authors acknowledge but do not resolve.","rationale":"The reader identified the correct load-bearing concern: the ε_s stability constant breaks the validity of the upper relaxation bound, creating a soundness gap that the authors acknowledge but do not formally resolve. My analysis confirms this is not merely a theoretical nicety — the perturbed upper bound is provably below ReLU at z = z̄, so it is genuinely invalid as an upper bound. This means the framework could, in principle, produce false robustness certifications. That said, the CONDITIONAL verdict is appropriate. The paper makes a genuine and novel contribution: it is the first to integrate formal robustness verification with 2PC privacy guarantees, the branch-free reformulation via ReLU (Eqs. 12–14) is elegant and correct as a reformulation, the security proof (Appendix B.1) is a standard and correct hybrid argument, and the experimental fidelity is strong (100% consistency across all tested architectures). The ε_s gap is bounded, acknowledged, and empirically small. The restriction to fully-connected networks limits immediate practical impact but is clearly scoped. The Newton-Raphson refinement and error analysis (Appendix B.3) are reasonable. No other concern rises to the level of the ε_s soundness issue: the security model is standard semi-honest with a trusted dealer, the FSS-based primitives are well-established, and the complexity analysis is straightforward. The verdict should remain CONDITIONAL — the work is sound in its cryptographic design and novel in its contribution, but unconditional soundness of the verification (the core property a verifier must provide) is not yet achieved.","tokens_in":25196,"tokens_out":4519,"duration_ms":108099,"concrete_test":"Construct a minimal 2-layer ReLU network with a single unstable neuron whose pre-activation bounds satisfy z̲ < 0 < z̄, and choose input perturbation radius ε so that the plaintext CROWN certified margin f_y,j is positive but smaller than ε_s · ||Â||_∞ (the regime identified in Remark 1). Run both plaintext CROWN (exact slopes, no ε_s) and SecureCROWN (with ε_s = 10^{-4}) on this instance. If the secure computation produces f_y,j ≤ 0 while plaintext produces f_y,j > 0, the soundness gap is practically exploitable. If no such instance can be found even under systematic search over margin magnitudes in [0, ε_s], the empirical soundness claim is substantially strengthened.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The reader correctly identifies the most load-bearing concern. Eq. (12) introduces ε_s into the denominator of the slope computation: α = ReLU(z̄)/(ReLU(z̄) + ReLU(-z) + ε_s). For an unstable neuron with bounds [z̲, z̄] where z̲ < 0 < z̄, the ideal CROWN slope is α* = z̄/(z̄ - z̲). With ε_s > 0, the perturbed slope α' = z̄/(z̄ - z̲ + ε_s) < α*. The CROWN upper bound is the chord through (z̲, 0) and (z̄, z̄), i.e., α*(z - z̲). The perturbed upper bound uses the same intercept formula β̄ = -α'z̲, giving the line α'(z - z̲). At z = z̄, this evaluates to z̄(z̄ - z̲)/(z̄ - z̲ + ε_s) < z̄ = ReLU(z̄). So the perturbed upper bound lies below ReLU at z = z̄, meaning it is NOT a valid upper bound for the activation. This breaks the soundness of the certified upper bound on the network output: the margin f_y,j could appear positive when the true worst-case margin is negative, leading to false robustness certifications. The authors acknowledge this in Remark 1 (Appendix B.3): 'a verification outcome could in principle change when the certified margin lies within O(ε_s) of zero.' They provide empirical evidence of 100% consistency (Table 4) but no formal fix, noting that 'a slope–intercept co-adjustment that restores provable soundness is left for future work.' For a verification framework whose entire purpose is to provide trustworthy guarantees, this is a genuine soundness gap, not merely a precision issue. The gap is bounded (O(ε_s) perturbation per neuron) and empirically small, but it is theoretically real and could be exploitable on adversarially constructed inputs near the robustness boundary.","agreement_with_reader":"agree"},"referee_report":{"model":"glm-5.2","summary":"The paper presents SecureCROWN, the first framework for privacy-preserving neural network robustness verification using 2PC. The framework enables a model owner and a data owner to jointly compute certified robustness bounds via Linear Bound Propagation (LBP) under the semi-honest security model. The key technical contribution is a branch-free reformulation of the conditional logic in CROWN's ReLU relaxation, replacing data-dependent branching with continuous arithmetic operations (Eqs. 12-14) that can be efficiently evaluated using FSS-based primitives. A Newton-Raphson refinement is introduced for secure reciprocal computation. The paper provides a security proof via a standard hybrid argument (Theorem 6.1), complexity analysis, depth-dependent error bounds (Theorems B.1, B.2), and experiments across 8 architectures on MNIST and CIFAR-10 demonstrating 100% verification consistency with plaintext CROWN.","tokens_in":25571,"tokens_out":1319,"duration_ms":143872,"significance":"The paper addresses a genuine gap at the intersection of formal verification and cryptography: no prior work combines robustness verification with privacy guarantees. The branch-free reformulation of CROWN's piecewise relaxation logic into ReLU-based arithmetic (Eqs. 12-14) is an elegant and correct observation that enables efficient vectorized secure computation. The security proof follows the standard hybrid approach appropriate for the semi-honest model. The error analysis (Theorems B.1, B.2, Corollary B.3) provides depth-dependent bounds with three regimes (stable, unit-norm, unstable). The experimental evaluation is thorough, covering multiple architectures, network conditions (LAN/WAN), and near-boundary verification cases. The replication package is publicly available. The discussion of extensions to other architectures (Appendix D) and malicious security (Appendix C) is informative for future work.","major_comments":[{"comment":"§5.3, Eq. (12) and Remark 1 (Appendix B.3): The stability constant ε_s introduces a soundness gap that is load-bearing for the paper's central claim of faithful verification semantics. For an unstable neuron with bounds [z̲, z̄], the ideal CROWN slope is α* = z̄/(z̄ - z̲). With ε_s > 0, the perturbed slope is α' = z̄/(z̄ - z̲ + ε_s) < α*. The perturbed upper bound uses the same intercept formula β̄ = -α'·z̲, giving the line α'(z - z̲). At z = z̄, this evaluates to z̄(z̄ - z̲)/(z̄ - z̲ + ε_s) < z̄ = ReLU(z̄). Thus the perturbed upper relaxation lies below the ReLU activation at z = z̄, meaning it is not a valid upper bound. This breaks the soundness of the certified upper bound on the network output: the margin f_{y,j} could appear positive when the true worst-case margin is negative, yielding false robustness certifications. The authors acknowledge this in Remark 1 ('a verification could","section":null}],"minor_comments":[{"comment":"Table 1: The MRE values for the 'Unknown' category on MNIST 7×[256] (1.32×10⁻²) and the 'Robust' category on CIFAR-10 10×[200] (1.73×10⁻³) are notably larger than other entries. The paper should discuss whether these reflect specific numerical instability patterns and whether they approach the threshold where verification consistency could break.","section":null},{"comment":"§7.1: The baseline plaintext CROWN is implemented in Python (single-threaded) while SecureCROWN is in C++ (4 threads). While the comparison is for correctness (not speed), clarifying this implementation difference would help readers interpret the MRE values.","section":null},{"comment":"Table 4: The sensitivity analysis only covers MNIST 5×[256]. Given that deeper networks (7×[256], 10×[200]) show higher MRE, a sensitivity analysis on at least one deeper architecture would strengthen the claim that ε_s robustness holds across network depths.","section":null},{"comment":"Appendix B.2, Table 5: The SecARS communication is listed as 'k+2(66)' which appears to be a specific instantiation for k=64. Clarifying the general formula would improve readability.","section":null},{"comment":"§3.1: The notation for lower and upper bounds uses z̲ and z̄, but in some places (e.g., Eq. 2) the subscript formatting is inconsistent. Standardizing throughout would improve clarity.","section":null},{"comment":"Appendix C: The malicious security cost comparison (3.2× online time, 8.7× communication) is informative but the MP-SPDZ baseline uses spdz2k while the paper's implementation uses FSS-based protocols. The comparison is between different protocol families, which should be noted.","section":null},{"comment":"References: The citation for ObliviGate [Song et al., 2026] has a future publication year; this should be verified.","section":null}],"recommendation":"major_revision","confidential_remarks":"The soundness gap from ε_s is the central issue. The authors are transparent about it (Remark 1), which is commendable, but transparency does not resolve the gap for a verification framework whose purpose is trustworthy guarantees. The fix is likely straightforward: either (a) use α' for the slope but adjust the intercept to ensure the perturbed line passes through (z̄, z̄) rather than (z̲, 0), or (b) add a post-hoc check that flags margins within O(ε_s) of zero as 'unknown' rather than 'robust'. Option (b) is particularly simple and would immediately restore soundness at the cost of a small number of additional 'unknown' verdicts. I would view either fix favorably. The cryptographic components (security proof, FSS-based protocols, complexity) are sound and do not require revision."},"author_rebuttal":{"model":"glm-5.2","summary":"We thank the referee for the careful and constructive review. The referee correctly identifies a soundness gap introduced by the stability constant ε_s in the slope computation (Eq. 12). We fully accept this criticism and will revise the manuscript to fix the issue. Below we address the major comment point by point.","responses":[{"response":"The referee's analysis is correct. We have verified the argument: with ε_s > 0, the perturbed slope α' = z̄/(z̄ − z̲ + ε_s) is strictly less than the optimal chord slope α* = z̄/(z̄ − z̲) for unstable neurons. Using the same intercept formula β̄ = −α'·z̲, the perturbed upper relaxation line evaluated at z = z̄ gives α'(z̄ − z̲) = z̄(z̄ − z̲)/(z̄ − z̲ + ε_s) < z̄ = ReLU(z̄). Thus the perturbed upper bound is not a valid relaxation of the ReLU activation, and the certified upper bound on the network output is not guaranteed to be sound. This is a genuine flaw in the current formulation, and we appreciate the referee identifying it precisely.","revision_made":"yes","referee_comment":"§5.3, Eq. (12) and Remark 1 (Appendix B.3): The stability constant ε_s introduces a soundness gap. The perturbed slope α' = z̄/(z̄ - z̲ + ε_s) < α* yields an upper relaxation line that lies below ReLU(z̄) at z = z̄, meaning it is not a valid upper bound. This breaks soundness of the certified upper bound and could yield false robustness certifications."}],"tokens_in":25009,"tokens_out":366,"duration_ms":491764,"standing_objections":[]},"desk_editor":{"model":"glm-5.2","letter":"Bottom line: this is the first paper to port CROWN-style robustness verification into a secure two-party computation setting, and the core technical idea — eliminating data-dependent branching in ReLU relaxation via branch-free arithmetic — is clean and correct. The soundness gap from the stability constant ε_s is real but bounded, and the authors are upfront about it. It deserves a serious referee. Here is my reasoning. What is genuinely new: nobody has done privacy-preserving robustness verification before. Prior MPC work covered secure inference (forward pass), but verification requires backward bound propagation with conditional logic that does not map cleanly onto secret-shared computation. The reformulation of CROWN's piecewise slope computation (Eq. 12) and intercept accumulation (Eqs. 13–14) into ReLU-based arithmetic that avoids per-neuron secure comparisons is the real contribution. It is derived directly from the plaintext equations, not circular. The security proof via standard hybrid argument over FSS primitives is appropriate for semi-honest. The error analysis (Theorems B.1, B.2) gives depth-dependent bounds with three regimes (ρ < 1, = 1, > 1), which is more than perfunctory. Experiments show 100% verification consistency with plaintext CROWN across 8 architectures, and the code is public. What is soft: the ε_s stability constant (Eq. 12) is the load-bearing concern, and the stress-test note is correct. With ε_s > 0, the perturbed slope α' = z̄/(z̄ − z̲ + ε_s) is strictly less than the optimal chord slope α* = z̄/(z̄ − z̲). The perturbed upper bound line α'(z − z̲) evaluates below ReLU(z̄) at z = z̄, so it is not a valid upper bound for the activation. This means the certified margin f_{y,j} could appear positive when the true worst-case margin is negative — a false robustness certificate. The authors acknowledge this in Remark 1 (Appendix B.3) and note that a slope-intercept co-adjustment restoring provable soundness is left for future work. That is an honest disclosure, but for a verification framework whose entire purpose is trustworthy guarantees, it is a genuine theoretical gap. The gap is O(ε_s) per neuron, empirically small (100% consistency even at 1000× default), and unlikely to matter in practice on standard benchmarks. But it is theoretically exploitable on adversarially constructed inputs near the robustness boundary. Scope limitations: fully-connected ReLU networks only. Convolutional layers are discussed but the Toeplitz unfolding would blow up communication. No attention or non-ReLU activations. These are reasonable limitations for a first paper but they cap immediate practical impact. Who this is for: researchers in formal verification and secure computation. The intersection is small but growing. The paper opens a new direction and the technical machinery (branch-free CROWN) is reusable. Recommendation: send to a serious referee who can check both the cryptographic security argument and the bound-propagation algebra. The ε_s soundness gap should be pressed on — the authors need either a formal fix or a clearer statement of when the guarantee holds and when it does not. But this is a real result that deserves review, not a desk reject.","headline":"First 2PC protocol for neural network robustness verification; soundness gap from stability constant is real but bounded and acknowledged.","tokens_in":26272,"tokens_out":750,"would_cite":true,"duration_ms":119678,"reading_group":"no","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"glm-5.2","headline":"SecureCROWN verifies neural network robustness without exposing model or data","keywords":[],"falsifier":"A network and input where the certified margin lies within O(epsilon_s) of zero, causing SecureCROWN to return a different verification decision than plaintext CROWN.","tokens_in":25362,"feed_emoji":"","tokens_out":953,"duration_ms":392921,"temperature":0.7,"pith_summary":"SecureCROWN is a protocol that lets two parties jointly verify the robustness of a neural network without either party revealing their private data. A model owner holds proprietary network parameters; a data owner holds sensitive input data. Using secure two-party computation (2PC), the protocol computes the same certified robustness bounds that a standard plaintext verifier would produce, revealing only the final yes-or-no-no result. The central technical obstacle is that robustness verification via Linear Bound Propagation requires data-dependent conditional branches (to determine ReLU activation states and coefficient signs), which are expensive or incompatible with secure computation protocols. SecureCROWN eliminates all such branching by reformulating every piecewise conditional as a unified arithmetic expression built from ReLU operations, which can be efficiently evaluated under secret sharing using function secret sharing (FSS) primitives. A Newton–Raphson refinement step is added to maintain numerical precision during secure division, since fixed-point rounding errors accumulate through the deep backward recursion that verification requires. The paper provides formal semi-honest security guarantees and shows experimentally that the protocol matches plaintext verification decisions with 100% consistency across eight network architectures, with runtimes ranging from 0.1 to 200 seconds.","feed_headline":"Privacy-preserving neural network verification matches plaintext results","feed_subtitle":"SecureCROWN lets a model owner and data owner jointly certify robustness without revealing model weights or input data, using branch-free Re","key_machinery":"Secure two-party computation (2PC) with additive secret sharing; function secret sharing (FSS) for efficient secure ReLU and comparison operations; branch-free reformulation of CROWN's Linear Bound Propagation; Newton–Raphson refinement for secure reciprocal computation; semi-honest security model with trusted dealer for offline preprocessing","core_discovery":"The key discovery is that the conditional logic inherent in CROWN-style neural network robustness verification—specifically, the piecewise definitions of ReLU relaxation slopes and the sign-dependent intercept accumulation in backward bound propagation—can be completely eliminated by reformulating conditionals as continuous arithmetic expressions using ReLU itself as a selector. This reformulation makes the entire verification circuit branch-free, enabling efficient vectorized execution under secure two-party computation. Combined with a Newton–Raphson-based reciprocal refinement to control division precision in fixed-point arithmetic, this yields a protocol that provably protects both model","pith_inferences":["If the branch-free reformulation strategy generalizes, it could enable privacy-preserving versions of complete verifiers (e.g., branch-and-bound methods) that use conditional logic more extensively than CROWN's incomplete verification, though at higher computational cost.","The 100% verification consistency observed empirically, combined with the acknowledged theoretical gap around the stability constant's effect on soundness, suggests that the practical soundness boundary depends on the distribution of certified margins near zero—an empirical property of trained networks rather than a worst-case guarantee.","The communication cost scaling as O(L²d²) for L-layer networks of width d implies a practical depth limit beyond which online verification becomes prohibitively expensive, potentially constraining applicability to moderately deep fully-connected networks unless convolution-specific optimizations are developed."],"forward_implications":["Privacy-preserving robustness verification becomes feasible in regulated domains (healthcare, finance) where model parameters are proprietary and input data is protected by law, removing the requirement that a single party hold both model and data in plaintext.","The branch elimination technique—reformulating piecewise conditionals as ReLU-based arithmetic—may transfer to other verification methods beyond CROWN that also rely on data-dependent branching, potentially enabling a broader class of privacy-preserving formal verification tools.","The error analysis showing depth-dependent error growth in fixed-point secure computation identifies a structural tension between verification depth and cryptographic precision, motivating future work on adaptive precision or soundness-preserving perturbation bounds.","The protocol's compatibility with batch preprocessing (generating correlated randomness offline for multiple queries) suggests a practical deployment model where a model owner pre-generates verification capacity amortized across many client queries."],"fun_headline_variants":["SecureCROWN verifies NN robustness without exposing private model or input data","Branch-free ReLU reformulation enables privacy-preserving robustness verification for NNs","Secure neural network verification via two-party computation matches plaintext results","Privacy-preserving verification matches plaintext via branch-free secure computation","Branch-free conditionals make secure two-party neural network verification feasible"],"cache_read_input_tokens":0,"weakest_assumption_plain":"The stability constant epsilon_s is added to the denominator of the slope computation to prevent division by zero, but it perturbs the relaxation away from its ideal form. The paper acknowledges that if this perturbation shifts a certified margin across zero, the verification outcome could change, and a full slope–intercept co-adjustment restoring provable soundness is left for future work.","fun_headline_variants_meta":{"raw":{"variants":["SecureCROWN verifies NN robustness without exposing private model or input data","Branch-free ReLU reformulation enables privacy-preserving robustness verification for NNs","Secure neural network verification via two-party computation matches plaintext results","Privacy-preserving verification matches plaintext via branch-free secure computation","Branch-free conditionals make secure two-party neural network verification feasible"]},"model":"glm-5.2","effort":"high","cost_usd":0.0,"raw_usage":{"total_tokens":1062,"prompt_tokens":504,"completion_tokens":558,"prompt_tokens_details":null},"tokens_in":504,"tokens_out":558,"duration_ms":95469,"temperature":1.0,"reasoning_tokens":601,"cache_read_input_tokens":0,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-07T21:36:48.466777+00:00","model_set":{"reader":"glm-5.2"},"falsifier":"A network and input where the certified margin lies within O(epsilon_s) of zero, causing SecureCROWN to return a different verification decision than plaintext CROWN.","supporting_citations":[],"review_version":1}