875
Certigrad——隨機計算圖優化係統
更多深度文章，請關注：https://yq.aliyun.com/cloud
Certigrad是一種概念證明，它是用於開發機器學習係統的一個新途徑。其中包含以下組件：
- 應用本身
- 基礎數據庫
- 應用在數學上所需求的形式化描述
- 應用滿足其形式化描述的機器可測證明
具體來說，Certigrad是一個優化的隨機計算圖形係統，我們使用Lean Theorem Prover調試係統，最終證明了在基礎數學上是正確的。
優化驗證
Certigrad項目的性能驗證
- 我們對數學基礎進行了理論化，而不是從最初的原理來構造它。
- 盡管我們的正確性定理隻適用於無限精度實數，但我們必須用浮點數執行。
- Eigen的調用來替換原始的張量操作。
-
Certigrad
1.下載我們的Lean項目從https://github.com/dselsam/lean/tree/certigrad並且根據在https://github.com/leanprover/lean中的說明構建/安裝。
2.下載Eigen並安裝。
3.下載這個庫，並在主目錄執行leanpkg --建立。
我們已經正式證明Certigrad是正確的(在上麵提到的問題)，但這並不意味著Certigrad是你所期望的那樣。它的意思是，根據假設，與上麵相關的定理是正確的。
Certigrad的設計是一個概念證明，不是一個生產係統。有許多功能需要添加，使之成為一個有用的工件。在發展的過程中，我們遇到了很多需要解決的問題來使我們的方法論經濟化，並且我們在解決這些挑戰比擴展和維護Certigrad作為目的本身更感興趣。
一篇描述了Certigrad背後的理念的文章可以在 https://arxiv.org/abs/1706.08605 看，並將在2017年的ICML中出現。
- Daniel Selsam，斯坦福大學
- Percy Liang，斯坦福大學
本文由北郵@愛可可-愛生活老師推薦，阿裏雲雲棲社區組織翻譯。
最後更新：2017-07-13 15:32:44