[2603.23878] The Luna Bound Propagator for Formal Analysis of Neural Networks

Computer Science > Machine Learning arXiv:2603.23878 (cs) [Submitted on 25 Mar 2026] Title:The Luna Bound Propagator for Formal Analysis of Neural Networks Authors:Henry LeCates, Haoze Wu View a PDF of the paper titled The Luna Bound Propagator for Formal Analysis of Neural Networks, by Henry LeCates and Haoze Wu View PDF HTML (experimental) Abstract: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. Comments: Subjects: Machine Learning (cs.LG); Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO) ACM classes: F.4.1; I.2.0 Cite as: arXiv:2603.23878 [cs.LG]   (or arXiv:2603.23878v1 [cs.LG] for this version)   https://doi.org/10.48550/arXiv.2603.23878 Focus to learn more arXiv-issued DOI via DataCite (pending registration) Submission history From: Henry LeCates [view email] [v1] Wed, 25 Mar 2026...