《TRAINING FOR FASTER ADVERSARIAL ROBUSTNESS VERIFICATION VIA INDUCING RELU STABILITY》論文分享報告
組員：楊根 黎君玉 張榮華
1 基礎知識
ReLU函數
線性整流函數（Rectified Linear Unit, ReLU），又稱修正線性單元，是一種人工神經網絡中常用的激活函數（activation function），通常指代以斜坡函數及其變種為代表的非線性函數。ReLU函數函數圖像如下所示。
對於進入神經元的來自上一層神經網絡的輸入向量 {\displaystyle x} x，使用線性整流激活函數的神經元會輸出
至下一層神經元或作為整個神經網絡的輸出（取決現神經元在網絡結構中所處位置。
sign（x）函數
sign（x），這是一個符號函數，用於把函數的符號析離出來，在數學和計算機運算中，其功能是取某個數的符號（正或負）：
當x>0，sign(x)=1;
當x=0，sign(x)=0;
當x<0， sign(x)=-1；
在通信中，sign(t)表示這樣一種信號：
當t≥0，sign(t)=1; 即從t=0時刻開始，信號的幅度均為1；
當t<0， sign(t)=-1；在t=0時刻之前，信號幅度均為-1
2問題描述
機器學習模型做出的預測通常很脆弱。容易受到對抗攻擊。驗證對所有攻擊是否都具有強大的抵抗力，驗證過程的速度很慢。
3 解決方案
目標：訓練不僅對對抗性擾動具有魯棒性的神經網絡，而且可以更容易地驗證其魯棒性。
在這項工作中，作者使用協同設計的原理來開發訓練技術，從而使模型既健壯又易於驗證。作者的技術依賴於改善網絡的兩個關鍵屬性：稀疏性和ReLU穩定性。具體來說，首先表明，在訓練過程中提高體重平衡的自然方法（如“ 1-正則化”）可以比目前的方法更快地得到驗證。之所以會加快速度，是因為通常來說，精確的驗證者受益於驗證任務表述中變量的減少。例如，對於依賴線性編程（LP）求解器的精確驗證器，稀疏權重矩陣意味着這些約束中的變量較少。然后，關注於ReLU網絡精確驗證的當前方法的主要速度瓶頸：需要精確驗證方法來“分支”，考慮每個ReLU的兩種可能情況（ReLU是活動的還是不活動的）。分支急劇增加了驗證的復雜性。因此，如果優化后的驗證者可以確定ReLU是穩定的，即對於輸入的任何擾動，ReLU將始終處於活動狀態或始終處於非活動狀態，則無需在ReLU上進行分支。這激發了本文提出的技術的關鍵目標：作者旨在通過最大化穩定ReLU的數量來最大程度地減少分支。將此目標稱為ReLU穩定性，並引入一種正則化技術來誘導它。能夠為MNIST和CIFAR10訓練重量稀疏和ReLU穩定的網絡，這些網絡可以被更快地驗證。具體來說，通過將誘發體重減輕的自然方法與強大的對抗訓練程序結合起來（參見Goodfellow等人（2015）），作者能夠訓練網絡，在這段時間內可以驗證近90％的輸入與以前的驗證技術相比，它很小。然后，通過添加用於誘導ReLU穩定性的正則化技術，作者可以訓練模型，使其能夠被驗證額外快4到13倍，同時又能保持MNIST的最新准確性。作者的技術對CIFAR模型的精確驗證顯示出類似的改進。特別是，對於∞范數約束的對手，作者實現了以下驗證速度和可證明的魯棒性結果：
4相關設計
三種訓練可驗證的網絡模型：
驗證網絡：
改善網絡的兩個關鍵屬性：稀疏性和ReLU穩定性。
稀疏性：自然正則化方法
ReLU穩定性：一種新的正則化方法
對於輸入的任何擾動，ReLU將始終處於活動狀態或始終處於非活動狀態，則無需在ReLU上進行分支。
旨在通過最大化穩定ReLU的數量來最大程度地減少分支。
4.1驗證網絡模型的魯棒性
具有ReLU非線性的k層全連接前饋DNN分類器4。可以將此類模型視為函數f（·，W，b），其中W和b代表每層的權重矩陣和偏差。對於輸入x，DNN的輸出f（x，W，b）定義為：
應用於其他p范數和更廣泛的擾動集。驗證網絡模型。對於帶有正確標簽y的輸入x，如果輸入x0使某個不正確標簽y的對數大於x0上的y的對數，則會造成分類錯誤。因此，我們可以將尋找對抗性擾動的任務表示為優化問題：
4.2重量稀疏性及其對驗證速度的影響
兩種自然的正則化方法：
l1-正則化和小權重修剪
4.3穩定性
驗證者面對的情況越多，必須考慮的分支就越多，從而導致驗證的復雜性呈指數增長。直觀地講，具有1000個ReLU的模型比僅有200個都需要分支的ReLU的模型更容易驗證。因此，如果在具有允許擾動集Adv（x）的輸入x上ReLU的數量使得被最大化。
計算出的上限和下限
如果，則可以分別用身份函數或零函數替換ReLU。
如果，則這些驗證者確定他們需要對該ReLU“分支”。
這里就是ReLU修剪
一個確切表示ReLU何時穩定的函數
不可微，近似：
Relu穩定性改進對可證明的對抗精度的影響
5實驗環境
在表3中。作者比較了它們的測試集准確性，PGD對抗性准確性（針對強大的40步PGD對抗性攻擊的魯棒性評估）和可證明的對抗性准確性。此外，為了表明作者的方法可以擴展到更大的體系結構，作者針對每個數據集和訓練並驗證了“ + RS（大）”網絡。在MNIST上可證明的對抗性泌尿激素的中間結果，比Wong等人的結果明顯要好。 （2018）對於較大的擾動= 0.3，並且可比較的= 0.1。在CIFAR10上，作者的方法不太有效，這也許表明，要使純魯棒的CIFAR分類器更穩定，必須使用更不穩定的ReLU。作者還遇到了許多實例，它們在CIFAR上達到了分配的120秒時間限制，尤其是對於ReLU穩定性較差的控制網絡。
6優缺點分析
- 使用協同設計的原理來開發強調驗證為目標的訓練方法，並且表明它們可以更快地驗證訓練后的模型。
- 證明自然正則化方法可以使確切的驗證問題變得更加易於處理。
- 提出了一種改善網絡ReLU穩定性的方法，並表明這種改進使驗證速度提高了4到13倍。
- 改善穩定性方法是通用的，它可以添加到任何訓練過程中，並且可以加快任何精確的驗證過程。