Pith. sign in

REVIEW 4 major objections 5 minor 55 references

Interior-Point Vanishing Problem in Semidefinite Relaxations for Neural Network Verification

T0 review · 4 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read Semidefinite verification of ReLU networks loses strict feasibility as depth grows, and removing inherited per-layer bound constraints restores solvability for most previously unsolved instances.

desk verdict Useful empirical paper on why SDP verification breaks on deeper networks, but the 'interior-point vanishing' theory overreaches: the strict-feasibility proof is missing and the real contribution is B-Remove. read the letter →

arxiv 2506.10269 v1 pith:2BWZFCST submitted 2025-06-12 cs.LG math.OC

Ryota Ueda , Takami Sato , Ken Kobayashi , Kazuhide Nakata This is my paper · ORCID
classification cs.LGmath.OC
keywords semidefiniteprogrammingrelaxationneuralnetworkverificationstrictfeasibilitySlater'sconditionReLUnetworksinterior-pointmethodsadversarialrobustnessboundpropagation
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

This paper argues that semidefinite programming (SDP) relaxation, one of the tightest convex methods for verifying ReLU networks, has a hidden scaling barrier: as the network grows deeper, the relaxed problem loses strict feasibility, the Slater condition that interior-point solvers need for numerical stability and certified optimality. The authors call this interior-point vanishing and support it with both a theoretical eigenvalue bound and experiments: for fully connected networks with ten or more layers, the strict-feasibility check returns optimal values at or below zero and standard interior-point solvers stop terminating with guarantees. They trace the damage to two constraints inherited from the original formulation, the ReLU equality constraints and the per-layer upper/lower bound constraints, and show that the bounds are not needed by the SDP and are actively harmful. Two of their five proposed relaxations, a small tolerance on the ReLU equality and, most strikingly, simply removing the per-layer bounds, let solvers succeed on 88% of the instances that prior SDP methods could not solve, about 41% of all tested instances.

What carries the argument

The central object is the lifted moment matrix $P = vv^\top$ (with the rank-one constraint dropped) from problem (5), and the strict-feasibility verification problem (7) that tests whether any feasible $P$ is positive definite by maximizing the shift $\lambda$ with $X+\lambda I$. The load-bearing identity is Theorem 3.6, an upper bound on $\lambda_{\min}(P)$ obtained by propagating trace bounds $T_i$ on $\operatorname{tr}(P[x_i x_i^\top])$ through Schur complements; it connects depth to small row norms of $\tilde W_i = (b_i\ W_i)$. The proposed remedies act on the two constraints identified as sensitive, the ReLU equality (5d) and the per-layer bound constraints (5e), by allowing a tolerance, using a Leaky-ReLU outer approximation, diagonal or weight scaling, or removing the bounds entirely.

What would settle it

Take a specific 10-layer ReLU network where the paper reports interior-point vanishing and directly compute the optimal value of the strict-feasibility problem (7) with arbitrary-precision arithmetic on the exact SDP data: a strictly positive optimal value would show strict feasibility is not actually lost, and a solver that terminates with a certified optimum on the original formulation would weaken the claim that a Slater point is necessary for scaling.

Watch

Extended reading notes

Core claim

The paper's central claim is that the SDP relaxation (5) of the ReLU verification problem is generically not strictly feasible once the network is deep, and that this is a property of the relaxation itself rather than of training. The formal core is Proposition 3.3 (an inactive neuron forces a zero diagonal entry of $P$, hence $\lambda_{\min}(P)=0$ for every feasible $P$) and Theorem 3.6, which bounds $\lambda_{\min}(P)$ by the smallest squared row norm of the extended weight matrices $\tilde W_i(j,:)$: $\lambda_{\min}(P) \le \min_i \min_j (1+T_i)\,\|\tilde W_i(j,:)\|_2^2$, where $T_i$ propagates input and activation bounds. Since realistic networks contain neurons whose extended weight rows are small, the bound pushes the minimum eigenvalue to zero; empirically the strict-feasibility verification problem (7) returns nonpositive optimal values at $L\ge 10$, and interior-point solvers fail. The paper then isolates the ReLU equality constraint (5d) and the upper-bound half of (5e) as the sensitive constraints, and demonstrates that relaxing the equality or removing the per-layer bounds restores solvability on the large majority of previously unsolved problems, with little verification-power loss for the bound removal.

Load-bearing premise

The theoretical argument that depth destroys strict feasibility uses an upper bound on the minimum eigenvalue as evidence that the minimum eigenvalue is actually zero, whereas a positive but tiny minimum eigenvalue would still satisfy strict feasibility.

Editorial extensions

If this is right

  • SDP-based verification of ReLU networks cannot be scaled to deep networks by simply using the standard SDP relaxation; at depths around ten layers the lack of strict feasibility prevents interior-point solvers from certifying optimality.
  • The per-layer upper and lower bound constraints, inherited from LP-based triangle relaxations, are unnecessary for the SDP formulation of ReLU and are counterproductive for feasibility, so future SDP verifiers should not add them.
  • Relaxing the ReLU equality constraint with a small tolerance, or removing the per-layer bounds, solves 88% of previously unsolved verification instances (41% of the total), at modest cost to relaxation quality in the bound-removal case.
  • Because the effect appears across standard, adversarial, and dual-formulation trained networks, any SDP-based verifier of deep networks must address strict feasibility regardless of training methodology.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The paper's minimum-eigenvalue bound suggests a concrete design rule it does not test: regularizing or scaling the extended weight rows of each layer to have a controlled minimum norm should delay interior-point vanishing in deeper networks.
  • If interior-point vanishing is the true cause of solver failure, then the reported difficulties of first-order methods for large-scale SDP verification may be partly an infeasibility artifact rather than only a scaling issue; the paper argues first-order methods should suffer more, but does not run that comparison.
  • The same 'valid constraints can destroy strict feasibility' mechanism likely applies to other convex relaxations built by adding cutting planes to an SDP; the paper only demonstrates it for the per-layer bounds in ReLU verification.
  • A direct test of the paper's central theoretical link would be to train deep networks with a cap on the minimum row norm of $\tilde W_i$ and measure whether the optimal value of the strict-feasibility problem (7) remains positive.
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

4 major / 5 minor

Summary. The paper studies semidefinite programming (SDP) relaxations for verifying ReLU neural networks. It introduces the concept of 'interior-point vanishing': the claim that, as network depth increases, the SDP relaxation loses strict feasibility (Slater's condition), causing numerical instability and solver failure for primal-dual interior-point methods. The authors support this with an empirical study (Table 1) showing that SDPA-GMP solves most instances for depths up to 8 but fails for depth 10 and above, and with two theoretical results: Proposition 3.3 on inactive neurons forcing zero diagonal entries of the PSD matrix, and Theorem 3.6 giving an upper bound on the minimum eigenvalue of feasible matrices. They then propose five modifications to the SDP formulation (ε-SDP, LeakySDP, D-Scale, W-Scale, and B-Remove) and report that B-Remove and ε-SDP substantially improve solver success rates. The paper also argues that the layer-wise bound constraints inherited from prior work are harmful to feasibility.

Significance. If the central claim were established, it would be an important negative result for SDP-based verification: it would explain why SDP verifiers struggle on deep networks and would justify abandoning or heavily modifying the standard formulation. The paper also makes a practical contribution by demonstrating, through experiments, that removing the per-layer bound constraints (B-Remove) dramatically improves solvability without much loss of relaxation quality (Figure 2 and Table 2). This empirical finding is interesting and potentially useful regardless of the theoretical interpretation. However, the theoretical support for the 'loss of strict feasibility' is not conclusive: Proposition 3.3 applies to neurons that are already removed by preprocessing, and Theorem 3.6 only provides an upper bound on the minimum eigenvalue, which is compatible with strict feasibility. The empirical evidence, while suggestive, does not clearly distinguish true loss of Slater's condition from numerical ill-conditioning of the interior-point method on nearly singular but strictly feasible SDPs.

major comments (4)
  1. [Section 3.3.1] The argument that inactive neurons cause interior-point vanishing does not apply to the SDP actually solved. Section 2.2.1 states that all neurons with upper bound u_ij = 0 are removed before solving. For a neuron that survives preprocessing, its computed upper bound is positive, and constraint (5e) is an inequality that does not force (P[x_i x_i^T])_jj = 0; it can be satisfied with a positive diagonal entry. Thus the sentence 'Consequently, we see that ... even a single inactive neuron can cause interior-point vanishing' (end of Section 3.3.1) is not supported. To make the argument, the paper would need to show that an un-removed inactive neuron (one whose true bound is zero but whose computed bound is positive) forces a zero diagonal entry in the relaxed SDP, which is not the case. This is a load-bearing point because the paper uses it to claim that the problem is inherent and cannot be trivially avoided.
  2. [Section 3.3.2, Theorem 3.6] Theorem 3.6 provides only an upper bound on λ_min(P): λ_min(P) ≤ min_{i,j} (1+T_i)||fW_i(j,:)||^2. This bound being small (e.g., 1e-8) is fully compatible with strict feasibility, which requires λ_min(P) > 0. The text immediately after Theorem 3.6 states that 'the minimum eigenvalue of any feasible P is constrained to be close to zero' and that 'a single such neuron can trigger the interior-point vanishing problem.' These inferences are invalid without a lower bound showing that the infimum of λ_min over the feasible set is zero, or a characterization of the recession cone forcing λ_min = 0. The paper does not provide such a result. Table 1 even shows positive optimal values for the strict feasibility verification problem (7) at depths up to 8, which are direct evidence of strict feasibility for those instances. The theoretical link from row norms to loss of Slater's condition is therefore missing.
  3. [Section 3.2, Table 1 and Section 6.2] The empirical evidence does not distinguish between true loss of strict feasibility and numerical ill-conditioning. For L=8 the solver succeeds on 98% of instances with a positive average objective (3.5e-9), meaning those instances are strictly feasible; for L≥10 the solver mostly fails and the reported objectives become slightly negative, which the authors attribute to numerical errors. Primal-dual interior-point methods are known to fail on nearly singular but strictly feasible SDPs, and small positive λ_min makes the central path difficult to follow. To support the 'fundamental barrier' claim, the paper should include a control experiment: for example, solve randomly generated SDPs with the same dimension, the same constraint count, and similarly tiny but positive λ_min, and show that the solver does not fail at the same rate. Alternatively, use exact arithmetic or facial reduction on small instances to certify whether Slater's condition actually fails. Without such a test, the observed solver failures may be a conditioning phenomenon rather than evidence of interior-point vanishing.
  4. [Abstract and Section 3.2] The claims in the abstract ('strict feasibility is likely to be lost') and in Section 3.2 ('the SDP-based verification problem (5) did not have strictly feasible solutions') are too strong relative to the presented evidence. The results show a monotonic decrease in the maximum feasible λ with depth, but λ remains positive for the depths where the solver succeeds (L=2 to L=8 in both datasets). A positive λ, however small, means the problem is strictly feasible. The conclusion should be reframed as evidence of 'near-loss' of strict feasibility or of numerical instability caused by tiny minimum eigenvalues, unless the authors provide a proof or a more direct test of infeasibility. This reframing does not diminish the practical value of the proposed methods, but it is essential for accuracy.
minor comments (5)
  1. [Section 3.3.1] The text refers to 'Theorem 3.3' when it means Proposition 3.3; the numbering and cross-references should be fixed throughout the manuscript.
  2. [Section 2.1] The statement of the verification problem is called 'Theorem 2.1' in the text following it, but it is a problem definition, not a theorem. The cross-reference should be corrected.
  3. [Section 3.3.2, Lemma 3.5] The proof of Lemma 3.5 is omitted with the phrase 'we omit the proof here.' Since this lemma is used to derive Theorem 3.6, the proof should either be included in the appendix or sketched in the main text.
  4. [Figure 2 and Section 5.3] The caption of Figure 2 is incomplete: the labels '-SDP' and 'LeakySDP' appear to be missing the prefix 'ε' and 'α', respectively. The caption should also state that the gap is computed only over instances where all methods converge.
  5. [Section 4.1] The parameter ε in ε-SDP is introduced without guidance on how to choose it. Since the paper reports results only for ε=0.01, a brief discussion of sensitivity to ε would improve reproducibility and help readers understand the trade-off between feasibility and tightness.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the paper's derivation chain is self-contained, and the contested steps are evidential or interpretive rather than reductions of the conclusions to their inputs.

full rationale

The paper does not fit any parameter and then relabel the fit as a prediction, nor does it import a load-bearing uniqueness theorem from the authors' prior work. The SDP relaxation (5) is obtained by a standard polynomial-lifting argument; Proposition 3.2 is a proved equivalence; Lemmas 3.4, 3.5, and Theorem 3.6 are derived from the constraints by induction and standard PSD block-matrix arguments; and the five proposed fixes are independent constraint relaxations or scalings, evaluated on the original verification SDPs. The self-citations to SDPA and SDPA-GMP concern the numerical solver used for experiments, not a mathematical premise that forces the central conclusion, so they are not load-bearing in the derivation. There is a mild self-reference in that the strict-feasibility diagnostic (7) is itself an SDP that can suffer from the same conditioning issues it is designed to detect, and the paper's interpretation of tiny positive eigenvalues as loss of strict feasibility is a logical gap; however, these are correctness and methodology concerns, not instances where the paper's conclusions are equivalent to its assumptions by construction. The claim that a small row norm or a small upper bound on lambda_min implies a zero eigenvalue is an invalid inference, not a circular one. Overall, the paper's central derivation is self-contained and externally benchmarked, so the circularity score is 0.

Assumptions & free parameters 2 free parameters · 5 assumptions · 0 invented entities

The paper introduces no new physical or mathematical entities. It relies on standard SDP theory and two hand-chosen relaxation parameters. The main assumptions are the validity of the SDP relaxation and the reliability of the solver-based strict feasibility check.

free parameters (2)
  • epsilon in epsilon-SDP = 0.01
    Tolerance for relaxing the ReLU equality constraint; chosen by hand and no sensitivity analysis is provided.
  • alpha in LeakySDP = 0.01
    Slope of the Leaky ReLU used to relax the activation; chosen by hand and no sensitivity analysis is provided.
assumptions (5)
  • standard math Slater's condition and strong duality for SDP require strict feasibility.
    Used in Section 3.1 to argue that the loss of strict feasibility undermines primal-dual interior-point methods.
  • standard math A positive semidefinite matrix with a zero diagonal entry is singular.
    Used in Proposition 3.3 to show that a forced zero diagonal element destroys positive definiteness.
  • domain assumption The polynomial lifting procedure yields a valid SDP relaxation of the QCQP verification problem.
    Invoked in Section 2.2 to justify formulation (5) from the original nonconvex problem.
  • domain assumption The bound propagation method alpha-CROWN provides valid lower and upper bounds for each ReLU unit.
    Used in Section 2.2.1 to preprocess inactive neurons and to supply li and ui for the constraints.
  • domain assumption The strict feasibility verification problem (7) accurately decides strict feasibility of the original SDP (6).
    Proposition 3.2 proves the equivalence, but the numerical reliability of solving (7) is taken for granted, which may be fragile when the problem itself is ill-conditioned.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Interior-Point Vanishing Problem in Semidefinite Relaxations for Neural Network Verification." pith.science (2026). https://pith.science/paper/2BWZFCST

@misc{pith2026250610269,
  author       = {Pith},
  title        = {Pith review of: Interior-Point Vanishing Problem in Semidefinite Relaxations for Neural Network Verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2BWZFCST}},
  note         = {Machine review of arXiv:2506.10269}
}
read the original abstract

Semidefinite programming (SDP) relaxation has emerged as a promising approach for neural network verification, offering tighter bounds than other convex relaxation methods for deep neural networks (DNNs) with ReLU activations. However, we identify a critical limitation in the SDP relaxation when applied to deep networks: interior-point vanishing, which leads to the loss of strict feasibility -- a crucial condition for the numerical stability and optimality of SDP. Through rigorous theoretical and empirical analysis, we demonstrate that as the depth of DNNs increases, the strict feasibility is likely to be lost, creating a fundamental barrier to scaling SDP-based verification. To address the interior-point vanishing, we design and investigate five solutions to enhance the feasibility conditions of the verification problem. Our methods can successfully solve 88% of the problems that could not be solved by existing methods, accounting for 41% of the total. Our analysis also reveals that the valid constraints for the lower and upper bounds for each ReLU unit are traditionally inherited from prior work without solid reasons, but are actually not only unbeneficial but also even harmful to the problem's feasibility. This work provides valuable insights into the fundamental challenges of SDP-based DNN verification and offers practical solutions to improve its applicability to deeper neural networks, contributing to the development of more reliable and secure systems with DNNs.

Figures

Figures reproduced from arXiv: 2506.10269 by the authors.

Figure 1
Figure 1. We allow the verification problem to take the value in the area between the Leaky ReLU and the x-axis [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
Figure 2
Figure 2. Average gap between the optimal objective values of our methods and the LayerSDP’s optimal. The numbers [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

55 extracted references · 48 canonical work pages

  1. [1]

    Strong Mixed-Integer Programming Formulations for Trained Neural Networks.Mathematical Programming, 183(1):3–39, 2020

    Ross Anderson, Joey Huchette, Will Ma, Christian Tjandraatmadja, and Juan Pablo Vielma. Strong Mixed-Integer Programming Formulations for Trained Neural Networks.Mathematical Programming, 183(1):3–39, 2020

    work page 2020

  2. [2]

    MOSEK ApS.MOSEK Fusion API for Python 11.0.4, 2025

    work page 2025

  3. [3]

    Neural Machine Translation by Jointly Learning to Align and Translate.arXiv Preprint arXiv:1409.0473, 2014

    Dzmitry Bahdanau. Neural Machine Translation by Jointly Learning to Align and Translate.arXiv Preprint arXiv:1409.0473, 2014

    arXiv 2014

  4. [4]

    Measuring Neural Net Robustness With Constraints.Advances in Neural Information Processing Systems, 29, 2016

    Osbert Bastani, Yani Ioannou, Leonidas Lampropoulos, Dimitrios Vytiniotis, Aditya Nori, and Antonio Criminisi. Measuring Neural Net Robustness With Constraints.Advances in Neural Information Processing Systems, 29, 2016

    work page 2016

  5. [5]

    Efficient Neural Network Verification via Layer-Based Semidefinite Relaxations and Linear Cuts

    Ben Batten, Panagiotis Kouvaros, Alessio Lomuscio, and Yang Zheng. Efficient Neural Network Verification via Layer-Based Semidefinite Relaxations and Linear Cuts. InProceedings of the Thirtieth International Joint Conference on Artificial Intelligence, pages 2184–2190, 2021

    work page 2021

  6. [6]

    Efficient Verification of ReLU-Based Neural Networks via Dependency Analysis

    Elena Botoeva, Panagiotis Kouvaros, Jan Kronqvist, Alessio Lomuscio, and Ruth Misener. Efficient Verification of ReLU-Based Neural Networks via Dependency Analysis. InProceedings of the AAAI Conference on Artificial Intelligence, pages 3291–3299, 2020

    work page 2020

  7. [7]

    Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers.Foundations and Trends® in Machine Learning, 3(1):1–122, 2011

    Stephen Boyd, Neal Parikh, Eric Chu, Borja Peleato, Jonathan Eckstein, et al. Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers.Foundations and Trends® in Machine Learning, 3(1):1–122, 2011

    work page 2011

  8. [8]

    The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results.arXiv Preprint arXiv:2412.19985, 2024

    Christopher Brix, Stanley Bak, Taylor T Johnson, and Haoze Wu. The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results.arXiv Preprint arXiv:2412.19985, 2024

    arXiv 2024

Show all 55 references
  1. [9]

    A Unified View of Piecewise Linear Neural Network Verification.Advances in Neural Information Processing Systems, 31, 2018

    Rudy R Bunel, Ilker Turkaslan, Philip Torr, Pushmeet Kohli, and Pawan K Mudigonda. A Unified View of Piecewise Linear Neural Network Verification.Advances in Neural Information Processing Systems, 31, 2018

    2018

  2. [10]

    End-to-End Autonomous Driving: Challenges and Frontiers.IEEE Transactions on Pattern Analysis and Machine Intelligence, 2024

    Li Chen, Penghao Wu, Kashyap Chitta, Bernhard Jaeger, Andreas Geiger, and Hongyang Li. End-to-End Autonomous Driving: Challenges and Frontiers.IEEE Transactions on Pattern Analysis and Machine Intelligence, 2024. 11 Interior-Point Vanishing Problem in Semidefinite Relaxations ...

    2024

  3. [11]

    Maximum Resilience of Artificial Neural Networks

    Chih-Hong Cheng, Georg N”uhrenberg, and Harald Ruess. Maximum Resilience of Artificial Neural Networks. InAutomated Technology for Verification and Analysis: 15th International Symposium, ATVA 2017, Pune, India, October 3–6, 2017, Proceedings 15, pages 251–268. Springer, 2017

    2017

  4. [12]

    Tight Certification of Adversarially Trained Neural Networks via Nonconvex Low-Rank Semidefinite Relaxations

    Hong-Ming Chiu and Richard Y Zhang. Tight Certification of Adversarially Trained Neural Networks via Nonconvex Low-Rank Semidefinite Relaxations. InInternational Conference on Machine Learning, pages 5631–5660. PMLR, 2023

    2023

  5. [13]

    Certified Adversarial Robustness via Randomized Smoothing

    Jeremy Cohen, Elan Rosenfeld, and Zico Kolter. Certified Adversarial Robustness via Randomized Smoothing. In Proceedings of the 36th International Conference on Machine Learning, pages 1310–1320. PMLR, 2019

    2019

  6. [14]

    Enabling Certification of Verification-Agnostic Networks via Memory-Efficient Semidefinite Programming.Advances in Neural Information Processing Systems, 33:5318–5331, 2020

    Sumanth Dathathri, Krishnamurthy Dvijotham, Alexey Kurakin, Aditi Raghunathan, Jonathan Uesato, Rudy R Bunel, Shreya Shankar, Jacob Steinhardt, Ian Goodfellow, Percy S Liang, et al. Enabling Certification of Verification-Agnostic Networks via Memory-Efficient Semidefinite Prog...

    2020

  7. [15]

    The MNIST Database of Handwritten Digit Images for Machine Learning Research.IEEE Signal Processing Magazine, 29(6):141–142, 2012

    Li Deng. The MNIST Database of Handwritten Digit Images for Machine Learning Research.IEEE Signal Processing Magazine, 29(6):141–142, 2012

    2012

  8. [16]

    Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks

    Ruediger Ehlers. Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks. InAutomated Technology for Verification and Analysis: 15th International Symposium, ATVA 2017, Pune, India, October 3–6, 2017, Proceedings 15, pages 269–286. Springer, 2017

    2017

  9. [17]

    Scalable Approximate Optimal Diagonal Precondi- tioning.arXiv preprint arXiv:2312.15594, 2023

    Wenzhi Gao, Zhaonan Qu, Madeleine Udell, and Yinyu Ye. Scalable Approximate Optimal Diagonal Precondi- tioning.arXiv preprint arXiv:2312.15594, 2023

    2023 arXiv

  10. [18]

    Explaining and Harnessing Adversarial Examples

    Ian J Goodfellow, Jonathon Shlens, and Christian Szegedy. Explaining and Harnessing Adversarial Examples. arXiv Preprint arXiv:1412.6572, 2014

    2014 arXiv

  11. [19]

    Efficient Neural Network Verification via Adaptive Refinement and Adversarial Search

    Patrick Henriksen and Alessio Lomuscio. Efficient Neural Network Verification via Adaptive Refinement and Adversarial Search. InProceedings of the 24th European Conference on Artificial Intelligence, pages 2513–2520. IOS Press, 2020

    2020

  12. [20]

    Cambridge University Press, Cambridge, England, 2 edition, Oct 2012

    Roger A Horn and Charles R Johnson.Matrix Analysis. Cambridge University Press, Cambridge, England, 2 edition, Oct 2012

    2012

  13. [21]

    Facial Reduction for Symmetry Reduced Semidefinite and Doubly Nonnegative Programs.Mathematical Programming, 200(1):475–529, 2023

    Hao Hu, Renata Sotirov, and Henry Wolkowicz. Facial Reduction for Symmetry Reduced Semidefinite and Doubly Nonnegative Programs.Mathematical Programming, 200(1):475–529, 2023

    2023

  14. [22]

    Safety Verification of Deep Neural Networks

    Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. Safety Verification of Deep Neural Networks. In Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I 30, pages 3–29. Springer, 2017

    2017

  15. [23]

    Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks

    Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. InComputer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part ...

    2017

  16. [24]

    Reluplex: A Calculus for Reasoning About Deep Neural Networks.Formal Methods in System Design, 60(1):87–116, 2022

    Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: A Calculus for Reasoning About Deep Neural Networks.Formal Methods in System Design, 60(1):87–116, 2022

    2022

  17. [25]

    ImageNet Classification With Deep Convolutional Neural Networks.Advances in Neural Information Processing Systems, 25, 2012

    Alex Krizhevsky, Ilya Sutskever, and Geoffrey E Hinton. ImageNet Classification With Deep Convolutional Neural Networks.Advances in Neural Information Processing Systems, 25, 2012

    2012

  18. [26]

    A Semidefinite Relaxation Based Branch-and-Bound Method for Tight Neural Network Verification

    Jianglin Lan, Benedikt Br¨uckner, and Alessio Lomuscio. A Semidefinite Relaxation Based Branch-and-Bound Method for Tight Neural Network Verification. InProceedings of the AAAI Conference on Artificial Intelligence, pages 14946–14954, 2023

    2023

  19. [27]

    World Scientific, 2009

    Jean Bernard Lasserre.Moments, Positive Polynomials and Their Applications, volume 1. World Scientific, 2009

    2009

  20. [28]

    SoK: Certified Robustness for Deep Neural Networks

    Linyi Li, Tao Xie, and Bo Li. SoK: Certified Robustness for Deep Neural Networks. InIEEE Symposium on Security and Privacy (SP), pages 1289–1310. IEEE, 2023

    2023

  21. [29]

    An ADMM-Based Interior-Point Method for Large-Scale Linear Programming.Optimization Methods and Software, 36(2-3):389–424, 2021

    Tianyi Lin, Shiqian Ma, Yinyu Ye, and Shuzhong Zhang. An ADMM-Based Interior-Point Method for Large-Scale Linear Programming.Optimization Methods and Software, 36(2-3):389–424, 2021

    2021

  22. [30]

    An Approach to Reachability Analysis for Feed-Forward ReLU Neural Networks.arXiv Preprint arXiv:1706.07351, 2017

    Alessio Lomuscio and Lalit Maganti. An Approach to Reachability Analysis for Feed-Forward ReLU Neural Networks.arXiv Preprint arXiv:1706.07351, 2017

    2017 arXiv

  23. [31]

    A Structural Geometrical Analysis of Weakly Infeasible SDPs.Journal of the Operations Research Society of Japan, 59(3):241–257, 2016

    Bruno F Lourenc ¸o, Masakazu Muramatsu, and Takashi Tsuchiya. A Structural Geometrical Analysis of Weakly Infeasible SDPs.Journal of the Operations Research Society of Japan, 59(3):241–257, 2016

    2016

  24. [32]

    Towards Deep Learning Models Resistant to Adversarial Attacks.International Conference on Learning Representations, 2018

    Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards Deep Learning Models Resistant to Adversarial Attacks.International Conference on Learning Representations, 2018. 12 Interior-Point Vanishing Problem in Semidefinite Relaxations f...

    2018

  25. [33]

    A Numerical Evaluation of Highly Accurate Multiple-Precision Arithmetic Version of Semidefinite Programming Solver: SDPA-GMP, -QD and -DD

    Maho Nakata. A Numerical Evaluation of Highly Accurate Multiple-Precision Arithmetic Version of Semidefinite Programming Solver: SDPA-GMP, -QD and -DD. InIEEE International Symposium on Computer-Aided Control System Design, pages 29–34, 2010

    2010

  26. [34]

    California Institute of Technology, 2000

    Pablo A Parrilo.Structured Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization. California Institute of Technology, 2000

    2000

  27. [35]

    Partial Facial Reduction: Simplified, Equivalent SDPs via Approximations of the PSD Cone.Mathematical Programming, 171:1–54, 2018

    Frank Permenter and Pablo Parrilo. Partial Facial Reduction: Simplified, Equivalent SDPs via Approximations of the PSD Cone.Mathematical Programming, 171:1–54, 2018

    2018

  28. [36]

    Semidefinite Relaxations for Certifying Robustness to Adversarial Examples.Advances in Neural Information Processing Systems, 31, 2018

    Aditi Raghunathan, Jacob Steinhardt, and Percy S Liang. Semidefinite Relaxations for Certifying Robustness to Adversarial Examples.Advances in Neural Information Processing Systems, 31, 2018

    2018

  29. [37]

    A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks.Advances in Neural Information Processing Systems, 32, 2019

    Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang. A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks.Advances in Neural Information Processing Systems, 32, 2019

    2019

  30. [38]

    Perturbation Analysis of Singular Semidefinite Programs and Its Applica- tions to Control Problems.Journal of Optimization Theory and Applications, 188:52–72, 2021

    Yoshiyuki Sekiguchi and Hayato Waki. Perturbation Analysis of Singular Semidefinite Programs and Its Applica- tions to Control Problems.Journal of Optimization Theory and Applications, 188:52–72, 2021

    2021

  31. [39]

    An Abstract Domain for Certifying Neural Networks.Proceedings of the ACM on Programming Languages, 3(POPL):1–30, 2019

    Gagandeep Singh, Timon Gehr, Markus P”uschel, and Martin Vechev. An Abstract Domain for Certifying Neural Networks.Proceedings of the ACM on Programming Languages, 3(POPL):1–30, 2019

    2019

  32. [40]

    SDPNAL+: A MATLAB Software for Semidefinite Programming With Bound Constraints (Version 1.0).Optimization Methods and Software, 35(1):87– 115, 2020

    Defeng Sun, Kim-Chuan Toh, Yancheng Yuan, and Xin-Yuan Zhao. SDPNAL+: A MATLAB Software for Semidefinite Programming With Bound Constraints (Version 1.0).Optimization Methods and Software, 35(1):87– 115, 2020

    2020

  33. [41]

    Intriguing Properties of Neural Networks

    Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow, and Rob Fergus. Intriguing Properties of Neural Networks. InInternational Conference on Learning Representations, 2014

    2014

  34. [42]

    Evaluating Robustness of Neural Networks With Mixed Integer Programming.arXiv Preprint arXiv:1711.07356, 2017

    Vincent Tjeng, Kai Xiao, and Russ Tedrake. Evaluating Robustness of Neural Networks With Mixed Integer Programming.arXiv Preprint arXiv:1711.07356, 2017

    2017 arXiv

  35. [43]

    Practical First-Order Methods for Large-Scale Semidefinite Programming

    Stephen Tu and Jingyan Wang. Practical First-Order Methods for Large-Scale Semidefinite Programming. Technical Report, University of California, Berkeley, 2014

    2014

  36. [44]

    Facial Reduction Algorithms for Conic Optimization Problems.Journal of Optimization Theory and Applications, 158:188–215, 2013

    Hayato Waki and Masakazu Muramatsu. Facial Reduction Algorithms for Conic Optimization Problems.Journal of Optimization Theory and Applications, 158:188–215, 2013

    2013

  37. [45]

    Efficient Formal Safety Analysis of Neural Networks.Advances in Neural Information Processing Systems, 31, 2018

    Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient Formal Safety Analysis of Neural Networks.Advances in Neural Information Processing Systems, 31, 2018

    2018

  38. [46]

    Beta-CROWN: Efficient Bound Propagation With Per-Neuron Split Constraints for Neural Network Robustness Verification

    Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta-CROWN: Efficient Bound Propagation With Per-Neuron Split Constraints for Neural Network Robustness Verification. Advances in Neural Information Processing Systems, 34:29909–29921, 2021

    2021

  39. [47]

    Towards Fast Computation of Certified Robustness for ReLU Networks

    Lily Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Luca Daniel, Duane Boning, and Inderjit Dhillon. Towards Fast Computation of Certified Robustness for ReLU Networks. InInternational Conference on Machine Learning, pages 5276–5285. PMLR, 2018

    2018

  40. [48]

    Provable Defenses Against Adversarial Examples via the Convex Outer Adversarial Polytope

    Eric Wong and Zico Kolter. Provable Defenses Against Adversarial Examples via the Convex Outer Adversarial Polytope. InInternational Conference on Machine Learning, pages 5286–5295. PMLR, 2018

    2018

  41. [49]

    Numerical Optimization, 2006

    Stephen J Wright. Numerical Optimization, 2006

    2006

  42. [50]

    Fashion-MNIST: A Novel Image Dataset for Benchmarking Machine Learning Algorithms.arXiv Preprint arXiv:1708.07747, 2017

    Han Xiao, Kashif Rasul, and Roland V ollgraf. Fashion-MNIST: A Novel Image Dataset for Benchmarking Machine Learning Algorithms.arXiv Preprint arXiv:1708.07747, 2017

    2017 arXiv

  43. [51]

    Fast and Com- plete: Enabling Complete Neural Network Verification With Rapid and Massively Parallel Incomplete Verifiers

    Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. Fast and Com- plete: Enabling Complete Neural Network Verification With Rapid and Massively Parallel Incomplete Verifiers. International Conference on Learning Representations, 2022

    2022

  44. [52]

    Latest Developments in the SDPA Family for Solving Large-Scale SDPs.Handbook on Semidefinite, Conic and Polynomial Optimization, pages 687–713, 2012

    Makoto Yamashita, Katsuki Fujisawa, Mituhiro Fukuda, Kazuhiro Kobayashi, Kazuhide Nakata, and Maho Nakata. Latest Developments in the SDPA Family for Solving Large-Scale SDPs.Handbook on Semidefinite, Conic and Polynomial Optimization, pages 687–713, 2012

    2012

  45. [53]

    A High-Performance Software Package for Semidefinite Programs: SDPA 7.Handbook on Semidefinite, Conic and Polynomial Optimization, 2010

    Makoto Yamashita, Katsuki Fujisawa, Kazuhide Nakata, Maho Nakata, Mituhiro Fukuda, Kazuhiro Kobayashi, and Kazushige Goto. A High-Performance Software Package for Semidefinite Programs: SDPA 7.Handbook on Semidefinite, Conic and Polynomial Optimization, 2010

    2010

  46. [54]

    ADADELTA: an Adaptive Learning Rate Method.arXiv preprint arXiv:1212.5701, 2012

    Matthew D Zeiler. ADADELTA: an Adaptive Learning Rate Method.arXiv preprint arXiv:1212.5701, 2012

    2012 arXiv

  47. [55]

    Scalable Neural Network Verification With Branch-and-Bound Inferred Cutting Planes.Advances in Neural Information Processing Systems, 2024

    Duo Zhou, Christopher Brix, Grani A Hanasusanto, and Huan Zhang. Scalable Neural Network Verification With Branch-and-Bound Inferred Cutting Planes.Advances in Neural Information Processing Systems, 2024. 13 Interior-Point Vanishing Problem in Semidefinite Relaxations for Neur...

    2024

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.