The Luna Bound Propagator for Formal Analysis of Neural Networks

About

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.

Henry LeCates, Haoze Wu · 2026

Related benchmarks

Task	Dataset	Result
Bound Propagation for Neural Network Verification	acasxu 2023	Propagation Width867.42	2
Bound Propagation for Neural Network Verification	cersyve	Width4.27	2
Bound Propagation for Neural Network Verification	cifar100 2024	Propagation Width4.63	2
Bound Propagation for Neural Network Verification	collins_rul_cnn 2022	Propagation Width35.8	2
Bound Propagation for Neural Network Verification	linearizenn 2024	Propagation Width43.44	2
Bound Propagation for Neural Network Verification	malbeware	Result Width5.42	2
Bound Propagation for Neural Network Verification	metaroom 2023	Propagation Width0.16	2
Bound Propagation for Neural Network Verification	safenlp 2024	Propagation Width22.77	2
Bound Propagation for Neural Network Verification	sat_relu	Propagation Width58.99	2
Bound Propagation for Neural Network Verification	tllverifybench 2023	Propagation Width207.98	2