论文标题
在表示正确的，纯粹的功能，有效的逆模式自动分化
Denotationally Correct, Purely Functional, Efficient Reverse-mode Automatic Differentiation
论文作者
论文摘要
反向模式分化用于优化，但它引入了参考，从而破坏了基础程序的纯度，因此众所周知它们更难优化。我们在具有数组操作的纯粹功能性语言上提出了反向模式分化。这是第一个提供可证明的有效，纯粹功能性且在说明正确正确的反向模式分化的方法。我们表明，我们的转换在语义上是正确的，并验证了廉价的梯度原理。受到类别的道具和汇编的启发，我们引入了一种新颖的中间表示，我们称之为“单一形式”。我们的反向模式转换被认为是通过此中间表示形式作为汇编方案。我们通过在反向模式转换后进行一般部分评估优化来获得可证明的有效梯度，而不是手动派生的梯度。对于简单的一阶程序，获得的输出程序类似于静态单个分配（SSA）代码。我们强调了我们的方法的模块化，并显示了如何通过更优化的原始功率轻松地丰富我们的语言，这是实践中某些加速的要求。
Reverse-mode differentiation is used for optimization, but it introduces references, which break the purity of the underlying programs, making them notoriously harder to optimize. We present a reverse-mode differentiation on a purely functional language with array operations. It is the first one to deliver a provably efficient, purely functional, and denotationally correct reverse-mode differentiation. We show that our transformation is semantically correct and verifies the cheap gradient principle. Inspired by PROPs and compilation to categories, we introduce a novel intermediate representation that we call 'unary form'. Our reverse-mode transformation is factored as a compilation scheme through this intermediate representation. We obtain provably efficient gradients by performing general partial evaluation optimizations after our reverse-mode transformation, as opposed to manually derived ones. For simple first-order programs, the obtained output programs resemble static-single-assignment (SSA) code. We emphasize the modularity of our approach and show how our language can easily be enriched with more optimized primitives, as required for some speed-ups in practice.
