王 莉，李曉娟，2，關(guān) 永，3，王 瑞，4，王佳岳

1(首都師范大學(xué) 信息工程學(xué)院，北京 100048)

2(首都師范大學(xué) 高可靠嵌入式系統(tǒng)技術(shù)北京市工程研究中心，北京 100048)

3(首都師范大學(xué) 北京成像理論與技術(shù)高精尖創(chuàng)新中心，北京 100048)

4(首都師范大學(xué) 輕型工業(yè)機(jī)器人與安全驗(yàn)證北京市重點(diǎn)實(shí)驗(yàn)室，北京 100048)

E-mail：lixj@cnu.edu.cn

1 引 言

神經(jīng)網(wǎng)絡(luò)是模仿大腦神經(jīng)元之間的相互作用組成的數(shù)學(xué)模型，在90年代末受當(dāng)時(shí)計(jì)算機(jī)水平的限制，神經(jīng)網(wǎng)絡(luò)由于完成不了大量神經(jīng)元之間的計(jì)算而陷入低潮.于20年代初，因?yàn)椴⑿杏?jì)算與GPU的發(fā)展，計(jì)算機(jī)的計(jì)算能力、運(yùn)行速度得到明顯提升，使得神經(jīng)網(wǎng)絡(luò)的研究與應(yīng)用再次被人們推入高潮.同時(shí)，由于神經(jīng)網(wǎng)絡(luò)在人工智能方面的大規(guī)模應(yīng)用，使其被廣泛部署于航天器控制[1]、駕駛環(huán)境預(yù)測與自動(dòng)駕駛[2-4]、機(jī)器人控制[5，6]、醫(yī)學(xué)圖像分析[7，8]等方面的軟硬件系統(tǒng)中[9]，而這些領(lǐng)域中一點(diǎn)微小的誤差都可能會(huì)帶來無法估量的損失，所以要求神經(jīng)網(wǎng)絡(luò)具有非常高的可信性.之前學(xué)術(shù)界關(guān)于神經(jīng)網(wǎng)絡(luò)可信性方面的研究主要是圍繞優(yōu)化訓(xùn)練過程以達(dá)到提高結(jié)果準(zhǔn)確性的目的，但是隨著人工智能的快速發(fā)展，對于應(yīng)用其中的神經(jīng)網(wǎng)絡(luò)的可信性要求更嚴(yán)格，僅通過神經(jīng)網(wǎng)絡(luò)的準(zhǔn)確性這點(diǎn)已經(jīng)不能充分保證其可信性.

由于可信性要求的提高，同之前的計(jì)算系統(tǒng)相比神經(jīng)網(wǎng)絡(luò)的可信性研究需要擴(kuò)展到可靠性、安全性、可用性之外，還包括不確定性、魯棒性和可解釋性等屬性[10].在此基礎(chǔ)上人們提出通過一些方法去對網(wǎng)絡(luò)進(jìn)行驗(yàn)證，目前關(guān)于神經(jīng)網(wǎng)絡(luò)可信性驗(yàn)證方法大致可分為以下類別：基于搜索的方法[11-14]、約束求解[15-19]、過度近似[20-22]和全局優(yōu)化[23，24]，還有一些是綜合上述方法展開驗(yàn)證.本文通過神經(jīng)網(wǎng)絡(luò)的研究現(xiàn)狀進(jìn)行分析，在描述神經(jīng)網(wǎng)絡(luò)可信性問題相關(guān)的屬性前提下，對利用形式化方法驗(yàn)證基于反例、抽象解釋、可滿足性求解、輸入/輸出可達(dá)性分析等可信性問題的核心算法進(jìn)行分類，最后對形式化方法驗(yàn)證神經(jīng)網(wǎng)絡(luò)可信性的發(fā)展趨勢進(jìn)行總結(jié)與展望.

2 神經(jīng)網(wǎng)絡(luò)可信性相關(guān)屬性

神經(jīng)網(wǎng)絡(luò)可信性[25-27]的最終要求是在輸入集的基礎(chǔ)上得到最終符合預(yù)期的輸出結(jié)果，經(jīng)過神經(jīng)網(wǎng)絡(luò)多次循環(huán)傳播得到的預(yù)期輸出概率結(jié)果，間接反應(yīng)出網(wǎng)絡(luò)的準(zhǔn)確性，但神經(jīng)網(wǎng)絡(luò)的輸出往往是難以預(yù)料的，因此僅通過網(wǎng)絡(luò)傳播過程準(zhǔn)確率的改善并不能充分說明該神經(jīng)網(wǎng)絡(luò)可信.隨著安全問題研究的深入，關(guān)于神經(jīng)網(wǎng)絡(luò)可信性驗(yàn)證的問題已經(jīng)轉(zhuǎn)變成了驗(yàn)證該神經(jīng)網(wǎng)絡(luò)一系列屬性是否成立，分析神經(jīng)網(wǎng)絡(luò)可信性的相關(guān)屬性如下：

可用性：神經(jīng)網(wǎng)絡(luò)能否完成預(yù)期操作以及是否能成功運(yùn)行出輸出結(jié)果；

可靠性：神經(jīng)網(wǎng)絡(luò)能否根據(jù)應(yīng)用部署的要求從而對數(shù)據(jù)進(jìn)行正確的操作處理；

安全性：神經(jīng)網(wǎng)絡(luò)面對攻擊時(shí)能否產(chǎn)生結(jié)果或?qū)τ诮Y(jié)果的準(zhǔn)確性影響如何；

不確定性(可達(dá)性)：由于神經(jīng)網(wǎng)絡(luò)的“黑盒狀態(tài)”，使得其輸出存在不確定性，在該情況下應(yīng)用神經(jīng)網(wǎng)絡(luò)能否保證輸出滿足預(yù)期要求或到達(dá)預(yù)期狀態(tài).

魯棒性：對神經(jīng)網(wǎng)絡(luò)進(jìn)行有限范圍干擾時(shí)，該區(qū)間內(nèi)網(wǎng)絡(luò)依舊能夠保持輸出和干擾前相同或能保證一定概率下相同；

區(qū)間屬性：不實(shí)際運(yùn)行神經(jīng)網(wǎng)絡(luò)的情況下，對應(yīng)網(wǎng)絡(luò)抽象出的模型與實(shí)際網(wǎng)絡(luò)之間的關(guān)系；

可解釋性：神經(jīng)網(wǎng)絡(luò)輸出的結(jié)果能否用人類能夠理解的語言方法合理的進(jìn)行解釋.

通過對神經(jīng)網(wǎng)絡(luò)可信性問題的相關(guān)屬性進(jìn)行說明后，本文將綜述一些使用形式化方法[28]驗(yàn)證神經(jīng)網(wǎng)絡(luò)可信性問題的核心算法，如圖1 形式化方法驗(yàn)證示意圖.該方法的優(yōu)勢在于避免了神經(jīng)網(wǎng)絡(luò)對于每個(gè)輸入值的測試，進(jìn)而提供一種可證明的保證方式以防止過大或無限狀態(tài)下網(wǎng)絡(luò)不可實(shí)現(xiàn)的情況，如給定一個(gè)神經(jīng)網(wǎng)絡(luò)和一個(gè)屬性，對其可信性形式化驗(yàn)證過程定義為檢查該屬性是否適用于該神經(jīng)網(wǎng)絡(luò)或者基于一定的數(shù)學(xué)邏輯推導(dǎo)出該網(wǎng)絡(luò)在此屬性下最后輸出是否處于安全狀態(tài).

圖1 形式化方法驗(yàn)證示意圖Fig.1 Schematic diagram of the formal method validation

保證神經(jīng)網(wǎng)絡(luò)的可信性可以通過循環(huán)訓(xùn)練調(diào)整參數(shù)提高準(zhǔn)確性、對網(wǎng)絡(luò)進(jìn)行驗(yàn)證來實(shí)現(xiàn)，其中驗(yàn)證方法是驗(yàn)證的關(guān)鍵，因此本文在神經(jīng)網(wǎng)絡(luò)可信性的一系列屬性基礎(chǔ)上抽象出可信性驗(yàn)證問題并概括近年來解決可信性問題的形式化方法分類以及各類方法核心算法的闡述.

3 神經(jīng)網(wǎng)絡(luò)可信性問題抽象

由于神經(jīng)網(wǎng)絡(luò)訓(xùn)練過程的“黑盒子”問題，使得循環(huán)訓(xùn)練次數(shù)再多也依舊存在不可預(yù)知的威脅，在此情況下，本文抽象出可信性驗(yàn)證問題并進(jìn)行概括分類為以下4種：

·基于反例驗(yàn)證：實(shí)際運(yùn)行中，神經(jīng)網(wǎng)絡(luò)輸入時(shí)可能會(huì)因?yàn)槭艿酵饨绲墓魧?dǎo)致輸出同預(yù)期輸出出現(xiàn)差異從而產(chǎn)生反例.而對于神經(jīng)網(wǎng)絡(luò)來說極小的擾動(dòng)都可能會(huì)導(dǎo)致訓(xùn)練結(jié)果的不準(zhǔn)確，此情況下神經(jīng)網(wǎng)絡(luò)的驗(yàn)證往往會(huì)部署新的逼近待驗(yàn)證網(wǎng)絡(luò)再通過一致性比較來驗(yàn)證網(wǎng)絡(luò)在攻擊下的安全性以及魯棒性.

·抽象解釋：神經(jīng)網(wǎng)絡(luò)的訓(xùn)練過程為給定網(wǎng)絡(luò)輸入集，根據(jù)相應(yīng)的計(jì)算規(guī)則在實(shí)際運(yùn)行之后不斷調(diào)整輸出與預(yù)期輸出之間的差距，訓(xùn)練過程中數(shù)據(jù)集過大或神經(jīng)網(wǎng)絡(luò)過于復(fù)雜時(shí)會(huì)出現(xiàn)運(yùn)行時(shí)間長、電腦負(fù)荷大等問題.在此基礎(chǔ)上提出了通過對神經(jīng)網(wǎng)絡(luò)模型抽象來將復(fù)雜的問題簡單化再解決的方法，同時(shí)由于其主要是對網(wǎng)絡(luò)抽象出的模型進(jìn)行驗(yàn)證所以其重點(diǎn)是研究區(qū)間屬性下的神經(jīng)網(wǎng)絡(luò)可信性驗(yàn)證問題；

·可滿足性求解：神經(jīng)網(wǎng)絡(luò)反向傳播后最后的輸出只能反映訓(xùn)練該網(wǎng)絡(luò)之后的準(zhǔn)確性概率，并沒有說明該網(wǎng)絡(luò)的運(yùn)行條件是否滿足或者是否存在一組參數(shù)可以使得網(wǎng)絡(luò)的屬性成立從而確定神經(jīng)網(wǎng)絡(luò)的可信性；

·輸入/輸出可達(dá)性分析：在神經(jīng)網(wǎng)絡(luò)輸入范圍已知的情況下，即使中間為黑盒子，通過對神經(jīng)網(wǎng)絡(luò)進(jìn)行形式化驗(yàn)證就可以根據(jù)網(wǎng)絡(luò)的輸入范圍利用一定的數(shù)學(xué)規(guī)則對網(wǎng)絡(luò)的狀態(tài)進(jìn)行可達(dá)性分析，檢查網(wǎng)絡(luò)在給定的輸入范圍里輸出是否在安全的區(qū)間里從而驗(yàn)證神經(jīng)網(wǎng)絡(luò)在不確定性問題下的可信性；

依據(jù)神經(jīng)網(wǎng)絡(luò)可信性對應(yīng)的相關(guān)屬性歸納可信性問題，并在這4類問題基礎(chǔ)上，對驗(yàn)證神經(jīng)網(wǎng)絡(luò)可信性的形式化方法的核心算法進(jìn)行分類分析.

4 神經(jīng)網(wǎng)絡(luò)可信性形式化方法分類

4.1 等價(jià)性驗(yàn)證

神經(jīng)網(wǎng)絡(luò)的輸入集在受到擾動(dòng)時(shí)可能會(huì)導(dǎo)致網(wǎng)絡(luò)的輸出結(jié)果產(chǎn)生錯(cuò)誤的分類，即使只是加入了很小的噪聲干擾，但是兩次網(wǎng)絡(luò)識別出的結(jié)果可能完全不同.輸入干擾導(dǎo)致的錯(cuò)誤分類也會(huì)成為網(wǎng)絡(luò)的安全隱患這一問題引起人們關(guān)注，進(jìn)一步研究對抗樣本[29]下神經(jīng)網(wǎng)絡(luò)安全性以及魯棒性的可信性驗(yàn)證問題具有重要意義.

對于神經(jīng)網(wǎng)絡(luò)對抗性問題的驗(yàn)證，首先是對抗性樣本的生成，如將FGSM[30，31]應(yīng)用于MNIST數(shù)據(jù)集攻擊后進(jìn)一步生成對抗性樣本.其次選取合適的方法進(jìn)行驗(yàn)證，即神經(jīng)網(wǎng)絡(luò)受到攻擊時(shí)對網(wǎng)絡(luò)進(jìn)行驗(yàn)證一般通過形式化方法中的等價(jià)性驗(yàn)證來實(shí)現(xiàn)，該方法主要是驗(yàn)證系統(tǒng)在受到干擾后對應(yīng)的輸出是否同未干擾時(shí)輸出相同，基本原理是在兩個(gè)系統(tǒng)之間根據(jù)相應(yīng)的數(shù)學(xué)規(guī)則、定理等對系統(tǒng)進(jìn)行描述，再用形式化的方法將兩個(gè)系統(tǒng)進(jìn)行一致性比較，神經(jīng)網(wǎng)絡(luò)中等價(jià)性驗(yàn)證的實(shí)現(xiàn)主要使用符號法即先將問題形式化為特定符號描述再通過相應(yīng)的求解方法如求解器、定理證明器等對一致性問題求解.Yu Li等人[32]提出了一種新的針對神經(jīng)網(wǎng)絡(luò)系統(tǒng)故障注入攻擊的DeepDyve動(dòng)態(tài)驗(yàn)證技術(shù).該技術(shù)與之前驗(yàn)證技術(shù)不同之處在于DeepDyve是為了查找網(wǎng)絡(luò)中輸出同預(yù)期輸出相同的數(shù)據(jù)而不是查找反例，其新部署一個(gè)逼近要驗(yàn)證的原神經(jīng)網(wǎng)絡(luò)的小型網(wǎng)絡(luò)之后通過檢查小型網(wǎng)絡(luò)產(chǎn)生的輸出是否具有一致性，在出現(xiàn)不一致的輸出時(shí)則對原神經(jīng)網(wǎng)絡(luò)進(jìn)行調(diào)整來使網(wǎng)絡(luò)具有可信性.該方法核心在于比較對抗性樣本下神經(jīng)網(wǎng)絡(luò)能否產(chǎn)生正確的輸出，主要對網(wǎng)絡(luò)的可用性，安全性以及魯棒性等可信性屬性進(jìn)行驗(yàn)證，而不是依據(jù)輸入產(chǎn)生預(yù)計(jì)輸出驗(yàn)證神經(jīng)網(wǎng)絡(luò)的可靠性、不確定性或者可解釋性等屬性.

4.2 抽象解釋驗(yàn)證

4.2.1 基于抽象的過度逼近

在現(xiàn)有的使用形式化驗(yàn)證神經(jīng)網(wǎng)絡(luò)的可信性方法中，模型檢測有數(shù)據(jù)量過大時(shí)導(dǎo)致狀態(tài)空間爆炸的問題，而定理證明由于是基于數(shù)學(xué)邏輯展開使得對于操作者的數(shù)學(xué)功底與邏輯思維要求比較高，這些常導(dǎo)致形式化驗(yàn)證方法在實(shí)際的應(yīng)用中受到局限.在這種情況下，采用抽象解釋的方法對神經(jīng)網(wǎng)絡(luò)進(jìn)行可信性驗(yàn)證，由于其不需要實(shí)際的運(yùn)行網(wǎng)絡(luò)使得該方法可以有效的避免以上局限性的問題，該方法主要思想是在可信性驗(yàn)證過程中將復(fù)雜的問題近似抽象以后通過分析其核心組成達(dá)到降低復(fù)雜度的目的，在神經(jīng)網(wǎng)絡(luò)可信性驗(yàn)證中抽象解釋一般在輸入集區(qū)間內(nèi)用抽象域去近似網(wǎng)絡(luò)的輸入，具體操作為在神經(jīng)網(wǎng)絡(luò)的輸入層上定義具體的域，輸入集合包含于該域，此時(shí)為了計(jì)算的效率選擇一個(gè)比較簡單的域作為抽象域，其可以過度逼近輸入層具體域中變量的范圍與關(guān)系，所以對于抽象域的選擇很關(guān)鍵，對驗(yàn)證的效率與準(zhǔn)確性有決定性作用，在形式上，一個(gè)抽象域由表示為一組邏輯約束.

基于過逼近的抽象方法是通過對神經(jīng)網(wǎng)絡(luò)或?qū)ζ漭斎爰M(jìn)行過度近似后在區(qū)間屬性下對網(wǎng)絡(luò)的可信性進(jìn)行驗(yàn)證.Timon Gehr等人[20]提出了使用AI2，基于過度逼近的方法引入抽象轉(zhuǎn)換器來獲得網(wǎng)絡(luò)的行為從而自動(dòng)證明神經(jīng)網(wǎng)絡(luò)的安全屬性.在實(shí)際應(yīng)用中，神經(jīng)網(wǎng)絡(luò)在輸入時(shí)時(shí)常會(huì)遇到干擾使得網(wǎng)絡(luò)對分類產(chǎn)生錯(cuò)誤的判斷，而實(shí)踐證明輸入擾動(dòng)能產(chǎn)生對抗性例子，AI從選取的抽象域中提取元素過度逼近輸入集合，根據(jù)抽象轉(zhuǎn)換器返回的結(jié)果來驗(yàn)證屬性，AI2需要分析神經(jīng)網(wǎng)絡(luò)運(yùn)算過程中每層神經(jīng)元產(chǎn)生的所有可能輸出，通過神經(jīng)網(wǎng)絡(luò)編碼成邏輯公式之后再用約束求解器來驗(yàn)證網(wǎng)絡(luò)的魯棒性，論文還針對選用不同的抽象域來說明抽象域?qū)τ谑褂肁I2驗(yàn)證神經(jīng)網(wǎng)絡(luò)魯棒性的影響.Yizhak Yisrael Elboher等人[33]提出抽象一個(gè)過度逼近原待驗(yàn)證網(wǎng)絡(luò)的小型網(wǎng)絡(luò)，并對該小型網(wǎng)絡(luò)進(jìn)行規(guī)范驗(yàn)證，如果待驗(yàn)證屬性在小型網(wǎng)絡(luò)滿足則該屬性也可以適用于原網(wǎng)絡(luò)，反之則提供一個(gè)反例，并使用該反例去反向調(diào)整網(wǎng)絡(luò)從而提高網(wǎng)絡(luò)的正確性.S.Gokulanathan等人[34]通過簡化神經(jīng)網(wǎng)絡(luò)來對其進(jìn)行驗(yàn)證.Ravi Mangal[35]等人提出了概率魯棒性的概念，通過抽象解釋去近似網(wǎng)絡(luò)的行為從而對神經(jīng)網(wǎng)絡(luò)中不滿足魯棒性的輸入集合過度逼近，使用重要性抽樣的方法來對其進(jìn)行對抗得到神經(jīng)網(wǎng)絡(luò)違反魯棒性概率的準(zhǔn)確估計(jì).該方法關(guān)鍵技術(shù)是對神經(jīng)網(wǎng)絡(luò)進(jìn)行一個(gè)抽象簡化之后進(jìn)行可信性驗(yàn)證，因此對于抽象出來的網(wǎng)絡(luò)具有完整的結(jié)構(gòu)是網(wǎng)絡(luò)可信性相關(guān)屬性可以得到驗(yàn)證的關(guān)鍵.

除了對網(wǎng)絡(luò)抽象[36]還可以對網(wǎng)絡(luò)的狀態(tài)進(jìn)行抽象來實(shí)現(xiàn)可信性的驗(yàn)證，如通過后繼狀態(tài)進(jìn)一步來反向推斷安全情況下神經(jīng)網(wǎng)絡(luò)的輸入狀態(tài).Xiaowu Sun等人[37]介紹了一種具有神經(jīng)網(wǎng)絡(luò)的自助機(jī)器人，通過構(gòu)造系統(tǒng)終止?fàn)顟B(tài)的抽象，并通過其可達(dá)性分析來計(jì)算安全的初始狀態(tài)集合，使得該機(jī)器人從安全的初始狀態(tài)出發(fā)保證其在具有多個(gè)障礙的空間里可以安全躲過障礙.基于有限狀態(tài)抽象，該方法能夠驗(yàn)證網(wǎng)絡(luò)的可用性、可靠性與區(qū)間屬性等可信性屬性，但是神經(jīng)網(wǎng)絡(luò)的安全性、不確定性以及魯棒性等屬性的可信性驗(yàn)證還有待進(jìn)一步研究實(shí)現(xiàn).

4.2.2 基于定理證明驗(yàn)證

形式化過程是開發(fā)一組通用的數(shù)學(xué)模型和定義的過程，其中定理證明[38]是基于演繹推理的廣泛用于物理系統(tǒng)驗(yàn)證的形式化方法技術(shù).通過定理證明的方法對神經(jīng)網(wǎng)絡(luò)的可信性進(jìn)行驗(yàn)證，先建立網(wǎng)絡(luò)對應(yīng)的數(shù)學(xué)模型，再利用推理驗(yàn)證其預(yù)期的性質(zhì)，是根據(jù)已有的公理或者已經(jīng)被證明出來的定理添加推理規(guī)則直到推出所要驗(yàn)證的定理的過程，如驗(yàn)證神經(jīng)網(wǎng)絡(luò)可信性屬性中的可解釋性，可以通過自然語言或者邏輯規(guī)則建立網(wǎng)絡(luò)相應(yīng)的數(shù)學(xué)模型，再用人類所能理解公理或定理進(jìn)行解釋.

在網(wǎng)絡(luò)可信性驗(yàn)證中，對于底層邏輯的判定問題，定理證明器可以自動(dòng)或交互式地完成，由于命題邏輯是可判定的，因此在該邏輯中表達(dá)的句子可以使用計(jì)算機(jī)程序自動(dòng)驗(yàn)證，而高階邏輯是不可判定的，因此用高階邏輯表示的句子定理必須以交互式的方式然后用戶提供指導(dǎo)來驗(yàn)證.Adnan Rashid等人[39]通過在HOL4定理證明器中形式化了z語法，開發(fā)了一個(gè)形式化推理分子反應(yīng)的演繹框架，并且在高階邏輯中形式化了z語法的邏輯運(yùn)算符和推理規(guī)則.Abdorrahim Bahrami等人[40]通過Coq定理證明器驗(yàn)證了一些基本神經(jīng)元結(jié)構(gòu)的動(dòng)態(tài)行為性質(zhì)，提出并證明了4個(gè)重要屬性，從單個(gè)神經(jīng)元的屬性與輸入和輸出之間的關(guān)系開始，轉(zhuǎn)向更復(fù)雜的屬性，從而提高整體神經(jīng)網(wǎng)絡(luò)的可信性.Coq實(shí)現(xiàn)了一個(gè)具有高度表達(dá)力的高階邏輯，通過直接引入神經(jīng)元結(jié)構(gòu)的建模數(shù)據(jù)類型，表達(dá)它們的屬性，也由于Coq在證明過程中具有通用性，使其可以證明任意參數(shù)值的屬性，如任何時(shí)間長度，輸入序列，或任意數(shù)量的神經(jīng)元等.定理證明主要用于驗(yàn)證網(wǎng)絡(luò)的可解釋性，網(wǎng)絡(luò)可解釋性基于網(wǎng)絡(luò)的可用性之上，通過一定的邏輯規(guī)則推理出網(wǎng)絡(luò)的輸出結(jié)果對網(wǎng)絡(luò)的可靠性、不確定性以及區(qū)間屬性進(jìn)行可信性驗(yàn)證.

通過基于抽象的過度逼近以及定理證明來解決神經(jīng)網(wǎng)絡(luò)可信性問題中的抽象問題，使得復(fù)雜的或者難以實(shí)現(xiàn)的可信性問題通過抽象簡化逐步實(shí)現(xiàn)驗(yàn)證的目的.

4.3 基于模型檢測驗(yàn)證

模型檢測[41，42]是通過對系統(tǒng)構(gòu)造出的模型狀態(tài)空間的遍歷來確定系統(tǒng)屬性的準(zhǔn)確性從而判斷系統(tǒng)是不是符合設(shè)計(jì)需求.在形式驗(yàn)證中，通?；谌鐖D2所示的轉(zhuǎn)換圖原型來定義神經(jīng)網(wǎng)絡(luò)的模型[43].對于神經(jīng)網(wǎng)絡(luò)的可信性驗(yàn)證，模型檢測在有限狀態(tài)下對網(wǎng)絡(luò)窮舉搜索，驗(yàn)證依賴屬性的可滿足問題，在結(jié)果為真的情況下則表明網(wǎng)絡(luò)是符合性質(zhì)的，反之則不符合并且會(huì)相應(yīng)的給出一個(gè)反例[45]，而且在網(wǎng)絡(luò)可靠的情況下根據(jù)對神經(jīng)網(wǎng)絡(luò)狀態(tài)是否可達(dá)預(yù)期狀態(tài)，模型檢測的方法可以驗(yàn)證在不確定性時(shí)對應(yīng)的輸入/輸出范圍問題下神經(jīng)網(wǎng)絡(luò)的可信性.因此，模型檢測方法驗(yàn)證網(wǎng)絡(luò)可信性的核心算法可以分為屬性可滿足性問題與狀態(tài)可達(dá)性問題.

圖2 神經(jīng)元狀態(tài)轉(zhuǎn)換圖原型[44]Fig.2 Prototype neuronal state transition diagram[44]

4.3.1 可滿足性求解

神經(jīng)網(wǎng)絡(luò)可信性驗(yàn)證中可滿足問題進(jìn)行分析后可以通過形式化方法中的模型檢測來解決，由于可滿足問題主要是驗(yàn)證屬性在神經(jīng)網(wǎng)絡(luò)中是否得到滿足，可以將驗(yàn)證問題轉(zhuǎn)化為一組約束再通過相應(yīng)的約束求解器進(jìn)行求解的過程.可信性屬性中的可用性和可靠性，便可以將其定義編碼成相應(yīng)的條件約束，再選擇合適的求解器進(jìn)行求解，如果結(jié)果為真，說明至少存在一組參數(shù)使得該網(wǎng)絡(luò)屬性成立，驗(yàn)證出網(wǎng)絡(luò)的可用/可靠性.研發(fā)成熟的求解器可以解決較大規(guī)模的實(shí)際問題，先后出現(xiàn)了各類求解器可給出能否有滿足相關(guān)約束問題的解，如SAT求解器、LP求解器、MILP求解器、SMT求解器等，求解器工作過程如圖3.將需要解決的實(shí)際問題建模為約束可滿足問題，其中關(guān)于使用該思想對神經(jīng)網(wǎng)絡(luò)進(jìn)行驗(yàn)證也一直是研究的熱點(diǎn)，近年通過可滿足問題進(jìn)行網(wǎng)絡(luò)可信性驗(yàn)證方法如下：

圖3 求解器工作過程圖Fig.3 Working process diagram of the solver

A.基于SAT和線性規(guī)劃組合方法

給定一組實(shí)值變量上的線性不等式和一個(gè)線性優(yōu)化函數(shù)(它們一起被稱為線性規(guī)劃)，對應(yīng)的線性規(guī)劃問題是利用求解器找到對滿足所有約束的最小化目標(biāo)函數(shù)變量的賦值，通過求解出滿足約束的值使得網(wǎng)絡(luò)在部署過程中滿足可信性.Ruediger Ehlers[46]提出了針對用分段線性激活函數(shù)的前饋神經(jīng)網(wǎng)絡(luò)的驗(yàn)證方法.基于SAT與線性規(guī)劃組合將神經(jīng)網(wǎng)絡(luò)線性近似，該近似可以添加到神經(jīng)網(wǎng)絡(luò)驗(yàn)證問題的SMT或MILP實(shí)例編碼中，可以在驗(yàn)證過程中排除未激活神經(jīng)元的大規(guī)模搜索，不僅將近似作為求解器的條件約束，還通過彈性濾波算法在發(fā)生沖突時(shí)尋找最小不可行線性約束集，使其與推測隱藏節(jié)點(diǎn)相位過程結(jié)合從而選擇安全的節(jié)點(diǎn)相位，對節(jié)點(diǎn)相位進(jìn)行單元傳播類推理，用于神經(jīng)網(wǎng)絡(luò)中的節(jié)點(diǎn)選擇.Hemali Angne等人[47]研究模擬圖神經(jīng)網(wǎng)絡(luò)來解決NP-complete問題，通過SAT公式將圖神經(jīng)網(wǎng)絡(luò)可視化來描述相應(yīng)的屬性.

B.可滿足性模理論的方法

用可滿足性模理論的方法驗(yàn)證神經(jīng)網(wǎng)絡(luò)的過程是將網(wǎng)絡(luò)抽象為一組線性算法約束的布爾組合，證明當(dāng)抽象模型是安全的時(shí)，具體的網(wǎng)絡(luò)則是安全的，當(dāng)模型不安全時(shí)則會(huì)提供相應(yīng)的反例來進(jìn)行網(wǎng)絡(luò)的改進(jìn).首先將網(wǎng)絡(luò)的約束轉(zhuǎn)換為布爾約束，再檢查相應(yīng)的算數(shù)理論中分配的一致性，當(dāng)存在滿足神經(jīng)網(wǎng)絡(luò)中所有約束的分配則說明網(wǎng)絡(luò)是可滿足的，即先給定網(wǎng)絡(luò)輸入的先決條件保證其滿足規(guī)定去輸出后置條件.

Luca Pulina等人[48]提出的驗(yàn)證方法考慮了檢查神經(jīng)網(wǎng)絡(luò)3種安全條件即網(wǎng)絡(luò)的輸出是不是在規(guī)定的安全區(qū)間、網(wǎng)絡(luò)的輸出是不是逼近局部的預(yù)期輸出、在輸入集出現(xiàn)微弱攻擊變化時(shí)輸出會(huì)不會(huì)受到影響，將檢查的條件編碼為線性算法的約束可滿足性問題，通過可滿足性問題對網(wǎng)絡(luò)進(jìn)行可信性驗(yàn)證.

在可滿足性模理論方法里，SMT求解器的應(yīng)用最為廣泛，同時(shí)SMT在線性邏輯約束優(yōu)化問題中也是解決問題的關(guān)鍵，利用SMT求解器找到滿足符合問題的約束條件和優(yōu)化目標(biāo)抽象出來的目標(biāo)函數(shù)和約束表達(dá)式的解的集合，再從集合里找到使得目標(biāo)函數(shù)取得最值的解為最優(yōu)解.Guy Katz等人[49]提出一種高效的SMT求解器Reluplex，其中神經(jīng)網(wǎng)絡(luò)可以抽象為線性組合，為了提高其性能給其增加了激活函數(shù)使其轉(zhuǎn)為非線性，但是非線性給神經(jīng)網(wǎng)絡(luò)的驗(yàn)證增加了不確定性，為了解決這個(gè)問題提出了將Reluplex用在ReLU激活函數(shù)的可滿足約束求解上.即在給定的輸入輸出情況下，設(shè)置兩個(gè)變量分別用于單個(gè)的ReLU節(jié)點(diǎn)去連接前后一層的節(jié)點(diǎn)，根據(jù)ReLU函數(shù)自身的取值以及輸入輸出值定義約束條件之后，使用求解器求解是否有滿足這些條件對應(yīng)的變量值，從而對神經(jīng)網(wǎng)絡(luò)進(jìn)行驗(yàn)證.Clark Barrett等人[50]提出基于單純形方法通過處理ReLU約束來進(jìn)一步對神經(jīng)網(wǎng)絡(luò)可信性問題進(jìn)行驗(yàn)證，通過在Reluplex基礎(chǔ)上將相關(guān)屬性編碼成其輸入約束進(jìn)行屬性可滿足性驗(yàn)證.Luca Pulina等人[51]提出通過SMT求解器編碼解決驗(yàn)證MLPs的輸出包含于具體的一個(gè)安全的區(qū)域里并且驗(yàn)證其逼近具體的值或在區(qū)域內(nèi)調(diào)整目標(biāo)的誤差方差.Xiaowei Huang等人[13]在SMT的基礎(chǔ)上提出了一種對于前饋神經(jīng)網(wǎng)絡(luò)分類決策進(jìn)行自動(dòng)驗(yàn)證的框架，使用離散化的方法進(jìn)行有限的窮舉搜索從而保證錯(cuò)誤分類被找到，進(jìn)一步將驗(yàn)證問題轉(zhuǎn)化為對反例的搜索問題.

C.基于MILP方法

對神經(jīng)網(wǎng)絡(luò)編碼過程中，將對應(yīng)的約束添加到MILP求解器中，根據(jù)求解的結(jié)果判斷網(wǎng)絡(luò)是否處于預(yù)測狀態(tài)來對網(wǎng)絡(luò)的可信性進(jìn)行驗(yàn)證.在給定的神經(jīng)網(wǎng)絡(luò)與輸入集合時(shí)，為網(wǎng)絡(luò)的輸出預(yù)測一個(gè)范圍并且可以保證所有的輸出均為該范圍內(nèi)的子集，通過非線性激活函數(shù)的分段線性化來定義神經(jīng)網(wǎng)絡(luò)語義到混合整數(shù)約束的編碼，將輸入約束添加到MILP中使得輸出變量分別實(shí)現(xiàn)最大化和最小化來推斷安全范圍，同時(shí)MILP查詢比較是否存在比局部極小值更優(yōu)的解來對局部最優(yōu)進(jìn)行選擇，從而達(dá)到利用神經(jīng)網(wǎng)絡(luò)的局部特性同時(shí)又解決了局部最小值的目的.Souradeep Dutta等人[52]提出一種有效的范圍估計(jì)算法，它在使用混合整數(shù)線性規(guī)劃問題的全局組合搜索和重復(fù)尋找由神經(jīng)網(wǎng)絡(luò)表示的函數(shù)的局部最優(yōu)的局部優(yōu)化之間迭代，通過修剪次優(yōu)節(jié)點(diǎn)，有效地減少了神經(jīng)網(wǎng)絡(luò)中活動(dòng)神經(jīng)元可能的組合搜索.Michael E.Akintunde等人[53]提出了一種基于MILP的代理-環(huán)境系統(tǒng)的驗(yàn)證，其中代理是通過前饋神經(jīng)網(wǎng)絡(luò)實(shí)現(xiàn)的，環(huán)境是不確定的.關(guān)于該類系統(tǒng)對CTL屬性的驗(yàn)證問題，假設(shè)神經(jīng)網(wǎng)絡(luò)與非確定性環(huán)境交互，其中環(huán)境狀態(tài)的非確定性使神經(jīng)網(wǎng)絡(luò)不能完全控制更新和觀察環(huán)境狀態(tài)，基于該假設(shè)下的系統(tǒng)演化不是線性的，而是針對分支時(shí)間時(shí)序邏輯研究這類系統(tǒng)的驗(yàn)證問題，即通過將系統(tǒng)在有限的執(zhí)行步驟中神經(jīng)網(wǎng)絡(luò)應(yīng)該產(chǎn)生的狀態(tài)編碼到MILP中進(jìn)行求解，驗(yàn)證系統(tǒng)在有限步驟的執(zhí)行下是否一直在安全狀態(tài)范圍里.Matteo Fischetti等人[54]研究了將神經(jīng)網(wǎng)絡(luò)建模為0-1的MILP并將對應(yīng)的輸出同ReLU結(jié)合通過二進(jìn)制的變量研究網(wǎng)絡(luò)的性質(zhì).Ansgar R?ssig等人[55]將MILP與逼近技術(shù)結(jié)合提出了一種驗(yàn)證神經(jīng)網(wǎng)絡(luò)輸入沒有獨(dú)立邊界的實(shí)例問題的求解器，建立比較線性逼近理論框架去處理ReLU對應(yīng)神經(jīng)網(wǎng)絡(luò)的線性松弛問題.

針對屬性可滿足問題的神經(jīng)網(wǎng)絡(luò)進(jìn)行可信性驗(yàn)證主要在于編碼時(shí)添加的約束，不管使用的是基于哪一種求解器的算法其核心都是對約束條件進(jìn)行一個(gè)求解的過程，只要添加的約束符合所要驗(yàn)證的屬性，那對應(yīng)求解出來的結(jié)果就是對神經(jīng)網(wǎng)絡(luò)可信性的說明.

4.3.2 狀態(tài)可達(dá)性研究

狀態(tài)可達(dá)性是神經(jīng)網(wǎng)絡(luò)在初始狀態(tài)經(jīng)過一個(gè)或多個(gè)操作之后下一個(gè)狀態(tài)是否達(dá)到的是預(yù)期狀態(tài)的問題，其對應(yīng)的就是在神經(jīng)網(wǎng)絡(luò)輸入/輸出范圍問題的基礎(chǔ)上根據(jù)一定的規(guī)則推斷出網(wǎng)絡(luò)的狀態(tài)從而將神經(jīng)網(wǎng)絡(luò)可信性問題轉(zhuǎn)換成網(wǎng)絡(luò)的可達(dá)性問題進(jìn)行研究，將可達(dá)性問題用于神經(jīng)網(wǎng)絡(luò)的可信性驗(yàn)證的研究主要有兩種：

A.通過神經(jīng)網(wǎng)絡(luò)函數(shù)值上下界之間值的可達(dá)性來驗(yàn)證網(wǎng)絡(luò)在不確定性下的可信性.

給定一個(gè)神經(jīng)網(wǎng)絡(luò)，用一個(gè)函數(shù)來計(jì)算輸入集與輸出函數(shù)值的上下界，假設(shè)給定條件該函數(shù)為 Lipschitz連續(xù)函數(shù)時(shí)該函數(shù)是通用的即上下界區(qū)間內(nèi)的所有值都是可達(dá)的，在證明了前饋神經(jīng)網(wǎng)絡(luò)函數(shù)是 Lipschitz連續(xù)時(shí)再進(jìn)一步證明了安全驗(yàn)證問題可以轉(zhuǎn)化為可達(dá)性求解問題，從而根據(jù)全局的最大值與最小值來對可達(dá)性問題求解來達(dá)到驗(yàn)證網(wǎng)絡(luò)可信性的目的.Wenjie Ruan等人[23]通過實(shí)例化可達(dá)性問題來對神經(jīng)網(wǎng)絡(luò)進(jìn)行安全驗(yàn)證、輸出范圍分析，并且針對可達(dá)性問題，提出了一種基于自適應(yīng)嵌套優(yōu)化的新算法對網(wǎng)絡(luò)的可信性進(jìn)行驗(yàn)證.

B.通過對神經(jīng)網(wǎng)絡(luò)輸出集的可達(dá)性與輸出范圍結(jié)合分析來驗(yàn)證網(wǎng)絡(luò)在不確定性下的的可信性.

神經(jīng)網(wǎng)絡(luò)被看成一個(gè)黑盒時(shí)，對給定輸入產(chǎn)生所需要的輸出時(shí)可能由于各種原因會(huì)導(dǎo)致不安全輸出，因此研究一個(gè)可能覆蓋所有神經(jīng)網(wǎng)絡(luò)輸出值的輸出可達(dá)集來對網(wǎng)絡(luò)進(jìn)行安全分析，對網(wǎng)絡(luò)的可信性驗(yàn)證來說十分重要，驗(yàn)證示意圖如圖4所示.Weiming Xiang[56]等人通過計(jì)算神經(jīng)網(wǎng)絡(luò)的輸出損失對于輸入與權(quán)重之間的數(shù)學(xué)期望來表示有界輸入下輸出的最大偏差，稱其為最大靈敏度，通過輸入空間的離散化來實(shí)現(xiàn)對輸入集的窮舉搜索，組合模擬產(chǎn)生的每層靈敏度以獲得輸出可達(dá)集的估計(jì)，將神經(jīng)網(wǎng)絡(luò)的輸出可達(dá)集估計(jì)問題公式化為一系列優(yōu)化問題，最后通過檢查估計(jì)的可達(dá)集和不安全區(qū)域之間的交集來對網(wǎng)絡(luò)進(jìn)行安全驗(yàn)證.S.Dutta等人[14]提出了一種基于MILP的算法專門用來對使用ReLU作為激活函數(shù)的神經(jīng)網(wǎng)絡(luò)進(jìn)行輸出范圍分析.Shiqi Wang等人[57]提出了通過符號區(qū)間算法來根據(jù)神經(jīng)網(wǎng)絡(luò)的輸入范圍去估計(jì)網(wǎng)絡(luò)的輸出范圍，即給定網(wǎng)絡(luò)的輸入范圍以及安全屬性，通過ReluVal按照神經(jīng)網(wǎng)絡(luò)傳播的方向計(jì)算出對應(yīng)的輸出范圍，同時(shí)設(shè)計(jì)誤差估計(jì)優(yōu)化算法提高輸出范圍的準(zhǔn)確率，如果在估計(jì)的輸出范圍里能夠滿足網(wǎng)絡(luò)的屬性則表明網(wǎng)絡(luò)的屬性得到驗(yàn)證，反之則在區(qū)間中抽取輸入檢查不安全情況，當(dāng)檢查到有與網(wǎng)絡(luò)屬性不符輸入的情況時(shí)，將其作為反例輸出.Guoqing Yang等人[58]在ReLU為激活函數(shù)的神經(jīng)網(wǎng)絡(luò)中使用 SHERLOCK驗(yàn)證工具對神經(jīng)網(wǎng)絡(luò)的輸出集進(jìn)行估計(jì)從而驗(yàn)證神經(jīng)網(wǎng)絡(luò)的可信性.Chih-Hong Cheng等人[59]提出了一種基于假設(shè)保證的神經(jīng)網(wǎng)絡(luò)驗(yàn)證方法，通過學(xué)習(xí)一個(gè)輸入屬性特征描述器，使得輸入滿足一定的約束前提時(shí)，神經(jīng)網(wǎng)絡(luò)的輸出不會(huì)出現(xiàn)預(yù)期以外的情況，通過把輸入集的特征聚合到神經(jīng)網(wǎng)絡(luò)的輸出中，再通過詢問輸入特征網(wǎng)絡(luò)是否可以輸出為true來解決安全驗(yàn)證問題從而直接對感知神經(jīng)網(wǎng)絡(luò)的安全性進(jìn)行驗(yàn)證.

圖4 輸出可達(dá)驗(yàn)證示意圖Fig.4 Output up to validation diagram

綜上對于關(guān)注輸入/輸出范圍問題下神經(jīng)網(wǎng)絡(luò)由于黑盒導(dǎo)致不確定性的神經(jīng)網(wǎng)絡(luò)可信性驗(yàn)證可以通過保證在初始狀態(tài)下部署的每一個(gè)狀態(tài)都能到達(dá)安全狀態(tài)來驗(yàn)證，或者可以通過在輸入/輸出范圍下來對網(wǎng)絡(luò)的輸出集進(jìn)行一個(gè)估計(jì)，使得網(wǎng)絡(luò)的輸出包含于該估計(jì)，同時(shí)該估計(jì)與不安全狀態(tài)不產(chǎn)生交集從而驗(yàn)證網(wǎng)絡(luò)的可信性，也由于該方法是基于區(qū)間范圍，其對于神將網(wǎng)絡(luò)的可用性、可靠性以及不確定性的驗(yàn)證比較有效，而關(guān)于網(wǎng)絡(luò)的安全性、魯棒性等屬性的驗(yàn)證具有一定局限性.

4.4 總 結(jié)

根據(jù)上述討論，在表1中分類總結(jié)了現(xiàn)有驗(yàn)證神經(jīng)網(wǎng)絡(luò)可信性的形式化方法，并結(jié)合對應(yīng)的基于反例驗(yàn)證、抽象解釋、可滿足性求解、輸入/輸出可達(dá)性4類不同的問題對網(wǎng)絡(luò)滿足的屬性驗(yàn)證的情況進(jìn)行分析.

表1 神經(jīng)網(wǎng)絡(luò)驗(yàn)證方法歸納說明Table 1 Summary of the neural network validation method

5 發(fā)展趨勢展望

神經(jīng)網(wǎng)絡(luò)在各類應(yīng)用上部署的廣泛性使其發(fā)展取得了可觀的成效，在人工智能領(lǐng)域作用越來越大，因此其安全方面的可信性研究逐漸成為人們關(guān)注的重點(diǎn)，研究的深入使得許多問題也逐漸暴露出來，因此，關(guān)于未來的研究可以考慮以下幾個(gè)方面：

1)魯棒性

神經(jīng)網(wǎng)絡(luò)的輸出結(jié)果受輸入集影響很大，即使是微小的擾動(dòng)對于網(wǎng)絡(luò)的輸出來說可能會(huì)得到一個(gè)完全顛覆的結(jié)果，因此，神經(jīng)網(wǎng)絡(luò)魯棒性的研究對于網(wǎng)絡(luò)可信性驗(yàn)證至關(guān)重要，在一定的程度內(nèi)保證神經(jīng)網(wǎng)絡(luò)具有容錯(cuò)性，使得輸出受干擾的影響盡可能降低，網(wǎng)絡(luò)的安全可信性得到保證.

2)定量驗(yàn)證

隨著研究的深入，單純的定性分析已經(jīng)不能夠滿足安全性的說明，近期有人引入定量驗(yàn)證的方法來對神經(jīng)網(wǎng)絡(luò)安全性進(jìn)行驗(yàn)證，如Teodora Baluta等人[60]提出了對神經(jīng)網(wǎng)絡(luò)的定量驗(yàn)證，從驗(yàn)證神經(jīng)網(wǎng)絡(luò)是否違反了屬性轉(zhuǎn)變成有多少輸入能夠滿足屬性.提供了一個(gè)新的分析框架將神經(jīng)網(wǎng)絡(luò)與屬性的給定集合建模為邏輯約束集合，使得量化神經(jīng)網(wǎng)絡(luò)滿足屬性的數(shù)量問題簡化為對屬性的模型計(jì)數(shù)問題，以定量的形式對神經(jīng)網(wǎng)絡(luò)屬性進(jìn)行滿足性驗(yàn)證.隨著定量分析概念的提出，關(guān)于該方法的研究也引起人們的關(guān)注，Du Xiaoning等人[61]基于遞歸神經(jīng)網(wǎng)絡(luò)，提出了一個(gè)定量分析框架(DeepStellar)用于在輸入出現(xiàn)擾動(dòng)時(shí)進(jìn)行安全分析，在其基礎(chǔ)上開發(fā)對抗樣本監(jiān)測器，檢測對抗攻擊從而保證神經(jīng)網(wǎng)絡(luò)的可信性.近年來神經(jīng)網(wǎng)絡(luò)驗(yàn)證主要在于定性上面，定量分析驗(yàn)證的提出為網(wǎng)絡(luò)可信性驗(yàn)證提供了一種新且有效的研究思路，值得人們進(jìn)入更深層次的研究.

3)特征提取[62]的準(zhǔn)確性

神經(jīng)網(wǎng)絡(luò)可信性驗(yàn)證屬性中輸入集的處理至關(guān)重要，而神經(jīng)網(wǎng)絡(luò)最初在處理輸入集的時(shí)候是一個(gè)特征提取過程，可以說特征的提取直接關(guān)系到網(wǎng)絡(luò)可信性驗(yàn)證結(jié)果.例如，圖像識別一只貓，連初始提取貓的特征都不正確，最后不可能得到正確的識別結(jié)果，并且目前關(guān)于人工智能的應(yīng)用部署里大部分都是基于特征提取而展開工作，因此，特征提取的準(zhǔn)確性是最后可信性驗(yàn)證的先決條件，也是需要考慮的關(guān)鍵之處.

4)可信性形式化驗(yàn)證方法的拓展

隨著研究的深入，神經(jīng)網(wǎng)絡(luò)的訓(xùn)練不足以體現(xiàn)網(wǎng)絡(luò)的安全性，近幾年使用形式化方法對網(wǎng)絡(luò)可信性驗(yàn)證處于快速發(fā)展階段，許多現(xiàn)有的方法還具有各自的局限性，所以，對于驗(yàn)證方法的完善以及提出創(chuàng)新性的方法和工具依舊是需要關(guān)注的重點(diǎn)之一.

5)神經(jīng)網(wǎng)絡(luò)可信性驗(yàn)證規(guī)范和驗(yàn)證技術(shù)的發(fā)展

神經(jīng)網(wǎng)絡(luò)在各類人工智能項(xiàng)目中的廣泛應(yīng)用使得對其可信性要求越來越高，也因此形式化方法驗(yàn)證神經(jīng)網(wǎng)絡(luò)可信性的研究成為熱潮，同時(shí)驗(yàn)證規(guī)范與驗(yàn)證技術(shù)要求會(huì)隨著發(fā)展逐漸嚴(yán)格，值得人們進(jìn)行更深入的研究.

6 結(jié) 語

由于對神經(jīng)網(wǎng)絡(luò)可信性要求的提高，關(guān)于其可信性驗(yàn)證成為近年來的研究熱點(diǎn)，除了早期的循環(huán)訓(xùn)練改善網(wǎng)絡(luò)以外，本文分類綜述了神經(jīng)網(wǎng)絡(luò)可信性研究的一系列屬性、可信性問題的抽象表達(dá)，并通過形式化的方法對神經(jīng)網(wǎng)絡(luò)可信性驗(yàn)證的研究現(xiàn)狀，對基于反例驗(yàn)證、抽象解釋、可滿足性求解、輸入/輸出可達(dá)性分析等問題驗(yàn)證過程的核心算法進(jìn)行闡述，最后提出目前發(fā)展的瓶頸、需考慮的問題以及未來的發(fā)展趨勢.