Semialgebraic Optimization for Lipschitz Constants of ReLU Networks

This paper is the first application of Lasserre’s moment-SOS hierarchy (exploiting sparsity) to verifying robustness of neural networks. Roughly speaking, the verification approaches can be divided into four categories: the SAT/SMT-based approaches represented by Katz Lab, the MILP-bsed approaches represented by VAS Group, the AI-based approaches represented by SRILAB, and the CROWN family represented by Zico Kolter, Luca Daniel and Cho-Jui Hsieh. All these previous works can be found in SoK which provides full benchmark results and state-of-the-art leaderboard on the certified robustness for deep neural networks. [bib, link, code]