PAVE：让多数 DNN 鲁棒性验证查询快速求解的帕累托验证方法

View PDF HTML (experimental)

Abstract:Formal verification of deep neural networks (DNNs) faces a fundamental scalability challenge: verifying robustness is NP-hard and state-of-the-art tools often time out on modern architectures. We propose PAreto VErification, or PAVE: by augmenting DNNs with early exits (EEs) and verifying exit-by-exit, we solve a large fraction of robustness queries---roughly 80% in our evaluation---in a small fraction of the time required for direct verification. The key insight is that many inputs in a robustness neighborhood exit at an early layer. Verifying this early-exit behavior is often a tractable problem,allowing verification to terminate long before the full network is analyzed. EEs can be added without modifying the base network, and incur at most a 0.3% accuracy change across our tested architectures. We formalize the novel robustness property for EE networks, prove it is Fixed-Parameter Tractable under a trace stability condition (which commonly holds in practice), and present a sound and complete verification algorithm. Two sound optimizations --- break (early termination when the winner dominates) and continue (skipping the inner loop when no runner-up can win) --- reduce SAFE-case verification time by up to 10x. Experiments on MNIST, CIFAR-10, and CIFAR-100 with networks from 600K to 33M parameters demonstrate that PAVE enables solving queries that were not solved otherwise, including formal verification of ResNet-18 on CIFAR-100.

Submission history

From: Yizhak Yisrael Elboher [view email]
[v1] Tue, 23 Dec 2025 20:36:54 UTC (186 KB)
[v2] Thu, 5 Nov 2026 11:25:04 UTC (187 KB)