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 审阅：袁虎