亚洲免费av电影一区二区三区,日韩爱爱视频,51精品视频一区二区三区,91视频爱爱,日韩欧美在线播放视频,中文字幕少妇AV,亚洲电影中文字幕,久久久久亚洲av成人网址,久久综合视频网站,国产在线不卡免费播放

        ?

        面向形式化證明的命令生成技術(shù)①

        2022-02-15 06:41:16莫廣帥黃文超
        關(guān)鍵詞:命令定理向量

        莫廣帥,熊 焰,黃文超

        1(中國科學(xué)技術(shù)大學(xué) 網(wǎng)絡(luò)空間安全學(xué)院,合肥 230027)

        2(中國科學(xué)技術(shù)大學(xué) 計算機(jī)科學(xué)與技術(shù)學(xué)院,合肥 230027)

        近年來,隨著軟件規(guī)模的快速增大,軟件系統(tǒng)安全問題日益增多.因此,開發(fā)者需要在軟件開發(fā)的過程中減少軟件漏洞,保障軟件安全.形式化證明利用數(shù)學(xué)方法對軟件屬性進(jìn)行建模,驗證軟件是否滿足相應(yīng)的安全目標(biāo).形式化方法已成為構(gòu)建高可信軟件系統(tǒng)的有效手段.

        通常檢測和分析大規(guī)模軟件系統(tǒng)需要使用具有高階邏輯描述能力的工具,如Coq[1]、Isabelle HOL[2,3].在證明工具中,證明人員使用策略與工具交互證明定理.但是,這種證明方式存在一定局限性,需要消耗證明人員大量的時間和精力.因此,實現(xiàn)定理證明的自動化是必不可少且有意義的工作.

        目前,研究者提出了許多自動化證明工作.Paulson等[4]利用現(xiàn)有的ATP 系統(tǒng)證明定理.Gransden 等[5]從已經(jīng)編譯成功的證明庫中匹配當(dāng)前的上下文狀態(tài).Alemi等[6]第一次將深度學(xué)習(xí)算法應(yīng)用于大規(guī)模的定理證明.但是這些工作存在向量信息不足、命令生成不完備等問題.

        現(xiàn)有的自動定理證明工作面臨兩個挑戰(zhàn).1)策略空間大.在Coq中,證明人員需要從221 個策略庫中生成合適的策略.2)參數(shù)結(jié)構(gòu)復(fù)雜.策略參數(shù)可以由全局表達(dá)式、復(fù)雜的代碼行和全局中搜索出的中間引理組成.

        針對定理證明工具中的命令生成問題,本文提出了以下工作:1)將機(jī)器學(xué)習(xí)與Coq 結(jié)合,利用LSTM等網(wǎng)絡(luò)預(yù)測證明中的策略和參數(shù).2)結(jié)合注意力機(jī)制,自動關(guān)注在訓(xùn)練過程中起決定作用的特征,捕捉重要的信息,減少無用信息的關(guān)注.

        1 相關(guān)工作

        本節(jié)介紹近年來自動化證明方面的研究工作.現(xiàn)有的自動化證明工作可以分為結(jié)合自動定理證明和結(jié)合交互式證明兩類.

        1.1 結(jié)合自動定理證明

        隨著自動化定理證明和機(jī)器學(xué)習(xí)的發(fā)展,在不需要手工設(shè)計特征的情況下,Alemi 等[6]首次證明了神經(jīng)網(wǎng)絡(luò)模型有助于進(jìn)行大規(guī)模自動邏輯推理,并第一次將深度學(xué)習(xí)應(yīng)用于大規(guī)模的定理證明.Wang 等[7]提出了一種基于深度學(xué)習(xí)的前提選擇方法.他們將一個高階邏輯公式表示為一個圖,完全保留語法和語義信息.然后為圖的每個節(jié)點指定一個初始嵌入向量,將所有節(jié)點的嵌入集合起來形成整個圖的嵌入.這種方式提高了前提選擇的準(zhǔn)確性.但是,ATP[8]仍然需要將定理轉(zhuǎn)換為合取范式(CNF),復(fù)雜的軟件系統(tǒng)依舊無法證明.

        一些工作將現(xiàn)有的交互式定理證明與自動定理證明結(jié)合,允許用戶直接使用現(xiàn)有的ATP 系統(tǒng).Paulson等[4]將Isabelle 證明助手中的定理轉(zhuǎn)換為一階邏輯,之后使用ATP 分析定理,并將證明轉(zhuǎn)換回Isabelle中,從而證明定理.類似的“理論”也被用于其他證明工具(Kaliszyk 等[3];Urban 等[9];Czajka 等[10]).這種證明方式基本上繞過了交互式證明工具,并將工作外包給外部ATP.然而,這種證明方式最大的缺陷在于定理轉(zhuǎn)化過程中可能會導(dǎo)致屬性的缺失.

        ATP 將定理的前提和目標(biāo)轉(zhuǎn)換為合取范式(CNF)中的一階子句,并通過證明一階子句來證明定理.ATP的優(yōu)點在于提高了定理證明過程的自動化程度,缺陷在于它很難完成復(fù)雜軟件系統(tǒng)功能正確性的全部驗證.針對軟件系統(tǒng)復(fù)雜的數(shù)據(jù)類型和邏輯,ATP 只能處理有限的情況.

        1.2 結(jié)合交互式定理證明

        在交互式定理證明中,開發(fā)人員利用證明工具手動編寫證明腳本來完成屬性的驗證.交互式定理證明的優(yōu)勢在于工具能夠為軟件的驗證產(chǎn)生證明過程,此外,手動編寫腳本使得復(fù)雜軟件的驗證成為可能.但是,交互式定理證明存在自動化程度低、驗證代價比較高等缺陷.

        機(jī)器學(xué)習(xí)算法的發(fā)展為定理自動證明提供了新的思路.一些工作注重與機(jī)器學(xué)習(xí)的交互:Komendantskaya等[11]側(cè)重于ITP和機(jī)器學(xué)習(xí)接口之間的交互式接口方法.但是這項工作并未嘗試生成證明,就其接口而言,重點在于是使許多沒有機(jī)器學(xué)習(xí)經(jīng)驗的用戶可以使用許多簡單但有用的選項.同樣的還有Hang 等[12]提供了Coq證明的結(jié)構(gòu)化Python 表示,包括證明中遇到的所有證明狀態(tài)、采取的步驟和表達(dá)式抽象語法樹(ASTs),還支持與Coq的輕量級交互,以便它可以用于動態(tài)構(gòu)建證明.但無法構(gòu)建復(fù)雜的策略以便生成證明.

        張恒若等[13]在2017年基于 Z3 設(shè)計了 Coq 自動證明的實現(xiàn).其將Coq 與Z3 約束求解器結(jié)合在一起,設(shè)計了一個編譯框架,將Coq中的定理翻譯為Z3 可判定的明提.最后在Coq中能夠調(diào)用Z3中的命令進(jìn)行證明演算.

        但是,張恒若等人工作缺陷在于:

        1)Coq 與Z3的類型系統(tǒng)存在巨大差異,無法準(zhǔn)確轉(zhuǎn)換定理表達(dá)式.

        2)Coq中的很多基本類型是開發(fā)者直接利用遞歸定義的,但在Z3中有其提供的基本類型.例如,Int (自然數(shù))在Coq中需要開發(fā)者用遞歸的方式手動定義,但在Z3中提供對應(yīng)的Int 類型.如果將Coq中的類型轉(zhuǎn)換為Z3中的類型,其解析證明的效率將會降低.

        另一些工作利用機(jī)器學(xué)習(xí)產(chǎn)生證明選項證明定理:Gauthier 等[14]通過從數(shù)據(jù)集中搜索少量候選策略來生成策略集,這些候選策略根據(jù)當(dāng)前需要證明的定理來生成.每個候選策略視為一個可能的行為,并通過學(xué)習(xí)值函數(shù)和蒙特卡羅樹搜索進(jìn)行評估,最后選出需要的策略.雖然比SEPIA 更具適應(yīng)性,但生成的策略仍然是從一個具有預(yù)定的固定集合中選擇的,并且難以將其推廣到數(shù)據(jù)集外的其他策略.

        Yang 等[15]通過與證明助手的交互,為定理證明提供了一個大規(guī)模的數(shù)據(jù)集和學(xué)習(xí)環(huán)境.其所使用數(shù)據(jù)集包括來自Coq 證明助手中的123 個開源軟件項目的71K 人工證明(Barras 等).數(shù)據(jù)集涵蓋了廣泛的應(yīng)用領(lǐng)域,包括數(shù)學(xué),計算機(jī)硬件,編程語言等.Yang 等以抽象語法樹的形式生成策略,可以用來證明以前的自動證明器所不能達(dá)到的新定理.

        2 方案設(shè)計

        本節(jié)將介紹系統(tǒng)的一些設(shè)計細(xì)節(jié).圖1是預(yù)測命令的框架圖.分為4 個模塊:數(shù)據(jù)提取模塊、向量構(gòu)建模塊、預(yù)測參數(shù)模塊和命令結(jié)合模塊.

        圖1 預(yù)測命令框架

        本節(jié)針對命令預(yù)測問題進(jìn)行抽象.首先,對于命令預(yù)測,本工作從Coq 證明助手中提取證明數(shù)據(jù),包括前提、目標(biāo)和一些結(jié)構(gòu)化信息.之后,這些前提和目標(biāo)以及其他的特征將被編碼成高維向量,經(jīng)過壓縮降維之后,作為神經(jīng)網(wǎng)絡(luò)模型輸入.機(jī)器學(xué)習(xí)模型將會分別預(yù)測策略和參數(shù).最后,本工作結(jié)合預(yù)測和參數(shù)形成證明命令.

        2.1 問題模型

        本工作將K[γ]定義為γ 預(yù)測概率,其中,γ 表當(dāng)前的狀態(tài)(當(dāng)前前提、目標(biāo)、策略).R代表狀態(tài)空間.

        在證明狀態(tài) γ ∈S,γ-predictor K[γ]

        被定義為在γ上預(yù)測的概率的函數(shù),其預(yù)測出的策略或者參數(shù):

        預(yù)測器P代表針對下一個證明狀態(tài)的預(yù)測.Γ 代表策略的預(yù)測,Λ 代表參數(shù)的預(yù)測:

        本工作的機(jī)器學(xué)習(xí)模型將會對當(dāng)前的狀態(tài)做兩種預(yù)測,一種是策略Ptac,一種是參數(shù)Parg.數(shù)學(xué)表示為:

        P(σ) 代表模型預(yù)測的命令,將策略Ptac和參數(shù)Parg結(jié)合在一起.

        2.2 信息提取

        Coq 將證明邏輯信息放在底層,并不在IDE 顯示.此外,由于定理的結(jié)構(gòu)過于復(fù)雜,其證明信息可能無法直接解析使用.本工作中,神經(jīng)網(wǎng)絡(luò)模型直接提取命令行中的信息構(gòu)建證明.

        2.3 向量構(gòu)建

        Coq 證明助手以類型為基礎(chǔ),如果直接使用證明工具中的數(shù)據(jù)作為編碼,可能導(dǎo)致數(shù)據(jù)冗余、訓(xùn)練效果差等情況.例如,ComCert 項目中的一個定理:

        Theorem identity_fn_applied_twice:

        Forall (f:bool->bool),(forall (x:bool),fx=x)->

        Forall (b:bool),f(f b)=b.

        在證明過程中,存在兩個子目標(biāo):

        f (f true)=true

        f (f false)=false

        兩個子目標(biāo)的證明腳本為:

        rewrite <- H.

        rewrite <- H.

        reflexivity.

        如果直接編碼子目標(biāo),由于參數(shù)改變,無法有效學(xué)習(xí)第一個子目標(biāo)中的經(jīng)驗,利用定理中類型替代參數(shù)是一個有效的選擇.因此,本工作所使用的數(shù)據(jù)特征有定理名稱、定理主體和參數(shù)類型.

        2.4 預(yù)測策略

        為了預(yù)測策略,本工作收集現(xiàn)有的Coq 證明庫和常見的項目組成數(shù)據(jù)集.為反應(yīng)策略預(yù)測的側(cè)重點,本工作主要使用以下幾個數(shù)據(jù)特征:

        1)當(dāng)前需要證明的目標(biāo);很多策略往往是根據(jù)目標(biāo)具體選擇的.例如,如果定理以forall 開頭,那么下一個策略可能是intro 或induction.

        2)上一步的策略;定理證明中策略的使用具有空間局部性.一些策略之后往往使用相同的策略.例如,如果前一個策略是intro,后面經(jīng)常使用auto;而inversion經(jīng)常在subset 后使用.

        3)當(dāng)前上下文中的前提.策略的局部參數(shù)存在當(dāng)前的上下文參數(shù)中.因此,當(dāng)前的前提需要作為預(yù)測策略的特征.考慮到下面的前提:

        H:is_path(cons (pair s d) m)

        這種情況下,機(jī)器學(xué)習(xí)模型可能預(yù)測inversion H或者rewrite->H,H 代表上下文中的假設(shè).

        所有的這些特征被編碼成一個高維的向量后,經(jīng)過PCA 降維成一個128 維的向量,然后送入一個每層擁有128 個節(jié)點的完全連接的3 層前饋神經(jīng)網(wǎng)絡(luò)(feed-forward neural network),計算策略的概率分布.圖2是針對策略的預(yù)測模型,目的是找出策略在策略分布圖中的權(quán)重.

        圖2 預(yù)測策略框架

        用于計算節(jié)點的前饋神經(jīng)網(wǎng)絡(luò)有3 層:輸入層,隱藏層與輸出層.

        對于給定的參數(shù)集合W,b,輸出層的輸出h為:

        其中,a1,a2,a3與輸入向量有關(guān).前饋神經(jīng)網(wǎng)絡(luò)的計算節(jié)點為GRU,相較于LSTM,GRU的模型計算效率更高.本工作只生成原子策略,而不包括“tac1;tac2”等復(fù)合策略.因為所有的定理都可以在沒有復(fù)合策略的情況下完成.

        2.5 預(yù)測參數(shù)

        圖3是預(yù)測參數(shù)的總體框架.將相應(yīng)的特征編碼為向量后,送入到機(jī)器學(xué)習(xí)模型中后,訓(xùn)練得到命令的分布.

        圖3 預(yù)測參數(shù)框架

        深度學(xué)習(xí)模型預(yù)測3 種參數(shù):1)假設(shè)中參數(shù);2)目標(biāo)中參數(shù);3)中間定理.

        預(yù)測參數(shù)模型使用以下幾個特征:1)預(yù)測的策略;2)當(dāng)前子目標(biāo);3)當(dāng)前前提.

        與預(yù)測策略相比,預(yù)測參數(shù)模型并沒有使用前一步策略這個特征.基于觀察,當(dāng)前使用的參數(shù)與上一步使用的命令并不存在關(guān)聯(lián).此外,當(dāng)前使用的參數(shù)與當(dāng)前的策略存在一定關(guān)聯(lián)性.

        例如,如果是原子性策略,那么策略就不需要模型預(yù)測參數(shù);intro 與rewrite 使用不同的參數(shù).因此,預(yù)測參數(shù)模型使用了當(dāng)前策略這一特征.

        與預(yù)測策略相似,將當(dāng)前特征編碼為128 維的向量表示.經(jīng)過PCA 降維之后,送入到神經(jīng)網(wǎng)絡(luò)中訓(xùn)練.最后對當(dāng)前狀態(tài)進(jìn)行預(yù)測,得到當(dāng)前參數(shù)的分布.

        2.6 注意力網(wǎng)絡(luò)

        為解決自動定理證明中的策略參數(shù)預(yù)測問題,本工作引入注意力機(jī)制,注意力機(jī)制可以自動關(guān)注在訓(xùn)練過程中起決定作用的特征,捕捉重要的信息,減少無用信息的關(guān)注.

        注意力機(jī)制包含兩部分結(jié)構(gòu):編碼部分(encoder)和解碼部分(decoder).本工作選取encoder和decoder都為LSTM.這是因為,相較于RNN,LSTM 采用一個cell state 來保存長期記憶,再配合門機(jī)制對信息進(jìn)行過濾,從而達(dá)到對長期記憶的控制.

        在編碼部分,h代表各個時刻的隱藏層狀態(tài).將隱藏層狀態(tài)匯總,生成編碼向量T.q代表對應(yīng)的權(quán)重.

        在解碼部分,h1~ht代表編碼器隱藏層狀態(tài),Si-1代表解碼器隱藏層狀態(tài).WaUa代表對應(yīng)神經(jīng)網(wǎng)絡(luò)層的權(quán)重,eij代表h1~ht與Si-1的相關(guān)程度.

        其中,αij表示第i個輸出中前一個隱藏層狀態(tài)Si-1與第j個輸入隱層向量hj之間的相關(guān)性.αij可以由eij傳入到對應(yīng)函數(shù)歸一化權(quán)重值得到.

        對h1~ht進(jìn)行加權(quán)求和得到此次解碼所對應(yīng)的輸出 (x1,x2,x3,···,xt)的編碼向量Ci.

        有了Ci之后,根據(jù)編碼向量Ci進(jìn)行解碼,先計算解碼器i時刻的隱藏層狀態(tài)Si,再計算解碼器i時刻的輸出Yi計算如下:

        2.7 結(jié)合策略和參數(shù)

        在預(yù)測策略和參數(shù)之后,本工作結(jié)合策略和參數(shù)形成證明命令.

        現(xiàn)有的工作使用貪婪搜索結(jié)合策略和命令.在這種結(jié)合方式將選擇概率最高的預(yù)測策略做證明.同樣,機(jī)器學(xué)習(xí)模型選擇概率最高的參數(shù).算法可以通過賦予第一個參數(shù)較高的權(quán)重來實現(xiàn)這種選擇.但是,這種方法的缺陷在于策略的最終選擇沒有考慮到參數(shù)與策略是否匹配.例如,預(yù)測模型可能會預(yù)測rewrite,但卻發(fā)現(xiàn)沒有合適的前提可以用來作為參數(shù).

        本工作并沒有將策略和參數(shù)的概率進(jìn)行標(biāo)準(zhǔn)化等處理,而是直接選出評分較高的策略,依據(jù)策略選擇最高概率的參數(shù).這種方式提供了策略和參數(shù)的平衡,將兩者都考慮在內(nèi).此外,可以根據(jù)策略的類型,來判斷是否使用相應(yīng)的參數(shù),進(jìn)行一些后期的選擇處理.本部分的實驗將會在ComCert 項目上進(jìn)行實驗.這部分會在相應(yīng)的實驗章節(jié)展示.

        3 實驗分析

        本工作利用機(jī)器學(xué)習(xí)與Coq 進(jìn)行信息交互,實現(xiàn)了在交互式定理證明工具中自動生成證明命令的框架.CompCert是驗證C 語言編譯器安全屬性的形式化項目.本小節(jié)預(yù)測CompCert 項目中的命令,測試本系統(tǒng)的生成命令的準(zhǔn)確率.

        實驗的環(huán)境配置是Intel Broadwell E5-2660V4 2.0 GHz CPU,128 GB的內(nèi)存,4 根1080Ti的GPU,操作系統(tǒng)是Ubuntu 16.04 LTS.

        本工作通過訓(xùn)練來自CompCert的162 個文件的證明數(shù)據(jù)并以其中13 個文件作為測試集.測試集包含501 個證明腳本,一共13 867 個證明命令,如表1.

        表1 預(yù)置文件

        在所有的證明命令中,本工作能夠預(yù)測28.31%(3926/13 867)的命令,而在proof 證明命令中,本工作能夠預(yù)測41.6% (3 968/9 537)的命令.證明命令包含策略和參數(shù).與其他工作相比,本工作命令準(zhǔn)確率提高2%.結(jié)合注意力機(jī)制,本工作對證明信息的向量構(gòu)建更豐富,機(jī)器學(xué)習(xí)模型更合適.

        3.1 策略預(yù)測結(jié)果

        在預(yù)測策略時,本工作測試了原始證明中的證明策略在前3 個預(yù)測和前5 個預(yù)測中出現(xiàn)的頻率.如表2.對于測試集證明中的策略,在前3 個預(yù)測中存在正確的策略占58.4%,在前5 個預(yù)測中存在正確的策略占65.6%.此外,從表中可以得知,一些常用的策略如intros,simpl 等預(yù)測的較為準(zhǔn)確,但是一些比較復(fù)雜的策略inversion 預(yù)測效果較差.簡要分析,有兩個方面的原因,一是這些策略使用的目標(biāo)場景復(fù)雜.二是訓(xùn)練集中這些策略較少.

        表2 預(yù)測策略

        表3為預(yù)測全部策略的次數(shù)的百分比以及正確的概率,表中為真實策略、策略的預(yù)測次數(shù)占比以及正確的百分比.例如simpl 策略在所有的預(yù)測數(shù)量中占10%,正確的概率為7%.

        表3 策略預(yù)測正確率

        3.2 參數(shù)預(yù)測結(jié)果

        在預(yù)測命令時,本工作預(yù)測了測試集中28.31%的命令.當(dāng)本工作預(yù)測策略正確時,命令中29.5%的參數(shù)是錯誤的.然而,需要注意的是,許多常見的策略沒有任何參數(shù),這些策略在證明的過程中占據(jù)了很大一部分比例.

        在交互式定理證明工具中,策略參數(shù)由中間定理、前提和一些復(fù)雜表達(dá)式組成.例如命令destruct(zie (pos0 + typesize ty0) pos),策略參數(shù)為zie (pos0 +typesize ty0) pos.這種復(fù)雜表達(dá)式組成的參數(shù)和當(dāng)前上下文環(huán)境和目標(biāo)定理有關(guān),現(xiàn)有的工作暫時無法生成.此外,這種形式的參數(shù)在手工定理證明中使用的較少,機(jī)器學(xué)習(xí)模型預(yù)測效果較差.復(fù)雜參數(shù)的一個處理方式是將對應(yīng)的參數(shù)加載到當(dāng)前證明的前提中,以上下文參數(shù)的方式處理中間定理,這些工作將會在未來的研究中探討.

        4 結(jié)論與展望

        本文將機(jī)器學(xué)習(xí)與定理證明工具Coq 結(jié)合,分別預(yù)測策略和參數(shù),提高命令預(yù)測的準(zhǔn)確度.本文首先提取Coq中證明信息,這些信息包括前提、目標(biāo)和一些結(jié)構(gòu)化數(shù)據(jù).然后,將這些前提和目標(biāo)以及其他的特征編碼成高維向量,作為神經(jīng)網(wǎng)絡(luò)模型的輸入.本文預(yù)測了測試集中28.31%的命令,驗證了本工作框架的有效性.在未來的研究中,本工作將會根據(jù)預(yù)測的命令形成完整的證明,提高證明的效率.

        猜你喜歡
        命令定理向量
        J. Liouville定理
        向量的分解
        只聽主人的命令
        聚焦“向量與三角”創(chuàng)新題
        A Study on English listening status of students in vocational school
        移防命令下達(dá)后
        “三共定理”及其應(yīng)用(上)
        向量垂直在解析幾何中的應(yīng)用
        這是人民的命令
        向量五種“變身” 玩轉(zhuǎn)圓錐曲線
        亚洲AV无码精品一区二区三区l| 中文字幕精品一区二区精品| 亚洲 自拍 另类小说综合图区| 国产精品无码精品久久久| 亚洲一区二区三区在线观看蜜桃| 色综合悠悠88久久久亚洲| 国产一区二区三区在线电影| 亚洲人成无码网www| 久久久诱惑一区二区三区| 麻豆国产精品一区二区三区 | 日本在线综合一区二区| 成人艳情一二三区| 特黄a级毛片免费视频| www.日本一区| 精品久久人妻av中文字幕| 日本又色又爽又黄的a片18禁| 国产一在线精品一区在线观看 | 尤物yw无码网站进入| 在线一区二区三区视频观看| 亚洲精品一区三区三区在线 | 日本h片中文字幕在线| 国产人妻人伦精品1国产盗摄| 亚洲国产精品线观看不卡| 天堂麻豆精品在线观看| 超碰人人超碰人人| 国产精品.xx视频.xxtv| 美女视频永久黄网站免费观看国产 | 欧美色欧美亚洲另类二区| 欧美专区在线| 青青青视频手机在线观看| 夜夜爽夜夜叫夜夜高潮| 人妻少妇被猛烈进入中文字幕| 亚洲VR永久无码一区| 五月激情在线视频观看| 成人午夜性a级毛片免费| 日韩av在线毛片| 久久精品蜜桃美女av| 先锋中文字幕在线资源| 香蕉视频毛片| 亚洲精品久久麻豆蜜桃| 亚洲国产精品无码久久久|