paperbot · PL 论文追踪

全部论文 待读 收藏

P2 𝜆ₛ: computable semantics for differentiable programming with higher-order functions and datatypes

λS:具有高阶函数与数据类型的可微编程的可计算语义
POPL 5(POPL)2021匹配度 3/10 · 该论文属于 PL 与机器学习交叉的形式语义方向,涉及可微编程、高阶函数与可计算语义,但与用户核心关注的静态分析、LLM/Agent 改进形式化验证、浮点程序分析或贝叶斯程序分析均无直接关联。引用 8 inbox
Benjamin Sherman, Jesse Michel, Michael Carbin
crossref: 2026-09-10

AI 速览

一句话:提出可微编程语言 λS,首次为高阶函数、高阶导数与 Lipschitz 不可微函数提供可计算语义。

深度学习优化目标日益复杂,常涉及积分、连续优化、求根等高阶函数;但 PyTorch、TensorFlow 等框架缺少这些函数的一等表示,开发者需手动推理并转写可微代码。本文提出可微编程语言 λS,首次为高阶函数、高阶导数以及 Lipschitz 但不可微函数提供语义。该语义可计算,值可计算到任意精度,并以 Haskell 嵌入式语言实现。借助 λS,积分、优化、求根等可微高阶函数可作为一等函数并自动求导。作者还构造了表示概率分布、隐式曲面与广义参数曲面的可微库,并给出案例研究,包括无需用户级微分代码的可微光线追踪与广义参数曲面的 Hausdorff 距离。

问题
可微编程框架难以一等表示积分、连续优化、求根等高阶函数,也缺少支持高阶导数与不可微函数的语义,开发者需手动转写可微代码。
方法
定义可微编程语言 λS,为高阶函数、高阶导数及 Lipschitz 但不可微函数给出可计算语义,并在 Haskell 中实现为嵌入式语言。
评估
通过构造概率分布、隐式曲面、广义参数曲面等高阶数据类型库,并以可微光线追踪和 Hausdorff 距离等案例验证自动求导与建模能力。
原文摘要(Abstract)

Deep learning is moving towards increasingly sophisticated optimization objectives that employ higher-order functions, such as integration, continuous optimization, and root-finding. Since differentiable programming frameworks such as PyTorch and TensorFlow do not have first-class representations of these functions, developers must reason about the semantics of such objectives and manually translate them to differentiable code. We present a differentiable programming language, λ S , that is the first to deliver a semantics for higher-order functions, higher-order derivatives, and Lipschitz but nondifferentiable functions. Together, these features enableλ S to expose differentiable, higher-order functions for integration, optimization, and root-finding as first-class functions with automatically computed derivatives. λ S ’s semantics is computable, meaning that values can be computed to arbitrary precision, and we implement λ S as an embedded language in Haskell. We use λ S to construct novel differentiable libraries for representing probability distributions, implicit surfaces, and generalized parametric surfaces – all as instances of higher-order datatypes – and present case studies that rely on computing the derivatives of these higher-order functions and datatypes. In addition to modeling existing differentiable algorithms, such as a differentiable ray tracer for implicit surfaces, without requiring any user-level differentiation code, we demonstrate new differentiable algorithms, such as the Hausdorff distance of generalized parametric surfaces.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1178,
  title = {𝜆ₛ: computable semantics for differentiable programming with higher-order functions and datatypes},
  author = {Benjamin Sherman and Jesse Michel and Michael Carbin},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {5},
  number = {POPL},
  year = {2021},
  doi = {10.1145/3434284}
}