Certigrad——随機計算圖優化系統

certigrad是一種新的開源的随機計算圖優化系統，它是用于開發機器學習系統的一個新途徑。其中包含以下元件：

應用本身

基礎資料庫

應用在數學上所需求的形式化描述

應用滿足其形式化描述的機器可測證明

随機計算圖擴充了像tensorflow和theano這樣的系統的計算圖，它允許節點表示随機變量，并通過定義損失函數來表示葉節點和圖中所有随機選擇的總和的期望值。certigrad允許使用者從我們提供的原語中構造任意的随機計算圖。該系統的主要目的是采用一個描述随機計算圖的程式，并運作随機算法（随機反向傳播），同時期望對參數的損失函數的梯度進行采樣。

<b>随機算法</b><b></b>

這是定理詳述，并證明了我們的随機反向傳播的實作是正确的：

<a href="https://github.com/dselsam/certigrad/blob/master/src/certigrad/backprop_correct.lean#l13-l25" target="_blank">https://github.com/dselsam/certigrad/blob/master/src/certigrad/backprop_correct.lean#l13-l25</a>

通俗地說，它表示，對于任意的随機計算圖， backprop計算一個張量的向量，使得這個向量的每個元素都是一個随機變量，(在期望中)等于這個參數的期望損失的梯度。

更通俗地說，∇ e[loss(graph)] = e[backprop(graph)].

<b>優化驗證</b><b></b>

我們還實作了兩個随機計算圖形轉換，一個是對圖形進行“重新參數化”，使得随機變量不再直接依賴于一個參數，另一個是将多元各向同性高斯分布的kl散度整合起來。

<a href="https://github.com/dselsam/certigrad/blob/master/src/certigrad/kl.lean#l79-l90" target="_blank">https://github.com/dselsam/certigrad/blob/master/src/certigrad/kl.lean#l79-l90</a>

<a href="https://github.com/dselsam/certigrad/blob/master/src/certigrad/reparam.lean#l70-l79" target="_blank">https://github.com/dselsam/certigrad/blob/master/src/certigrad/reparam.lean#l70-l79</a>

<b>certigrad項目的性能驗證</b><b></b>

certigrad還包括建構随機計算圖的前端文法。下面是一個示例程式，它描述了一個簡單的變分自動編碼器:

<a href="https://github.com/dselsam/certigrad/blob/master/src/certigrad/aevb/prog.lean#l16-l38" target="_blank">https://github.com/dselsam/certigrad/blob/master/src/certigrad/aevb/prog.lean#l16-l38</a>

我們證明上述兩個經過認證的優化非常符合原始自動編碼器的順序：

<a href="https://github.com/dselsam/certigrad/blob/master/src/certigrad/aevb/transformations.lean#l52-l57" target="_blank">https://github.com/dselsam/certigrad/blob/master/src/certigrad/aevb/transformations.lean#l52-l57</a>

我們還證明了反向傳播将正确地工作于結果模型，也就是說它滿足了所有必要的前提條件:

<a href="https://github.com/dselsam/certigrad/blob/master/src/certigrad/aevb/grads_correct.lean#l20-l27" target="_blank">https://github.com/dselsam/certigrad/blob/master/src/certigrad/aevb/grads_correct.lean#l20-l27</a>

<b>形式證明</b><b></b>

在證明定理的過程中，lean建構了一個正式的證明證書，可以通過一個小型的獨立可執行程式自動驗證，其可靠性基于将精益核心邏輯嵌入到集合理論中的良好的元理論參數，其實施得到了許多開發商的嚴密審查。是以，沒有人需要能夠了解為什麼一個證明是正确的，以便相信它是正确的。

<b>問題</b><b></b>

我們的證明采用了一個非常高的标準，但是有一些方法證明了certigrad沒有達到純粹的理想。

我們對數學基礎進行了理論化，而不是從最初的原理來構造它。

盡管我們的正确性定理隻适用于無限精度實數，但我們必須用浮點數執行。

為了性能，我們在運作時用對eigen的調用來替換原始的張量操作。

系統在虛拟機中執行，虛拟機的設計不像核心邏輯的驗證檢查器那樣值得信賴。

可證明的正确性不必以計算效率為代價:證明隻需檢查一次，并且不引入任何持續的成本或運作時開銷。盡管我們在這項工作中驗證的算法缺乏很多優化，但大多數時間訓練機器學習系統都是用矩陣來做的，而且我們可以通過與矩陣運算(eigen)的優化庫連接配接來實作競争性能。我們使用adam在mnist上訓練了一個自動編碼變異貝葉斯（aevb）模型，發現我們的性能與tensorflow（在cpu上）具有競争力。

我們有一個腳本，可以在mnist上用adam來訓練aevb。

<a href="https://github.com/dselsam/certigrad/blob/master/src/certigrad/aevb/mnist.lean#l44-l66" target="_blank">https://github.com/dselsam/certigrad/blob/master/src/certigrad/aevb/mnist.lean#l44-l66</a>

盡管我們的方法引入了許多新的挑戰，但它也帶來了實質性的好處。

<b>調試</b><b></b>

首先，我們的方法論提供了一種系統地調試機器學習系統的方法。

實作錯誤在機器學習系統中很難發現，更不用說進行本地化和位址處理了，因為還有許多其他潛在的不需要的行為。例如，一個實施的錯誤可能導緻不正确的梯度，進而導緻學習算法停滞，但是這樣的症狀也可能是由于訓練資料中的噪聲，模型選擇不當，不利的優化環境，不适當的搜尋政策，或數值不穩定。這些其他問題是如此普遍，以至于人們常常認為任何不想要的行為都是由其中一個原因引起的。是以，實際的實作錯誤可以在不檢測的情況下無限期地存在。在随機程式中，錯誤更難以檢測，因為一些錯誤可能隻會扭曲随機變量的分布并且可能需要編寫自定義的統計測試來檢測。

使用我們的方法論，正式的規範可以被用于在邏輯層次上進行詳盡地測試和調試機器學習系統，而不需要借助于經驗性的測試。驗證該規範的過程将暴露所有的實作錯誤、疏忽和隐藏的假設。一旦它被證明了，每個感興趣的人都可以确信，實作是正确的，而不需要信任任何涉及的人或者了解程式是如何工作的。

<b>合成</b><b></b>

其次，我們的方法論可以使實作的某些部分自動合成。

然而使用現狀方法，編譯器不知道程式應該做什麼，是以隻能捕獲表面的文法錯誤，用我們的方法論，這個定理證明了程式應該做什麼，并且能夠提供更多有用的幫助。作為一個簡單的例子，假設我們要将一個2層mlp編譯成一個單一的原始運算符，以避免運作時圖形處理的開銷。通常這涉及到手工推導複合函數的梯度。然而，由于在我們的方法論中，定理證明者知道基礎數學，包括相關的梯度規則和張量的代數性質，它可以幫助推導出新算子的梯度。

合成的可能性不僅僅是自動化代數推導。在開發certigrad時，我們開始證明該規範在實施系統的困難部分之前已經被使用，并且使用所産生的證明義務來幫助确定程式需要做什麼。正式的規範，以及最終的正确性的機器可校驗的證明，使我們能夠正确地實施系統，而無需對系統為什麼正确的一緻而全局的了解。事實上，我們主要把這一重擔轉移到電腦上。

<b>積極優化</b><b></b>

第三，我們的方法論可能使安全自動化比其他方法更積極的轉換。例如，我們可以編寫一個程式，搜尋一個可以被分析的随機計算圖的組成部分，它利用了大型積分恒等式庫，以及人類無法手動模拟的過程方法。這樣的過程可能能夠在許多模型上實作超人為差異減少，但可能非常難以可靠地實作;如果該過程能夠為給定的變換生成一個機器可檢查的證書，那麼不管過程本身的複雜性如何，這個轉換都可以被信任。

<b>文檔</b><b></b>

第四，一個正式的規範(即使沒有正式的證明)可以作為一個系統的精确文檔，并且可以讓我們更容易地了解代碼的各個部分，在不同的地方所假定的先決條件，以及不變量的維護。這種精确的文檔對于任何軟體系統都是有用的，但是對于機器學習系統尤其有用，因為不是所有的開發人員都有必要的數學知識來填補非正式描述的空白。

我們的方法論對于高保證系統來說可能已經很經濟了，但是仍然有許多工作要做，以使它在主流的開發中變得實用，而正确性僅僅是“可選的”。然而，我們的方法論的一個關鍵方面是它可以被逐漸采用。你可以隻寫一小段代碼，然後簡單地包裝和公理化(就像我們對eigen做的那樣)。你也可以編寫淺層的正确性，并且隻證明其中的一些屬性是成立的。我們希望随着時間的推移，随着工具的成熟，開發人員将會發現，進一步追求我們的方法論是值得的，并且能夠收獲更多的好處。

lean仍然在開發中，而外部功能接口(ffi)還沒有被移植到主分支。我們複制lean項目以添加c ++代碼來将eigen加入到lean的虛拟機中，但是，一旦ffi被釋出，我們将把certigrad移植到lean主分支。

至此之前：

3.下載下傳這個庫，并在主目錄執行leanpkg --建立。

注意：搭建certigrad目前需要大約15分鐘和大約7 gb的記憶體消耗。

我們已經正式證明certigrad是正确的(在上面提到的問題)，<b>但這并不意味着certigrad是你所期望的那樣。</b>它的意思是，根據假設，與上面相關的定理是正确的。

certigrad的設計是一個概念證明，不是一個生産系統。有許多功能需要添加，使之成為一個有用的工件。在發展的過程中，我們遇到了很多需要解決的問題來使我們的方法論經濟化，并且我們在解決這些挑戰比擴充和維護certigrad作為目的本身更感興趣。

daniel selsam，斯坦福大學

percy liang，斯坦福大學

david l. dill，斯坦福大學

文章原标題《certigrad - certified stochastic computation graphs by daniel selsam》，

作者：daniel selsam，斯坦福大學學生 譯者：tiamo_zn 審閱：袁虎