Provably Tightest Linear Approximation for Robustness Verification of Sigmoid-like Neural NetworksVirtual
The robustness of deep neural networks is crucial to modern AI-enabled systems. Formal verification has been demonstrated effective in providing certified robustness guarantees. 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 a theoretical foundation. 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 experimental results demonstrate the promising performance achievement of our approaches over state of the art: (i) achieving up to 436.36% improvement to certified lower robustness bounds; and (ii) exhibiting notably more precise verification results on convolutional networks.
Wed 12 OctDisplayed time zone: Eastern Time (US & Canada) change
16:00 - 18:00 | Technical Session 19 - Formal Methods and Models IResearch Papers / Journal-first Papers / Tool Demonstrations at Ballroom C East Chair(s): Michalis Famelis Université de Montréal | ||
16:00 20mResearch paper | Automatic Comment Generation via Multi-Pass Deliberation Research Papers Fangwen Mu Institute of Software Chinese Academy of Sciences, Xiao Chen Institute of Software Chinese Academy of Sciences, Lin Shi ISCAS, Song Wang York University, Qing Wang Institute of Software at Chinese Academy of Sciences | ||
16:20 10mDemonstration | Building recommender systems for modelling languages with DroidVirtual Tool Demonstrations Lissette Almonte Universidad Autónoma de Madrid, Esther Guerra Universidad Autónoma de Madrid, Iván Cantador Universidad Autónoma de Madrid, Juan de Lara Autonomous University of Madrid Pre-print Media Attached | ||
16:30 10mDemonstration | RobSimVer: A Tool for RoboSim Modeling and AnalysisVirtual Tool Demonstrations Dehui Du East China Normal University, Ana Cavalcanti University of York, JihuiNie East China Normal University | ||
16:40 20mResearch paper | Provably Tightest Linear Approximation for Robustness Verification of Sigmoid-like Neural NetworksVirtual Research Papers Zhaodi Zhang East China Normal University, Yiting Wu East China Normal University, Si Liu ETH Zurich, Jing Liu East China Normal University, Min Zhang East China Normal University | ||
17:00 20mResearch paper | Efficient Synthesis of Method Call Sequences for Test Generation and Bounded VerificationVirtual Research Papers Yunfan Zhang Peking University, Ruidong Zhu Peking University, Yingfei Xiong Peking University, Tao Xie Peking University | ||
17:20 20mPaper | Demystifying Performance Regressions in String SolversVirtual Journal-first Papers Yao Zhang , Xiaofei Xie Singapore Management University, Singapore, Yi Li Nanyang Technological University, Yun Lin National University of Singapore, Sen Chen Tianjin University, Yang Liu Nanyang Technological University, Xiaohong Li TianJin University Link to publication DOI | ||
17:40 20mResearch paper | Detecting Semantic Code Clones by Building AST-based Markov Chains ModelVirtual Research Papers Yueming Wu Nanyang Technological University, Siyue Feng Huazhong University of Science and Technology, Deqing Zou Huazhong University of Science and Technology, Hai Jin Huazhong University of Science and Technology |