一句话：提出 SART 理论，打破不稳定 ReLU 神经元与二元变量的一一对应，从编码源头降低神经网络完备验证的复杂度。
神经网络在安全关键领域的部署需要完备形式验证，而主要瓶颈来自编码复杂度：传统方法为每个不稳定 ReLU 神经元分配一个二元变量。本文提出符号-绝对值重构理论（SART），通过建立形式化可约简判据，从根本上打破不稳定神经元与二元变量之间的一一映射，实现更细粒度建模，使每个不稳定神经元平均对应少于一个二元变量。基于 SART，作者给出完备验证所需二元变量数的理论下界，并在 P≠NP 假设下证明末层变量可压缩 50%，而中间层变量无法进一步减少。为突破“仅末层”的限制，作者将验证重构为序列过程，提出渐进收紧验证器 LayerABS，把中间层轮流视作临时末层并传播紧界，使增益扩展到整个网络。文章还揭示权重符号的数值对称性可使最坏情况复杂度达到理论最优，为验证友好架构设计提供指导。作为通用底层编码，SART 与具体算法无关；在无抽象编码及与抽象技术结合的完整/不完备验证器上，均于多个基准超越当前最优方法。
Complete formal verification of neural networks is crucial for their deployment in safety-critical domains. A key bottleneck stems from encoding complexity: traditional methods assign one binary variable per unstable ReLU neuron. We propose the Sign-Absolute Reformulation Theory (SART), which fundamentally breaks the conventional one-to-one mapping between unstable neurons and binary variables by establishing formal reducibility criteria. This allows for finer-grained modeling, where each unstable neuron corresponds on average to fewer than one binary variable, thereby reducing verification complexity at its source. Based on SART, we derive a theoretical lower bound on the number of binary variables required for complete verification and, under the assumption that 𝑃 ≠ 𝑁𝑃, prove that variables in the final layer can be compressed by 50%, while the number of variables in intermediate layers cannot be further reduced. To overcome the apparent “last-layer-only” limitation, we recast verification as a sequential process and, crucially, show that the gain lifts to the entire network: LayerABS, a SART-based progressive tightening verifier, iteratively treats intermediate layers as temporary final layers and propagates tight bounds that shrink the global search space and binaryvariable counts. Furthermore, we reveal a structural law influencing verification complexity: when the signs of weights of unstable neurons satisfy numerical symmetry, with positive and negative weights equal or differing by at most one, the worst-case verification complexity achieves the theoretical optimum, offering theoretical guidance for the design of verification-friendly architectures. As a general-purpose underlying encoding, the value of SART is independent of specific algorithms. To comprehensively evaluate its effectiveness, we first evaluate the abstraction-free SART encoding, and then integrate it with abstraction techniques to construct the complete verifier LayerABS and its incomplete variant Incomplete-LayerABS. Across benchmarks, our methods surpass state-of-the-art baselines, validating SART’s practical impact.
@article{paperbot3812,
title = {SART: Sign-Absolute Reformulation Theory for Binary Variable Reduction in Neural Network Verification},
author = {Jin Xu and Miaomiao Zhang and Bowen Du},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798237}
}