高效的CHAD
摘要：基于组合同态自动微分（CHAD）算法的基本原理，我们展示了如何利用众所周知的方法进行优化，以得到一种简单且通用的逆向模式自动微分（AD）技术，其具有预期的逆向AD算法的正确计算复杂性。具体而言，我们展示了稀疏向量和状态传递式代码的标准优化（以及对于高阶语言的去功能化闭包转换），使得我们可以获得一个纯粹的函数式算法，其计算复杂性接近正确的复杂性，并利用（函数式的）可变更新来解决最终的对数因子。我们提供了我们的复杂性证明的Agda形式化表示。最后，我们讨论了这些技术如何应用于不同iating并行函数式程序：关键观察是 1）所有所需的可变性都是（可交换的、可结合的）累积，这样我们就可以保留任务并行性；2）我们可以为大多数数据并行数组原语编写数据并行导数。
作者：Tom Smeding, Matthijs V''ak''ar
论文ID：2307.05738
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-07-14