The Luna Bound Propagator for Formal Analysis of Neural Networks

2026/03/31 by Henry LeCates, Haoze Wu
Computer Science · #cs.AI #cs.LG #cs.LO

paper · pdf · doi:10.48550/arxiv.2603.23878

Accepted at SAS'26

arxiv created 2026/08/04 · arxiv updated 2026/08/06

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.

Citations

• The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results
• Proof Minimization in Neural Network Verification
• Abstraction-Based Proof Production in Formal Verification of Neural Networks
• Cubing for Tuning
• The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results
• Neural Network Verification with PyRAT
• Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
• Lightweight Online Learning for Sets of Related Problems in Automated Reasoning
• Convex Bounds on the Softmax Function with Applications to Robustness Verification
• General Cutting Planes for Bound-Propagation-Based Neural Network Verification
• Neural Network Verification with Proof Production
• Efficient Neural Network Analysis with Sum-of-Infeasibilities
• Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification
• PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations
• NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems
• PyTorch: An Imperative Style, High-Performance Deep Learning Library
• Efficient Neural Network Robustness Certification with General Activation Functions
• On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models
• Efficient Formal Safety Analysis of Neural Networks
• Towards Deep Learning Models Resistant to Adversarial Attacks