{"id":"1a2af57c-0955-4faa-817b-6f00cb4654e6","arxiv_id":"2607.03232","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"low","formal_verification":"none","parameter_count":2,"one_line_summary":"An untargeted SDP relaxation certifies full multi-class ReLU robustness in a single solve, with stable-active neuron pruning that shrinks the matrices and accelerates convergence.","lead":"A new quadratic model and SDP relaxation certify ReLU network robustness against every target class in one optimization instead of one solve per class. The approach plus active-neuron pruning yields large speed-ups on multi-class data and is offered as a path toward ImageNet-scale verification.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.5","headline":"No significant objection identified; the central equivalence and pruning validity hold under the paper's stated conditions.","rationale":"The paper's strongest claim is the equivalence of Theorem 1 together with the soundness of the resulting single SDP and of the active-neuron pruning. Both statements are proved under the usual ReLU quadratic encoding and McCormick envelopes; no hidden assumption that would invalidate them was found. The only soft spot is the practical tightness of the four selected linear relaxations once stable active neurons are eliminated—an effect already quantified by the authors and correctly identified by the Reader. Because that effect can only make the method more conservative (never unsound), it does not overturn the central algorithmic contribution. The experimental comparison remains transparent, code is public, and the modest network sizes are typical for SDP-based incomplete verifiers. Hence the Reader's CONDITIONAL verdict is left unchanged.","tokens_in":15661,"tokens_out":536,"duration_ms":5255,"concrete_test":"Re-run the 9x100 and 9x200 experiments of Table 1 twice: once with the original α-β-CROWN bounds and once after artificially widening every pre-activation interval by 20 %. If the number of certified points falls by more than 15 % under the widened bounds while the unpruned SDP_T baseline stays essentially unchanged, the pruning-induced looseness is confirmed as the dominant practical limitation; otherwise the concern is overstated.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The reader's weakest_assumption correctly flags that loose pre-activation bounds can make the four selected McCormick-style relaxations of cross-layer products (eqs. 30–31) turn a certifiable instance into an inconclusive one after active-neuron pruning. That risk is real and is already acknowledged by the authors in §5.3 (certification-rate drop on the small 9x100 net). It is not, however, a load-bearing flaw in the central claim: Theorem 1 equates v(QP_U) with min_j v(QP_T^j) independently of any bound quality, Proposition 4 only requires a non-negative lower bound of the SDP, and Proposition 6 merely quantifies the size reduction. The pruning step replaces equalities by valid inequalities; it never produces a false positive certificate. Consequently the mathematical core (single-solve multi-class certification + size reduction that preserves soundness) stands, while the practical tightness issue remains an ordinary engineering caveat for incomplete verifiers.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.5","summary":"The paper introduces an untargeted quadratic program (QP_U) for multi-class adversarial robustness certification of ReLU networks. Binary indicators β_j select the worst target class so that a single optimization equals the minimum of the classical per-target problems (Theorem 1). A chordal SDP relaxation of QP_U, tightened by McCormick envelopes, RLT cuts and two new quadratic inequalities (28)–(29), therefore certifies full robustness whenever its optimal value is non-negative (Proposition 4). Stable-active neurons are pruned by linear substitution; the resulting cross-layer products are restored by four McCormick inequalities (30)–(31), reducing matrix dimensions (Proposition 6) while preserving soundness. Experiments on MNIST (9\times100, 9\times200) and CIFAR-100 (FCNNA) show that the single-solve formulation is substantially faster than three prior targeted SDP baselines once the number of classes grows, and that active-neuron pruning further reduces wall-clock time.","tokens_in":15913,"tokens_out":953,"duration_ms":9501,"significance":"If the claims hold, the work removes the linear dependence of SDP certification cost on the number of classes—an obstacle that currently prevents SDP methods from scaling to ImageNet-scale label sets. The active-neuron pruning technique is generic and can be applied to any existing chordal SDP verifier. The mathematical core (Theorem 1, Propositions 4–6) is elementary yet previously unexploited; the accompanying code repository and explicit comparison against three published SDP baselines make the contribution immediately usable and falsifiable.","major_comments":[{"comment":"Section 5.3 and Figures 2a–b: on the 9\times100 network the active-neuron pruning step measurably lowers the certification rate of SDP_U (while the same pruning leaves the targeted baselines almost unchanged). The authors correctly note that the four selected McCormick inequalities (30)–(31) relax equalities; however, no quantitative bound is given on how much the optimal value can drop, nor is a systematic comparison of alternative selections of the four inequalities provided. Because the paper’s central selling point is that the single-solve model remains competitive after pruning, a short ablation that reports the gap between the pruned and unpruned SDP values (or a simple dual-feasibility certificate of the lost tightness) is needed before the practical claim can be fully accepted.","section":null},{"comment":"Table 1 and Section 5.2: the RLT cut percentage is set to 100 % for SDP_U on 9\times100 and FCNNA but only 60 % on 9\times200, while the targeted baselines are restricted to 10 %. The text attributes the higher percentage to the single-solve formulation, yet no experiment isolates the contribution of the extra cuts from the contribution of class aggregation. Without that isolation it is difficult to judge how much of the reported speed-up and accuracy gain is truly due to the untargeted model versus simply being able to afford more cuts.","section":null}],"minor_comments":[{"comment":"Several appendix cross-references appear as “Appendix??” (e.g., after the RLT heuristic, after the pruning derivation, after the network architectures). These should be resolved or the material moved into the main text.","section":null},{"comment":"Notation for the chordal blocks is inconsistent: P_k is introduced both as the full matrix and as the two-layer submatrix; a short clarifying sentence after equation (13) would help.","section":null},{"comment":"Figure 1 caption mentions “blue and purple” blocks that are hard to distinguish in grayscale printouts; a pattern or label would improve accessibility.","section":null},{"comment":"Proposition 5 claims validity of inequalities (28)–(29) but the proof is omitted; a one-paragraph argument (or a pointer to the appendix) should be added.","section":null}],"recommendation":"minor_revision","confidential_remarks":"The mathematical core is sound and the experimental design is fair. The two major comments are engineering rather than foundational; once the authors supply the missing ablation on pruning tightness and the RLT-percentage isolation, the paper is ready for acceptance. Fit for a computational-optimization or verification venue is excellent."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"The useful bit is the untargeted quadratic program that folds every target class into one objective with binary indicators, so one SDP certifies full multi-class robustness instead of looping over targets. Theorem 1 shows the optimum equals the min over the usual targeted problems, and Proposition 4 therefore lets a non-negative SDP bound certify everything at once. That is the real engineering win for datasets with dozens or hundreds of classes.\n\nThey also give a generic pruning of stable-active neurons: replace them by their linear expressions, restore the missing cross-layer products with McCormick bounds so the chordal decomposition stays intact, and keep only four of the resulting inequalities. Proposition 6 quantifies the matrix-size drop. The same pruning works on ordinary targeted SDPs, which is a nice freebie. Two new quadratic cut families (28)–(29) tighten the multi-class model further. Experiments on 9x100, 9x200 and a CIFAR-100 FCNNA compare wall-clock and certified accuracy against three prior SDP baselines; code is public. On the larger nets and the 67-class composite the single-solve version is clearly faster and still competitive on certificates.\n\nSoft spots are ordinary for this literature. Networks remain modest fully-connected nets; RLT percentage and which four McCormick bounds to keep are free parameters; and when pre-activation intervals from α-β-CROWN are loose the pruning can turn a certifiable instance into an inconclusive one (they show the drop on 9x100). It never produces a false positive, so soundness is intact. Scalability claims would be stronger with deeper or convolutional nets and automatic cut selection, but that is future work, not a hole in the present claims.\n\nAnyone working on incomplete SDP verifiers or multi-class robustness should read it. The math is clean, the comparison is fair, and the central equivalence holds. I would send it to referees.","headline":"Clean single-solve multi-class SDP plus generic active-neuron pruning; solid math and transparent experiments, ordinary incomplete-verifier caveats on size and tightness.","tokens_in":16559,"tokens_out":471,"would_cite":true,"duration_ms":4889,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["90C22","68T07","90C26"],"pacs":[],"model":"grok-4.5","headline":"One SDP can certify a neural net against every wrong class at once, instead of one class at a time.","keywords":["adversarial robustness","neural network certification","semidefinite programming","ReLU networks","incomplete verification","multi-class robustness","neuron pruning","quadratic programming"],"falsifier":"Run SDP_U and the best targeted SDP baseline on the same 100-class network and the same 1000 images; if the single-model method is not faster by a large factor while certifying at least as many images, the claimed scalability advantage fails.","tokens_in":16558,"feed_emoji":"🛡️","tokens_out":616,"duration_ms":6455,"temperature":0.7,"pith_summary":"Certifying that a ReLU network cannot be fooled inside a small ball around an input usually means solving a separate hard optimization problem for every possible wrong label. The authors rewrite the problem as a single untargeted quadratic program whose optimum is exactly the worst of those per-class optima. A semidefinite relaxation of that program therefore either certifies full multi-class robustness in one shot or returns an inconclusive negative bound. They further shrink the matrices by algebraically eliminating every neuron that is stably active, replacing the missing cross-layer products with four simple linear inequalities. On networks with dozens of classes the single-model approach stays fast while class-by-class SDP methods become prohibitive, giving a practical incomplete verifier for large multi-class data sets.","feed_headline":"One SDP certifies every wrong class at once","feed_subtitle":"An untargeted quadratic model plus active-neuron pruning scales neural-net verification to large label sets","key_machinery":"The untargeted quadratic model QP_U together with its chordal SDP relaxation SDP_U: binary indicators select the worst target class inside one matrix, McCormick and custom quadratic cuts keep the relaxation tight, and stable-active neurons are pruned by recursive linear substitution plus four bounding inequalities that preserve chordal structure.","core_discovery":"The untargeted quadratic program QP_U has the same optimal value as the minimum of the classical targeted programs over every wrong class. Consequently any non-negative lower bound obtained from its SDP relaxation certifies that the network is robust to every possible target simultaneously, and the same bound is obtained without looping over classes.","pith_inferences":[],"forward_implications":[],"fun_headline_variants":["One SDP certifies robustness against every wrong class","Untargeted SDP verifies all targets in a single solve","SDP bound proves multi-class robustness without class loops","Pruned SDP certifies large multi-class nets in one shot","Quadratic untargeted model speeds SDP neural-net verification"],"cache_read_input_tokens":128,"weakest_assumption_plain":"The pre-activation bounds coming from the bound-propagation routine must be tight enough that the McCormick envelopes and the four linear relaxations of cross-layer products still let the SDP produce a useful non-negative number; if those bounds are loose, pruning can turn a certifiable instance into an inconclusive one.","fun_headline_variants_meta":{"raw":{"variants":["One SDP certifies robustness against every wrong class","Untargeted SDP verifies all targets in a single solve","SDP bound proves multi-class robustness without class loops","Pruned SDP certifies large multi-class nets in one shot","Quadratic untargeted model speeds SDP neural-net verification"]},"model":"grok-4.5","effort":"low","cost_usd":0.00523,"raw_usage":{"total_tokens":1349,"prompt_tokens":620,"num_sources_used":0,"completion_tokens":81,"cost_in_usd_ticks":52300000,"prompt_tokens_details":{"text_tokens":620,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":648,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":620,"tokens_out":81,"duration_ms":6024,"temperature":1.0,"reasoning_tokens":648,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-12T03:57:05.477763+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"Run SDP_U and the best targeted SDP baseline on the same 100-class network and the same 1000 images; if the single-model method is not faster by a large factor while certifying at least as many images, the claimed scalability advantage fails.","supporting_citations":[],"review_version":1}