【牛津大学博士论文】可微分编程的结构基础，176页pdf

这篇博士论文支持一个更广泛的论点，即范畴语义是研究和设计编程语言的有力工具。它专注于在简单类型函数设置中可微分编程的基础方面。尽管使用的大部分范畴理论可以归结为更基础的描述，但其影响对于获得本论文中的结果确实至关重要。某些证明的简洁性和某些定义与洞见的紧凑性得益于我的范畴理论背景得以简化。

反向传播是允许神经网络快速学习的关键算法。它使得机器学习最近的一些令人印象深刻的进步成为可能。随着模型的复杂性增加，同样需要复杂的数据结构，这要求我们能够超越标准的可微分性。这种新兴的概括被称为可微分编程。其思想是允许用户编写代表（可微分函数的一般化）的富有表现力的程序，其梯度计算可以通过自动微分进行自动化。在这篇论文中，我为可微分编程奠定了一些基础。这是通过三种方式完成的。

首先，我提出了一个简单的高阶函数语言，并定义自动微分为保留结构的程序转换。这种语言采用了微分空间的表示语义，并证明了转换是正确的，即AD生成的程序确实计算原始程序的梯度，使用逻辑关系论证。

其次，我扩展了前一章描述的语言，引入了如条件和递归等新的有表现力的程序结构。在这样的设置中，即使是一阶程序也可能代表不必是可微分的函数。我为这样的语言引入了更适合的表示语义，并展示了如何将AD扩展到这样的设置中，以及现在关于AD的哪些保证仍然成立。这种扩展的语言模拟了文献中可以找到的对表现力的更现实的需求，例如在现代的概率性编程语言中。

第三，我呈现了已开发理论的详细应用。我首先展示了如何将AD扩展到非常规的新类型和新原语的一般方法。然后，我展示了关于AD的保证对于在某些应用中的使用是足够的，例如随机梯度下降的变量变换公式，但在简单的梯度下降中可能不足够。最后，探索了概率编程的特定背景中的更多应用。首先，给出了概率程序的跟踪语义在几乎所有地方都是可微分的表示证明。其次，得到了在欧几里得空间中的概率程序的后验分布的特征：它们相对于某个在可数的光滑流形的并集上的Hausdorff度量的和具有密度。

总的来说，这些贡献为我们提供了更深入的对可微分编程的理解。它们为研究现实复杂程序的类似可微分性的属性提供了一个基础设置，超越了像可微分性或凸性这样的常规设置。它们提供了证明这些程序的某些属性，并将自动微分模块化扩展到带有新类型和原语的更丰富的背景的一般方法。