Pith. sign in

REVIEW 2 major objections 4 minor 46 references

Fast SDP certification of neural networks : towards large multi-class datasets

T0 review · 2 major / 4 minor · reviewed 2026-07-12 · grok-4.5

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read One SDP can certify a neural net against every wrong class at once, instead of one class at a time.

desk verdict Clean single-solve multi-class SDP plus generic active-neuron pruning; solid math and transparent experiments, ordinary incomplete-verifier caveats on size and tightness. read the letter →

arxiv 2607.03232 v1 pith:VQCGFO62 submitted 2026-07-03 math.CO stat.ML

Margot Boyer (CEDRIC - OC) , Clément Rambour (ISIR) , Zacharie Alès (UMA) , Amélie Lambert (CEDRIC - OC) This is my paper · ORCID
classification math.COstat.ML MSC 90C2268T0790C26
keywords adversarialrobustnessneuralnetworkcertificationsemidefiniteprogrammingReLUnetworksincompleteverificationmulti-classneuronpruningquadratic
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 4 minor

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 imes100, 9 imes200) 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.

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 (2)
  1. Section 5.3 and Figures 2a–b: on the 9 imes100 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.
  2. Table 1 and Section 5.2: the RLT cut percentage is set to 100 % for SDP_U on 9 imes100 and FCNNA but only 60 % on 9 imes200, 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.
minor comments (4)
  1. 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.
  2. 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.
  3. Figure 1 caption mentions “blue and purple” blocks that are hard to distinguish in grayscale printouts; a pattern or label would improve accessibility.
  4. 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; the untargeted QP_U equivalence, SDP relaxation, and active-neuron pruning are standard valid reformulations that do not reduce by construction to fitted inputs or self-justifying citations.

full rationale

The central claims rest on elementary reformulation of the multi-class min (Theorem 1 equates v(QP_U) to min_j v(QP_T^j) by introducing binary indicators eta_j that select the worst target, with the non-negativity property of Proposition 4 following immediately) and on standard SDP linearization of quadratic ReLU constraints plus McCormick envelopes. The active-neuron pruning (Section 4.3, eqs. 30–31, Proposition 6) replaces equalities by valid inequalities derived from bounds; it preserves soundness of any non-negative certificate while only risking tightness. Pre-activation bounds L_k, U_k come from an external tool (α-β-CROWN) and RLT percentages are free parameters that affect only computational tightness, never validity. Self-citations ([2], [23], [33]) are used solely as baselines or for chordal/RLT building blocks that are independently established; none is load-bearing for uniqueness or for the new multi-class equivalence. No fitted parameter is renamed a prediction, no ansatz is smuggled, and no result is definitionally equivalent to its own input. The derivation chain is therefore self-contained and non-circular.

Assumptions & free parameters 2 free parameters · 4 assumptions · 3 invented entities

The paper is a methods contribution that inherits the standard SDP relaxation framework for non-convex quadratic programs and the chordal-decomposition technique of earlier verification papers. The only free numerical choices are the fraction of RLT cuts retained and the four deterministic McCormick bounds kept after pruning; both affect tightness, not soundness of a non-negative certificate. No new physical entities are postulated.

free parameters (2)
  • RLT cut percentage p = 60 % or 100 %
    Hand-chosen (100 % for 9x100 and FCNNA, 60 % for 9x200) to keep the SDP tractable; directly controls the number of linear inequalities and therefore the obtained bound.
  • number of McCormick bounds retained after pruning = 4
    Only four linear inequalities (two lower, two upper) are generated per ReLU even though exponentially many combinations exist; the selection is deterministic but arbitrary and affects tightness.
assumptions (4)
  • domain assumption A non-negative lower bound on the certification problem is a valid robustness certificate (incomplete verification principle).
    Stated in the introduction and used throughout; standard in the incomplete-verifier literature.
  • standard math The SDP lift of a quadratic program with the usual linearization of products and the PSD constraint yields a valid lower bound.
    Classical Shor-style relaxation; invoked when (SDP) and (SDP_U) are introduced.
  • domain assumption Pre-activation bounds L_k, U_k computed by α-β-CROWN are valid (though possibly loose).
    Used to construct the quadratic bound constraints and all McCormick envelopes; external tool whose correctness is assumed.
  • standard math Chordal decomposition of the moment matrix into consecutive-layer blocks preserves the SDP feasible set for the ReLU constraints.
    Taken from Batten et al. / Vandenberghe & Andersen and used for both the targeted and untargeted formulations.
invented entities (3)
  • untargeted quadratic program (QP_U) with binary class indicators β_j
    purpose: Encode the min over all target classes inside a single optimization so that one SDP certifies full robustness.
    Defined in Section 4.1; the binary variables and the equality sum β_j = 1 are new relative to prior targeted SDP models.
  • pair of quadratic inequalities (28)–(29) coupling two adversarial logits and their indicators
    purpose: Tighten the multi-class SDP by forcing the selected adversarial logit to dominate the others.
    Introduced in Section 4.2 and proved valid for (QP_U) in Proposition 5; not present in earlier SDP verifiers.
  • stable-active neuron pruning with McCormick restoration of cross-layer products
    purpose: Remove variables corresponding to permanently active ReLUs while keeping a valid (relaxed) SDP of smaller size.
    Described in Section 4.3; the four linear inequalities (30)–(31) replace the missing quadratic terms.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Fast SDP certification of neural networks : towards large multi-class datasets." pith.science (2026). https://pith.science/paper/VQCGFO62

@misc{pith2026260703232,
  author       = {Pith},
  title        = {Pith review of: Fast SDP certification of neural networks : towards large multi-class datasets},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/VQCGFO62}},
  note         = {Machine review of arXiv:2607.03232}
}
read the original abstract

We present a new quadratic model for the certification problem in adversarial robustness, which simultaneously accounts for all possible target classes. Building on this model, we propose a novel semidefinite programming (SDP) relaxation for incomplete verification. A key advantage of our approach is that it certifies robustness in a single optimization, avoiding the need for a separate resolution per class. This yields a significant computational speed-up and enables scalability to large datasets with many classes. To further improve efficiency, we also propose an effective pruning strategy of active neurons, thus reducing the problem dimensionality and accelerating convergence.

Figures

Figures reproduced from arXiv: 2607.03232 by the authors.

Figure 1
Figure 1. Multiclass certification Our method provides a new quadratic formu￾lation for certifying a DNN across all labels simultaneously. It relies on binary variables {βj} indicating the class associated with the worst adversarial exam￾ple. To further reduce the number of variables, we also propose a pruning strat￾egy that removes both inactive (blue) and active (yellow) neurons. By use of a chordal decomposition of the SDP… view at source ↗
Figure 2
Figure 2. Impact of stable active neuron pruning on SDP-based certification. (a [PITH_FULL_IMAGE:figures/full_fig_p014_2.png] view at source ↗
Figure 3
Figure 3. Time vs # of classes We compare the runtime performance of SDPU and SDPT in [PITH_FULL_IMAGE:figures/full_fig_p015_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

46 extracted references · 10 linked inside Pith

  1. [1]

    Journal of Global Optimization43(2), 471–484 (2009)

    Anstreicher, K.M.: Semidefinite programming versus the reformulation- linearization technique for nonconvex quadratically constrained quadratic programming. Journal of Global Optimization43(2), 471–484 (2009)

    2009

  2. [2]

    In: Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence

    Batten, B., Kouvaros, P., Lomuscio, A., Zheng, Y.: Efficient Neural Network Verification via Layer-based Semidefinite Relaxations and Linear Cuts. In: Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence. pp. 2184–2190. International Joint Conferences on Artificial Intelligence Organization, Montreal, Canada (Aug 2021)

    2021

  3. [3]

    AAAI34(04), 3291–3299 (Apr 2020)

    Botoeva, E., Kouvaros, P., Kronqvist, J., Lomuscio, A., Misener, R.: Effi- cient Verification of ReLU-Based Neural Networks via Dependency Analy- sis. AAAI34(04), 3291–3299 (Apr 2020)

    2020

  4. [4]

    JMLR (2020)

    Bunel,R.,Turkaslan,I.,Torr,P.H.S.,Kumar,M.P.,Lu,J.,Kohli,P.:Branch and Bound for Piecewise Linear Neural Network Verification. JMLR (2020)

    2020

  5. [5]

    Carlini, N., Wagner, D.: Towards Evaluating the Robustness of Neural Net- works (Mar 2017), arXiv:1608.04644 [cs]

    arXiv 2017

  6. [6]

    In: D’Souza, D., Narayan Kumar, K

    Cheng, C.H., Nührenberg, G., Ruess, H.: Maximum Resilience of Artificial Neural Networks. In: D’Souza, D., Narayan Kumar, K. (eds.) Automated Technology for Verification and Analysis, vol. 10482, pp. 251–268. Springer International Publishing, Cham (2017), series Title: Lecture Notes in Com- puter Science

    2017

  7. [7]

    Chiu, H.M., Chen, H., Zhang, H., Zhang, R.Y.: SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming (Jun 2025)

    2025

  8. [8]

    In: ICML

    Chiu, H.M., Zhang, R.Y.: Tight Certification of Adversarially Trained Neu- ral Networks via Nonconvex Low-Rank Semidefinite Relaxations. In: ICML. pp. 5631–5660. PMLR (Jul 2023)

    2023

Show all 46 references
  1. [9]

    NeurIPS (2018)

    Dathathri, S., Kurakin, A., Raghunathan, A., Uesato, J., Bunel, R., Shankar, S., Steinhardt, J., Goodfellow, I., Liang, P., Kohli, P.: Enabling certification of verification-agnostic networks via memory-efficient semidef- inite programming. NeurIPS (2018)

    2018

  2. [10]

    Ehlers, R.: Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks (Aug 2017), arXiv:1705.01320 [cs]

    2017 arXiv

  3. [11]

    Ferrari, C., Muller, M.N., Jovanovic, N., Vechev, M.: Complete Verifica- tion via Multi-Neuron Relaxation Guided Branch-and-Bound (Apr 2022), arXiv:2205.00263 [cs]

    2022 arXiv

  4. [12]

    Constraints23(3), 296–309 (Jul 2018)

    Fischetti, M., Jo, J.: Deep neural networks and mixed integer linear opti- mization. Constraints23(3), 296–309 (Jul 2018)

    2018

  5. [13]

    Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and Harnessing Adver- sarial Examples (Mar 2015), arXiv:1412.6572 [stat]

    2015 arXiv

  6. [14]

    In: IJCAI

    Gowal, S., Dvijotham, K., Stanforth, R., Mann, T., Kohli, P.: A dual ap- proach to verify and train deep networks. In: IJCAI. pp. 6156–6160. IJCAI (7 2019) Fast SDP certification of neural networks : towards large multi-class datasets 17

    2019

  7. [15]

    https://doi.org/10.48550/arXiv.2407.15049, http://arxiv.org/abs/2407.15049, arXiv:2407.15049 [math.OC]

    Han, Q., Lin, Z., Liu, H., Chen, C., Deng, Q., Ge, D., Ye, Y.: Accel- erating Low-Rank Factorization-Based Semidefinite Programming Algo- rithms on GPU (Aug 2024). https://doi.org/10.48550/arXiv.2407.15049, http://arxiv.org/abs/2407.15049, arXiv:2407.15049 [math.OC]

    2024 doi arXiv

  8. [16]

    In: IJCAI

    Henriksen, P., Lomuscio, A.: DEEPSPLIT: An Efficient Splitting Method for Neural Network Verification via Indirect Effect Analysis. In: IJCAI. pp. 2549–2555. IJCAI, Montreal, Canada (Aug 2021)

    2021

  9. [17]

    Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neuralnetworks.In:Internationalconferenceoncomputeraidedverification. pp. 3–29. Springer (2017)

    2017

  10. [18]

    Jaeckle, F., Lu, J., Kumar, M.P.: Neural Network Branch-and-Bound for Neural Network Verification (Jul 2021), arXiv:2107.12855 [cs]

    2021 arXiv

  11. [19]

    Advances in neural information processing systems33, 3647–3658 (2020)

    Jung, S., Ahn, H., Cha, S., Moon, T.: Continual learning with node- importance based adaptive group sparse regularization. Advances in neural information processing systems33, 3647–3658 (2020)

    2020

  12. [20]

    Computer Aided Verification (May 2017), arXiv:1702.01135 [cs]

    Katz, G., Barrett, C., Dill, D., Julian, K., Kochenderfer, M.: Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. Computer Aided Verification (May 2017), arXiv:1702.01135 [cs]

    2017 arXiv

  13. [21]

    Kurakin,A.,Goodfellow,I.,Bengio,S.:Adversarialexamplesinthephysical world (Feb 2017)

    2017

  14. [22]

    AAAI 37(12), 14946–14954 (Jun 2023)

    Lan, J., Brückner, B., Lomuscio, A.: A Semidefinite Relaxation Based Branch-and-Bound Method for Tight Neural Network Verification. AAAI 37(12), 14946–14954 (Jun 2023)

    2023

  15. [23]

    AAAI36(7), 7272– 7280 (Jun 2022)

    Lan, J., Zheng, Y., Lomuscio, A.: Tight Neural Network Verification via Semidefinite Relaxations and Linear Reformulations. AAAI36(7), 7272– 7280 (Jun 2022)

    2022

  16. [24]

    AAAI37(12), 14937–14945 (Jun 2023)

    Lan, J., Zheng, Y., Lomuscio, A.: Iteratively Enhanced Semidefinite Relax- ations for Efficient Neural Network Verification. AAAI37(12), 14937–14945 (Jun 2023)

    2023

  17. [25]

    IEEE symposium on security and privacy (SP) (Apr 2023), arXiv:2009.04131 [cs]

    Li, L., Xie, T., Li, B.: SoK: Certified Robustness for Deep Neural Networks. IEEE symposium on security and privacy (SP) (Apr 2023), arXiv:2009.04131 [cs]

    2023 arXiv

  18. [26]

    Liao, Y., Genest, B., Meel, K., Aryaman, S.: Solution-aware vs global ReLU selection: partial MILP strikes back for DNN verification (Jul 2025), arXiv:2507.23197 [cs]

    2025 arXiv

  19. [27]

    ICLR (Dec 2019)

    Lu, J., Kumar, M.P.: Neural Network Branching for Neural Network Veri- fication. ICLR (Dec 2019)

    2019

  20. [28]

    Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards Deep Learning Models Resistant to Adversarial Attacks (Sep 2019)

    2019

  21. [29]

    Mathematical Pro- gramming10(1), 147–175 (1976)

    McCormick, G.: Computability of global solutions to factorable non-convex programs: Part i - convex underestimating problems. Mathematical Pro- gramming10(1), 147–175 (1976)

    1976

  22. [30]

    In: CVPR

    Moosavi-Dezfooli, S.M., Fawzi, A., Frossard, P.: DeepFool: A Simple and Accurate Method to Fool Deep Neural Networks. In: CVPR. pp. 2574–2582. IEEE, Las Vegas, NV, USA (Jun 2016) 18 M. Boyer et al

    2016

  23. [31]

    Version 9.2

    MOSEK ApS: The MOSEK optimization toolbox for MATLAB manual. Version 9.2. (2019), http://docs.mosek.com/9.0/toolbox/index.html

    2019

  24. [32]

    Papernot, N., McDaniel, P., Jha, S., Fredrikson, M., Celik, Z.B., Swami, A.: The Limitations of Deep Learning in Adversarial Settings (Nov 2015)

    2015

  25. [33]

    NeurIPS (2018)

    Raghunathan, A., Steinhardt, J., Liang, P.: Semidefinite relaxations for cer- tifying robustness to adversarial examples. NeurIPS (2018)

    2018

  26. [34]

    NeurIPS (2019)

    Salman, H., Yang, G., Li, J., Zhang, P., Zhang, H., Razenshteyn, I., Bubeck, S.: Provably Robust Deep Learning via Adversarially Trained Smoothed Classifiers. NeurIPS (2019)

    2019

  27. [35]

    Serra,T.,Kumar,A.,Ramalingam,S.:LosslessCompressionofDeepNeural Networks (Feb 2020), arXiv:2001.00218 [cs]

    2020 arXiv

  28. [36]

    SIAM Journal Discrete Mathematics3, 411–430 (1990)

    Sherali, H., Adams, W.: A hierarchy of relaxation between the continuous and convex hull representations for zero-one programming problems. SIAM Journal Discrete Mathematics3, 411–430 (1990)

    1990

  29. [37]

    Proceedings of the ACM on Programming Languages 3(POPL), 1–30 (Jan 2019)

    Singh, G., Gehr, T., Püschel, M., Vechev, M.: An abstract domain for certi- fying neural networks. Proceedings of the ACM on Programming Languages 3(POPL), 1–30 (Jan 2019)

    2019

  30. [38]

    ICLR (Feb 2019)

    Tjeng, V., Xiao, K., Tedrake, R.: Evaluating Robustness of Neural Networks with Mixed Integer Programming. ICLR (Feb 2019)

    2019

  31. [39]

    Foundations and Trends in Optimization1(4), 241–433 (May 2015)

    Vandenberghe, L., Andersen, M.S.: Chordal Graphs and Semidefinite Op- timization. Foundations and Trends in Optimization1(4), 241–433 (May 2015)

    2015

  32. [40]

    NeurIPS (2021)

    Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S., Hsieh, C.J., Kolter, Z.: Beta- CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Neural Network Robustness Verification. NeurIPS (2021)

    2021

  33. [41]

    ICML (2018)

    Weng,T.W.,Zhang,H.,Chen,H.,Song,Z.,Hsieh,C.J.,Boning,D.,Dhillon, I.S., Daniel, L.: Towards Fast Computation of Certified Robustness for ReLU Networks. ICML (2018)

    2018

  34. [42]

    ICML (2018)

    Wong, E., Kolter, J.Z.: Provable Defenses against Adversarial Examples via the Convex Outer Adversarial Polytope. ICML (2018)

    2018

  35. [43]

    In: Gurfinkel, A., Ganesh, V

    Wu, H., Isac, O., Zeljić, A., Tagomori, T., Daggitt, M., Kokke, W., Re- faeli, I., Amir, G., Julian, K., Bassan, S., Huang, P., Lahav, O., Wu, M., Zhang, M., Komendantskaya, E., Katz, G., Barrett, C.: Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. In: Gurfinkel, ...

    2024

  36. [44]

    NeurIPS (2022)

    Zhang, H., Wang, S., Xu, K., Li, L., Li, B., Jana, S., Hsieh, C.J., Kolter, J.Z.: General Cutting Planes for Bound-Propagation-Based Neural Network Verification. NeurIPS (2022)

    2022

  37. [45]

    NeurIPS (2020)

    Zhang, R.Y.: On the Tightness of Semidefinite Relaxations for Certifying Robustness to Adversarial Examples. NeurIPS (2020)

    2020

  38. [46]

    NeurIPS (2024)

    Zhou, D., Brix, C., Hanasusanto, G.A., Zhang, H.: Scalable Neural Net- work Verification with Branch-and-bound Inferred Cutting Planes. NeurIPS (2024)

    2024

Pith tools

Reviewed July 12, 2026 · model on record in the stance chip above.