paperbot · PL 论文追踪

全部论文 待读 收藏

P1 Provably Tightest Linear Approximation for Robustness Verification of Sigmoid-like Neural Networks

面向 Sigmoid 类神经网络鲁棒性验证的可证明最紧线性近似
ASE Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering2022匹配度 6/10 · 论文属于神经网络鲁棒性形式化验证,与“PL→AI 在机器学习系统中应用静态/形式化分析”有交集,且强调可证明紧致性定义与工程实现;但不涉及 Agentic/LLM、浮点程序分析或贝叶斯程序分析,也不是用 LLM/Agent 改进验证,因此不是研究方向核心。引用 12 inbox
Zhaodi Zhang, Yiting Wu, Si Liu, Jing Liu, Min Zhang
crossref: 2026-09-12

AI 速览

一句话:提出网络级紧致性统一定义,并设计两种可证明最紧的线性近似,显著提升 Sigmoid 类网络鲁棒性验证精度。

深度神经网络鲁棒性的形式化验证至关重要,而 Sigmoid 类激活函数的非线性使验证通常依赖过近似,带来精度损失。现有工作致力于寻找更紧的近似,但其紧致性定义多为启发式、缺乏理论基础,且仅在某些网络上占优。本文通过实证分析神经元级紧致性刻画后,提出网络级紧致性(network-wise tightness)作为统一定义,并指出其计算是复杂的非凸优化问题。作者从两个不同视角绕过该复杂度,设计了两种可证明最紧的线性近似方法。实验表明,所提方法优于现有技术:认证鲁棒下界最高提升 251.28%,在卷积网络上给出明显更精确的验证结果。

问题
Sigmoid 类激活函数的非线性迫使鲁棒性验证使用过近似,但现有紧致性定义是启发式的、缺乏理论支撑,导致验证精度不足。
方法
通过实证分析现有神经元级紧致性刻画,提出网络级紧致性作为统一定义,证明其计算为非凸优化问题,并从两个角度设计可证明最紧的线性近似以规避复杂度。
评估
在神经网络鲁棒性验证基准上与现有技术对比,认证下界最高提升 251.28%,并在卷积网络上获得更精确的验证结果。
原文摘要(Abstract)

The robustness of deep neural networks is crucial to modern AI-enabled systems and should be formally verified. Sigmoid-like neural networks have been adopted in a wide range of applications. Due to their non-linearity, Sigmoid-like activation functions are usually over-approximated for efficient verification, which inevitably introduces imprecision. Considerable efforts have been devoted to finding the so-called tighter approximations to obtain more precise verification results. However, existing tightness definitions are heuristic and lack theoretical foundations. We conduct a thorough empirical analysis of existing neuron-wise characterizations of tightness and reveal that they are superior only on specific neural networks. We then introduce the notion of network-wise tightness as a unified tightness definition and show that computing network-wise tightness is a complex non-convex optimization problem. We bypass the complexity from different perspectives via two efficient, provably tightest approximations. The results demonstrate the promising performance achievement of our approaches over state of the art: (i) achieving up to 251.28% improvement to certified lower robustness bounds; and (ii) exhibiting notably more precise verification results on convolutional networks.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@inproceedings{paperbot7306,
  title = {Provably Tightest Linear Approximation for Robustness Verification of Sigmoid-like Neural Networks},
  author = {Zhaodi Zhang and Yiting Wu and Si Liu and Jing Liu and Min Zhang},
  booktitle = {ASE},
  year = {2022},
  doi = {10.1145/3551349.3556907}
}