面向高阶、递归、概率语言的自动微分指称语义
编程语言
2021-12-07 v2
摘要
自动微分(AD)旨在计算用户自定义函数的导数，但在图灵完备语言中，这一简单规范并未完全刻画 AD 的行为：AD 有时与可微程序的真实导数不一致；当 AD 应用于不可微或含副作用的程序时，所得代码具有何种保证（若有）并不清楚。我们研究了一种具表达力的可微编程语言，带有分段解析原语、高阶函数和一般递归。我们的主要结果是，即便在此一般设定下，Lee 等人[2020]正确性定理（原针对无偏序或递归的一阶语言证明）的一个版本仍成立：所有程序都指称所谓的 PAP 函数，且 AD 计算它们的正确内涵导数。Mazza 与 Pagani[2021]近期关于 AD 在零测度输入集上与可微递归程序的真实导数不一致的定理，可作为该事实的直接推论导出。我们还将该框架应用于研究概率程序，并通过一种新颖的指称论论证恢复了 Mak 等人[2021]的近期结果。
引用
@article{arxiv.2111.15456,
title = {Towards Denotational Semantics of AD for Higher-Order, Recursive, Probabilistic Languages},
author = {Alexander K. Lew and Mathieu Huot and Vikash K. Mansinghka},
journal= {arXiv preprint arXiv:2111.15456},
year = {2021}
}
备注
Presented at the NeurIPS 2021 differentiable programming workshop