1 神經網絡有各種問題 ?

傳統的程序有各種各樣的問題，比如大家熟知的錯誤，漏洞，后門等等。我猜大家可能不難同意我們必須通過測試，分析甚至驗證來保證傳統程序的質量。

神經網絡實質上不過是一種相對特殊的 (基于 Tensorflow 或者 PyTorch 的 API 的) 程序。只是這類程序的架構、設計比較特殊而已。這類程序也有很多類似傳統程序的問題。我們可以說所有的傳統程序里的問題，基本上神經網絡都有。比如說傳統程序會出錯、有安全漏洞，神經網絡里也有。

關于神經網絡的問題，我給大家舉幾個例子。

第一個例子是神經網絡也容易出錯。神經網絡不像傳統程序是基于邏輯來做判斷然后出結果的，而是通過大量訓練來調整里面的參數然后基于這些參數做預測的。因為神經網絡通常很復雜（比如參數巨多），有些犄角旮旯的地方就訓練不到。結果就是很容易找到反例讓它出錯。

比如下圖所示的例子，有人（UC Berkerly 的一個團隊）研究發現在停車牌（STOP）上面噴點漆或者貼個紙條，自動駕駛車里基于神經網絡的路標識別系統就會識別出錯。比如上面的路標會被錯誤地識別成 “限速 45”。這當然是個安全攸關的問題，因為有這些有停車牌的地方需要停車是有原因的，一旦停車牌被錯誤識別，自動駕駛車就不會停車，從而可能造成事故。這個例子從傳統程序的角度看就是一個程序錯誤。

第二個例子是一個公平性的問題。下圖顯示的是美國某個警察局訓練的一個神經網絡的輸出。給定一個罪犯的犯罪記錄、罪犯的背景，如人種、年紀等等，這個神經網絡被用來預測一個罪犯會不會在 6 個月內再犯。如果預測說該罪犯再犯的幾率很大，那么當然警察們需要對他多加注意。研究發現這個神經網絡有很大的公平性的問題。比如，下圖中顯示的黑人，雖然她的犯罪記錄要比旁邊的白人少很多，但這個神經網絡就是預測她再犯的幾率大得多。實際上，只要是黑人，再犯的幾率就會被預測得很高。這樣當然不公平。當然你也可以說這不是個問題，因為歷史記錄就是黑人更容易犯罪。但我們想不想要這樣一個系統來作為我們行動的指導，從而加深偏見，這個至少值得考慮。就我們對公平的定義而言，我們可以說這個神經網絡不公平。傳統軟件當然也可能有公平性的問題，但不嚴重，因為除非你的程序邏輯愣是加了某些有偏見的判斷，要不然一般不會有問題。但神經網絡就不同了，這些偏見很可能悄悄地通過數據或者訓練過程被加進去了。

再比如傳統的程序會有后門，神經網絡里也有。當然傳統程序的后門不算是一個特別大的問題，因為傳統程序的后門基本就是在某種特定的情況下，觸發了一個特定的語句。比如在某個地方加一個特殊的 if-then-else。這種后門在有了代碼審查等一系列常規檢查以后，加起來還是挺難的。但是在神經網絡里加后門非常非常容易。為什么神經網絡的后門是個嚴重的問題？因為神經網絡大家都看不懂，所以里面的后門基本上很難被發現。后面我會具體講神經網絡的后門問題，包括怎么加和怎么防范。

再比如傳統程序會有敏感信息泄露的問題，神經網絡也是一樣。神經網絡的信息竊取相對更容易。你花費了很大力氣收集了大量數據訓練了一個模型，別人隨便就可以把模型偷走。比如他只要能提交一定數量的數據（比如幾千個），生成對應的預測。然后他自己就可以根據這些數據訓練一個模型，基本能做到和你的模型有差不多的準確率。

因為傳統軟件的各種各樣的問題，我們知道傳統程序必須做各種各樣的測試和分析。相對而言，神經網絡現在還處于一個剛起步的階段，大家主要還是在把能做的趕緊堆一塊，看看效果再說。還沒有真正的把那些安全相關的問題理清楚，繼而提出解決方案。所以這塊還是有很多研究可以做的。

2 如何保證神經網絡的質量？?

那么具體我們需要做什么呢？

我們可以從傳統軟件那邊吸取經驗。經過幾十年的發展，我們有一系列的方法來把控傳統軟件的質量。我大概把這些方法分成 4 類，即理論 、 工具 、 流程   和   標準 。

理論：理論的部分是指我們發明了各種各樣的基于邏輯的用來分析程序的理論，比如說 Hoare Logic，Type Theory，和 Temporal Logic 等等。正因為有了這些理論，我們可以發展各種程序分析技術（比如測試，驗證，以及靜態分析），并且討論它們的完備性或正確性。

工具：我們同時也開發了各種各樣的工具。比如說我們現在一整個行業提供各種各樣的軟件開發，測試以及分析的工具。甚至如果你對軟件的質量要求很高的話，我們也有可以做形式化驗證的各種工具，比如模型檢測器，理論證明器等等。

流程：當然我們同時也認識到這些理論和工具并不能完全消除傳統程序的問題，所以我們也發展了各種各樣的軟件開發的流程。這些流程是用來指導程序員在開發軟件的時候，需要做哪些事情怎樣交流等等，以幫助程序員盡量的減少各種各樣的軟件問題?，F在比較出名的是敏捷方法。

標準：最后我們還有各種各樣的標準來告訴軟件開發人員什么的軟件要達到什么的標準。比如這個程序只是個手機上的小游戲，那么你只要能達到一定的穩定性，能用就行。但如果這個程序是用來控制一個安全相關的系統的，比如說控制著一個發電站的系統，那么你就需要達到一個更高標準的安全性。那么你怎么達到一個更高的標準呢？這些標準就可以告訴你必須要用哪些方法哪類工具測試分析你的軟件等等。

以上這些東西當然不能完全把所有軟件的問題解決，但是至少我們可以把軟件的質量控制在一個比較可以接受的范圍。雖然時不時還是會有嚴重的軟件漏洞被發現，但至少正常情況下，一般都夠用了。

而就神經網絡這種特殊的程序而言，我們還欠缺保證神經網絡的質量理論、工具、流程和標準。或者一句話來說： 現在基本啥都沒有。

3 我們的研究 ?

我們最近開始了一個比較大的項目，想要把這些東西都填補上。比如關于神經網絡分析的理論，傳統的程序分析絕大多數是基于幾個基礎的概念，而這些基礎的概念在神經網絡要么缺失要么還有待完善。比如 其中一個很基礎的概念是因果關系 。傳統程序的因果關系是很明確的。比如說一個程序的結果出錯了，通過分析控制流和數據流，我就可以知道，哪些語句有可能影響我最后這個結果。這個控制流和數據流就是很明確的因果關系。但神經網絡中的因果關系就不是那么明確了。神經網絡里的大多數神經元都是到處相連的，那么理論上對于錯誤的結果，所有的神經元都是有責任的。如果所有的神經元都有責任，那我要怎么做錯誤定位和修復？

另一個基礎的概念是可解釋性。傳統程序的可解釋性一般不是個問題。因為傳統程序大多是人寫的，那么只要找幾個專家、有夠多的時間，我們是可以把它理解的。假如確實有個很難的錯誤要修復，那么我只要找專家來看，我們還是相信最后肯定可以看懂然后對癥下藥。而神經網絡大家一般認為可解釋性比較差，這讓很多事情變得很難辦。那么我們要研究怎么定義和提高神經網絡的可解釋性，并用它來解決上述神經網絡的問題。

另一個基礎的概念是抽象。傳統程序的開發以及分析都是基于各種各樣的抽象的技術。比如程序開發的時候我們有基于函數，類，包等等不同的結構化的抽象，程序分析的時候有抽象解釋等等方法。而神經網絡的本身并沒有很多結構化的抽象，同時如何對神經網絡做抽象來進行分析也才剛剛開始在發展。

同樣， 針對神經網絡的工具、流程和標準都還欠缺 。比如針對神經網絡的測試分析工具才開始發展，有多好用還不是很清楚。同樣的，大家都知道要有針對神經網絡的流程和標準，就我所知現在有好幾十家不同的公司、機構也在試著去提他們的標準，但目前為止還沒有一套大家公認比較好用的流程或者標準。

總而言之，我想說的是如果確實想要把神經網絡作為一個新型的編程方式，用它來取代很多傳統的程序的話，那么我們必須要把這幾個方面：理論、工具、流程和標準，都要慢慢地發展起來。我們這方面也慢慢積累了一些工作，比如公平性相關的工作   [1] [2] [3] [4] ，魯棒性相關的工作   [5] [6] [7] ，后門相關的工作   [8] ，抽象相關的工作   [9] [10]   等等。如果大家感興趣，歡迎討論合作。

4 神經網絡中的后門  ?

以上當然都是些比較高屋建瓴的討論，接下來我介紹一個具體分析神經網絡的的例子，神經網絡的后門問題。然后通過這個例子看我們是怎么用程序分析的一些技術和方法來解決這個問題。

剛才提到傳統程序里面可能有后門，但一般認為不是一個特別大的問題，因為傳統程序有可解釋性，后門相對比較容易通過代碼審查發現。但是神經網絡不一樣，神經網絡的問題在于人沒法理解它里面到底在做什么，結果就是在里面埋一個后門是很容易的事情。

我介紹兩個簡單的例子。第一個例子，假設你從第三方那兒拿到了一個神經網絡用來做路標識別。這個神經網絡里很容易就可以被埋上一個后門。比如任何路標，只要在這個路標上貼上這個特定的貼紙，那么這個神經網絡就會把這個標志識別成 “限速 60”。大家可以想象埋進這個后門相當容易，我只要在訓練集里加上幾十張貼有這個貼紙的路標，把它們統一標記為 “限速 60”。訓練完了以后這個神經網絡自然就有了這個后門。

再比如一個人臉識別的神經網絡，我們很容易就可以在里面埋一個后門：任何一個人只要帶了某一副特殊的眼鏡，就會被識別成另外一個特定的人。比如像下圖所示的例子，上面的某男戴了這幅眼鏡以后就被識別成下面的女演員。想象一下如果這個人臉識別的系統和自動支付是綁在一起的，就可能造成很大的問題。

針對這種神經網絡里的后門，已經有各種各樣的研究怎么解決這個問題，比如有測試的方法等等。我們想解決的是一個更難一些的問題：給定一個神經網絡，我怎么來保證里面不存在后門。這個工作還是比較有意思的，一是因為我們是第一個做這個的，二是因為這個問題比較難，就算是怎么定義這個問題本身都還不是特別清楚。

5 后門問題一  ?

解決問題的第一步也是最重要的一步是定義問題。我們針對這個問題有兩個不同的定義，我先從第一個相對簡單的問題開始。

問題一：假定你給我一個已經訓練好的神經網絡模型，一個目標預測，同時再告訴我這個后門是什么觸發的，比如是一個貼紙，你還得告訴我這個貼紙最大是多大。一般情況下，這個貼紙不應該太大，不然你把整張圖片替換成你想要的目標的圖片，那肯定不能算是后門了。最后你還要同時提供給我一些特定的圖片。我們的問題是怎么保證不存在一個后門攻擊可以 100% 的在這些圖片上成功。   為什么要提供這些圖片呢？你可以這么理解，對人臉識別系統來說，這些圖片是級別很低的人的照片，而目標預測是公司總裁，這樣我們的問題就是怎么證明不存在一個貼紙，貼到這些級別很低的人的照片上以后，這個人就被識別成總裁了。

具體我們是怎么解決這個問題的呢？我用一個特別簡單的例子來給大家解釋一下。假設說我們現在有兩個圖片，每個圖片里面只有兩個像素點。大家知道每個像素點都是 [0,255] 中的一個數字。比如說這兩個圖片是 [3,5] 和 [1,10]。再假設后門只能通過第一個像素點觸發。同時我現在有 0 和 1 兩種預測結果，而黑客想要的是 1。我們的問題就是： 存不存在一個值 x，把這兩個圖片變成 [x,5] 和 [x,10] 以后，這個神經網絡的預測都是 1？

我們解決這個問題的辦法簡單來說就是把它變成一個約束求解的問題。我們把這個神經網絡看成一個函數 N 的話，這個約束就是：

上面的約束里，第一個條件是 x 的值必須在合法范圍內，后面兩個約束是說這個神經網絡必須輸出 1。有了這個約束，只要我能把它解出來找到一個滿足條件的 x 的值，就說明存在一個滿足我們條件的后門。反過來，如果我證明這個約束無解，那么我就證明了不存在這么一個后門攻擊。

這個約束看起來還是挺簡單的。第一個條件就是一個簡單的線性不等式。下面兩個條件比較麻煩一點，因為它用到了代表神經網絡的函數 N。這個還是比較復雜的。

為了簡單起見，我們假設這個神經網絡是個 feed-forward 神經網絡。它可以有很多層，每一層的每一個神經元都是兩個函數，第一個是 weighted sum，第二個是一個 activation function。其中的 activation function 比較麻煩，因為它是非線性的。常用的 activation function 有 ReLU、SigMod、和 Tanh。也就是說我們把 N 展開以后，它就是一堆 weighted sum 和 activation function。這個 weighted sum 的部分不難，因為它就是個線性的約束。我們知道一堆線性的函數疊起來還是線性的。同時線性的約束一般認為還是比較容易解的?，F有的一些工業級的解線性約束的工具還是很好用的。

比較復雜的是這些非線性的 activation function。解非線性的函數基本上都比較難。比如說 ReLU，ReLU 寫成程序的話，實際就是 ReLU(x) = if (x>= 0) { x } else { 0 }   這樣一個簡單的函數。雖然這個程序很簡單，但是因為它不是線性的，就很麻煩。因為它有一個條件判斷，那么理論上你需要分別處理兩種情況。問題是一個神經網絡里面很可能有幾千甚至上億個神經元，如果每一個神經元你都要分析兩種情況的話，那么就有指數級的情況需要分析了。

那么我們怎么辦？

我們的辦法就是用程序分析里常用的抽象解釋的方法把這個非線性的 activation function 用線性的函數來近似。如下圖所示，我們可以用上下兩條線來近似中間藍色的 ReLU 函數。直觀的說，這個 ReLU 出來的結果，我們不知道它是什么結果，有可能是 0，也有可能是 x。但是我知道它肯定是在這兩條線范圍之內的，我只要用這兩條線把它包起來，那么我們可以保證你所有可能的結果，我都考慮到了。只要我們就可以保證不會漏掉任何情況，那么我們的驗證結果如果是不存在后門的話，我們是可以確實不存在的。

同樣的，我們也可以用線性的函數來近似其他的 activation function。一旦我把所有的 activation function 都用線性的近似了，那么整個約束就變成了線性的，這樣這個問題就基本解決了。因為線性的約束加上另外一個線性的，結果還是線性的。所以到最后我們就 把一個神經網絡抽象成了一個巨大的但是是線性的約束 。我們就可以用現有的解線性約束的工具直接求解了。比如說 Z3、還有一些工業級的工具，很容易就可以解出來了。當然也看這個神經網絡有多大，一般幾千個神經元的神經網絡問題不大。

這里有個小細節要注意。因為中間經過了抽象，如果我解出來一個解，這個解不一定真的可以觸發后門。因為我們抽象的時候把 activation function 的范圍變大了，這個解有可能是不滿足原來的約束的。比如說在上圖里面，一個真的解應該在這個藍線上面。但我們找到的解可能在旁邊的陰影的部分。當然這個問題不大，因為找到解以后我們測試一下看是不是真的有后門很容易。重要的是我保證如果我說沒有后門的話，肯定沒有后門。

6 后門問題二  ?

上面介紹的是問題一的解決方法。當然你可以說這個問題的設定有點嚴格。因為現實的后門攻擊就和神經網絡一樣，很少能做到 100% 成功率的。同時上面的設立里需要用戶提供一些特定的圖片，用戶可能不知道如何選擇這些圖片。下面我介紹我們解決的更實際些的一個后門問題。

問題二: 給定一個神經網絡、一個預測目標，同樣假設一個關于貼紙大小的約束，怎么證明不存在一個成功率至少是 Pr（比如說 80%）的后門攻擊？

上面的問題設定對后門的成功率有一定的要求。這個在實際中是有意義。因為如果后門的成功率很低，那么攻擊者就需要嘗試很多次，也就更容易被發現。

我們解決這個問題的方法是基于下面的推導。如果存在一個成功率至少是 Pr 的后門攻擊，那么在隨機抽取的 K 張圖片上存在一個成功率 100% 的后門攻擊的概率至少是：，也就是說在隨機抽取的 K 張圖片上不存在一個成功率 100% 的后門攻擊的概率最多是 。倒過來說，只要我們證明在隨機抽取的 K 張圖片上不存在一個成功率 100% 的后門攻擊的概率超過   ，我們就可以推出不存在一個成功率至少是 Pr 的后門攻擊。

那么我們怎么判斷在隨機抽取的 K 張圖片上不存在一個成功率 100% 的后門攻擊的概率是不是超過   呢？答案就是 統計假設檢驗 (hypothesis testing) 。簡單來說就是反復地隨機采樣，然后做一個概率分析。具體做法就是隨機選 K 張圖片，然后用剛才解決第一個問題的方法來判斷是不是存在一個成功率 100% 的后門攻擊。然后再選 K 張圖片再來判斷。

如果我連續試了比如說 1000 次，結論都是不存在對 K 張圖片成功率 100% 的后門，那么你可以直觀的想象在隨機抽取的 K 張圖片上不存在一個成功率 100% 的后門攻擊的概率已經很高了。就算其中有幾組 K 張圖片存在成功率 100% 的后門攻擊，只要不存在的次數夠多，我也一樣可以說明在隨機抽取的 K 張圖片上不存在一個成功率 100% 的后門攻擊的概率很高。當然具體多高是有算法可以算的，如果大家感興趣，我們用的是 SPRT 算法。這個算法主要就是告訴我們什么時候隨機的次數和結果可以讓我們證明在隨機抽取的 K 張圖片上不存在一個成功率 100% 的后門攻擊的概率超過 。具體的細節大家可以看   [8] 。

同樣的，我們解決第二個問題的方法里有個小細節很有意思。就是關于 K 的取值的問題，理論上我可以選擇任意 K，因為我們的算法證明里對 K 的取值并沒有什么要求。但實際操作上不是，比如說我可以把 K 選得特別小，比如 1。就是說我每次抽一張圖片，然后我去看在這一個圖片上能不能做個后門攻擊，也就是說存不存在一個貼紙貼在上面可以把它的預測改了。這個的結果很可能是存在。因為我們知道神經網絡不魯棒，對于單張圖片的這種所謂后門攻擊，實際就等同于惡意擾動（adversarial perturbation）。我們都知道惡意擾動一般隨便改幾個像素點，基本都能把預測改了。但如果是這樣的話，這個結果對我們來說沒有意義，因為每次抽取 K 張圖片都發現存在一個成功率 100% 的后門攻擊的話，我沒法得出我想要的結論。所以 K 不能選得太小。同時 K 也不能選太大，因為我們問題一的解決方法要求我們求解一個約束，而 K 越大的話，這個約束也復雜（因為這個約束要求該后門攻擊在每一張圖片上都成功）。你可以想象如果 K 是 100 萬的話，這個約束包括對 100 萬張圖片的約束，結果是我們求解不出來了。這樣當然我們也沒法得到任何結論。我們也沒有想到什么理論來解決這個問題。我們最后是通過實驗來確定了一個比較好用的 K 值，一般就是在 5 到 10 之間。

7 實驗結果  ?

我們把上面介紹的方法實現在我們的一個叫 Socrates 的神經網絡驗證平臺上了。

Socrates ： https://socrates4nn.github.io/

也用一些常見的比如在 MNIST 數據集上訓練的神經網絡做了一系列實驗。比如 MNIST 上訓練的識別數字的神經網絡，我們試著看是不是存在后門攻擊，比如說在任何數字上加一個小小的白色的方塊都可以讓它識別成 2。我們試的網絡大概有幾百到幾千的神經元，不算太大。好消息是絕大多數情況我們都可以驗證。

有個出乎意料的結果是我們發現有些神經網絡就算沒有被攻擊，也天然存在一些后門。比如下圖所示的幾個例子，雖然這個神經網絡我們沒有特意去埋后門，但是第一排的數字加上右側的小白方塊以后都被識別成了 2?？偟膩碚f，任何數據在這個位置加上這個小白塊以后都有 80% 的概率被識別成 2。至于為什么會有種現象，我這里賣個關子，就不展開討論了。

8 更多的難題  ?

上面說的是怎么解決兩個神經網絡后門攻擊的問題，具體的技術細節大家可以看   [8] 。 當然上面的兩個問題的設定相對都還是比較簡單，后續還有很多很多很多很好玩的問題 還 沒有解決，因為各種各樣有創意的后門攻擊還在不停的出現。 我舉個很簡單的例子，比如有一種后門攻擊是這樣的：黑客把訓練集里面所有的綠色的車挑出來，都標記成青蛙。那么你可以想象訓練出來的神經網絡自然而然就會把綠色的車識別成青蛙。這個叫做語義后門。因為知道這是個后門需要我們理解語義（也就是說車不應該是青蛙）。而從神經網絡的角度，一個神經網絡怎么知道綠色的車不應該是個青蛙呢？

你同時可以想見這種后門也是安全攸關的，比如說如果你的自動駕駛車把前面的綠車識別成了青蛙，那我就不確定會發生什么了。那我們怎么解決這種語義后門的問題呢？比如給我一個神經網絡，我怎么檢查里面是不是有這種語義后門？這個問題我們正在試圖解決。大家可以想想要怎么定義這個問題。

9 結語  ?

最后我想說的還是： "神經網絡是一種特殊的程序，而就神經網絡這種特殊的程序而言，我們還欠缺保證神經網絡的質量理論、工具、流程和標準。"

樂觀的講，其實神經網絡有這個各種各樣的問題也是好事，就像傳統軟件的問題造就了一整個軟件質量相關的產業， 相信很快大家也會看到一整個神經網絡質量相關的產業 。