符合表示准确、纯函数式的高效逆向模式自动微分
摘要：使用反向模式微分进行优化引入了引用，这破坏了底层程序的纯净性，使它们难以优化。我们在纯函数式语言中提出了一种纯粹功能的数组操作的反向模式微分。它是第一个可以提供经过证明的高效、纯函数式和表示正确的反向模式微分。我们展示了我们的转换在语义上是正确的，并验证了廉价梯度原则。受到PROPs和编译为类别的启发，我们引入了一个新颖的中间表示，我们称之为'一元形式'。我们的反向模式转换被分解为通过这个中间表示的编译方案。通过在我们的反向模式转换之后执行通用的部分求值优化，我们获得了经过证明的高效梯度，而不是手动导出的梯度。对于简单的一阶程序，获得的输出程序类似于静态单赋值（SSA）代码。我们强调我们方法的模块化，并展示了如何在实践中通过更多优化的原语来丰富我们的语言。
作者：Mathieu Huot, Amir Shaikhha
论文ID：2212.09801
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-04-27