The Luna Bound Propagator for Formal Analysis of Neural Networks

TL;DR

Luna is a C++ implementation of alpha-CROWN, enhancing neural network verification by providing more efficient and tighter bounds, and is publicly available for integration into verification systems.

Contribution

Introduces Luna, a C++ bound propagator supporting multiple analysis methods, improving performance and tightness over existing Python implementations.

Findings

Luna outperforms state-of-the-art alpha-CROWN in bound tightness.

Luna is more computationally efficient.

Luna supports a general computational graph for neural network verification.

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.