Multi-Neuron Relaxation and PRIMA

Single-neuron relaxations---the standard approach in bound propagation---treat each ReLU independently. For a ReLU with multiple inputs like $z = \text{ReLU}(w_1 x + w_2 y + b)$ , they first reduce it to a single variable $\hat{z} = w_1 x + w_2 y + b$ , then apply the standard triangle relaxation to $z = \text{ReLU}(\hat{z})$ .

This works and scales efficiently, but it misses critical opportunities for tightness. Multi-neuron relaxation methods consider multiple input variables jointly, computing tighter convex polytopes that dramatically improve verification bounds.

This guide explores multi-neuron relaxations as described in the verification literature, focusing on how they work, why they’re tighter, and when the computational cost is worthwhile.

The Convex Barrier and Its Solution

Before understanding multi-neuron relaxations, we must understand the fundamental limitation they overcome.

The Convex Barrier

Salman et al. proved the convex barrier: single-neuron linear inequality based verification approaches cannot be tighter than linear programming (LP) based approaches. All methods like CROWN, DeepPoly, and IBP are fundamentally limited by this barrier when they relax each ReLU independently.

This means no matter how clever your single-neuron relaxation is, you cannot beat LP tightness without considering neurons jointly.

Breaking the Barrier

Singh et al. and Tjandraatmadja et al. discovered the key insight: for ReLU that takes multiple input variables, considering those inputs together produces tighter convex polytopes than applying single-neuron relaxations along the combined direction.

Example: Consider $z = \text{ReLU}(x + y)$ where $x, y \in [-1, 1]$ .

Single-neuron approach: Let $w = x + y$ , so $w \in [-2, 2]$ . Apply triangle relaxation to $z = \text{ReLU}(w)$ treating $w$ as a single variable.
Multi-neuron approach: Consider the 2D space $(x, y)$ directly. Compute the tightest convex polytope in the $(x, y, z)$ space that contains $\{(x, y, \text{ReLU}(x+y)) : x, y \in [-1, 1]\}$ .

The multi-neuron polytope is strictly tighter. The single-neuron approach loses information by projecting onto the $w$ -direction before relaxing.

Visualization: The verification literature illustrates this comparison for $z = \text{ReLU}(x+y)$ where $x, y \in [-1, 1]$ :

Single ReLU polytope (brown region) gives a looser upper bound for $z$

Multi-neuron convex relaxation (two dark blue facets) gives a tighter upper bound

The improvement comes from exploiting the 2D structure of the input space rather than collapsing to 1D.

Multi-Neuron Relaxation Methods

Several methods exploit multi-neuron relaxations, each with different tradeoffs.

k-ReLU

k-ReLU considers $k$ input variables simultaneously when relaxing a ReLU.

Formulation: For $z = \text{ReLU}(w_1 x_1 + w_2 x_2 + \cdots + w_k x_k + b)$ with bounds $x_i \in [\underline{x}_i, \overline{x}_i]$ :

Compute the tightest convex polytope in the $(x_1, \ldots, x_k, z)$ space
Project onto relevant dimensions for bound propagation
Use the resulting linear constraints in verification

Parameters: Practical implementations use $k \leq 5$ as the polytope complexity grows exponentially with $k$ .

Advantage: Provably tighter than single-neuron relaxations while maintaining polynomial-time verification through LP.

PRIMA

PRIMA (Probabilistic Relaxation for Multi-neuron Analysis) provides a systematic framework for multi-neuron relaxations with efficient heuristics.

Key features:

Considers $k$ inputs jointly (typically $k \leq 5$ )
Uses heuristics to select which neurons benefit most from multi-neuron treatment
Balances tightness gains against computational overhead
Scales to medium-sized networks (tens of thousands of neurons)

Implementation: PRIMA formulates verification as a linear program over an extended domain that includes multi-neuron constraints. The LP is larger than single-neuron methods but remains polynomial-time solvable.

The Challenge: Exponential Constraints

Tjandraatmadja et al. identified the fundamental challenge: the tightest convex polytope for multi-neuron relaxation may contain an exponential number of linear constraints relative to the number of input variables.

This makes it impractical to enumerate all constraints. The key to scalable multi-neuron verification is selecting which constraints to include.

C2V: Heuristic Constraint Selection

C2V (Cutting-plane 2 Verification) addresses this through heuristic constraint selection:

Start with a base set of constraints (single-neuron bounds)
Iteratively add cutting planes from the multi-neuron polytope that most tighten bounds
Stop when budget is exhausted or no significant improvement

Advantage: Achieves most of the tightness gain with a small fraction of the total constraints.

Active-Set

Active-Set improves upon C2V with:

Gradient-based optimization to identify the most valuable constraints
Better heuristics for constraint selection based on impact estimation
Adaptive budgets that allocate more constraints to critical layers

Result: Better tightness-cost tradeoff than C2V, enabling verification of larger networks.

GCP-CROWN

GCP-CROWN takes a different approach: extract convex constraints from MILP solvers and integrate them into linear inequality propagation.

This can be viewed as leveraging multi-neuron relaxations within branch-and-bound complete verification, using tight bounds for pruning.

Tightness vs. Scalability Tradeoff

The verification literature characterizes the spectrum of linear relaxation methods:

Method	Neurons per Constraint	Tightness	Scalability	Best Use Case
IBP	1 (intervals)	Loosest	Best	Very large networks, IBP-trained models
CROWN	1 (single-neuron)	Moderate	Excellent	General verification
DeepPoly	1 (single-neuron)	Good	Excellent	General verification
k-ReLU	k (multi-neuron)	Very tight	Moderate	Medium networks, tight bounds needed
PRIMA	k (multi-neuron)	Tightest	Limited	Critical verification tasks
LP	All (complete polytope)	Exact (convex hull)	Poor	Small networks only

Scalability Insights:

IBP: Most scalable, typically loosest. However, on models specifically trained for IBP, certified robustness can be quite satisfactory on large CIFAR-10 and Tiny ImageNet datasets.

Multi-neuron relaxations: Tightest but least scalable among linear relaxation methods. Effective heuristics enable multi-neuron methods to significantly improve scalability with small tightness loss. Can verify decent robustness on medium-sized CIFAR-10 models with around $10^5$ neurons more efficiently than complete verification.

Deep networks limitation: For very deep neural networks (layers $\geq 10$ ), due to amplification of over-approximation, linear relaxation based approaches cannot certify nontrivial robustness.

Practical Verification Workflow

When to Use Multi-Neuron Relaxations

Use multi-neuron methods when:

Single-neuron methods (CROWN, DeepPoly) return “unknown” but you need tighter bounds
Network has moderate size (thousands to tens of thousands of neurons)
Verification budget allows 5-20x longer runtime than single-neuron methods
Properties are difficult and require every bit of tightness
Complete methods (MILP, SMT) timeout

Don’t use when:

Single-neuron methods already verify successfully
Network is very large (hundreds of thousands of neurons)
Network is very deep (>10 layers)---over-approximation dominates
Speed is critical---use CROWN or DeepPoly instead
Need complete verification---use branch-and-bound or SMT directly

Hybrid Verification Strategy

The most effective approach combines methods:

Start with IBP or CROWN for rapid initial bounds
Identify uncertain regions where bounds are loose
Apply multi-neuron relaxations (PRIMA, k-ReLU) to tighten critical bounds
Use complete verification (branch-and-bound) only for remaining uncertain regions

This staged approach maximizes efficiency while ensuring adequate tightness.

Implementation Considerations

Parameter Selection

Number of jointly considered inputs ( $k$ ):

$k=1$ : Single-neuron (DeepPoly, CROWN)
$k=2$ : Pairwise multi-neuron (moderate cost)
$k=3,4,5$ : Higher-order (expensive but tighter)

Practical implementations rarely exceed $k=5$ due to exponential constraint growth.

Constraint budget: Limit the number of multi-neuron constraints to control overhead:

Small networks (100s of neurons): Allow 50-100% as many multi-neuron constraints as neurons
Medium networks (1000s): 10-20% constraint budget
Large networks (10k+): 1-5% constraint budget

Layer selection: Focus multi-neuron relaxations on:

Early and middle layers (strongest correlations)
Layers with many uncertain neurons
Skip layers with mostly stable neurons (clearly active/inactive)

Software Tools

Available implementations:

PRIMA verifier: Reference implementation with LP-based solving
ERAN: Abstract interpretation framework supporting multi-neuron domains
auto_LiRPA: GPU-accelerated bound propagation with multi-neuron support
GCP-CROWN: Integration with branch-and-bound verification

Theoretical Perspective

Abstract Interpretation View

Multi-neuron relaxations can be understood through abstract interpretation:

Abstract domain: Convex polytopes in extended space including multiple neurons jointly
Concretization: Each abstract element represents a set of possible neuron activation combinations
Soundness: The abstract element over-approximates all reachable states
Precision: Multi-neuron domains are more precise (tighter) than single-neuron domains

This perspective clarifies why multi-neuron relaxations improve tightness: they use more expressive abstract domains that can represent relationships single-neuron domains cannot capture.

Connection to Complete Methods

Multi-neuron relaxations bridge incomplete and complete verification:

LP-based verification uses the complete single-neuron polytope (convex hull)
Multi-neuron relaxations use subsets of the complete multi-neuron polytope
Complete verification (MILP, SMT) considers all combinations (potentially exponential)

The tightness hierarchy: IBP < single-neuron < multi-neuron < LP < complete

Current Research Directions

Active research areas in multi-neuron verification:

Learned constraint selection: Use machine learning to predict which multi-neuron constraints most tighten bounds, replacing hand-crafted heuristics.

Adaptive refinement: Start with single-neuron bounds, selectively add multi-neuron constraints only where needed, minimizing overhead.

GPU acceleration: Parallelize multi-neuron constraint generation and LP solving for practical scalability.

Integration with training: Train networks to have structure amenable to multi-neuron relaxations, reducing the constraint budget needed for tight bounds.

Efficient polytope representations: Develop compressed representations of multi-neuron polytopes that maintain tightness while reducing constraint counts.

Final Thoughts

Multi-neuron relaxations represent a fundamental advance in incomplete verification. By considering multiple neuron inputs jointly rather than independently, they break through the convex barrier that limits single-neuron methods.

The key insight---that ReLU with multiple inputs can be relaxed more tightly by considering the input space directly---has profound implications. It shows that verification tightness isn’t just about algorithmic cleverness; it’s about choosing the right level of abstraction.

However, tightness comes at computational cost. The exponential growth of polytope constraints with input dimension necessitates careful heuristics for constraint selection. Methods like C2V, Active-Set, and PRIMA demonstrate that with effective heuristics, multi-neuron relaxations can achieve dramatic tightness gains while remaining practical for medium-sized networks.

Understanding multi-neuron relaxations clarifies the landscape of verification methods. They occupy a crucial middle ground: tighter than single-neuron methods (CROWN, DeepPoly) but more scalable than complete methods (MILP, SMT). For verification tasks where single-neuron methods fail and complete methods timeout, multi-neuron relaxations often provide the solution.

Multi-neuron approaches are “the tightest but least scalable” among linear relaxation methods. With effective heuristics, they can verify medium-sized CIFAR-10 models with around $10^5$ neurons more efficiently than complete verification. This defines their niche: networks too complex for single-neuron methods but too large for complete verification.