用于神经网络形式化分析的 Luna 界限传播器
机器学习
2026-05-13 v2 人工智能
计算机科学中的逻辑
摘要
参数化 CROWN 分析，亦称 alpha-CROWN，已成为神经网络验证中实用且成功的抽象解释方法。然而，现有 alpha-CROWN 的实现仅限于 Python，这使其难以集成到现有的 DNN 验证器和长期生产级系统中。我们引入 Luna，一个基于抽象解释的新型界限传播器，其实现基于 C++。Luna 支持区间界限传播、DeepPoly/CROWN 分析以及针对通用计算图的 alpha-CROWN 分析。我们描述了 Luna 的架构，并展示了其在 VNN-COMP 2025 支持的基准测试中，相较于最先进的 alpha-CROWN 实现，在界限紧密性和计算效率方面均取得优异性能。Luna 已公开可用，链接为 https://github.com/ai-ar-research/luna。
关键词
引用
@article{arxiv.2603.23878,
title = {The Luna Bound Propagator for Formal Analysis of Neural Networks},
author = {Henry LeCates and Haoze Wu},
journal= {arXiv preprint arXiv:2603.23878},
year = {2026}
}
备注
32 pages, 29 Figures