Multi-Neuron Relaxation and PRIMA

Multi-Neuron Relaxation and PRIMA¶

January 2026 NNV Guide 8 min read 1,652 words

Zhongkui Ma This guide is based on SoK: Certified Robustness for Deep Neural Networks. It covers multi-neuron relaxation techniques including PRIMA and the convex barrier theorem.

Verification Methods PRIMA Polyhedra

Single-neuron relaxations—the standard approach in bound propagation [Singh et al., 2019, Weng et al., 2018, Zhang et al., 2018]—treat each ReLU independently. For a ReLU with multiple inputs like \(z = \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 = \relu(\hat{z})\).

This works and scales efficiently, but it misses critical opportunities for tightness. Multi-neuron relaxation methods [Singh et al., 2019, Müller et al., 2022, Palma et al., 2021, Tjandraatmadja et al., 2020] 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. [Salman et al., 2019] proved the convex barrier: single-neuron linear inequality based verification approaches cannot be tighter than linear programming (LP) based approaches. All methods like CROWN [Zhang et al., 2018], DeepPoly [Singh et al., 2019], and IBP [Gowal et al., 2019] 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. [Singh et al., 2019] and Tjandraatmadja et al. [Tjandraatmadja et al., 2020] 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 = \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 = \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, \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 = \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 [Singh et al., 2019] considers \(k\) input variables simultaneously when relaxing a ReLU.

Formulation: For \(z = \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) [Müller et al., 2022] 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. [Tjandraatmadja et al., 2020] 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) [Tjandraatmadja et al., 2020] 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 [Palma et al., 2021] 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 [Zhang et al., 2022] 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:

Table 21 Linear Relaxation Methods Comparison¶
Method	Neurons per Constraint	Tightness	Scalability	Best Use Case
IBP [Gowal et al., 2019]	1 (intervals)	Loosest	Best	Very large networks, IBP-trained models
CROWN [Zhang et al., 2018]	1 (single-neuron)	Moderate	Excellent	General verification
DeepPoly [Singh et al., 2019]	1 (single-neuron)	Good	Excellent	General verification
k-ReLU [Singh et al., 2019]	k (multi-neuron)	Very tight	Moderate	Medium networks, tight bounds needed
PRIMA [Müller et al., 2022]	k (multi-neuron)	Tightest	Limited	Critical verification tasks
LP [Ehlers, 2017]	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-20× 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 [Müller et al., 2022]: Reference implementation with LP-based solving
ERAN [Singh et al., 2019]: Abstract interpretation framework supporting multi-neuron domains
auto_LiRPA [Xu et al., 2020]: GPU-accelerated bound propagation with multi-neuron support
GCP-CROWN [Zhang et al., 2022]: Integration with branch-and-bound verification

Theoretical Perspective¶

Abstract Interpretation View¶

Multi-neuron relaxations can be understood through abstract interpretation [Singh et al., 2019, Gehr et al., 2018]:

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 [Xu et al., 2020] 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 [Singh et al., 2019, Müller et al., 2022, Tjandraatmadja et al., 2020] 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 [Tjandraatmadja et al., 2020], Active-Set [Palma et al., 2021], and PRIMA [Müller et al., 2022] 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 [Zhang et al., 2018], DeepPoly [Singh et al., 2019]) 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.

Next Guide

Continue to SDP-Based Verification: Semi-Definite Programming for Tighter Bounds to explore semi-definite programming approaches that provide even tighter bounds through quadratic relaxations.

[1]

Ruediger Ehlers. Formal verification of piece-wise linear feed-forward neural networks. In International Symposium on Automated Technology for Verification and Analysis, 269–286. Springer, 2017.

[2] (1,2)

Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. AI²: safety and robustness certification of neural networks with abstract interpretation. In 2018 IEEE Symposium on Security and Privacy (SP), 3–18. IEEE, 2018.

[3] (1,2,3)

Sven Gowal, Krishnamurthy Dj Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovic, Timothy Mann, and Pushmeet Kohli. Scalable verified training for provably robust image classification. In Proceedings of the IEEE International Conference on Computer Vision, 4842–4851. 2019.

[4] (1,2,3,4,5,6,7)

Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev. PRIMA: precise and general neural network certification via multi-neuron convex relaxations. Proceedings of the ACM on Programming Languages, 6(POPL):1–33, 2022.

[5] (1,2,3,4)

Alessandro De Palma, Harkirat Behl, Rudy R Bunel, Philip Torr, and M. Pawan Kumar. Scaling the convex barrier with active sets. In International Conference on Learning Representations. 2021.

[6] (1,2)

Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang. A convex relaxation barrier to tight robustness verification of neural networks. In Advances in Neural Information Processing Systems, 9832–9842. 2019.

[7] (1,2,3,4,5,6,7,8,9,10,11,12,13,14)

Gagandeep Singh, Rupanshu Ganvir, Markus Püschel, and Martin Vechev. Beyond the single neuron convex barrier for neural network certification. In Advances in Neural Information Processing Systems, 15072–15083. 2019.

[8] (1,2,3,4,5,6,7)

Christian Tjandraatmadja, Ross Anderson, Joey Huchette, Will Ma, Krunal Kishor PATEL, and Juan Pablo Vielma. The convex relaxation barrier, revisited: tightened single-neuron relaxations for neural network verification. Advances in Neural Information Processing Systems, 33:21675–21686, 2020.

[9] (1,2)

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. In International Conference on Machine Learning, 5276–5285. 2018.

[10] (1,2,3)

Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems, 2020.

[11] (1,2,3)

Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh, and J. Zico Kolter. General cutting planes for bound-propagation-based neural network verification. arXiv preprint arXiv:2208.05740, 2022.

[12] (1,2,3,4,5)

Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In Advances in neural information processing systems, 4939–4948. 2018.