Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2603.23878 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909034017193984 |
|---|---|
| author | LeCates, Henry Wu, Haoze |
| author_facet | LeCates, Henry Wu, Haoze |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_23878 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | The Luna Bound Propagator for Formal Analysis of Neural Networks LeCates, Henry Wu, Haoze Machine Learning Artificial Intelligence Logic in Computer Science F.4.1; I.2.0 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. |
| title | The Luna Bound Propagator for Formal Analysis of Neural Networks |
| topic | Machine Learning Artificial Intelligence Logic in Computer Science F.4.1; I.2.0 |
| url | https://arxiv.org/abs/2603.23878 |