用C++实现的神经网络验证工具，速度和精度均优于现有方法。
The Luna Bound Propagator for Formal Analysis of Neural Networks
- 基于抽象解释的边界传播框架，支持多种分析方法。
- 在VNN-COMP 2025基准上，计算效率更高且边界更紧。
- 适合需要高性能验证的工业级深度神经网络系统。
参数化CROWN分析（即alpha-CROWN）已成为神经网络验证中一种实用有效的抽象解释方法。然而，现有的alpha-CROWN实现仅限于Python，难以集成到现有深度神经网络验证器及长期生产系统中。本文提出Luna，一个基于抽象解释的边界传播器，采用C++实现，支持区间边界传播、DeepPoly/CROWN分析以及通用计算图上的alpha-CROWN分析。我们介绍了Luna的架构，并在VNN-COMP 2025的基准测试中证明其在边界紧致性和计算效率方面均优于当前最先进的alpha-CROWN实现。Luna已开源，地址为https://github.com/ai-ar-research/luna。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。