Semidefinite Relaxations: Lifting Without a Universal Ranking

Linear programming relaxations provide polynomial-time verification but sometimes yield loose bounds. Complete methods provide exact answers but don’t scale. What if you want tighter bounds than LP without the exponential cost of complete methods?

Semi-definite programming (SDP) offers a way to constrain quadratic relationships, which a linear relaxation cannot express at all. SDP-based verification lifts the problem to a matrix variable and imposes a PSD constraint on it. The tradeoff is cost---SDP solvers are slower than LP solvers---and the question of whether that cost buys anything is a property of the network rather than of the method.

This guide covers how the lifting is set up, what it keeps and what it gives up, and when the extra cost is justified.

Why Semi-Definite Programming?

Linear programs optimize over polytopes (linear constraints). Semi-definite programs optimize over spectrahedra (positive semi-definite matrix constraints). This richer geometry captures relationships that linear constraints cannot.

What changes: SDP can express quadratic constraints and products of variables, through positive semi-definite (PSD) matrix constraints. Whether that yields a tighter bound on a given network is a separate question, answered per instance rather than by the word “SDP” — see Lifting to Quadratic Form below.

Semi-Definite Program (SDP)

A semi-definite program has the form:

$$\begin{aligned} \text{minimize} \quad & \langle C, X \rangle \\ \text{subject to} \quad & \langle A_i, X \rangle = b_i \quad \forall i \\ & X \succeq 0 \end{aligned}$$

where:

• $X$ is a symmetric matrix variable
• $X \succeq 0$ means $X$ is positive semi-definite (all eigenvalues non-negative)
• $\langle A, B \rangle = \text{trace}(A^T B)$ is the matrix inner product

Complexity: SDP can be solved in polynomial time using interior-point methods. Practical solvers (CVXPY, SCS, Mosek) handle SDPs with thousands of variables.

SDP vs LP for Verification

LP relaxations use linear inequalities to over-approximate the neural network’s behavior. They’re fast (polynomial time) but conservative.

SDP relaxations replace the variables with a lifted matrix and impose a PSD constraint on it. They are slower, and whether the resulting bound is tighter is a property of the instance.

There is no ordering between the two, and the reason is worth being precise about. Every LP can be written in SDP form — a diagonal matrix variable makes the linear constraints matrix constraints — so the two formalisms are not incomparable. But that is a statement about how a program is written, not about which feasible set is smaller. The LP relaxation is a set of $z$ defined by linear inequalities in $z$. The SDP relaxation is a set of lifted matrices $X$ defined by a PSD constraint and some linear constraints on the entries of $X$. They are different objects over different variables, and neither contains the other. An SDP bound can come out tighter than an LP bound on one network and looser on the next, and the level of each is set by what the constraints leave free.

The one comparison that does hold is per-instance: on a given problem, solve both and compare. A method that can be looser on some instance and tighter on others is not ranked, and any table that puts “tight” in one column and “moderate” in the other is describing a tendency rather than a guarantee.

SDP Formulation for Neural Networks

The SDP formulation for neural network verification extends the LP approach by introducing a matrix variable that captures second-order relationships between neurons.

Lifting to Quadratic Form

Standard approach: For a network with variables $z$ (all neuron activations), verify bounds on outputs.

SDP approach: Introduce a lifted variable $X = zz^T$, a matrix encoding all pairwise products of neuron activations.

Why this helps: ReLU and other non-linearities create quadratic relationships. By explicitly representing these products in $X$, the SDP can encode tighter constraints.

Basic SDP Formulation

Given: Neural network $f_\theta$, input region $\mathcal{X}$, output neuron $k$ to bound.

Variables:

• $z \in \mathbb{R}^n$: All neuron pre/post-activations
• $X \in \mathbb{R}^{n \times n}$: Lifted matrix with $X_{ij} = z_i z_j$

Objective: Minimize $z_k$ (output neuron $k$)

Constraints:

1. Linear layer constraints: For $z_j = \sum_i W_{ji} z_i + b_j$:

   $$z_j = \langle W_j, z \rangle + b_j$$

2. Input bounds: $\underline{x} \leq x \leq \overline{x}$ for input $x$

3. ReLU constraints: For $y = \text{ReLU}(z)$ with bounds $\underline{z} \leq z \leq \overline{z}$:

   • If $\overline{z} \leq 0$: $y = 0$ (inactive)
   • If $\underline{z} \geq 0$: $y = z$ (active)
   • If $\underline{z} < 0 < \overline{z}$: Use SDP relaxation

4. Lifted consistency: $X_{ij} = z_i z_j$ (exactly)

5. PSD constraint: $\begin{bmatrix} X & z \\ z^T & 1 \end{bmatrix} \succeq 0$

Key insight: The PSD constraint $\begin{bmatrix} X & z \\ z^T & 1 \end{bmatrix} \succeq 0$ enforces that $X$ represents outer products, making $X_{ij} \approx z_i z_j$ without requiring exact equality (which would be non-convex).

ReLU Relaxation in SDP

For uncertain ReLUs ($\underline{z} < 0 < \overline{z}$), the SDP formulation adds tighter constraints than LP:

LP triangle relaxation:

SDP quadratic relaxation (additional constraint beyond LP):

This constraint captures the fact that when ReLU is active ($y = z$), both $y$ and $z$ are positive, so their product is positive. When inactive ($y = 0$), the product is zero.

Why it’s tighter: The quadratic constraint $y \cdot z \geq 0$ is non-linear, which LP cannot express. SDP encodes it via the lifted matrix $X$ with the PSD constraint.

Nuclear Norm and Rank Constraints

An alternative SDP formulation uses the nuclear norm (sum of singular values) to encourage low-rank structure in the lifted matrix $X$.

Nuclear Norm Regularization

Motivation: The exact relationship $X = zz^T$ implies $X$ is rank-1. Relaxing this constraint makes the problem convex, but allowing arbitrary $X$ can be loose.

Middle ground: Minimize the nuclear norm $\|X\|_* = \sum_i \sigma_i(X)$ where $\sigma_i$ are singular values.

SDP formulation with nuclear norm:

Effect: The nuclear norm penalty encourages $X$ to be low-rank, closer to the rank-1 structure of true outer products. The parameter $\lambda$ balances tightness (higher $\lambda$) and conservativeness (lower $\lambda$).

Nuclear norm as SDP: The nuclear norm minimization can be reformulated as an SDP constraint:

This makes nuclear norm optimization tractable within the SDP framework.

Tightness Improvements

What is worth claiming here, and what is not. Three things, of very different standing:

• Nuclear-norm regularisation tightens the bound — yes, by shrinking the feasible set with an additional valid constraint, so the bound cannot get worse. The mechanism is structural, not empirical.
• SDP can be tighter than LP — yes, on some networks, and this section has already said why there is no ordering between the two formalisms: they are different objects over different variables, so an SDP bound comes out tighter on one network and looser on the next. A percentage like “20-50% tighter for typical networks” claims a per-instance fact across a distribution, which is the one thing the earlier part of this chapter argues cannot be claimed.
• The gain is largest where many ReLUs are uncertain — plausible from the mechanism, since that is where the relaxation has the most freedom, and it is the right thing to check first when an SDP run underperforms.

So the practical guidance is a procedure rather than a number: run both, compare on the network at hand, and use the tighter bound. Where a reported percentage is the only evidence available, the report should say which network and which $\epsilon$ produced it.

Comparison with Other Methods

SDP vs LP-Based Methods

LP-based methods:

• Pros: Fast, scalable to large networks
• Cons: Loose bounds (misses quadratic relationships)

SDP-based methods:

• Pros: Tighter bounds (captures products via PSD constraints)
• Cons: Slower (cubic to quartic complexity)

When SDP wins: networks with strong neuron correlations, and properties where a looser bound would simply not answer the question. Network size is a cost consideration rather than a suitability criterion — the question is whether the extra expressiveness is needed, not whether the network is under a particular size.

SDP vs Multi-Neuron Relaxations

Multi-neuron relaxations (PRIMA (Mueller et al. 2022)):

• Approach: Add pairwise product terms explicitly for selected neuron pairs
• Complexity: Depends on number of pairs $k$; roughly $O(n + k)$ where $k \ll n^2$
• Tightness: Tight for selected pairs, but greedy pair selection may miss important correlations

SDP-based methods:

• Approach: Encode all pairwise products via lifted matrix $X$
• Complexity: $O(n^{4.5})$ for general SDP solvers
• Tightness: Constrains all pairwise products at once, rather than a selected subset

Tradeoff: multi-neuron methods choose which pairs to relate and therefore pay for only those; SDP constrains the full lifted matrix and pays for it. Neither dominates: on a network where the relevant products are few and identifiable, a selective method can match or beat a full lifting; on one where they are not identifiable, lifting can be tighter.

SDP vs Complete Methods

Complete methods (Marabou (Katz et al. 2019), branch-and-bound):

• Pros: Exact answers (verified or counterexample)
• Cons: Exponential worst-case complexity, don’t scale to large networks

SDP methods:

• Pros: Solvable in polynomial time, and it can capture products a linear or per-neuron bound drops
• Cons: Still incomplete (might return “unknown”), and the lift has to be built whether or not the products in it turn out to matter

When to choose SDP over complete: When the network is too large for complete methods but LP/CROWN are too loose. SDP fills the gap between fast incomplete and slow complete methods.

Practical Implementation

Using SDP Solvers

Available solvers:

• CVXPY: High-level Python interface, supports multiple SDP solvers
• SCS: Splitting Conic Solver, fast for large-scale problems
• MOSEK: Commercial solver, highly optimized
• SDPT3/SeDuMi: MATLAB-based solvers

Typical workflow:

import cvxpy as cp
import numpy as np

# Define network layers, input bounds, etc.
n_neurons = 100  # Total neurons (all layers)

# Variables
z = cp.Variable(n_neurons)  # Neuron activations
X = cp.Variable((n_neurons, n_neurons), symmetric=True)  # Lifted matrix

# Objective: minimize output neuron
objective = cp.Minimize(z[-1])

# Constraints
constraints = []

# Linear layer constraints: z_j = W @ z + b
# (add for each layer)

# Input bounds
constraints.append(z[:input_dim] >= x_lower)
constraints.append(z[:input_dim] <= x_upper)

# ReLU constraints (triangle + quadratic)
# For each uncertain ReLU with pre-activation z_i, post-activation y_j:
# constraints.append(y_j * z_i >= 0)  # SDP quadratic constraint

# PSD constraint (lifted consistency)
lifted = cp.bmat([[X, z.reshape(-1, 1)],
                  [z.reshape(1, -1), np.array([[1]])]])
constraints.append(lifted >> 0)  # PSD

# Solve
problem = cp.Problem(objective, constraints)
problem.solve(solver=cp.SCS)

lower_bound = problem.value

Performance Considerations

Scalability challenges:

• Matrix size: $X \in \mathbb{R}^{n \times n}$ has $O(n^2)$ entries. For $n = 1000$, that’s 1 million variables.
• Solver time: SDP solvers have $O(n^{4.5})$ complexity. Doubling network size increases time by ~22x.

Optimizations:

Sparsity exploitation: Many entries of $X$ may be irrelevant (neurons in different layers don’t interact directly). Exploit this sparsity to reduce variable count.

Layer-by-layer solving: Similar to LP, solve SDP layer-by-layer rather than for the entire network. This keeps $n$ small (neurons per layer) rather than large (total neurons).

Warm-starting: When solving multiple similar SDPs (different output neurons, slightly different bounds), initialize solver with previous solution.

GPU acceleration: Some recent work explores GPU-accelerated SDP solving, though traditional SDP solvers are CPU-based.

When to Use SDP-Based Verification

Use SDP when:

• LP or CROWN return “unknown” and you need tighter bounds
• The network is small enough that the per-layer SDPs are affordable — which depends on your solver and budget, not on a fixed neuron count
• Properties are critical---extra computational cost justified for tightness
• Strong neuron correlations (convolutional layers, residual connections)
• Computational budget allows hours for verification

Don’t use when:

• Network is very large (thousands to millions of neurons)---LP/CROWN/PRIMA faster
• LP already verifies the property---no need for tighter bounds
• Need complete verification---use SMT or branch-and-bound instead
• Rapid iteration required---SDP too slow for tight feedback loops

When SDP earns its cost: SDP-based verification is incomplete, like the bound-based methods, and pays more per instance than they do. Whether that is worth it depends on whether the products it constrains are the ones the instance is short of. It is most useful when:

• Simple incomplete methods fail to verify
• Complete methods are too slow
• Network size is moderate (not tiny, not huge)
• Tightness matters more than speed

Current Research and Extensions

Active research directions:

Tighter SDP relaxations: Beyond basic nuclear norm, researchers explore additional constraints (e.g., exploiting network structure like convolution, adding higher-order tensor relaxations) to tighten bounds further.

Faster solvers: Developing specialized SDP solvers for neural network verification that exploit problem structure for faster solving.

Hybrid SDP-MILP: Combine SDP relaxations with integer programming for select neurons, balancing tightness and completeness.

Integration with training: Train networks that are easier to verify via SDP (e.g., encouraging low nuclear norm in activations).

Probabilistic SDP: Extend SDP to handle probabilistic guarantees, combining with randomized smoothing (Cohen et al. 2019).

Limitations

Computational cost: $O(n^{4.5})$ complexity limits SDP to moderately-sized networks. Large-scale verification requires faster methods.

Still incomplete: SDP provides tighter bounds than LP but might still return “unknown.” For definitive answers, complete methods are needed.

Solver numerical issues: SDP solvers can face numerical instability, especially for large problems or poorly-scaled constraints. Careful problem formulation and solver tuning are required.

No ordering between the methods: There is no theorem that an SDP bound is at most an LP bound on every network, and none in the other direction either. What decides it is which product terms a given instance actually needs. For some networks the gain is marginal, and for some it goes the other way.

Key Takeaways

SDP-based verification represents a sophisticated approach to incomplete verification: encoding neural networks as semi-definite programs captures quadratic relationships that simpler methods miss. The positive semi-definite constraint---a subtle but powerful tool from convex optimization---enables reasoning about products and correlations without sacrificing polynomial-time solvability.

While SDP doesn’t scale to massive networks like CROWN or IBP (Gowal et al. 2019) do, it fills an important niche. For critical properties on moderately-sized networks where LP is too loose and complete methods are too slow, SDP provides the right balance.

SDP-based verification shows why it is tempting to arrange these methods on a line: it expresses constraints an interval bound and a linear bound cannot, at higher cost. The line is a useful picture and an unreliable ranking — the levels differ in what they can express, not in a tightness that holds per instance, and a method lower down can beat one higher up on a given network. Choosing between them is per instance, and that is the subject of the next sections.