Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Luna Bound Propagator for Formal Analysis of Neural Networks

Henry LeCates, Haoze Wu

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.

The Luna Bound Propagator for Formal Analysis of Neural Networks

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.
Paper Structure (27 sections, 1 equation, 2 figures, 1 table)

This paper contains 27 sections, 1 equation, 2 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries on Bound Propagation
  3. The Bound Propagator
  4. Bounded Model
  5. Bounded Node Modules
  6. Bound Propagation Engine
  7. CROWN
  8. $\alpha$-CROWN
  9. Front End.
  10. Code, Installation, and Availability.
  11. Evaluation
  12. Experimental Setup
  13. Results and Analysis
  14. Conclusion and Next Steps
  15. Architecture and Core Components
  16. ...and 12 more sections

Figures (2)

  • Figure 1: High-level overview of 's system architecture.
  • Figure 2: Example Python API usage: loading an ONNX model, setting input bounds, and computing $\alpha$-CROWN bounds.