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.

翻译：参数化CROWN分析（即alpha-CROWN）已成为一种在实践中成功的神经网络验证抽象解释方法。然而，现有alpha-CROWN实现仅限于Python，这使其难以集成到现有DNN验证器及长期生产级系统中。我们提出Luna——一种基于C++实现的新型抽象解释边界传播器。Luna支持在通用计算图上进行区间边界传播、DeepPoly/CROWN分析以及alpha-CROWN分析。本文描述了Luna的架构，并证明其在VNN-COMP 2025基准测试中的边界紧致性与计算效率均优于现有最先进的alpha-CROWN实现。Luna已开源至https://github.com/ai-ar-research/luna。