斯坦福提出机器学习开发新思路：无Bug的随机计算图Certigrad（已开源）

正文

请到「今天看啥」查看全文

正确性

随机反向传播

以下定理可以证明我们的随机反向传播实现是正确的：https://github.com/dselsam/certigrad/blob/master/src/certigrad/backprop_correct.lean#L13-L25

通俗地说，它表示：对于任何随机计算图，backprop 计算了张量的向量，如此，每一个向量元素都是一个随机变量，这个随机变量等同于关于此参数的图的期望损失梯度。

更通俗地说：∇ E[loss(graph)] = E[backprop(graph)]

优化验证

研究人员实现了两个随机计算图转换，一个是对图进行「重新参数化」（reparameterize），让随机变量不再直接依赖于一个参数；另一个用于整合多元各向同性高斯（multivariate isotropic Gaussian）的 KL 散度。

• https://github.com/dselsam/certigrad/blob/master/src/certigrad/kl.lean#L79-L90

• https://github.com/dselsam/certigrad/blob/master/src/certigrad/reparam.lean#L70-L79

验证 Certigrad 程序属性

Certigrad 还包括构建随机计算图的前端语法。这里是一个解释原生变分自编码器的示例程序：

• https://github.com/dselsam/certigrad/blob/master/src/certigrad/aevb/prog.lean#L16-L38

研究人员证明了上述两个经过验证的优化的确符合原始自动编码器的顺序：

• https://github.com/dselsam/certigrad/blob/master/src/certigrad/aevb/transformations.lean#L52-L57

反向传播在结果模型上已被证明可以正确运行，它可以满足所有必要前提条件：

• https://github.com/dselsam/certigrad/blob/master/src/certigrad/aevb/grads_correct.lean#L20-L27

正式证明

在证明定理的过程中，Lean 构建了一个正式的证书，它可以通过一个小型独立可执行程序进行自动验证，它的可靠性是基于构建良好的元理论嵌入到 Lean 的逻辑核心中，而 Lean 的可靠性已被大量开发者所证明。

问题

尽管在证明期间研究者们使用了非常高的标准，但 Certigrad 仍然有一些不够理想的地方。

• 我们对其数学基础进行了公理化，而不是从基本原理的层面上进行构建。

• 在一些地方我们采用了浮点数，即使我们的正确性定理只适用于无限精度的实数。

• 为了保证性能，我们在运行时用 Eigen 调用替换原始张量运算。

请到「今天看啥」查看全文