The Luna Bound Propagator for Formal Analysis of Neural Networks

This paper introduces Luna, a C++-implemented bound propagator that supports Interval Bound Propagation, CROWN, and alpha-CROWN analyses on general computational graphs, offering competitive performance in bound tightness and efficiency while addressing the integration limitations of existing Python-based alpha-CROWN implementations.

The Gist

Imagine you are a security guard at a high-tech factory. Inside this factory, there is a giant, complex machine (a Neural Network) that takes raw materials (inputs) and turns them into finished products (outputs).

Your job is to guarantee that no matter what raw materials you feed into the machine, the final product will never be defective. But here's the catch: the machine is so complicated and has so many moving parts that you can't possibly test every single combination of raw materials. It would take forever!

This is where Luna comes in.

The Problem: The "Python" Bottleneck

For a while, the best security guards (mathematical tools called $\alpha$-CROWN) were written in a programming language called Python. Python is great for learning and prototyping—it's like a Swiss Army knife that's easy to carry around.

However, in the real world of industrial security, you often need tools built with C++, which is like a heavy-duty, industrial-grade power drill. It's faster, more robust, and integrates easily into massive, existing security systems.

The problem? Trying to use the Python "Swiss Army knife" inside a C++ "power drill" system is clumsy. It's slow to start up, hard to connect, and creates a lot of friction. Many factories just couldn't use the best security tools because they were stuck in the wrong language.

The Solution: Enter Luna

The authors, Henry LeCates and Haoze Wu, built Luna.

Think of Luna as a brand-new, industrial-grade power drill that does the exact same job as the Swiss Army knife, but it's built specifically for the heavy-duty factory floor. It's written in C++, meaning it's fast, sturdy, and fits perfectly into any existing security system without the awkward integration issues.

How Luna Works (The Magic Trick)

To understand how Luna keeps the factory safe, imagine the machine has a "safety envelope."

1. The Box: You give the machine a box of raw materials (e.g., "The temperature must be between 20°C and 25°C").
2. The Prediction: You need to know: "If the temperature is anywhere in that box, what will the final product look like?"
3. The Bound Propagation: Luna acts like a super-smart shadow. It traces every possible path the raw materials could take through the machine.
   • The Old Way (IBP): It draws a very loose, big box around the output. It's safe, but the box is so big it might include "defective" products that aren't actually possible. It's too cautious.
   • The Better Way (CROWN): It tightens the box by looking at the specific rules of the machine's gears.
   • The Best Way ($\alpha$-CROWN): This is where Luna shines. It uses a "tuning knob" (mathematically called $\alpha$) to adjust the shape of the safety box in real-time. It asks, "What is the tightest possible box that still guarantees safety?" It solves a puzzle to find the perfect fit, ensuring the safety box is as small as possible without ever letting a defect slip through.

Why Luna is a Game-Changer

The paper compares Luna to the current champion (called auto_LiRPA). Here is the verdict:

• Speed: Luna is like a Formula 1 car compared to a sedan. In tests, it finished jobs 3 times faster in some cases.
• Efficiency: Because it doesn't have the "startup overhead" of switching languages, it gets to work immediately.
• Accuracy: It draws the safety boxes just as tightly (or even tighter) than the old tools. It doesn't sacrifice safety for speed.

The Big Picture

Before Luna, if you wanted to use the best neural network verification tools, you had to build your whole system around Python, or suffer through slow, clunky connections.

Luna breaks down that wall. It takes the most powerful mathematical analysis available and packages it into a tool that engineers can easily plug into their existing, high-performance systems.

In short: The authors didn't invent a new way to check for safety; they built a better delivery truck to get that safety check to the people who need it, faster and more reliably than ever before. This allows researchers to stop worrying about "how to connect the tool" and start focusing on solving the harder problems of making AI truly safe.

Technical Summary

1. Problem Statement

Neural network verification relies heavily on bound propagation techniques (such as CROWN and $\alpha$-CROWN) to compute sound output bounds for a given input region. While the parameterized CROWN analysis ($\alpha$-CROWN) has emerged as a state-of-the-art method offering a strong balance between precision and efficiency, its practical implementations (notably auto_LiRPA) are written exclusively in Python.

This creates significant engineering barriers:

• Integration Overhead: Integrating Python-based verifiers into systems written in C++ or MATLAB incurs non-trivial start-up and inter-process communication costs.
• Production Limitations: Python's runtime characteristics make it difficult to embed $\alpha$-CROWN into long-term, production-level verification pipelines or high-performance solvers (like branch-and-bound search shells).
• Lack of Native Interfaces: There is a need for a stable, native interface (Foreign Function Interface) to allow seamless integration with other verification tools.

2. Methodology: The Luna Framework

The authors introduce Luna, the first C++ implementation of the $\alpha$-CROWN analysis, designed to be a high-performance, easily integrable bound propagator.

Core Architecture

Luna is built on the Torch Deep Learning Library and follows a modular architecture (illustrated in Figure 1 of the paper):

1. Input Parsing:
   • Accepts neural networks in ONNX format.
   • Accepts verification specifications in VNN-LIB format.
   • Parses these into a Bounded Model, which consists of a bound-aware computational graph, input domains, and linear output constraints.
2. Bounded Model Representation:
   • The network is represented as a Directed Acyclic Graph (DAG) where nodes correspond to layer operations.
   • Each node maintains three types of bounds: Interval Bound Propagation (IBP) (concrete), CROWN (linear relaxation), and $\alpha$-CROWN (optimized).
   • Bounded Node Modules: Specific modules handle operator-specific bound computations. Non-linear activation nodes (e.g., ReLU) inherit from a base class that manages learnable $\alpha$ parameters.
3. Bound Propagation Engine:
   • CROWN Analysis: Performs linear bound propagation via backward topological traversal. It employs a lazy intermediate bound computation strategy: it recursively traverses the dependency graph to compute tightest possible input bounds for unstable neurons before performing the backward pass, avoiding unnecessary computation on stable neurons.
   • $\alpha$-CROWN Analysis: Extends CROWN by introducing learnable slope parameters ($\alpha$) for non-linearities. It wraps the CROWN engine and optimizes $\alpha$ using Projected Gradient Descent to minimize the output bound width.
   • Parallelization: Leverages Torch for parallel tensor and bound computations.
4. Interfaces:
   • CLI: For command-line execution with ONNX/VNN-LIB inputs.
   • Native C++ API: For direct integration into other C++ tools.
   • Python Bindings: Via pybind11 for ease of use and testing.

Key Technical Innovations

• Lazy Bound Computation: The engine avoids redundant backward passes by only computing intermediate bounds when necessary (i.e., when a node depends on unstable neurons), significantly reducing computational overhead compared to naive implementations.
• Memory Management: Nodes store only long-lived metadata; per-run quantities (symbolic coefficients) are recomputed on demand to minimize memory footprint.
• Optimization Loop: The $\alpha$-optimization loop uses gradient tracking to iteratively refine $\alpha$ parameters, caching the best solution found so far and employing early stopping based on convergence.

3. Key Contributions

1. First C++ Implementation of $\alpha$-CROWN: Luna provides a native C++ backend for $\alpha$-CROWN, removing the Python dependency barrier for integration into diverse verification ecosystems.
2. Stable Foreign Function Interface: Designed specifically for integration into production systems, offering a command-line interface, a native C++ API, and Python bindings.
3. Comprehensive Feature Set: Supports Interval Bound Propagation (IBP), standard CROWN, and parameterized $\alpha$-CROWN over general computational graphs.
4. Open Source Availability: The code (20k lines of C++17) is released under a permissive BSD license with a comprehensive test suite (unit, integration, and property-based tests).

4. Experimental Results

The authors evaluated Luna against auto_LiRPA (the current state-of-the-art Python implementation) using benchmarks from VNN-COMP 2025.

• Setup: Experiments ran on a cluster with 40 CPU cores and 192GB RAM, with a 300-second timeout per instance. Hyperparameters (20 iterations, 0.5 learning rate) were kept identical for fairness.
• Performance Metrics:
  • Runtime: Luna was consistently faster. For example, on the cifar100_2024 benchmark, Luna was 3x faster (44.88s vs. 136.59s). On tllverifybench_2023, it was 2.4x faster.
  • Success Rate: Luna successfully completed more instances within the timeout. On cifar100_2024, it finished 170 instances compared to auto_LiRPA's 100.
  • Bound Tightness: Luna produced tighter or equivalent bounds on 9 out of 11 benchmark sets. In cases where bounds differed, Luna's were tighter in 5 out of 7 instances.
• Conclusion: Luna achieves competitive (and often superior) bound tightness while significantly reducing runtime and start-up overhead.

5. Significance

The significance of Luna lies in its potential to democratize and industrialize neural network verification:

• Lowering Engineering Barriers: By providing a native C++ implementation, Luna allows researchers and engineers to integrate powerful bound propagation techniques into existing C++-based verifiers (like Marabou, NNV, or custom production tools) without the overhead of Python interop.
• Facilitating Future Research: By offloading the complexity of bound propagation to a highly optimized, stable library, researchers can focus on solving other algorithmic bottlenecks in verification (e.g., search strategies, splitting heuristics) rather than re-implementing bound propagation engines.
• Production Readiness: The architecture is designed for low per-invocation overhead and high parallelism, making it suitable for real-world, large-scale verification tasks.

In summary, Luna bridges the gap between theoretical advances in $\alpha$-CROWN analysis and practical, high-performance deployment in formal verification systems.