The Luna Bound Propagator for Formal Analysis of Neural Networks

Henry LeCates; Haoze Wu

cs.LGMar 25, 2026

The Luna Bound Propagator for Formal Analysis of Neural Networks

Authors: Henry LeCates, Haoze Wu

Organizations: Amherst College, USA

Abstract

The parameterized CROWN analysis, a.k.a., alpha-CROWN has emerged as a practically successful abstract interpretation method for neural network verification. However, existing implementations of alpha-CROWN are limited to Python, which complicates integration into existing DNN verifiers and long-term production-level systems. We introduce Luna, a new abstract-interpretation-based bound propagator implemented in C++. Luna supports Interval Bound Propagation, the DeepPoly/CROWN analysis, and the alpha-CROWN analysis over a general computational graph. We describe the architecture of Luna and show that it outperforms the state-of-the-art alpha-CROWN implementation in terms of both bound tightness and computational efficiency on supported benchmarks from VNN-COMP 2025. Luna is publicly available at https://github.com/ai-ar-research/luna.

Figures & tables

Panel of Figure 1 — Figure 1: Family of valid linear relaxations for an unstable ReLU neuron with pre-activation bounds $[l,u]$ . The lower bound can be given by any line across the origin with slope $\alpha\in[0,1]$ . Standard CROWN fixes $\alpha$ heuristically, while $\alpha$ -CROWN treats $\alpha$ as an optimizable parameter.

Figure 2: High-level overview of Luna ’s system architecture.

Category	Operation	CROWN	$\alpha$ -CROWN
Linear	Fully Connected (Gemm)	✓	✓
	Convolution	✓	✓
	BatchNormalization	✓	✓
Nonlinear Activation	ReLU	✓	✓
Nonlinear Activation	Sigmoid	✓	–
Elementwise	Add	✓	✓

Table 1: Currently supported operations in the Luna bound propagator.

Panel of Figure 3 — Figure 3: Example CLI usage: verifying an ONNX model against a VNN-LIB property using $\alpha$ -CROWN with optimized upper and lower bounds.

Panel of Figure 4 — Figure 4: Example C++ API usage: loading an ONNX model, setting input bounds, and computing optimized bounds via $\alpha$ -CROWN.

Panel of Figure 5 — Figure 5: Example Python API usage: loading an ONNX model, setting input bounds, and computing an optimized bound via $\alpha$ -CROWN.

Category	Benchmark	Application	Network Types	# Params	Effective Input Dim
Complex	LinearizeNN	NN controller approximation	FC. + Conv. + Vision Transformer + Residual + ReLU	203,000	4
CNN & ResNet	Collins RUL CNN	Condition Based Maintenance	Conv. + ReLU, Dropout	60,000 – 262,000	400 – 800
	cifar100	Image Classification	FC + Conv. + Residual, ReLU + BatchNorm	2.5M – 3.8M	3072
	Metaroom	—	Conv. + FC, ReLU	466,000 – 7.4M	5376
	MalBeWare	Malware Classification	FC + Conv. + ReLU	102,000 – 1.5M	4,000
	cersyve	Neural Certificates for Control Systems	FC + Residual + ReLU	1,000 – 4,000	2 – 6

Table 2: Considered benchmarks from the VNN-COMP benchmark suite. # Params refers to the number of learnable parameters (weights and biases) in the network. Effective Input Dim is the number of input dimensions over which input properties are defined (e.g., cifar100 processes

32\times 32\times 3

images, giving an effective input dimension of 3,072).

Bench. (# inst.)	Luna			auto_LiRPA
Bench. (# inst.)	Width	Time (s)	Finished	Width	Time (s)	Finished
acasxu_2023 (184)	867.42	1.41	184	882.90	6.19	184
cersyve (12)	4.27	1.23	12	4.38	6.77	12
cifar100_2024 (200)	4.63	44.88	170	4.62	136.59	100
collins_rul_cnn_2022 (62)	35.80	3.57	62	35.98	5.78	62
cora_2024 (60)	12073.43	8.37	60	12067.97	9.53	60

Table 3: CPU comparison of Luna and auto_LiRPA . Width: average interval across output dimensions. Time: average runtime per instance. Finished: instances for which the analysis terminated and returned bounds within the 300 s timeout. Width and Time averages include only instances where both tools finished.

Figure 6: Bound width (left) and runtime (right) for Cifar100 2024

Bench. (# inst.)	Luna			auto_LiRPA
Bench. (# inst.)	Width	Time (s)	Finished	Width	Time (s)	Finished
acasxu_2023 (185)	863.74	3.94	185	879.27	13.06	185
cersyve (12)	4.27	3.79	12	4.38	13.08	12
cifar100_2024 (200)	4.23	13.32	200	4.23	25.37	200
collins_rul_cnn_2022 (62)	35.80	2.45	62	35.98	9.33	62
cora_2024 (60)	12073.44	5.25	60	12067.99	11.93	60

Table 4: GPU comparison of Luna and auto_LiRPA . Width: average interval across output dimensions. Time: average runtime per instance. Finished: instances for which the analysis terminated and returned bounds within the 300 s timeout. Width and Time averages include only instances where both tools finished.

Figure 7: Bound width (left) and runtime (right) for Cifar100 2024 (GPU)

Network	Luna		auto_LiRPA
Network	Avg. Time (s)	Std. Dev.	Avg. Time (s)	Std. Dev.
Nano	0.53	0.02	4.81	0.10
Tiny	0.53	0.02	4.78	0.08

Table 5: Startup time comparison of Luna and auto_LiRPA (averaged over 50 iterations).

Appendix figures & tables24 assets

Supplementary material from the paper’s appendix.

Appendix

Panel of Figure 8 — Figure 8: Linear relaxation bounds for ReLU over the unstable interval $[\ell,u]$ . The upper bound is the line from $(\ell,0)$ to $(u,u)$ . The lower bound is chosen as $h_{L}=x$ when $u\geq|\ell|$ (Case 1), and $h_{L}=0$ when $u<|\ell|$ (Case 2).

Panel of Figure 9 — Figure 9: Linear relaxation bounds for $\sigma(x)=1/(1+e^{-x})$ over $[\ell,u]$ (blue dashed: $h_{U}$ ; red dashed: $h_{L}$ ). Case 1 ( $0\leq\ell$ ): $\sigma$ is concave, so $h_{U}$ is a tangent line and $h_{L}$ is the chord through the endpoints. Case 2 ( $u\leq 0$ ): $\sigma$ is convex and the roles are swapped. Case 3 ( $\ell<0<u$ ): $\sigma$ transitions from convex to concave; $h_{U}$ passes through $(\ell,\sigma(\ell))$ and is tangent at some $d\geq 0$ , while $h_{L}$ passes through $(u,\sigma(u))$ and is tangent at some $d\leq 0$ , found via binary search.

Panel of Figure 10 — Figure 10: Family of valid linear relaxations for an unstable ReLU neuron with pre-activation bounds $[l,u]$ . The upper bound (blue dashed) is uniquely determined as the line connecting the points $(l,0)$ and $(u,u)$ . The lower bound (red) can be given by any valid slope, $\alpha\in[0,1]$ . Standard CROWN selects $\alpha$ via heuristic choice, while $\alpha$ -CROWN treats each $\alpha_{i}$ as an optimizable parameter.

Figure 11: Bound width (left) and runtime (right) for Acasxu 2023

Figure 12: Bound width (left) and runtime (right) for Cersyve

Figure 13: Bound width (left) and runtime (right) for Collins Rul Cnn 2022

Figure 14: Bound width (left) and runtime (right) for Cora 2024

Figure 15: Bound width (left) and runtime (right) for Linearizenn 2024

Figure 16: Bound width (left) and runtime (right) for Malbeware

Figure 17: Bound width (left) and runtime (right) for Metaroom 2023

Figure 18: Bound width (left) and runtime (right) for Safenlp 2024

Figure 19: Bound width (left) and runtime (right) for Sat Relu

Figure 20: Bound width (left) and runtime (right) for Tllverifybench 2023

Figure 21: Bound width (left) and runtime (right) for Acasxu 2023 (GPU)

Figure 22: Bound width (left) and runtime (right) for Cersyve (GPU)

Figure 23: Bound width (left) and runtime (right) for Collins Rul Cnn 2022 (GPU)

Figure 24: Bound width (left) and runtime (right) for Cora 2024 (GPU)

Figure 25: Bound width (left) and runtime (right) for Linearizenn 2024 (GPU)

Figure 26: Bound width (left) and runtime (right) for Malbeware (GPU)

Figure 27: Bound width (left) and runtime (right) for Metaroom 2023 (GPU)

Figure 28: Bound width (left) and runtime (right) for Safenlp 2024 (GPU)

Figure 29: Bound width (left) and runtime (right) for Sat Relu (GPU)

Figure 30: Bound width (left) and runtime (right) for Tllverifybench 2023 (GPU)

Network	Layers	Activation	# Params	Input Dim
Nano	1	ReLU	1	1
Tiny	2	ReLU	4	1

Appendix

Table 6: Test networks used in startup time experiments.

Explore similar work

Learning Lookahead Lemmas for Neural Network Verification
Jul 31, 2026Liam Davis, Haoze WuNeural Network Verification ReLU Neural Networks
Amherst College
Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial
May 26, 2026Haoyu Li, Xiangru Zhong, Hao Cheng +2Neural Network Verification
Department of Computer Science · Department of Electrical and Computer Engineering, University of Illinois Urbana-Champaign, Urbana, IL 61801, USA
CLAD: Constrained Abstract Domain for Neural Network Verification
Sep 28, 2026Hai Duong, Thanh Le, ThanhVu NguyenNeural Network Verification Neural Network Robustness
Department of Computer Science George Mason University Fairfax, VA, USA · Unaffiliated Yokosuka, Japan

Jul 31, 2026J/K move · Enter open · S save

Learning Lookahead Lemmas for Neural Network Verification

Liam Davis, Haoze Wu

Amherst College

Neural Network Verification ReLU Neural Networks Branch and Bound Tree Search

Open paper AskPDF arXiv

State-of-the-art neural network verifiers use the branch-and-bound procedure as their core solving mechanism. We introduce an inprocessing framework for neural network verification driven by the lookahead procedure. Under this framework, lookahead derives new lemmas over the phases of unstable ReLUs, which are collected into an implication graph that is used to prune the search space and vivify boolean cuts. We instantiate the framework in two state-of-the-art verifiers, Marabou and

α

β

-CROWN, and demonstrate that it improves performance in both, proving up to 34% more instances unsatisfiable.

Abstract

Explore similar work

Learning Lookahead Lemmas for Neural Network Verification

Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial

CLAD: Constrained Abstract Domain for Neural Network Verification