Single-Neuron, Multivariate, and Multi-Neuron Relaxations

“Use more variables” can mean two different improvements. One keeps several inputs of a single neuron. Another handles several activation outputs together. Both can tighten a relaxation, but they should not be called the same construction.

One scalar activation

For $y=\operatorname{ReLU}(z)$ with $z\in[l,u]$ crossing zero, the triangle constraints give the exact convex hull in the $(z,y)$ plane.

That is a local statement about two variables over an interval. It says nothing yet about whether every feasible combination of several such pairs can be produced by one common network input.

One neuron with several inputs

Consider $y=\operatorname{ReLU}(x_1+x_2)$ on $[-1,1]^2$. Reducing the input to $z=x_1+x_2\in[-2,2]$ loses how that sum arose.

The scalar triangle permits $(x_1,x_2,y)=(1,-1,1)$. But a convex combination of graph points whose first coordinate is 1 and second coordinate is -1 must use only graph points at that same corner. Their output is zero, so this point is outside the true multivariate graph hull.

A tighter multivariate single-neuron relaxation therefore retains information that the scalar interval reduction discarded. This is the setting of Tjandraatmadja et al., NeurIPS 2020.

Several neurons sharing an input

Now return to $h_1=\operatorname{ReLU}(x)$ and $h_2=\operatorname{ReLU}(-x)$ for $x\in[-1,1]$.

The relation $h_1-h_2=x$ is true on the entire joint graph, so it is also true on its convex hull. Two independent triangle hulls do not enforce it: they permit $x=0,h_1=0,h_2=1/2$.

For $g=h_1-h_2-x+1/4$, the true value is $1/4$ but the independent relaxation permits $-1/4$. Adding the joint equality restores the exact value on this example. The benefit comes from a relation among outputs, not from solving the same LP more accurately.

k-ReLU and PRIMA

In k-ReLU, by Singh et al. (2019), $k$ counts ReLUs considered jointly. It is not the number of inputs to one scalar ReLU. Joint constraints retain relationships that independent activation abstractions can lose.

PRIMA, by Mueller et al. (2022), develops scalable convex-hull approximation algorithms for multi-neuron abstractions, extending beyond ReLU. The role of the geometry is to obtain useful joint constraints without paying for an unrestricted exact construction in every case. This chapter introduces the problem it addresses; it does not derive the complete partial-double-description algorithm or its complexity proof.

Grouping is a budget decision. More constraints can tighten a particular feasible set, but generating and using them costs time and memory. Group selection, overlap, the input abstraction and how constraints enter the verifier all matter.

LP is not a precision level

An LP solver optimises the linear feasible set it is given. That set may contain box constraints, scalar triangles, multivariate cuts, multi-neuron constraints or a mixture.

Consequently, a ladder such as “single neuron < multi-neuron < LP < complete” is not meaningful. Multi-neuron constraints can themselves be used in an LP. Exact solution of a relaxation is distinct from exact solution of the original network problem.

Likewise, branch-and-bound can use stronger convex relaxations inside its nodes. Joint abstraction and case splitting are compatible techniques, not mutually exclusive categories.

A small exercise

Why does the equality $h_1-h_2=x$ remain valid after taking the convex hull of the joint graph?

Answer

Every graph point satisfies the same linear equality. A convex combination preserves a linear equality, so every point of the convex hull satisfies it too. This argument does not require enumerating the hull’s facets.

Key Takeaways

Scalar, multivariate single-neuron, and multi-neuron relaxations have different objects. State which variables and relationships are retained.

Exact local hulls need not give an exact network relaxation. The missing information can be a relation between different activations.

LP describes a solving form, not a fixed tightness class. Precision depends on the actual constraints.

Next Phase

That is the end of Phase 2: Methods & Tools. Phase 3 moves from bounds to a run: specifying the property, testing it, and reporting what came back.

Further Reading

Singh, Ganvir, Pueschel and Vechev, “Beyond the Single Neuron Convex Barrier for Neural Network Certification”, NeurIPS 2019 https://proceedings.neurips.cc/paper/2019/hash/0a9fdbb17feb6ccb7ec405cfb85222c4-Abstract.html — this is k-ReLU, by Singh et al. rather than by Tjandraatmadja.

Tjandraatmadja et al., “The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification”, NeurIPS 2020 https://arxiv.org/abs/2006.14076.

Mueller, Makarchuk, Singh, Pueschel and Vechev, “PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations”, PACMPL (POPL) 2022 https://arxiv.org/abs/2103.03638.

For related work on constructing activation-hull approximations, see WraLU and WraAct, and distinguish the maintained library discussion from the paper artifacts.