mlsanityData to 7 Oct 2026

The Luna Bound Propagator for Formal Analysis of Neural Networks

arXiv 2603.23878 ↗First posted 25 Mar 2026cs.LG cs.AI cs.LOcited by 0

Not on the map. Why?

Abstract (arXiv)

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.

Key facts. No citing papers in the map yet (data through 7 Oct 2026). Builds on 21 of its 38 references that are in the map. First posted on arXiv 25 Mar 2026.

Builds on

21 of 38 references.

References · 21

  1. 2019PyTorch: An Imperative Style, High-Performance Deep Learning Librarycited by 20,160
  2. 2017Towards Deep Learning Models Resistant to Adversarial Attackscited by 6,326
  3. 2018Efficient Neural Network Robustness Certification with General Activation Functionscited by 439
  4. 2018On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Modelscited by 322
  5. 2021Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verificationcited by 224
  6. 2018Efficient Formal Safety Analysis of Neural Networkscited by 165
  7. 2020NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systemscited by 128
  8. 2022General Cutting Planes for Bound-Propagation-Based Neural Network Verificationcited by 102
  9. 2024Marabou 2.0: A Versatile Formal Analyzer of Neural Networkscited by 81
  10. 2021PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximationscited by 77
  11. 2024The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Resultscited by 42
  12. 2025The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Resultscited by 26
9 more
  1. 2022Efficient Neural Network Analysis with Sum-of-Infeasibilitiescited by 24
  2. 2022Neural Network Verification with Proof Productioncited by 22
  3. 2023Convex Bounds on the Softmax Function with Applications to Robustness Verificationcited by 19
  4. 2022Scalable Verification of GNN-based Job Schedulerscited by 18
  5. 2024Neural Network Verification with PyRATcited by 9
  6. 2025Abstraction-Based Proof Production in Formal Verification of Neural Networkscited by 5
  7. 2025Proof Minimization in Neural Network Verificationcited by 4
  8. 2023Lightweight Online Learning for Sets of Related Problems in Automated Reasoningcited by 2
  9. 2025Cubing for Tuningcited by 1

Built on by

Not cited yet.