基于Softplus函數(shù)的神經(jīng)網(wǎng)絡(luò)的Reluplex算法驗(yàn)證研究

陸明遠(yuǎn) 侯春燕 王勁松

(天津理工大學(xué)計(jì)算機(jī)科學(xué)與工程學(xué)院 天津 300384)

(1933044495@qq.com)

形式化驗(yàn)證是通過(guò)數(shù)學(xué)方法證明一個(gè)系統(tǒng)沒(méi)有漏洞且實(shí)現(xiàn)了設(shè)計(jì)者的規(guī)劃，在軟硬件檢測(cè)中都有較多應(yīng)用.人工神經(jīng)網(wǎng)絡(luò)則在人工智能領(lǐng)域和相關(guān)的工業(yè)生產(chǎn)中不可或缺.既然要了解一個(gè)神經(jīng)網(wǎng)絡(luò)系統(tǒng)的綜合性能并評(píng)價(jià)和檢驗(yàn)其自我學(xué)習(xí)的效果，就必須采用合適方式來(lái)驗(yàn)證神經(jīng)網(wǎng)絡(luò)，可以充分地運(yùn)用形式化驗(yàn)證的方法來(lái)進(jìn)行指導(dǎo)和輔助[1-2].在進(jìn)行神經(jīng)網(wǎng)絡(luò)驗(yàn)證方面的研究時(shí)，通過(guò)對(duì)深度神經(jīng)網(wǎng)絡(luò)選擇不同的激活函數(shù)進(jìn)行測(cè)試和比較研究，能更好地了解神經(jīng)網(wǎng)絡(luò)的魯棒性、感知能力和深度學(xué)習(xí)能力[3]，并對(duì)比分析不同激活函數(shù)的適用性，從而更有利于對(duì)神經(jīng)網(wǎng)絡(luò)深度學(xué)習(xí)的總體研究[4].

1 研究現(xiàn)狀

近年來(lái)形式化驗(yàn)證的實(shí)踐方法在不斷發(fā)展，其應(yīng)用層面涉及到測(cè)驗(yàn)IEEE標(biāo)準(zhǔn)、客戶端與服務(wù)端傳輸數(shù)據(jù)校驗(yàn)、程序穩(wěn)定性等.形式化驗(yàn)證的相關(guān)應(yīng)用軟件也逐漸成為各大廠商愿意進(jìn)行商業(yè)投資的方向之一[5-6].

數(shù)十年來(lái)在仿照高等動(dòng)物的神經(jīng)網(wǎng)絡(luò)系統(tǒng)對(duì)信息進(jìn)行反饋功能的機(jī)制下[7]，人工神經(jīng)網(wǎng)絡(luò)已能高效完成許多看似艱巨的任務(wù)計(jì)劃[8]，其結(jié)構(gòu)框架也在愈發(fā)復(fù)雜深邃化，解決工業(yè)、服務(wù)業(yè)和學(xué)術(shù)研究方面的能力普遍增強(qiáng)[9].而Reluplex作為針對(duì)神經(jīng)網(wǎng)絡(luò)錯(cuò)誤進(jìn)行檢驗(yàn)校對(duì)的算法，充分運(yùn)用了形式化驗(yàn)證技術(shù)與可滿足性模理論(SMT)的方法，可以采用具體的輸入數(shù)據(jù)充分驗(yàn)證各個(gè)神經(jīng)網(wǎng)絡(luò)的特性，對(duì)研究和優(yōu)化神經(jīng)網(wǎng)絡(luò)的深度學(xué)習(xí)能力有很大幫助[10-11].

2 Reluplex算法簡(jiǎn)介

單純形算法(Simplex)是迭代算法的1個(gè)子類型，該算法一般先嘗試假設(shè)出1個(gè)最初的解集并進(jìn)行代入測(cè)試，隨后分析出這個(gè)解集是否為問(wèn)題的最優(yōu)解.如果不是，就在目前已有解的基礎(chǔ)上通過(guò)約束條件優(yōu)化得到1組更合適的解集，于是不斷地迭代更替下去，目標(biāo)參數(shù)越來(lái)越接近于期望值.Reluplex算法則將Simplex應(yīng)用于深度神經(jīng)網(wǎng)絡(luò)驗(yàn)證領(lǐng)域，它擅長(zhǎng)于驗(yàn)證無(wú)人機(jī)是否會(huì)發(fā)生碰撞的安全性事故[10].Reluplex允許互為決定的非基本變量Xb，Xf暫時(shí)不符合邏輯關(guān)系，以Update操作與迭代操作糾偏之前的取值范圍與等式關(guān)系[10]，這是其之于Simplex的改進(jìn).

(1)

(2)

(3)

(4)

(5)

下標(biāo)b和i表示輸入，f和j表示輸出，l表示下限.在Reluplex的5點(diǎn)基本操作中，Updateb與Updatef均是給非基本變量重新賦值，以糾正其之前的數(shù)值超出取值范圍的錯(cuò)誤，導(dǎo)致式子左邊的基本變量超出取值范圍，就要采用PivotForRelu操作來(lái)迭代，將其移到右邊與非基本變量相互易位，若引起方程組內(nèi)別的式子里的基本變量也超出取值范圍，便繼續(xù)迭代，最終方程組內(nèi)任何式子都符合各個(gè)限制規(guī)則.ReluSplit操作采取拆分的方式判定lower(Xi)=0與upper(Xi)=0時(shí)Relu分別為激活狀態(tài)與未激活狀態(tài).ReluSuccess操作則設(shè)定Xb與Xf在邏輯上的相互關(guān)系，若Xb>0，則將Xf調(diào)整成等同于Xb；若Xb≤0，Xf則調(diào)整成0[10]，所有變量最終都要符合約束條件.而Relu激活函數(shù)在深度學(xué)習(xí)算法中相對(duì)較為常見(jiàn)[12-13]，它在輸入的數(shù)值為負(fù)數(shù)時(shí)，始終保持對(duì)外輸出數(shù)值0；而在輸入的數(shù)值為正數(shù)時(shí)，輸出則保持與其輸入量一致.

Relu激活函數(shù)(如圖1所示)為

圖1 Relu激活函數(shù)圖像

3 算法設(shè)計(jì)

3.1 理論分析

Relu激活函數(shù)也有著自身的局限性.由于它在負(fù)半軸上的斜率始終為0并保持輸出0，這使得它在具體的環(huán)境下很容易變成“垂死的Relu”，從而在訓(xùn)練深度神經(jīng)網(wǎng)絡(luò)的過(guò)程中表現(xiàn)得非常脆弱[14].在這種情況下，需要對(duì)Relu激活函數(shù)進(jìn)行改進(jìn)，將其替換成其他與之類似的激活函數(shù)進(jìn)行測(cè)試，進(jìn)行相應(yīng)的比較研究，從而能更好地了解深度神經(jīng)網(wǎng)絡(luò)的安全性和不同激活函數(shù)的適用性[15].將Reluplex算法中所運(yùn)用的Relu函數(shù)更換成比其更平滑的Softplus函數(shù)，可以改良其算法的實(shí)現(xiàn)效果[16].可以將Softplus視為比ReLu更平滑的近似替代品，根據(jù)神經(jīng)科學(xué)家的相關(guān)研究，Softplus比Relu更加接近腦神經(jīng)元的激活模型[17-18].

Softplus函數(shù)(如圖2所示)為

f(x)=ln(1+ex).

圖2 Softplus的函數(shù)圖像

Softplus的導(dǎo)函數(shù)(如圖3所示)則為

圖3 Softplus的導(dǎo)函數(shù)圖像

如圖4所示，當(dāng)x較小時(shí)，Softplus的斜率接近于0，比Relu函數(shù)要平滑得多，隨著x的逐漸增大，Softplus的導(dǎo)函數(shù)越來(lái)越無(wú)限接近于1，從而逐漸與Relu函數(shù)趨同起來(lái).

圖4 Relu激活函數(shù)和Softplus激活函數(shù)的對(duì)比

Updateb1=(Xi?B,(Xi,Xj)∈,α(Xj)≠

(αupdate(α,Xi,α(Xj)-α(Xi))).

(6)

Updateb2=(Xi?B,(Xi,Xj)∈,α(Xj)≠

(αupdate(α,Xi,()·α(Xj)-α(Xi))).

(7)

Updatef=(Xj?B,(Xi,Xj)∈,α(Xj)≠

(αupdate(α,Xj,max(()·

α(Xi),α(Xi))-α(Xj))).

(8)

PivotForRelu=(Xi∈B,?Xl·(Xi,Xl)∈∨
(Xl,Xi)∈,Xj?B,Ti,j≠0)/
(Tpivot(Ti,j),BB∪{Xj}{Xi})，

(9)

(10)

PivotRelu和ReluSplit在處理的基本原則上仍然與原算法保持一致.

ReluSuccess=(?x∈,l(x)≤α(x)≤u(x),

?〈Xb,Xf〉∈,α(Xf)=max(()·

(11)

改進(jìn)后的Reluplex便具備了驗(yàn)證基于Softplus激活函數(shù)的神經(jīng)網(wǎng)絡(luò)的能力，此后還能對(duì)比這2種激活函數(shù)在效果上的不同.Softplus以自身特有的平滑的梯度直接避免了“垂死的Relu”的缺陷[19]，而Softplus的梯度又經(jīng)常小于1但永遠(yuǎn)不至于消失，在“均值激活”靠向0時(shí)，會(huì)使儲(chǔ)存信息的矩陣中有很小的非對(duì)角數(shù)值，從而神經(jīng)網(wǎng)絡(luò)的訓(xùn)練速度更快[20-21].Softplus所具有的靈活變化的非線性的導(dǎo)函數(shù)也使得神經(jīng)網(wǎng)絡(luò)的連接方式更符合其所需的非線性因素[22]，也有利于Softplus激活的神經(jīng)網(wǎng)絡(luò)的自我學(xué)習(xí)能力[23].Softplus較斜率恒定的Relu的平衡性能更強(qiáng)[24]，從而讓深度學(xué)習(xí)的效率進(jìn)一步提高[25-26].

3.2 算法實(shí)現(xiàn)

算法1.設(shè)定輸出與輸入的函數(shù)關(guān)系的斜率.

① voidexample1_Softplus

②Reluplex←newReluplex(9);

③p←ebound/(1+ebound);

④Reluplex→setSoftplusValue(p);

⑤update(Xb,(1/getSoftplusValue())·

Xf-Xb,true);

⑥ if ((!_dissolvedReluVariables.exists(Xf))

&&reluPairIsBroken(Xb,Xf))

⑦update((Xf,getSoftplusValue·

Xb)-Xf,true);

⑧ endif

如算法1，要更換所驗(yàn)證的激活函數(shù)，先將p賦值為Softplus的斜率，隨之需把輸入變量Xb設(shè)定成與輸出變量Xf相對(duì)應(yīng)，正好把Xb賦值為(1/getSoftplusValue())·Xf.若Xf并不存在或者Xf與Xb之間的關(guān)聯(lián)性已經(jīng)喪失，由于原先的輸入變量Xb還在，此時(shí)將Xf調(diào)整為getSoftplusValue·assignment[Xb].

算法2.分配并判斷變量是否一致的算法.

① boolReluPairIsBroken(Xb,Xf)

② doublebpoi←assignment[Xb];

③ doublefpoi←assignment[Xf];

④ return (fpoi≠bpoi·getSoftplusValue).

如算法2，Xf≠Xb·getSoftplusValue應(yīng)該更新，則輸出true.

算法3.設(shè)定取值上限的算法.

① if (ReluPairs=Xf)/*有待修復(fù)的數(shù)據(jù)作為輸出變量的Xf*/

②setupperBounds((1/getSoftplusValue)·

bound);

③ elsesetupperBounds(getSoftplusValue·

bound);

④ endif

如算法3，更新操作之前若需要對(duì)Xf更新，那么設(shè)定Xb的上標(biāo)(1/getSoftplusValue)·bound，如果需要對(duì)Xb更新，那么設(shè)定Xf的上界getSoftplusValue·bound，如此設(shè)定神經(jīng)網(wǎng)絡(luò)的輸出與輸入的比率關(guān)系.

算法4.根據(jù)Xf與Xb的基本條件進(jìn)行調(diào)整的算法.

① if (fpoi≥0) and (bpoi≥0)

② Δb←0;

③ Δf←0;

④ endif

⑤ else if (fpoi≥0) and (bpoi<0)

⑥ Δf←0;

⑦ Δb←(1/getSoftplusValue)·fpoi-

bpoi;

⑧ endif

⑨ else if (fpoi<0) and (bpoi≥0)

⑩ Δb←0;

bpoi;

如算法4，有“Xf≥0，Xb≥0”“Xf≥0，Xb<0”“Xf<0，Xb≥0”“Xf<0，Xb<0”4類條件，都根據(jù)具體條件調(diào)整Xf與Xb維持其與Softplus激活函數(shù)下關(guān)系對(duì)應(yīng).

算法5.積分累加的算法.

①u←ebound/(1+ebound);/*Softplus的斜率先前已賦過(guò)值*/

②integral(u(t),i,j,k);/*i是下限，j是上限，k是從下限到上限需經(jīng)歷的次數(shù)*/

③ {i←0;

④j←t;

⑤ Δl←(j-i)/k;

⑥t←i;

⑦sum←0;

⑧ for (a←0;a≤k;a←a+1) {

⑧t←t+Δl;/*激活函數(shù)的橫坐標(biāo)數(shù)值t不斷變化*/

⑩sum←sum+u(t) ·Δl;/*對(duì)每段積分進(jìn)行累加*/

為避免計(jì)算量無(wú)窮大，Reluplex對(duì)輸入數(shù)值的變更過(guò)程并非完全連續(xù)的，它以10-10為最小單位.如算法5通過(guò)積分累加的手段，輸入數(shù)值在橫坐標(biāo)上每經(jīng)過(guò)極短的長(zhǎng)度便更新1次斜率，Xf=Xf+f′(Xb)·setSoftplusValue，依次累加，得到輸出變量Xf與輸入變量Xb的近似于Softplus激活函數(shù)的關(guān)系，便能夠檢驗(yàn)基于Softplus激活函數(shù)的神經(jīng)網(wǎng)絡(luò).

算法6先將列鏈表內(nèi)的數(shù)值都存儲(chǔ)在對(duì)應(yīng)的矩陣中，再將需取代的行非空作為整個(gè)循環(huán)的基本條件，若將被取代的變量與新變量都在同一行，直接刪除列鏈表內(nèi)被取代的變量并重新調(diào)整相關(guān)系數(shù).再以函數(shù)addEntry重新補(bǔ)充相關(guān)系數(shù)，將輸出變量Xf的系數(shù)乘上其在該點(diǎn)的斜率SoftplusValue，結(jié)尾清除所有列.

算法6.矩陣操作的算法.

① voidreplaceNonBasicWithAnotherNonBasic

(beReplaced,replace,SoftplusValue)

② while (beReplacedEntry≠NULL)

③current←beReplacedEntry;

④beReplacedEntry←beReplacedEntry→

nextInColumn();

⑤rowcurrent→getRow();

⑥Entry·entryInTarget←NULL;

⑦ if (denseMap.exists(row))

⑧entryInTarget←denseMap[row];

⑨entryInTarget→getRow();

⑩entryInTarget→getColumn();

current→getValue());

SoftplusValue·current→

getValue());

denseMap.clear();

4 實(shí)驗(yàn)結(jié)果

在原Reluplex求解器中，Reluplex.h是其最主要的源程序，調(diào)整Reluplex.h的源代碼，使其激活函數(shù)由Relu變成Softplus，隨后分別對(duì)求解器的10個(gè)properties腳本文件進(jìn)行運(yùn)行測(cè)試，獲取輸出的數(shù)據(jù)信息與先前Relu激活函數(shù)下獲取的信息對(duì)比分析.還導(dǎo)入別的神經(jīng)網(wǎng)絡(luò)TestNetwork.nnet，TestNetwork2.nnet來(lái)檢驗(yàn)，使得其能更好地顯示驗(yàn)證效果.通過(guò)在Linux系統(tǒng)下分別測(cè)試2種激活函數(shù)下的properties腳本文件得到相應(yīng)的數(shù)據(jù)輸出文件，對(duì)其測(cè)試效果進(jìn)行對(duì)比評(píng)判.

無(wú)人機(jī)默認(rèn)由左向右行駛，由神經(jīng)網(wǎng)絡(luò)引導(dǎo)無(wú)人機(jī)躲避別的飛機(jī)，神經(jīng)網(wǎng)絡(luò)得到?jīng)_突解除(clear-of-conflict)信號(hào)則會(huì)放松警惕，驗(yàn)證無(wú)人機(jī)是否有潛在的碰撞的可能性，從而訓(xùn)練神經(jīng)網(wǎng)絡(luò)的魯棒對(duì)抗性.這10個(gè)腳本所對(duì)應(yīng)的10個(gè)特性都是無(wú)人機(jī)防撞系統(tǒng)中的不同基本情況.例如：前2個(gè)特性都是入侵的飛機(jī)距離較遠(yuǎn)且速度比無(wú)人機(jī)慢；第3個(gè)至第4個(gè)特性都是入侵者在正前方；第5個(gè)至第6個(gè)特性都是從左側(cè)入侵；第7個(gè)至第8個(gè)特性都垂直距離過(guò)大；第9個(gè)特性為從右側(cè)入侵；第10個(gè)特性則為入侵者極其遙遠(yuǎn).

在圖5～10的曲線中，標(biāo)記為“Softplus”和“Relu”后的數(shù)字是與其所對(duì)應(yīng)的測(cè)試的第幾個(gè)腳本文件.橫坐標(biāo)是無(wú)人機(jī)模擬系統(tǒng)的45個(gè)測(cè)試點(diǎn)(有的腳本的子程序?qū)?shù)據(jù)的約束條件使其僅能檢驗(yàn)其中的局部測(cè)試點(diǎn))，縱坐標(biāo)是各測(cè)試點(diǎn)的耗時(shí)，達(dá)到12 h說(shuō)明檢測(cè)超時(shí).每個(gè)腳本文件的子程序都設(shè)定相應(yīng)的輸入來(lái)違反其特性，測(cè)試結(jié)果為UNSAT表明違反不成功從而特性成立；測(cè)試結(jié)果為SAT則說(shuō)明違反特性成功，意味著無(wú)人機(jī)會(huì)有碰撞的風(fēng)險(xiǎn)性.

如圖5所示，在第1個(gè)特性文件中，Softplus函數(shù)則僅有8個(gè)測(cè)試點(diǎn)超時(shí)，其余測(cè)試點(diǎn)都得出了UNSAT的結(jié)果，而之前采用的Relu激活函數(shù)則有20個(gè)測(cè)試點(diǎn)超時(shí)且其他測(cè)試點(diǎn)耗時(shí)也多于Softplus.

圖5 第1個(gè)特性下測(cè)試點(diǎn)的情況

如圖6所示，第2個(gè)特性文件是從第10個(gè)測(cè)試點(diǎn)開(kāi)始的，Softplus下只有2個(gè)超時(shí)點(diǎn)，其余測(cè)試點(diǎn)都得出了SAT的結(jié)果，這與原算法采用Relu激活函數(shù)驗(yàn)證的結(jié)果完全一樣，并比Relu要節(jié)省時(shí)間.

圖6 第2個(gè)特性下測(cè)試點(diǎn)的情況

如圖7所示，在第3個(gè)特性文件中，Softplus激活函數(shù)沒(méi)有任何超時(shí)的測(cè)試點(diǎn)，這與之前使用的Relu函數(shù)的情況是一樣的，并在每個(gè)測(cè)試點(diǎn)上所停留的時(shí)間比Relu要短.

圖7 第3個(gè)特性下測(cè)試點(diǎn)的情況

如圖8所示，在第4個(gè)特性文件中，除前3個(gè)測(cè)試點(diǎn)耗時(shí)略多些，Softplus激活函數(shù)的其余測(cè)試點(diǎn)都在25 min以內(nèi)得到了結(jié)果.所有測(cè)試點(diǎn)均為UNSAT，與原求解器下Relu的驗(yàn)證情況一樣,但相對(duì)高效得多.

圖8 第4個(gè)特性下測(cè)試點(diǎn)的情況

如圖9所示，T1至T8為8個(gè)測(cè)試點(diǎn)，這些腳本的子程序僅能檢驗(yàn)其中的局部測(cè)試點(diǎn).Softplus激活函數(shù)在第6個(gè)到第9個(gè)特性文件的所有測(cè)試點(diǎn)都超時(shí)，這與原算法中Relu激活函數(shù)的驗(yàn)證結(jié)果完全相同.而第5個(gè)和第10個(gè)特性文件的驗(yàn)證結(jié)果則全部得出UNSAT的結(jié)果，相對(duì)而言原算法中Relu激活函數(shù)在第10個(gè)特性文件有1個(gè)超時(shí)點(diǎn),而在第5個(gè)特性文件的各個(gè)測(cè)試點(diǎn)所花的時(shí)間要更多一些.

圖9 第5～10個(gè)特性下測(cè)試點(diǎn)的情況

如圖10所示，在新引入不同的神經(jīng)網(wǎng)絡(luò)訓(xùn)練數(shù)據(jù)集后，4個(gè)特性文件和其對(duì)應(yīng)的各2個(gè)測(cè)試點(diǎn)也都得到了其驗(yàn)證結(jié)果，均為UNSAT，Softplus沒(méi)有發(fā)生超時(shí)情況，并比Relu所花時(shí)間要短一些.

圖10 新網(wǎng)絡(luò)里4個(gè)特性下測(cè)試點(diǎn)的情況

實(shí)驗(yàn)數(shù)據(jù)證實(shí)了改進(jìn)后的Reluplex算法完全具備驗(yàn)證Softplus激活函數(shù)的能力.Softplus函數(shù)在大多數(shù)測(cè)試點(diǎn)中均比Relu函數(shù)明顯節(jié)省時(shí)間并成功地解決了局部原本超時(shí)而無(wú)解的測(cè)試點(diǎn).

5 總 結(jié)

使Reluplex能檢驗(yàn)Softplus激活函數(shù)后，再對(duì)基于Softplus的無(wú)人機(jī)神經(jīng)網(wǎng)絡(luò)的所有測(cè)試點(diǎn)檢測(cè)并參照Relu下的結(jié)果進(jìn)行對(duì)比研究，可以看出Softplus訓(xùn)練神經(jīng)網(wǎng)絡(luò)的成效比Relu要迅速且平穩(wěn).

在選擇神經(jīng)網(wǎng)絡(luò)的激活函數(shù)時(shí)要盡可能將其平滑化和避免垂死的情況[27].通過(guò)對(duì)Softplus激活函數(shù)的深度神經(jīng)網(wǎng)絡(luò)驗(yàn)證研究，擴(kuò)展優(yōu)化了對(duì)神經(jīng)網(wǎng)絡(luò)進(jìn)行形式化驗(yàn)證的方法，并看到了激活函數(shù)不同時(shí)所具有的效果，最終成功地檢驗(yàn)了神經(jīng)網(wǎng)絡(luò)的安全性，證明了該技術(shù)在驗(yàn)證現(xiàn)實(shí)世界的深度神經(jīng)網(wǎng)絡(luò)的可靠性上有著不小的潛力.