下面只是我的思考筆記，所以會非常自由和不嚴謹，不論是驗證還是AI都不是我的研究方向，存在大量謬誤

最近由于課程原因，我開始讀一些神經(jīng)網(wǎng)絡相關(guān)的東西。 由于我本身的研究還是黑魔法防御術(shù)， 神經(jīng)網(wǎng)絡，這種神必的計算機煉丹學的安全問題也讓我感受到相比其他至少還有一點興趣。畢竟神經(jīng)網(wǎng)絡再特殊也只是一種程序， 那么傳統(tǒng)的安全方法理應能在這里面得到應用。

什么是神經(jīng)網(wǎng)絡

這個問題做AI的同學比我懂得實在是太多，我實在也沒法班門弄斧。但是我想從更加簡單的層面，單純的程序角度，來解構(gòu)一下神經(jīng)網(wǎng)絡。
首先，神經(jīng)網(wǎng)絡程序和傳統(tǒng)程序的有一個很明顯的區(qū)別，他并不是一個程序。常見的神經(jīng)網(wǎng)絡程序都會分為訓練（1）和最后生成的模型（2）兩個部分，兩個程序。訓練程序一般是一個巨大的loop函數(shù)，不斷的更新矩陣中的參數(shù)值，而這個過程中的interesting part是如何更新的問題。這一步從面向語言編程(language oriented programing)的角度來說應當是可以被抽象DSL的部分。我們可以假設有理想語言, 他的語義應當是用于描述這個巨大的loop函數(shù)的中間過程，神經(jīng)元鏈接方式, 神經(jīng)元更新方式 加上程序的終止條件 loss函數(shù)。這樣看來這一部分應當會有一個合適的declarative language(也許是logic式+函數(shù)式的混合語言，直覺感覺帶類型系統(tǒng)可能會有意義)。
而訓練最終得到是一個巨大的矩陣，并把矩陣上記錄的輸入填入被連接好的神經(jīng)元當中。這個部分是另一個完全不同的程序，語言的語義在這里其實已經(jīng)沒有必要了。之前都在說神經(jīng)元，其實我覺得這完全是個誤導人的詞匯，這個就是一個普通函數(shù)，而且這個函數(shù)非常簡單，他只在某些情況下會有輸出， 那么也就是說使用帶算數(shù)的來抽象應該是夠用了。訓練完成后運行的那個程序本質(zhì)是函數(shù)之間的組合，而且這個最后組合的函數(shù)中的絕大多數(shù)一定是deterministic的，甚至可以說邏輯分支幾乎是即使是存在遞歸，遞歸的深度也非常的淺，并且大多數(shù)情況下總能停機(此處存疑，如果有誰能懂的話，希望能告訴我=。=)。

煉丹安全存在形式化表達？

如果我們希望證明一個程序是安全的，那么我們必須定義在這樣的程序中什么是安全。目前絕大多數(shù)的研究主要聚焦在程序2，也就是訓練以后生成好的函數(shù)。 給出一個前條件，是對輸入數(shù)據(jù)的某種約束，比如用飛機做例子，兩個飛機相遇為了防止碰撞我們可以大致的給出兩飛機距離和機體相關(guān)數(shù)據(jù)（特征數(shù)據(jù)）范圍。給出一個后條件，最后神經(jīng)網(wǎng)絡控制器無法算出一個會導致飛機相撞的值域。這個其實是類似霍爾邏輯的表達。如果模型可拆分成子模型，例如有的神經(jīng)網(wǎng)絡是多種不同神經(jīng)網(wǎng)絡的組合，那么根據(jù)霍爾邏輯的傳遞性，應當也可以在模型之間很自然的添加約束，并且實現(xiàn)證明。

說實話如果模型不怎么復雜，特別是針對forward network這個函數(shù)就必然是deterministic的，有輸入輸出嚴格11對應，那其實就退化到了一個規(guī)劃問題，給出輸入自變量的值域，驗證函數(shù)輸出不在某個返回內(nèi)。這里的只要算法是complete其實就很完美了。如果再簡單一點，把神經(jīng)元函數(shù)限定到Relu，Relu函數(shù)基本上就是個線性函數(shù)，有的人就會選擇直接把問題退化到線性規(guī)劃。我不喜歡這種做法，這樣的退化讓方法完全失去了普適性，也就是說基本可以斷言，此類方法完全無法擴展到復雜網(wǎng)路，我不覺得這是正確的研究趨勢。

但是從這里我們不難看到目前所有的研究都只能驗證程序2相關(guān)的部分，而對于程序1是直接無視的，但是從編程的角度來說，程序員能控制的最多的其實是程序1，由于神經(jīng)網(wǎng)絡的輸入數(shù)據(jù)非常復雜，往往包含大量的參數(shù)（而且參數(shù)大量存在非int，bool等簡單類型）。也許目前是認為1的部分不可以驗證？但是如果能給出程序2的前條件，也就是說我們已經(jīng)有了程序1的后條件。 對于程序1，他的輸入的數(shù)據(jù)分布能不能作為某種前條件？我這么說實在是不是很好，也就是說如果我們希望驗證程序1，那么我們必須找到程序1，訓練過程中的不變量，就像要找loop invariant一樣才對。

那么傳統(tǒng)安全的一些東西能不能用。比如類non-interference，這么說可能不對，因為我們程序中是不存在有高安全變量和低安全變量的。但是由于AI存在某些倫理學上的擔憂，比如大家希望兩種feature在最終訓練出來的模型中是不能有相關(guān)系的，比如，性別信息可能對數(shù)據(jù)引入bias但是我們又希望在訓練的時候把這個數(shù)據(jù)放進去，這種情況產(chǎn)生的一種可能就是某一個至關(guān)重要的feature可能和性別之間有練習，我們能否證明在一個良好的模型中這樣的聯(lián)系并不存在？但是這樣的話，如何形式化的描述？這是不是一種超性質(zhì)？我完全沒有頭緒。但是我覺得存在可能性。

程序分析的視角

從我的直覺可以感受到，AI驗證可能可以從傳統(tǒng)的模式檢查等技術(shù)中得到一些驗證，而實際上也確實有人去做了，那么作為常見的形式化方法，程序分析能不能用呢。
傳統(tǒng)程序分析針對就是我們?nèi)粘Ｖ凶畛Ｒ姷某绦?這類程序一般擁有非常復雜的程序軌跡(trace)，而程序分析，本質(zhì)就是設計一種解釋器，可靠的去over approximate這些trace, 然后對抽象之后的程序進行運行，得到一些靜態(tài)性質(zhì)。但是對于神經(jīng)網(wǎng)絡中的程序2，似乎并不是這樣的，除非網(wǎng)絡的結(jié)構(gòu)非常復雜，那樣程序才會有很多分支，才有用這些技術(shù)的價值。也許對于復雜網(wǎng)絡，這里存在某些可能性？

Fuzz

Fuzz其實面對的問題也是和程序分析一樣的，如果說是trace based fuzzing,我覺得應該沒有太大的作用。但是trace說到底也只是觀察程序的一種方法，如果我們換個思路，從每個神經(jīng)元的值變化入手，嘗試去使用進化算法，不斷刪選優(yōu)秀變異，有沒有可能呢？而且這里很明顯和Adversal Attack存在某種聯(lián)系，法茲器可能可以用于生成counter example.但是這真的就只能是我的純猜測了，如果能有類似的研究我也會很感興趣？