The Luna Bound Propagator for Formal Analysis of Neural Networks
This work addresses the integration and deployment issues for DNN verifiers in production-level systems, though it is incremental as it reimplements existing methods in a new language.
The paper tackles the challenge of integrating neural network verification tools into production systems by introducing Luna, a C++-based bound propagator that supports Interval Bound Propagation, CROWN, and alpha-CROWN analyses, achieving competitive performance with state-of-the-art implementations in terms of bound tightness and computational efficiency on VNN-COMP 2025 benchmarks.
The parameterized CROWN analysis, a.k.a., alpha-CROWN, has emerged as a practically successful bound propagation 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 bound propagator implemented in C++. Luna supports Interval Bound Propagation, the CROWN analysis, and the alpha-CROWN analysis over a general computational graph. We describe the architecture of Luna and show that it is competitive with the state-of-the-art alpha-CROWN implementation in terms of both bound tightness and computational efficiency on benchmarks from VNN-COMP 2025.