神經網絡驗證和測試技術研究綜述

李 舵，董超群，司品超，何 曼，劉錢超

1.戰略支援部隊信息工程大學，鄭州450001

2.江南計算技術研究所 軟件測評中心，江蘇 無錫214083

隨著大數據的產生和算力的提升，以神經網絡（Neural Network，NN）為代表的人工智能技術發展迅猛，并在圖像處理、文本分析、語音識別、自動駕駛等領域取得了突破性的進展。將人工智能技術集成到軟件中，或是開發基于人工智能技術的軟件應用正逐漸成為潮流和趨勢。人工智能軟件一般開發樣式為：首先根據任務構建模型，然后利用大量訓練數據訓練模型，接著在測試數據集上檢驗模型的性能，最后投入使用。這類軟件和傳統軟件相比，在實現機理和編碼樣式上有著本質的不同，導致如何有效保證人工智能軟件的質量成為一個難題。此外，人工智能技術在應用過程中也暴露了一些問題，引發人們對人工智能技術安全性、可靠性和可解釋性等方面的擔憂。

神經網絡是人工智能領域的重要研究方向。神經網絡是一種通過模仿動物神經網絡特征進行信息處理的算法數學模型，主要由輸入層、隱藏層、輸出層構成，每層由若干個神經元組成，上一層的神經元通過權重與下一層的神經元相連，整個網絡通過數據集訓練，不斷更新權重等參數，最終在一些具體任務上獲得較好的性能。典型的神經網絡有卷積神經網絡（Convolutional Neural Networks，CNN）和循環神經網絡（Recurrent Neural Networks，RNN），其中CNN 廣泛應用在圖像處理領域，而RNN 因其能夠較好地處理時間序列上的數據而廣泛應用于語音、文本處理等領域。近些年來，為了獲得更好的性能，神經網絡朝著深度神經網絡（Deep Neural Networks，DNN）和深度學習（Deep Learning，DL）的方向發展。然而，隨著神經網絡層數的增加，模型愈加復雜，可解釋性越差，神經網絡模型越接近于“黑盒”，其潛在的威脅和隱患就越難以發現。隨著神經網絡技術部署在自動駕駛系統、疾病預防與檢測系統、惡意軟件檢測系統等安全攸關領域，對神經網絡技術進行全面的檢驗，及時發現神經網絡技術存在的缺陷和隱患，進而保證神經網絡技術應用的質量就顯得更為重要。目前，針對神經網絡的驗證和測試的研究越來越多，這些研究圍繞如何有效驗證神經網絡屬性、如何有效測試和發現神經網絡存在的缺陷等問題進行積極探索，并取得了一定的進展。

已有一些研究人員對機器學習或神經網絡相關領域的測試評估工作進行了總結。文獻[1-3]主要分析了機器學習系統測試現狀和面臨的風險挑戰。Huang 等人[4]從評估深度神經網絡系統可信性、安全性出發，分別從驗證、測試、可對抗攻擊和防御、解釋性技術等方面介紹了針對DNN 系統驗證測試的進展。王贊等人[5]圍繞測試度量指標、測試輸入生成、測試預言、測試應用和評測數據集五方面對深度神經網絡測試近年來的研究成果進行了系統而深入的梳理，并對神經網絡測試未來的發展進行了展望。此外，曾春燕等人[6]從自解釋模型、特定模型解釋、不可知模型解釋和因果可解釋性四方面對DL模型可解釋性方法進行了總結分析。

圍繞神經網絡的驗證和測試技術，對已有的研究成果進行細致的梳理總結，從驗證技術、基于覆蓋的測試技術、基于對抗樣本的測試技術、融合傳統測試技術等多個角度剖析神經網絡驗證和測試技術研究現狀，為相關領域研究人員提供參考。文章組織結構如圖1所示。本文與上述相關綜述文獻有相似之處，但有以下三點不同：（1）側重從技術角度出發，分析當前神經網絡驗證和測試的主要技術。（2）對現有技術進行了較為詳細的歸納和分類，條理清晰。（3）既指出已有研究成果的貢獻，又指出當前工作存在的不足，從正反兩方面闡述神經網絡測試的研究進展，供讀者思考和參考。

圖1 文章組織結構Fig.1 Organization structure of this paper

1 神經網絡驗證和測試

本章對神經網絡驗證和測試中的一些基本概念進行介紹。

1.1 神經網絡

一個神經網絡可以表示為一個元組N=(L,C,Φ)。其中，L={Lk|k∈{1,2,…,K}} 代表一系列網絡層，C=L×L代表層與層之間的連接，Φ={Φk|k∈{2,3,…,K}}代表一系列函數。對于一個神經網絡N，L1代表輸入層，LK代表輸出層，其余代表隱藏層。網絡層Lk包含Nk個神經元，Lk層第m個神經元可表示為nk,m，值為uk,m。每一個神經元前一個網絡層中的每個神經元相連，并存在如下關系：

其中，wk-1,i,m代表第k-1 層中的神經元和nk,m的連接權重，bk,m為偏置。由于存在非線性激活函數，比如ReLU，則神經元激活值vk,m計算過程為：

如果將每一層計算過程用Φk表示，則對于輸入x，整個神經網絡從輸入到輸出可表示為f的函數：

將神經網絡符號化表示，可以是函數表示或編碼表示，在此基礎上進行推理和證明，一般是進行神經網絡驗證的必要準備。

1.2 神經網絡驗證技術和測試技術

神經網絡驗證技術是通過一定手段確定一個屬性（例如，給定輸入的局部魯棒性）是否在神經網絡上成立，如果成立，則能夠提供嚴格的數學證明，如果不成立，則要提供證明或是提出反例。很多場景下，由于神經網絡的高度復雜性，推導和準確計算出給定輸入的輸出值難以實現，這時候為了簡化計算，一般會引入一個誤差，從而確保計算過程能順利進行，前提條件是保證誤差最終能夠收斂。驗證問題通常具有很高的復雜度，神經網絡的高維度和非線性，使得神經網絡的驗證是NP難的[7]。神經網絡驗證一般在小規模網絡上進行，對大規模網絡進行驗證會面臨計算復雜度高、時間開銷大的問題。

神經網絡測試技術是通過一定方式生成測試用例，通過觀察輸出結果與預期結果之間的關系來檢查和發現神經網絡的缺陷，從而對神經網絡某方面的屬性或能力做出判斷。相比驗證技術，測試技術不需要提供嚴格的數學證明，計算成本相對較低，但在結果的可信度上不如驗證技術。測試技術一般需要以一定的測試指標為指導，傳統軟件測試通常以覆蓋率為指標指導測試用例生成，如代碼覆蓋、路徑覆蓋、MC/DC 等。由于神經網絡沒有明確的控制流和數據流，這些指標在神經網絡測試中并不適用。因此，神經網絡測試技術主要根據神經網絡的特點，圍繞指導測試用例生成、檢測神經網絡潛在缺陷、解決測試預言等問題展開研究。

1.3 神經網絡驗證和測試目的和方法

神經網絡的驗證和測試主要為了發現神經網絡潛在威脅或缺陷，客觀評價神經網絡的一些屬性，從而更好地保證神經網絡技術應用的質量。

魯棒性是神經網絡的一個重要屬性，神經網絡的魯棒性是指神經網絡在各種輸入攝動下表現出的穩定程度。神經網絡魯棒性可以分為全局魯棒性和局部魯棒性，局部魯棒性描述刻畫了神經網絡在一定輸入范圍、區域內的魯棒性，全局魯棒性則要考慮在所有輸入下的魯棒性。安全性是神經網絡另外一個重要屬性，安全性從神經網絡自身脆弱性和易受的外部攻擊出發，衡量神經網絡的抵抗內部和外部風險的能力。在某種程度上，安全性和魯棒性有相似之處。對抗樣本的存在使得神經網絡安全性面臨挑戰，對抗樣本是指通過蓄意構造細微的擾動，生成新的樣本，來欺騙神經網絡，對抗樣本問題廣泛存在于各種神經網絡中，成為威脅神經網絡技術應用的一個隱患。

在驗證方面，Lipschitz屬性常被用來衡量神經網絡魯棒性。Lipschitz的定義為：給定神經網絡及其函數f，輸入區域η?[0,1]n，對任意x1,x2∈η，在P范數下，如果存在一個常量L，使得恒成立，則稱L是Lipschitz 常量。Lipschitz 連續性一般用于刻畫神經網絡全局魯棒性。此外，一些研究則從神經網絡輸出可達性、區間屬性等角度對神經網絡屬性進行分析和驗證。在測試方面，針對如何生成有效的測試用例，一些學者從覆蓋指標出發，提出了適用于神經網絡的覆蓋指標；或者從對抗樣本角度入手，通過生成對抗樣本檢驗神經網絡的魯棒性和安全性；還有一些學者將傳統測試技術應用到神經網絡測試中，用于解決測試預言問題、檢測代碼缺陷等。

2 驗證技術

針對神經網絡樣本驗證技術的分類，Huang 等人[4]將DNN驗證技術分為約束求解、基于搜索的方法、全局優化和過度逼近四種方法，具有一定合理性，但是不夠全面，分類界限較為模糊。從是否能夠準確計算結果出發，將驗證技術分為精確求解和近似求解兩大類，每一類又進一步細化，對目前驗證技術進行詳細介紹。

2.1 精確求解

精確求解，就是對神經網絡的屬性進行全面、準確的驗證，能夠得出準確的結果。神經網絡驗證問題是一個NP 完全問題，因此精確求解會面臨組合爆炸的問題。考慮到約束求解器在求解大規模組合問題上的成功應用，一些學者嘗試將神經網絡的驗證問題轉換為約束問題，然后通過約束求解器進行求解，并且取得了不錯的效果。神經網絡驗證常用的求解器有可滿足性模理論（Satisfiability Modulo Theories，SMT）求解器、可滿足性（Satisfiability，SAT）求解器、混合整數線性規劃（Mixed Integer Linear Programming，MILP）求解器等。

2.1.1 SMT

Huang 等人[8]基于SMT 求解器提出了用于驗證前饋神經網絡（Feedforward Neural Network，FNN）安全性的自動化框架DLV（Deep Learning Verification）。該框架能夠保證神經網絡如果存在錯誤分類的行為，那么一定能夠被發現。該方法將輸入視為空間中一點，并指定鄰域作為搜索范圍，通過定義一系列的圖像操作，來對輸入圖像的鄰域進行全面的搜索。在此過程中，利用SMT 求解器來實現神經網絡進行逐層傳播分析算法，檢測神經網絡分類器存在的不安全行為。作者在MNIST、CIFAR-10、ImageNet 等數據集和相應的網絡上進行了實驗，發現該方法能夠檢測出比FGSM（Fast Gradient Sign Method）、JSMA（Jacobian Saliency Map Algorithm）等對抗樣本算法擾動更小的對抗樣本，證明了其檢驗神經網絡魯棒性的有效性。

Katz 等人[9]提出了用于驗證包含線性函數和ReLU激活函數的神經網絡特性的框架Reluplex。Reluplex是一種利用SMT 求解器對驗證問題進行按需拆分的方法。從賦值開始，Reluplex 始終保持對所有變量的賦值，即使這些變量違反了某些約束。它利用單純形法對約束中的線性約束進行求解，如果不存在解，則意味著反例搜索失敗。如果存在解，會出現兩種情況：一種情況是這個解滿足ReLU約束，生成一個反例；否則，將不滿足的ReLU 約束分為兩種情況進一步考慮。這是一種利用遞歸思想求解的方法，將問題不斷分解來尋找可滿足的解。作者在一個包含300個ReLU節點的網絡上進行實驗，證明該方法的有效性。

Ehlers[10]也提出了利用SMT 求解器驗證神經網絡的方法Planet。該方法引入了一種神經網絡的全局線性近似，作為一種邊界方法來過度逼近每個隱藏單元可能的值集。同時采用凸松弛的方法用線性約束去近似代替非線性約束，這樣就將約束問題轉化為線性規劃問題，并能夠保證提供比Reluplex 更緊的弛豫。此外，Planet 利用沖突分析來發現不能導致可滿足的分裂組合，從而允許它們對（子）問題進行進一步的修剪。

2.1.2 SAT

二值化神經網絡（Binarized Neural Network，BNN）的連接權重和激活值只有+1 和-1 兩種情況，比一般全精度網絡要簡單得多，一些學者對其進行布爾編碼，并將神經網絡驗證問題轉化為SAT問題進行求解。

Cheng 等人[11]將BNN 驗證問題歸結為組合電路驗證中的SAT問題，并利用SAT求解器進行求解。首先對BNN 進行編碼，主要將BNN 中的雙極域運算替換為布爾運算，然后為BNN驗證問題構造一個組合聯接器，并將組合聯接器編碼為相應的SAT問題。此外，作者還提出利用XNOR進行提取和利用因子分解技術對BNN驗證進行優化。最后作者通過在MNIST、German Traffic Sign兩個數據集上進行實驗，證明了所提方法的有效性。

Narodytska 等人[12-13]將BNN 進行布爾編碼，從布爾可滿足性的角度來分析BNN 的屬性。作者將BNN 分為內部塊和外部塊兩部分，首先對內部塊和外部塊分別進行布爾編碼，從而將神經網絡編碼為布爾公式。然后將內部塊和外部塊的每一層一步步從MILP 編碼、ILP編碼最后轉化為SAT 編碼。接著對神經網絡屬性進行編碼，結合神經網絡編碼，最終可得到一個SAT 公式組。作者結合反例引導搜索的思想，利用SAT求解器對上述SAT 公式進行求解。通過實驗比較了ILP、純SAT和所提方法在檢測對抗魯棒性上的性能，結果表明作者所提方法在證明神經網絡魯棒性方面要優于其他兩種方法。

2.1.3 MILP

Lomuscio等人[14]將ReLU函數的約束編碼為MILP，結合線性規劃表示的輸出規范，輸出集的驗證問題最終變成MILP 的可達性問題，并從結果可達性角度對神經網絡的屬性做出判斷。對于神經網絡第i層，MILP 編碼為：

其中M是一個“足夠大”的常數。通過這種編碼，可以將可達性分析簡化為求解一個定義在這些約束上的線性規劃問題。最后作者在MNIST數據集上驗證了該方法的可行性。

Bunel等人[15-16]將分支定界的思想引入到MILP問題的求解中。該方法將MILP 的輸入域不斷地拆分成子域，同時在子域上計算最小值的上下限，通過子域最小值的上下限來跟蹤計算全局最小值的界限。當全局最小值的上界與下界相差小于一定標量時，就認為收斂。在分支的過程中，還可以引入啟發式求解算法，加快求解。在實驗中，作者將BlackBox、Reluplex、Planet、MIPplanet等方法和所提方法BaB、BaBSB 進行對比，結果發現無論是小規模網絡還是大規模網絡，所提方法在發現錯誤的效率上都要優于其他方法。

但是，簡單地使用MILP 來驗證神經網絡或計算輸出范圍的效率并不高，因此一些工作就研究如何加速求解過程。Cheng等人[17]利用啟發式算法加速MILP求解過程，同時嘗試利用并行化的方法進行加速。Dutta 等人[18]交替使用局部搜索和全局搜索來有效計算輸出范圍。其中在局部搜索階段，使用梯度下降法尋找局部最大值（或最小值），而在全局搜索階段，使用MILP對問題進行編碼，以檢查局部最大值（或最小值）是否為全局輸出范圍。Tjeng 等人[19]提出了一種基于MILP 的方法驗證分段線性神經網絡的屬性。將非線性的公式和預求解算法相結合，最大限度減少MILP 問題中的二元變量的數量，改善數值條件，能夠比單純使用MILP快幾個數量級。

精確求解驗證將神經網絡的屬性驗證轉化為約束求解問題，并應用求解器進行求解。這種方法雖然能夠全面準確驗證神經網絡的屬性，但是也存在計算復雜度高，難以推廣到大規模網絡上等問題。在神經網絡規模越來越大的今天，采用精確求解的驗證技術去驗證神經網絡具有很大的局限性。

2.2 近似求解

一些學者認為，精確求解的方法將神經網絡驗證問題考慮得過于全面，導致問題復雜度過高，時間開銷過大，可以適當地將驗證問題簡化，采用近似的方法進行求解。近似求解驗證技術主要可以分為抽象解釋、線性松弛、半定規劃或對偶等方法。

2.2.1 抽象解釋

抽象解釋的方法是基于Cousot 等人[20]提出的程序分析構造和逼近程序理論。該理論的基本思想是在處理復雜的計算問題或模型時，通過對問題進行近似抽象，取出其中的關鍵部分進行分析，從而減少問題的復雜程度。神經網絡的輸入輸出空間可以視為一個具體域C，因為C空間過于龐大，難以直接計算，所以選擇一個相對簡單的域A作為抽象域，它過度逼近C中變量的范圍和關系，那么神經網絡在C上的一些屬性就可以在A上計算和研究。在抽象解釋中，選擇合適的抽象域很重要，它決定了抽象解釋的效率和精度。驗證神經網絡比較常用的抽象域有區間抽象域（Interval Domain）、Zonotope 抽象域（Zonotope Domain）和多面體抽象域（Polytope Domain）。

Gehr 等人[21]利用抽象解釋的方法開發了端到端的驗證工具AI2。AI2選擇Zonotope作為抽象域，并證明了該抽象域比區間抽象域精度更高。為了便于把神經網絡驗證問題轉換成抽象解釋的表示，作者首先將神經網絡表示為條件仿射變換（Conditional Affine Transformations，CAT）的組合；然后通過定義一定的抽象轉換函數來捕獲全連接和卷積神經網絡的行為；最后計算抽象輸出以檢查神經網絡的行為。與此同時，作者提出了一個有界powerset域，用于在精度和可擴展性之間進行權衡。通過在20個網絡上的實驗評估表明，AI2不僅能夠有效證明神經網絡的某些屬性（例如魯棒性），在速度和精度上也明顯優于其他分析器。

Singh等人[22]提出快速高效證明神經網絡魯棒性的方法DeepZ。作者為ReLU、sigmod、tanh 等激活函數設計新的逐點Zontope 抽象轉換器，抽象轉換器能夠最小化Zonotope 到二維輸入輸出平面的投影，支持浮點運算，并適用于前饋網絡、卷積網絡、殘差網絡等不同類型的網絡。作者通過實驗證明了該方法能夠有效驗證神經網絡的局部魯棒性。

此外，Singh 等人[23]為了解決驗證神經網絡可拓展性和精度方面的挑戰，基于抽象解釋提出了DeepPoly。該方法將浮點Polytope 和Interval 相結合，并且針對激活函數和Maxpool 算子的特性而專門定制了抽象變換器，這些抽象轉換器能夠很好地處理前饋網絡和卷積網絡，另外還支持浮點運算，因此在可擴展性和精度上都有所提高。Mirman等人[24]提出一種基于抽象解釋訓練神經網絡的方法。該方法使用定義在Zonotope 域的抽象轉換器，可用于計算微分和梯度下降，提高了神經網絡魯棒性的可證明性。Li 等人[25]將一種新的符號傳播技術運用到抽象解釋中，將神經元的激活值以符號形式表示，在抽象域上對從輸入層到輸出層的傳播過程進行分析。利用表達式象征性地表示每個神經元激活如何由前幾層的神經元激活值決定，這樣就比僅簡單地使用抽象解釋獲得更高的精度。

2.2.2 過度逼近

Weng等人[26]分析了ReLU網絡的區間屬性和Lipschitz連續屬性，提出了兩種算法Fast-Lin和Fast-Lip。該方法采用逐層計算邊界的思路，其中Fast-Lin用于對神經網絡中的ReLU 單元進行線性逼近，Fast-Lip 采用梯度對Lipschitz常數進行逼近。作者通過實驗證明，在獲得相似精度的求解中，他們所提的算法比基于線性規劃的方法更快。

Zhang等人[27]受到Weng工作的啟發，提出了一種基于過度逼近的驗證框架CROWN。對于ReLU、sigmod等激活函數，采用線性或者二次函數進行逼近，從而能夠有效地計算神經網絡給定數據點的最小失真認證下界。在時間復雜度上，與Reluplex等需要指數級時間的方法相比，該方法能夠在多項式時間內求解，與此同時，該方法比Fast-Lin和Fast-Lip有更好的性能表現。

Boopathy 等人[28]提出了針對CNN 魯棒性的驗證框架CNN-Cert。該框架將線性邊界技術應用到非線性函數（例如非線性激活函數、殘差塊和池化操作等）的操作中。首先將每個非線性函數視作一個構建塊，計算出每個構建塊上界和下界；然后將計算出的上下邊界插入到網絡中并反向傳播到上一層。那么整個網絡就可以看作一個個級聯的構建塊，網絡輸出的上限和下限以及輸入的上限和下限就有一定的線性關系。作者通過實驗證明了該方法在時間和性能上優于Fast-Lin和CROWN等方法。

2.2.3 對偶或半定規劃

Dvijotham等人[29]將神經網絡驗證問題轉為優化問題，并利用問題的對偶進行求解。主要思想是將神經網絡在多種約束條件下的輸出表示為拉格朗日松弛，那么原來目標函數和約束條件在每一層都是可分離的，因此支持獨立優化每一層中的變量。通過構造對偶優化問題，采用梯度方法就可以獲得驗證目標的嚴格界限。Wong等人[30]認為，直接考慮通過線性規劃方法對含ReLU的網絡進行驗證求解是不可行的，而從線性規劃的對偶問題出發，任何可行對偶解都提供了原始解的有保證的下界。沿著這一思路出發，在激活函數邊界計算中，通過對偶函數可以計算每一層輸出的上下界，并通過層層傳導，最后可以計算整個輸出的邊界。

Raghunathan 等人[31]針對神經網絡魯棒性證明，提出了一種基于半定規劃的凸優化松弛算法。這種方法使用線性規劃和二次約束代替優化問題的非線性ReLU約束，將其轉化為二次約束二次規劃，并進一步放寬到一個半定規劃。該方法能聯合解釋中間激活，并捕獲線性規劃松弛所不能捕獲的相互作用，比基于線性規劃松弛算法更加嚴謹。在Raghunathan工作基礎上，Richard等人[32]利用幾何技術來分析半定規劃的緊致性。將對抗性攻擊問題的最小二乘約束分解為一系列的投影問題，其中最后一個問題將一個點投影到一個非凸雙曲線上（高維雙曲線），那么當且僅當該投影位于雙曲線的長軸上時，半定松弛是緊致的。

2.2.4 其他技術

Lipschitz常量常用于評估神經網絡模型的魯棒性，一些研究圍繞計算Lipschitz常量展開。

Hein等人[33]認為計算DL模型全局Lipschitz上限來評價模型的魯棒性過于粗糙，提出通過計算DL 模型的全局Lipschitz下界來評估模型的魯棒性，并提出了通過正則化優化函數Cross-Lipschitz 來計算這個下限，但是該方法僅適用于連續可微的神經網絡。受Hein工作的啟發，Weng等人[34]基于極值理論，提出了新的魯棒性指標CLEVER。該方法將極值理論應用到ReLU 激活函數中，把DL 魯棒性分析轉換為局部Lipschitz 常數估計。雖然CLEVER能夠較好地反映DL的魯棒性，但也存在計算復雜度高的問題。Wu 等人[35]研究了DL 逐點穩健性的兩個變體，即最大安全半徑問題和特征魯棒性問題，旨在量化單個特征在對抗性擾動方面的魯棒性。在Lipschitz連續性假設下，可以將優化問題轉化為兩人回合制游戲問題，并在游戲中引入博弈思想，那么最大安全半徑和特征魯棒性的上下界可以用兩人游戲的上下界代替。計算邊界過程中，采用蒙特卡洛算法計算兩人游戲的上界，利用A*算法和Alpha-Beta 剪枝算法計算兩人游戲的下界。

此外，Ruan等人[36]專注于L0范數，并研究量化DNN的全局魯棒性問題，將全局魯棒性定義為對測試數據集的最大安全半徑的期望。他們提出了一種迭代生成網絡魯棒性下限和上限的方法，該方法可以隨時返回中間結果，并采用逐漸嚴格約束的方式修改上下界限。此外，數值采用張量存儲的方式能夠支持并行化計算，加速求解。作者還證明了該方法可以在有限時間內收斂到最優值。

此外，也有一些學者[37-38]嘗試將精確求解和近似求解的方法相結合，從而在精度和時間上獲得平衡。

神經網絡驗證技術總結如表1所示。

表1 神經網絡驗證技術總結Table 1 Summary of neural network verification technology

驗證技術能夠對神經網絡屬性進行嚴格的證明，為神經網絡技術應用特別是在安全攸關領域的應用提供了保證。精確求解驗證將神經網絡驗證問題轉化為約束求解問題，利用求解器進行求解，從而為神經網絡提供全面嚴格的驗證，具有精度高、可信度高的特點，但是由于求解問題的復雜度往往很大，很難應用到大規模網絡上。此外，精確求解在不同網絡之間的通用性也存在不足，像SAT求解僅適用于BNN網絡，SMT則大多適用于前饋神經網絡。近似求解驗證，借助抽象模型、過度逼近、對偶等方法，在犧牲一定精度的前提下，將復雜問題進行簡化，實現對問題的快速求解。近似求解驗證技術能夠應用到大規模網絡上，并且對不同類型的網絡都有一定的適用性。精確求解和近似求解的精度和適用網絡規模的關系如圖2所示。此外，精確求解和近似求解相結合的方法，能夠平衡精度和時間兩者關系，并表現出較好的性能，是一個值得研究的方向。

圖2 驗證技術精度和網絡規模之間的關系Fig.2 Relationship between accuracy and network size of verification technology

3 基于覆蓋的測試技術

傳統軟件測試中，測試覆蓋率是衡量軟件測試充分性的一個重要指標，能夠幫助人們客觀認識軟件質量，改進測試工作。比較典型的覆蓋指標有代碼覆蓋、路徑覆蓋、MC/DC。由于在開發和編程樣式上與傳統軟件有著本質的不同，這些覆蓋指標很難直接用在基于神經網絡開發的程序或軟件上，一些學者開始嘗試研究適用于神經網絡的覆蓋指標。

基于覆蓋的測試技術一般流程如圖3 所示。首先以隨機測試輸入為測試用例，以一定的覆蓋指標為指導，在神經網絡上測試這些用例，并獲得相關覆蓋報告；然后對測試用例進行篩選，選擇具有高覆蓋率的測試用例作為最終測試用例；最后對未被篩選的測試用例，采用一定的策略提高它們的覆蓋率，并作為新的測試用例，進入下一輪測試用例的測試和篩選中。其中提高測試用例覆蓋率的策略一般采用啟發式搜索算法。

圖3 基于覆蓋的測試技術一般流程Fig.3 General flow of testing technology based on coverage

3.1 神經元覆蓋

Pei等人[39]首次提出了神經元覆蓋（Neuron Coverage，NC）指標，通過觀察和計算神經網絡中各神經元的激活情況來指導測試。設神經元n的輸出值為V(n)，同時設置一個閾值k，如果V(n)＞k，則認為該神經元被激活；否則沒被激活。則有，其中N表示神經網絡中激活神經元的數量，Nall表示神經網絡中神經元總量。作者還提出了用于測試神經網絡的白盒測試框架DeepXplore，以NC作為指標指導測試輸入生成，結合差分測試的思想，最大程度檢測神經網絡存在的異常行為。最后在MNIST、ImageNet、Driving、Contagio、Drebin等數據集和多種網絡上進行了廣泛的實驗，結果證明了DeepXplore 在發現神經網絡異常行為方面的有效性。Tian等人[40]基于NC測試指標提出了測試自動駕駛車輛的碰撞檢測工具DeepTest。DeepTest 通過模擬現實世界中駕駛環境的變化，如下雨、起霧、光照條件，對圖像進行變換，利用貪婪搜索的技術來生成神經元覆蓋率最大化的測試輸入，以檢測神經網絡在上述條件下的錯誤行為。

3.2 MC/DC變體

Sun 等人[41]認為神經元覆蓋指標過于粗糙，并不能有效測試DNN，受到MC/DC 覆蓋準則的啟發，提出了基于符號變化、值變化的四種覆蓋指標：符號-符號覆蓋（Sign-Sign Coverage，SSC）、值-符號覆蓋（Value-Sign Coverage，VSC）、符號-值覆蓋（Sign-Value Coverage，SVC）和值-值覆蓋（Value-Value Coverage，VVC）。通過上述四個覆蓋準則引導測試輸入生成，捕獲DNN 中的錯誤行為。同時，測試用例的生成融合了符號方法和啟發式搜索算法，能夠達到加速測試用例生成的效果。最后通過MNIST、CIFAR-10、ImageNet 的實驗，證明了該方法在檢測神經網絡缺陷上的有效性。

3.3 拓展神經元覆蓋

Ma等人[42]拓展了NC思想，在DeepGauge中引入了三個新的神經元級覆蓋指標和兩個層級覆蓋指標。神經元級覆蓋指標包括k多節神經元覆蓋（k-Multisection Neuron Coverage，KMNC）、神經元邊界覆蓋（Neuron Boundary Coverage，NBC）和強神經元激活覆蓋（Strong Neuron Activation Coverage，SNAC）；層級覆蓋包括Top-k神經元覆蓋（Top-kNeuron Coverage，TKNC）和Top-k神經元模式（Top-kNeuron Patterns，TKNP）。作者希望通過最大程度刻畫神經元、網絡層等不同層面的狀態變化，來發現網絡存在的異常行為。最后在MNIST、ImageNet上進行實驗，證明了這些覆蓋指標能夠有效捕獲包括對抗樣本在內的異常輸入，與DeepXplore 相比，能夠在更細粒度的層次上捕獲神經網絡的異常行為。此外，Ma 等人[43]將組合測試的方法應用到神經網絡測試中，提出了指導測試輸入生成的方法DeepCT。引入t-路組合稀疏覆蓋（t-Way Combination Sparse Coverage，TWCSC）和t-路組合稠密覆蓋（t-Way Combination Dense Coverage，TWCDC）兩個指標，充分考慮同一層神經元的各種狀態組合，來分析神經網絡的局部魯棒性。作者通過實驗證明，以這兩個指標引導測試輸入生成，能夠在使用較少測試用例的情況下，獲得令人滿意的缺陷檢測能力。

Lee等人[44]結合覆蓋指標和自適應的神經元選擇策略提出了神經網絡白盒測試框架Adapt。該框架采用NC和TKNC作為覆蓋指標，并定義了神經元矩陣和29種神經元特征，通過參數化神經元選擇策略和學習方式獲得適當參數。實驗表明，該方法在提高覆蓋率和發現對抗輸入方面比現有的白盒和灰盒技術更有效。

Xie等人[45]提出了一種覆蓋指標引導的模糊測試框架DeepHunter。該框架將NC、KMNC、NBC、SNAC、TKNC這五種覆蓋指標作為度量標準，在測試輸入生成的過程中，采用變異測試方法，以四種種子選擇策略生成變異體，然后利用覆蓋指標的反饋指導測試輸入生成，用于檢測神經神經網絡系統的潛在缺陷。實驗結果證明，該框架在覆蓋范圍、缺陷檢測數量和多樣性方面要優于同一時期的其他方法。

3.4 意外覆蓋

Kim等人[46]認為現有的神經元覆蓋指標粒度較粗，并不能描述神經網絡所表現出的細微行為，于是提出了神經網絡充分性測試框架SADL（Surprise Adequacy for Deep Learning Systems）。在框架中，引入了意外充分性（Surprise Adequacy，SA）的概念，用于衡量輸入分布和訓練數據的分布差距，并基于此提出了意外覆蓋（Surprise Coverage，SC）指標。SADL 首先衡量單個測量輸入相對于訓練數據的SA，然后利用單個測試輸入的意外程度去衡量整個測試輸入的SA，在此過程中采用核密度估計和基于歐式距離兩種方法計算SC。作者通過廣泛的實驗證明了SADL 能夠準確地捕獲異常輸入，并指導神經網絡的訓練。

3.5 路徑覆蓋

Wang等人[47]認為傳統測試中的控制流和數據流對神經網絡來說沒有實際意義，提出了一種基于路徑覆蓋的測試方法DeepPath。為了評估DNN 測試的充分性，對神經元傳播路徑進行了研究，并定義了l長度強激活路徑覆蓋（l-length Strong Activated Path coverage，l-SAP）、l長度輸出激活路徑覆蓋（l-length Output Activated Path coverage，l-OAP）和l-長度全狀態路徑覆蓋（l-length Full State Path coverage，l-FSP）三種覆蓋指標，用于指導測試輸入生成。最后在MNIST 上進行實驗，證明了該方法能夠更好地識別對抗樣本和評估模型的魯棒性。

此外，文獻[48-50]分別從神經元激活概率和偏差、狀態級別和轉換級別、數據集定量投影等角度提出了覆蓋指標，用于測試神經網絡的充分性。基于覆蓋的測試技術總結如表2所示。

表2 基于覆蓋的測試技術總結Table 2 Summary of testing technology based on coverage

以上覆蓋指標都力圖從神經網絡結構的某個角度刻畫神經網絡的行為，指導神經網絡測試。從覆蓋粒度層面來說，NC、SSC、DSC、SVC、DVC 等覆蓋指標從單個神經元符號或值出發，描述神經網絡可能的狀態和行為空間；KMNC、NBC、SNAC、SC 將單個神經元的狀態刻畫進一步細化，產生的狀態空間也就越大，能夠發現神經網絡更細微的行為差異；TWCSC、TWCDC 則考慮同一網絡層不同神經元之間的狀態組合，l-SAP、l-OAP、l-FSP 考慮不同網絡層之間神經元的傳播路徑；TKNC、TKNP 從網絡層級定義覆蓋指標，粒度較粗，但提供了神經網絡行為的宏觀視角，可配合更細粒度的覆蓋指標使用。通過整理總結文獻中的實驗結果，對各個覆蓋指標的有效性進行了對比。圖4 給出了各種覆蓋指標在檢測異常輸入上的能力對比，其中連線表示二者存在比較關系，箭頭指向在能力更強的覆蓋指標。可以看出，覆蓋指標的粒度越細，分析神經網絡行為的能力就越強，越容易發現細微擾動的異常輸入。

圖4 各種覆蓋指標有效性對比Fig.4 Comparison of effectiveness of various coverage indicators

目前，針對神經網絡的測試技術尚處于探索階段，一些學者認為，上述方法雖然在發現異常輸入和指導測試用例生成上起到一定的作用，但是覆蓋指標和神經網絡安全性、魯棒性的相關性非常有限，因此出現了一些質疑的文章[50-54]。Yan 等人[54]認為目前的神經網絡覆蓋標準和模型質量沒有很強的相關性，同時在指導測試輸入生成上和生成對抗樣本的方法具有相似性，一些覆蓋標準僅需數十個測試用例就可以達到100%的覆蓋，難以獲得更多關于缺陷的信息。作者通過對DeepXplore、DeepGauge、DeepHunter、SADL 等方法展開實驗，證明了這些覆蓋指標與模型魯棒性之間沒有很強的相關性。

4 基于對抗樣本的測試技術

Szegedy等人[55]發現，通過圖片添加細微的、人眼不易識別的擾動，能夠使神經網絡圖像分類識別錯誤。對抗樣本的概念由此產生，并逐漸成為研究的熱點問題，許多學者將對抗樣本問題歸結于神經網絡分類器的魯棒性存在問題，并研究各種生成對抗樣本算法，用于評估神經網絡模型的魯棒性。對抗樣本算法依據生成方式可以分為白盒方式和黑盒方試，依據攻擊是否定向可以分為有目標攻擊和無目標攻擊。本文將從白盒和黑盒的角度對基于對抗樣本的測試技術進行介紹。

基于對抗樣本的測試技術的一般流程如圖5所示：對初始測試輸入，分別采用白盒方式和黑盒方式的對抗樣本算法生成對抗性測試輸入，然后將初始測試輸入、對抗性測試輸入交給神經網絡進行測試，根據測試結果對神經網絡模型魯棒性進行評估。

圖5 基于對抗樣本的測試技術一般流程Fig.5 General flow of testing technology based on adversarial samples

4.1 白盒方式

白盒方式生成對抗樣本技術主要圍繞神經網絡的梯度展開攻擊，針對像素添加擾動生成對抗樣本。白盒方式需要神經網絡內部結構、參數的信息，在一些梯度隱藏或遮蓋、模型內部參數不可知場景下往往會失效。

GoodFellow 等人[56]提出了一種基于梯度攻擊的方法FGSM。FGSM可以表示為：

其中，x為輸入圖片，y為圖片標簽，?用于限制擾動大小，J是損失函數，θ是模型參數。該方法通過損失函數的梯度來決定圖片像素變化的方向，將所有像素等比例地放大或縮小，一步就可以生成對抗樣本。其中?越大，生成對抗樣本的成功率就越高，但也越容易被察覺。Kurakin等人[57]提出了基于FGSM 改進的迭代算法I-FGSM。該方法通過小步迭代的方式逐步增大損失函數，能夠生成比FGSM更有效的對抗樣本。

Dong 等人[58]在FGSM 和I-FGSM 的基礎上提出了一種基于動量迭代的方法MI-FGSM。動量的方法能夠在損失函數的梯度上累計速度向量，從而達到加速梯度下降的目的。在擾動中使用動量的方法，能夠幫助穩定擾動更新方向和逃逸局部極值，提高對抗樣本的成功率。實驗表明，MI-FGSM攻擊能力比FGSM和I-FGSM更強大，同時擁有更好的遷移性。

Papernot等人[59]提出了一種基于神經網絡前向導數的方法JSMA。首先依據前向導數，給輸入的每個維度分配一個顯著值，顯著值能夠體現該維度對輸出概率的靈敏度，進而整張圖像就可以生成一張雅可比顯著圖；然后通過雅可比顯著圖來捕捉神經網絡預測最敏感的特征，從而有選擇性地對圖像的某些像素進行修改。JSMA對顯著像素點的尋找采用貪婪搜索，通常生成對抗樣本時間比FGSM要長，但是擾動相對較小。

Moosavidezfooli 等人[60]提出了一種迭代算法Deep-Fool，用于生成最小化范數擾動的對抗樣本。DeepFool從分類超平面的角度分析如何將一張圖像分類錯誤，這種情況下，圖像到分類超平面的距離就是代價最小的地方，然后通過迭代方法生成擾動，每一步將分類邊界內的像素修改到邊界外，直至分類器分類錯誤為止。通過在8個分類器和3個數據集上的實驗證明了該方法可以高效地生成對抗樣本，并作為模型魯棒性的評價指標。

Carlini 等人[61]提出了基于優化的對抗樣本生成方法C&W，用于評估模型的魯棒性。該方法將發現一個對抗樣本歸結為一個約束優化問題，即：

通過引入一個新的優化變量避免盒約束，并使用梯度下降法求解該優化問題，作者分別提出了適用于L0、L2、L∞三種不同范數攻擊方式，能夠在較小擾動下找到對抗樣本。在MINIST、CIFAR-10和ImageNet上的實驗表明，該方法優于同一時期的其他方法，且在不同網絡上具有很強的適用性，可以作為廣泛評價神經網絡模型魯棒性的指標。

4.2 黑盒方式

黑盒方式生成對抗樣本的技術不需要模型結構、參數等信息，通用性更強，但是在生成對抗樣本的質量和效率上往往不如白盒方式。

Papernot 等人[62]認為，一般的白盒方式生成對抗樣本需要DNN結構、參數等信息，這些信息在現實中很難直接獲得，不具有普遍適用性，因此提出了通過構造替代模型來生成對抗樣本。首先根據常識選擇模型的大體結構，并偽造訓練數據；然后通過受攻擊模型獲取標簽等信息，再偽造測試數據；最后在替代模型上訓練和測試數據集，獲取其中的參數。作者對Amazon和Google多個托管模型展開實驗，生成對抗樣本欺騙成功率分別為96.19%和88.94%，證明了該方法具有普遍適用性。

Narodytska等人[63]采用一種損失函數梯度近似的方式來構造對抗樣本，并基于貪婪局部搜索生成對抗樣本。在每一輪的迭代搜索過程中，該方法首先通過一個局部鄰域來重新定義當前圖像，并根據網絡輸出優化目標函數；然后采用局部搜索的方式，改變圖像中的幾個像素值，觀察輸出的變化，進而生成當前圖像損失函數梯度的近似；最后便可以利用近似梯度生成對抗樣本。作者通過在ImageNet 的實驗證明，平均只需0.5%的像素擾動就可以達到欺騙成功的目的。

Su 等人[64]提出了一種通過修改像素值生成對抗樣本的方法One-Pixel，通過在少數幾個像素上修改像素值，達到欺騙分類器的目的。該方法的關鍵在于找到整張圖片中對分類器做出判斷影響最大的幾個像素點。作者采用一種差分進化算法來搜索這些像素點，并對像素點做任意強度的修改，來生成對抗樣本。雖然該方法生成的對抗樣本不易被察覺，但是往往時間較長，且成功率不高。

Zhang等人[65]提出了一種基于模糊測試的黑盒方法DeepSearch。該方法從正確分類圖像開始，采用一定策略將圖像中的像素值變異成可能導致對抗輸入的值，一旦發現對抗性輸入，就開始迭代優化，以最小化圖像的范數擾動。同時將分層分組的策略應用到過程中，減少了查詢次數，同時提高了模糊化和細化的效率。

此外，還有一些學者研究了自然界中的對抗樣本[66-68]，這里就不做過多介紹。基于對抗樣本的測試技術總結如表3所示。

表3 基于對抗樣本的測試技術總結Table 3 Summary of testing technology based on adversarial samples

隨著大量對抗樣本生成算法的提出，神經網絡模型在對抗攻擊下的安全性成為熱點問題。一些學者將多種對抗樣本算法集成到工具中，用于評估神經網絡在對抗攻擊下的安全性。

Goodfellow 等人開發了針對機器學習模型進行對抗攻擊的Python 庫CleverHans[69]。該庫集成了FGSM、C&W等數十種對抗樣本生成算法，支持JAX、PyTorch、TensorFlow三種機器學習框架，并能夠針對對抗樣本對機器學習模型進行基準測試。百度安全團隊開發了對抗樣本工具箱AdvBox[70]。該工具箱集成了包括白盒和黑盒方式在內的10 種對抗樣本生成算法，除了原生支持百度自身研發的學習框架PaddlePaddle，還支持PyTorch、Caffe、MxNet、Keras、TensorFlow 等框架，兼容性強，能夠為模型安全性研究和應用提供重要支持。

IBM 推出了對抗性魯棒工具箱ART（Adversarial Robustness Toolbox）[71]。該工具不僅能夠評估機器學習模型的魯棒性，同時還提供了多種防御措施，指導模型進行重新訓練，提高模型在對抗攻擊下的魯棒性。阿里巴巴聯合浙江大學研發了DL 模型安全分析平臺Deep-Sec[72]。該平臺集成了16 種對抗樣本攻擊方法和13 種防御方法，使研究人員既能夠多方面評估DL 模型的安全性，又可以評估攻擊和防御算法的有效性。

此外，清華大學THUNLP 團隊開發了文本對抗攻擊工具包OpenAttack[73]。該工具包支持多種對抗樣本生成算法，并覆蓋了字、詞、句等不同級別擾動粒度的攻擊。該工具建立了針對文本對抗攻擊的評測指標，包括攻擊成功率、對抗樣本質量、攻擊效率等8個不同指標，同時支持用戶自己設計評測指標，具有可用性強、覆蓋面廣、可拓展性強等特點。

對抗樣本的廣泛存在說明神經網絡模型魯棒性和安全性面臨挑戰，這給模型評估工作帶來了困難。基于對抗樣本的測試技術，從攻擊者的角度入手，通過在圖像上構造擾動產生異常輸入作為測試輸入，然后觀察神經網絡模型在各種測試輸入下的表現，對模型的魯棒性、安全性做出判斷。基于白盒方式的測試技術依賴神經網絡模型的內部信息，產生樣本擾動較小，成功率高，但是通用性不強，如果模型對梯度進行遮蓋、隱藏，或者模型內部信息不可知，那么攻擊方法很難奏效。基于黑盒的測試技術，通過構造替代模型或是近似模擬模型梯度的方式生成對抗樣本，雖然產生的對抗樣本質量較低，但是通用性較強，危害性更大。結合白盒方式和黑盒方式的對抗樣本生成算法生成測試輸入，對模型魯棒性進行全面的評價，具有一定可行性，但是現有的對抗樣本生成算法還只是對抗樣本空間中的一小部分，該方法并不能評估模型在潛在對抗樣本下的魯棒性。

5 融合傳統測試技術

除上述測試技術外，一些學者將傳統測試技術應用到神經網絡測試中，比如模糊測試、蛻變測試、變異測試和符號執行，用于檢測DNN內部存在的缺陷，緩解測試預言或評估模型或數據集的質量。

5.1 模糊測試

模糊測試是一種傳統測試技術，它通過生成隨機數據作為測試輸入，以檢測程序崩潰、內存泄漏等問題，并成功應用于系統安全和漏洞檢測中。將模糊測試用于神經網絡測試，可以有效檢測神經網絡模型的內部缺陷，確保模型應用的安全。

Guo等人[74]提出了用于指導DL系統暴露錯誤行為的差分模糊測試框架DLFuzz。DLFuzz 通過不斷對輸入進行細微的突變，來最大化神經元覆蓋以及原始輸入和變異輸入之間的預測差異，同時定義了四種神經元選擇策略來提高神經元覆蓋率。在MNIST和ImageNet數據集上實驗評估表明，與DeepXplore相比，DLFuzz能夠以20.11%的時間產生338.59%的對抗性輸入，測試輸入生成效率遠高于DeepXplore。

Odena 等人[75]開發了一種覆蓋引導模糊測試工具TensorFuzz。該工具包括輸入選擇器、變異器、目標函數、覆蓋率分析器等模塊。在模糊測試過程中，突變算子以神經元覆蓋指標為指導，同時利用基于屬性的測試技術，對目標進行約束。通過最近鄰算法來計算覆蓋率，檢查覆蓋率是否更新，如果產生了新的覆蓋，則在輸入空間進行隨機搜索，否則繼續執行突變。通過在MNIST 數據集上的實驗證明，在產生同等數量的突變情況下，TensorFuzz發現錯誤的效率要遠高于隨機測試。

Zhang等人[76]提出了一種覆蓋引導對抗生成的模糊測試框架CAGFuzz。該框架借鑒了覆蓋引導灰盒模糊測試（Coverage-guided Grey-box Fuzzing，CGF）的思想，首先劃分數據集并根據存儲時間設置優先級，作為模糊測試的初始輸入；然后利用對抗樣本生成器生成對抗樣本，通過深度特征約束和計算余弦相似度確定需要保留的樣本；最后使用神經元覆蓋率指導生成過程，如果保留的對抗樣本出現了新的覆蓋，則將其納入測試集中。作者通過六種模型在三個數據集上的實驗證明了該方法在發現DNN潛在錯誤方面的有效性。

5.2 蛻變測試

測試預言是測試工作的關鍵問題之一，蛻變關系是指在多個程序執行過程中，程序輸入變化和輸出變化之間的關系。例如為了測試函數sinx的實現，可以檢測當輸入由x變為π－x時輸出的變化，如果sinx不等于sin(π－x)，則程序存在錯誤。其中，sinx=sin(π－x)就構成一組蛻變關系，它扮演著測試預言的角色，可以幫助檢測程序缺陷。

Ding 等人[77]提出了一種基于蛻變測試的深度學習驗證框架。框架分為系統、數據、數據項三個層次，針對這三個層次分別定義了系統級蛻變關系、數據集級蛻變關系和數據項級蛻變關系。通過蛻變測試檢查不同DNN 分類模型、不同數據集和不同數據項之間的分類精度，最終驗證模型或數據集的質量。

Dwarakanath 等人[78]針對DNN 分類器提出了四種蛻變關系：（1）訓練數據和測試數據輸入通道排列變化；（2）訓練數據和測試數據運算順序排列變化；（3）歸一化測試數據；（4）縮放測試數據。作者利用這四種蛻變關系在多個網絡上進行實驗，結果表明該方法能夠有效捕獲代碼實現上的缺陷，檢錯率達到71%。Zhu 等人[79]針對人臉識別應用提出了一種數據蛻變測試框架，并定義了四種蛻變關系：（1）帶上眼鏡；（2）化妝；（3）改變發型；（4）改變頭發顏色。最后，通過在四個人臉識別系統上對CelebA和PubFig人臉數據集的實驗證明了該方法的有效性。

Sharma 等人[80]提出了一種用于檢測數據集平衡性的測試方法TILE。作者設計了四種蛻變關系，該方法結合蛻變關系和等價模型檢驗，能夠有效檢測訓練數據的平衡性。劉佳洛等人[81]針對DNN圖像分類程序提出了一種蛻變測試框架。根據數據集的幾何屬性以及模型特性構造三種蛻變關系，結合變異測試在VGG 網絡和CIFAR-10 數據集上進行實驗，驗證該框架在檢測模型實現錯誤方面的效率和有效性。

5.3 變異測試和符號執行

在傳統軟件測試中，變異測試通過注入錯誤來評估測試輸入揭示錯誤的能力。其中檢測到的故障與所有注入故障的比率稱為突變分數，用以評估測試用例的質量。神經網絡的變異測試主要從代碼層面、數據層面、模型層面展開。

Ma等人[82]將變異測試應用到DL模型中，用于評估測試數據的質量。定義了一組源碼級別的變異操作和模型級別的變異操作，分別將錯誤注入到DL 源碼和模型中，通過分析注入故障的檢測程度來評估測試數據的質量。作者在MINIST、CIFAR-10 數據集上對三個DL模型的實驗證明了該測試框架的有效性。Shen 等人[83]提出了一種神經網絡變異分析的方法MuNN，定義了五種針對神經網絡模型的變異算子，通過計算突變分數衡量測試數據的充分性。Jahangirova等人[84]對Ma和Shen提出的20 種變異算子進行實證研究，指出了這些變異算法應用時需要進行適當的配置，并重新定義了殺死變異，用于指導在DL模型上的變異測試。

符號執行是一種程序分析技術，用于測試被測軟件是否違反某些屬性。動態符號執行（Concolic Testing）使用隨機測試輸入執行被測程序，同時并行執行符號執行，以檢測程序的漏洞。

Sun 等人[85]提出了一種基于符號執行的DNN 測試和調試工具DeepConcolic。該工具由預處理、測試標準、符號執行引擎、遺傳算法搜索引擎、測試套件、測試預言等模塊組成。首先預處理模塊根據測試標準對測試輸入數據格式化，以便符號執行引擎和遺傳算法搜索引擎進行操作；然后通過符號執行引擎和遺傳算法搜索引擎生成測試用例，其中符號執行引擎支持線性規劃和全局優化兩種分析技術；最后依據神經元覆蓋和MC/DC變體生成測試用例的覆蓋率報告。此外，Gopinath 等人[86]將神經網絡轉化為命令式程序，然后利用符號分析的方法對神經網絡進行分析和驗證。Agarwal等人[87]將神經網絡局部解釋構建決策樹，然后應用符號執行來檢測DNN中的個體差異，進而指導測試用例生成。

融合傳統測試技術總結如表4所示。目前，神經網絡測試在測試輸入生成、測試預言、測試充分性、缺陷檢測等方面面臨諸多挑戰。融合傳統測試技術將傳統測試技術在解決這類問題上的經驗，應用到神經網絡測試中，這樣就可以沿著既有的技術路線，針對神經網絡的特點展開測試，在取得不錯測試效果的同時，降低了測試成本。模糊測試能夠有效地指導測試輸入生成，檢測神經網絡錯誤行為；蛻變測試針對測試預言問題，通過構建蛻變關系指導測試輸入生成，發現神經網絡內部缺陷；變異測試通過對代碼、數據、模型進行變異，能夠有效評估測試用例集的質量；利用符號執行分析技術分析神經網絡，能夠以更少的執行次數發現錯誤，同時以更高效率生成高質量測試輸入。此外，將多種傳統測試技術相結合，例如蛻變測試+變異測試，用于指導測試用例生成，同時檢查測試用例的質量，也是一條可行的途徑。

表4 融合傳統測試技術總結Table 4 Summary of fusing traditional testing technology

6 總結和展望

針對神經網絡驗證和測試技術，本文從驗證技術、基于覆蓋的測試技術、基于對抗樣本的測試技術、融合傳統測試技術等方面對該領域內的研究現狀進行了梳理和總結，對其中關鍵技術進行了歸納和分類，并對一些技術的基本思想和實現進行了簡要介紹。

雖然目前神經網絡的驗證和測試工作取得了一定的進展，但是距全面檢測神經網絡缺陷，有效保證神經網絡應用的質量還有一段距離，神經網絡驗證和測試工作還面臨諸多挑戰。神經網絡的驗證和測試需要對以下內容進行研究：

（1）適用大規模網絡的精確驗證技術。神經網絡朝著大規模的方向發展，大規模神經網絡的驗證需求將進一步上升，隨著大規模神經網絡應用在一些安全攸關的領域，勢必要求更加精確、高效的驗證技術。

（2）有效的度量指標。如何有效刻畫神經網絡的屬性，如何客觀評價神經網絡，如何有效指導神經網絡測試的有效進行，這些都需要以科學、有效的度量指標為牽引。

（3）更具通用性的測試技術和方法。當前測試技術多是針對神經網絡在特定應用領域的測試，往往缺乏普遍適用性，因此成本較高。研究更具通用性的測試技術和方法，能夠提高測試效率和降低測試成本。

（4）合理規范的驗證測試流程。傳統軟件測試有著較為成熟的流程和規范，測試工作更加科學、全面，而神經網絡驗證和測試工作缺乏合理規范的流程，在具體操作層面還存在主觀性和片面性。

隨著神經網絡技術的推廣和應用，如何有效地驗證和測試神經網絡將成為一個亟待解決的問題。圍繞如何建立科學有效的測試度量指標、如何設計更具可行性測試技術、如何規范測試流程等問題，還需要做進一步深入的研究。