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

在審

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

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

步驟S1：?jiǎn)伪槌橄蠓治?；?duì)一個(gè)給定的輸入域在神經(jīng)網(wǎng)絡(luò)的抽象語(yǔ)義下進(jìn)行逐層推導(dǎo)，得到其對(duì)應(yīng)的輸出；

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

步驟S3：輸入域劃分；對(duì)于給定的輸入域，若單遍抽象分析產(chǎn)生的不變式無(wú)法驗(yàn)證性質(zhì)是否成立時(shí)，則采用非確定首層神經(jīng)元引導(dǎo)的劃分策略產(chǎn)生劃分謂詞，再基于劃分謂詞對(duì)輸入域進(jìn)行劃分，生成兩個(gè)子驗(yàn)證問(wèn)題；

步驟S4：子驗(yàn)證問(wèn)題精化；在每個(gè)子驗(yàn)證問(wèn)題中，利用劃分謂詞對(duì)輸入變量的區(qū)間值范圍進(jìn)行精化；

步驟S5：迭代驗(yàn)證；對(duì)于每個(gè)無(wú)法驗(yàn)證的子問(wèn)題，重復(fù)步驟S1至S4。

2.根據(jù)權(quán)利要求1所述的基于迭代抽象分析的神經(jīng)網(wǎng)絡(luò)安全性質(zhì)驗(yàn)證方法，其特征在于，所述步驟S1的步驟包括：

步驟S11：基于上一層神經(jīng)元的抽象表示計(jì)算當(dāng)前層神經(jīng)元執(zhí)行ReLU激活函數(shù)之前的抽象表示；

步驟S12：基于ReLU激活函數(shù)之前的抽象表示，對(duì)于激活函數(shù)狀態(tài)無(wú)法確定的神經(jīng)元利用線性松弛技術(shù)，近似計(jì)算ReLU激活函數(shù)執(zhí)行之后的抽象表示；

步驟S13：從輸入層開(kāi)始，重復(fù)步驟S11和S12直到計(jì)算出輸出層神經(jīng)元的抽象表示。

3.根據(jù)權(quán)利要求2所述的基于迭代抽象分析的神經(jīng)網(wǎng)絡(luò)安全性質(zhì)驗(yàn)證方法，其特征在于，所述步驟S11中神經(jīng)元抽象表示的計(jì)算方式是：

給定一個(gè)神經(jīng)網(wǎng)絡(luò)N，設(shè)它的輸入向量是X＝{x₁,x₂…,x_n},其中n是輸入層的維度；對(duì)于每個(gè)輸入神經(jīng)元，引入表示它的區(qū)間值范圍，其中x_i,都是數(shù)值常量；則稱(chēng)為N的區(qū)間輸入域；

對(duì)于神經(jīng)網(wǎng)絡(luò)每個(gè)神經(jīng)元s，定義它的抽象數(shù)據(jù)表示為(R_s,A_s)，其中A_s表示神經(jīng)元s的激活狀態(tài)；具體而言，它有三種可能狀態(tài)：激活、不激活和狀態(tài)未知；R_s表示節(jié)點(diǎn)的抽象值表示，它是一個(gè)四元組其中：

(1)分別表示神經(jīng)元s執(zhí)行激活函數(shù)之前或后的符號(hào)化下界和上界，它們都是基于輸入層神經(jīng)元的線性表示；

(2)分別表示符號(hào)表達(dá)式的值下界和值上界；類(lèi)似地，表示了符號(hào)表達(dá)式的的值下界和值上界；

整個(gè)神經(jīng)網(wǎng)絡(luò)N的抽象表示記作(R,A)，即為N中的每個(gè)神經(jīng)元都維護(hù)上述抽象數(shù)據(jù)表示。

4.根據(jù)權(quán)利要求3所述的基于迭代抽象分析的神經(jīng)網(wǎng)絡(luò)安全性質(zhì)驗(yàn)證方法，其特征在于，首先，單個(gè)神經(jīng)元s的符號(hào)化上下界的計(jì)算依賴(lài)于上一層節(jié)點(diǎn)的輸出，如果s位于隱含層第一層，則:

其中，w₁,w₂,…,w_n表示神經(jīng)網(wǎng)絡(luò)中對(duì)應(yīng)邊的權(quán)重值，b表示該神經(jīng)元的偏移值；如果s位于隱含層第j(j≥2)層或者輸出層，則：

其中，y_i表示前一隱含層(即第(j-1)層)的第i個(gè)神經(jīng)元，且：

其次，對(duì)于神經(jīng)元s,基于其符號(hào)化上下界以及神經(jīng)網(wǎng)絡(luò)的區(qū)間輸入域D，直接計(jì)算出的值上下界和

再次，基于神經(jīng)元s當(dāng)前的激活狀態(tài)和計(jì)算得到的值上下界和對(duì)它的激活狀態(tài)進(jìn)行更新，并將更新后的激活狀態(tài)記為′：

5.根據(jù)權(quán)利要求4所述的基于迭代抽象分析的神經(jīng)網(wǎng)絡(luò)安全性質(zhì)驗(yàn)證方法，其特征在于，所述步驟S12中計(jì)算ReLU函數(shù)執(zhí)行之后神經(jīng)元抽象表示的線性松弛公式是：