一句话:提出首个可靠微分参数不连续性的一阶可微语言 Potto,并给出指称语义与支持分离编译的高效实现。
物理模拟、图形学和概率推断常需对接触、遮挡等引起的不连续过程求导。PyTorch、JAX 等可微语言忽略不连续性,对参数不连续性(条件式含至少一个实值参数和积分变量)会错误求导。本文提出 Potto,首个可靠微分参数不连续性的一阶可微语言;给出程序及其导数的指称语义并证明二者一致,实现支持分离编译。在两项规模递增的图像风格化基准上,编译时间分别加速 88.1x 和 441.2x,运行时分别加速 2.5x 和 7.9x;还实现了带分离编译 shader 的原型可微渲染器。
Computations in physical simulation, computer graphics, and probabilistic inference often require the differentiation of discontinuous processes due to contact, occlusion, and changes at a point in time. Popular differentiable programming languages, such as PyTorch and JAX, ignore discontinuities during differentiation. This is incorrect for parametric discontinuities —conditionals containing at least one real-valued parameter and at least one variable of integration. We introduce Potto, the first differentiable first-order programming language to soundly differentiate parametric discontinuities. We present a denotational semantics for programs and program derivatives and show the two accord. We describe the implementation of Potto, which enables separate compilation of programs. Our prototype implementation overcomes previous compile-time bottlenecks achieving an 88.1x and 441.2x speed up in compile time and a 2.5x and 7.9x speed up in runtime, respectively, on two increasingly large image stylization benchmarks. We showcase Potto by implementing a prototype differentiable renderer with separately compiled shaders.
@article{paperbot2560,
title = {Distributions for Compositionally Differentiating Parametric Discontinuities},
author = {Jesse Michel and Kevin Mu and Xuanda Yang and Sai Praveen Bangaru and Elias Rojas Collins and Gilbert Bernstein and Jonathan Ragan-Kelley and Michael Carbin and Tzu-Mao Li},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA1},
year = {2024},
doi = {10.1145/3649843}
}