arXiv cs.AI· Yizhak Y. Elboher, Avraham Raviv, Amihay Elboher, Zhouxing Shi, Hillel Kugler, Guy Katz·· 11 小时前AI 评分31
PAVE：通过早退机制实现帕累托式 DNN 验证，多数查询快速求解
Pareto DNN Verification: Fast for Most Queries
AI 导读
研究者提出 PAVE（PAreto VErification）方法，通过给 DNN 增加早退（EE）并逐出口验证，在评测中约 80% 的鲁棒性查询上以远少于直接验证的时间完成求解。
正文 · AI 翻译
摘要：深度神经网络（DNN）的形式化验证面临根本性的可扩展性挑战：验证鲁棒性是 NP 难问题，最先进的工具在现代架构上常常超时。我们提出 PAreto VErification，即 PAVE：通过为 DNN 增加提前退出（EE）并逐退出进行验证，我们在评估中以直接验证所需时间的一小部分解决了大部分鲁棒性查询——约 80%。关键洞察在于，鲁棒性邻域中的许多输入会在较早的层退出。验证这种提前退出行为通常是一个可处理的问题，使得验证可以在分析完整网络之前很久就终止。EE 可以在不修改基础网络的情况下添加，并且在我们测试的架构上最多带来 0.3% 的准确率变化。我们形式化了 EE 网络的一种新颖鲁棒性性质，证明了它在迹稳定性条件（实践中通常成立）下是固定参数可处理的，并提出了一种可靠且完备的验证算法。两项可靠的优化——break（当胜出者占优时提前终止）和 continue（当没有次优者可能胜出时跳过内层循环）——将 SAFE 情况下的验证时间最多减少 10 倍。在 MNIST、CIFAR-10 和 CIFAR-100 上使用 600K 到 33M 参数的网络进行的实验表明，PAVE 能够解决原本无法解决的查询，包括在 CIFAR-100 上对 ResNet-18 的形式化验证。
| 主题： | 机器学习（cs.LG）；人工智能（cs.AI） |
| 引用为： | arXiv:2512.20755 [cs.LG] |
| （或 arXiv:2512.20755v2 [cs.LG] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2512.20755 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Yizhak Yisrael Elboher [查看电子邮件]
[v1]
2025年12月23日 星期二 20:36:54 UTC（186 KB）
[v2]
2026年11月5日 星期四 11:25:04 UTC（187 KB）
来源：arXiv cs.AI · arxiv.org