[發(fā)明專利]一種基于迭代抽象分析的神經(jīng)網(wǎng)絡(luò)安全性質(zhì)驗證方法

在審

• 申請?zhí)枺?/td>: 202010382022.4
• 申請日: 2020-05-08
• 公開（公告）號: CN111475321A
• 公開（公告）日: 2020-07-31
• 發(fā)明（設(shè)計）人: 陳立前;尹幫虎;王戟;劉江潮;董威;毛曉光;文艷軍;劉萬偉;尹良澤
• 申請（專利權(quán)）人: 中國人民解放軍國防科技大學(xué)
• 主分類號: G06F11/00
• 分類號: G06F11/00;G06N3/04;G06N3/08
• 代理公司: 湖南兆弘專利事務(wù)所(普通合伙) 43008
• 代理人: 周長清

本發(fā)明公開了一種基于迭代抽象分析的神經(jīng)網(wǎng)絡(luò)安全性質(zhì)驗證方法，其步驟包括：步驟S1：單遍抽象分析；對一個給定的輸入域在神經(jīng)網(wǎng)絡(luò)的抽象語義下進(jìn)行逐層推導(dǎo)，得到其對應(yīng)的輸出；步驟S2：基于不變式進(jìn)行性質(zhì)驗證；通過檢查不變式與待驗證性質(zhì)的關(guān)系，判斷性質(zhì)是否成立；步驟S3：輸入域劃分；對于給定的輸入域，若單遍抽象分析產(chǎn)生的不變式無法驗證性質(zhì)是否成立時，則采用非確定首層神經(jīng)元引導(dǎo)的劃分策略產(chǎn)生劃分謂詞，再基于劃分謂詞對輸入域進(jìn)行劃分，生成兩個子驗證問題；步驟S4：子驗證問題精化；驟S5：迭代驗證；對于每個無法驗證的子問題，重復(fù)上述步驟。本發(fā)明具有原理簡單、能夠提高神經(jīng)網(wǎng)絡(luò)安全性質(zhì)完備驗證的效率等優(yōu)點。

技術(shù)領(lǐng)域

本發(fā)明主要涉及到神經(jīng)網(wǎng)絡(luò)技術(shù)領(lǐng)域，特指一種基于迭代抽象分析的神經(jīng)網(wǎng)絡(luò)安全性質(zhì)驗證方法。

背景技術(shù)

神經(jīng)網(wǎng)絡(luò)近年來被廣泛應(yīng)用于安全攸關(guān)領(lǐng)域，包括自動駕駛、醫(yī)療診斷、飛行器防碰撞系統(tǒng)等。在此類系統(tǒng)中，任何一個安全性質(zhì)被違背都可能帶來非常嚴(yán)重的后果。例如，近些年，特斯拉自動駕駛系統(tǒng)因故障出現(xiàn)多起車毀人亡的事件。通常情況下，安全攸關(guān)系統(tǒng)都進(jìn)行了盡可能充分的測試，但這些測試難以保證在極端場景下系統(tǒng)的高可靠性。因此，確保神經(jīng)網(wǎng)絡(luò)系統(tǒng)的高可靠性已經(jīng)成為人工智能技術(shù)在安全攸關(guān)領(lǐng)域廣泛應(yīng)用的重要前提。

驗證技術(shù)是判斷一個神經(jīng)網(wǎng)絡(luò)系統(tǒng)是否可靠的重要途徑。具體而言，驗證問題是指給定一組關(guān)于輸入的約束，對于輸入約束中變量的每一組可能的具體取值，經(jīng)過神經(jīng)網(wǎng)絡(luò)的逐層計算，都會得到一組輸出，判斷這些輸出是否滿足預(yù)先設(shè)定的關(guān)于輸出的一組約束(即安全性質(zhì))。

現(xiàn)有的基于區(qū)間傳播的神經(jīng)網(wǎng)絡(luò)安全性質(zhì)完備驗證方法包括以下四個步驟：

S1:基于區(qū)間值傳播的單遍抽象分析。

S2:性質(zhì)驗證。

S3:基于區(qū)間二分法的輸入域劃分。

S4:對于劃分得到的子驗證問題，重復(fù)步驟S1至S3。

現(xiàn)有的神經(jīng)網(wǎng)絡(luò)安全性質(zhì)完備驗證技術(shù)存在的主要缺點是驗證效率低，具體原因來自以下三個方面：

1)單遍抽象分析精度低；目前基于區(qū)間值傳播的抽象分析過程在碰到ReLU激活函數(shù)時，需要利用ReLU函數(shù)之前的符號表示計算出ReLU函數(shù)之后的神經(jīng)元的數(shù)值區(qū)間范圍,該過程丟失了神經(jīng)元之間的線性關(guān)系，從而導(dǎo)致逐層計算過程中引入大量精度損失。由于精度損失會逐層傳播并放大，其后果是導(dǎo)致單遍抽象分析的精度很低，不足以驗證性質(zhì)是否成立，導(dǎo)致單遍抽象驗證成功率低。

2)未利用待驗證的目標(biāo)性質(zhì)；目前迭代驗證過程中，每次都只利用了前向抽象分析產(chǎn)生的不變式來判斷性質(zhì)是否成立，而未利用待驗證性質(zhì)對待驗證問題進(jìn)行優(yōu)化，從而導(dǎo)致迭代驗證的目標(biāo)性不強，驗證效率低。

3)劃分方法過于簡單和盲目；目前的劃分方法是從輸入層選取一個神經(jīng)元，對神經(jīng)元的數(shù)值區(qū)間范圍進(jìn)行二分,得到兩個子區(qū)間，再對每個子區(qū)間進(jìn)行驗證。這種劃分方法沒有考慮神經(jīng)網(wǎng)絡(luò)的結(jié)構(gòu)特征，導(dǎo)致劃分得到的子區(qū)間與原來的區(qū)間相比，對于驗證性質(zhì)是否成立的效果不顯著，從而使得需要很深的劃分深度才能驗證性質(zhì)，驗證效率低。

發(fā)明內(nèi)容

本發(fā)明要解決的技術(shù)問題就在于：針對現(xiàn)有技術(shù)存在的技術(shù)問題，本發(fā)明提供一種原理簡單、能夠提高神經(jīng)網(wǎng)絡(luò)安全性質(zhì)完備驗證的效率、降低時間開銷的基于迭代抽象分析的神經(jīng)網(wǎng)絡(luò)安全性質(zhì)驗證方法。

為解決上述技術(shù)問題，本發(fā)明采用以下技術(shù)方案：

一種基于迭代抽象分析的神經(jīng)網(wǎng)絡(luò)安全性質(zhì)驗證方法，其步驟包括：

步驟S1：單遍抽象分析；對一個給定的輸入域在神經(jīng)網(wǎng)絡(luò)的抽象語義下進(jìn)行逐層推導(dǎo)，得到其對應(yīng)的輸出；

步驟S2：基于不變式進(jìn)行性質(zhì)驗證；通過檢查不變式與待驗證性質(zhì)的關(guān)系，判斷性質(zhì)是否成立；