๐โ: computable semantics for differentiable programming with higher-order functions and datatypes
Benjamin Sherman, Jesse Michel, Michael Carbin
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, ๐ ๐ , that is the first to deliver a semantics for higher-order functions, higher-order derivatives, and Lipschitz but nondifferentiable functions. Together, these features enable ๐ ๐ to expose differentiable, higher-order functions for integration, optimization, and root-finding as first-class functions with automatically computed derivatives. ๐ ๐ 's semantics is computable, meaning that values can be computed to arbitrary precision, and we implement ๐ ๐ as an embedded language in Haskell.
We use ๐ ๐ 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.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 5f042250-49e8-4f8f-b249-cc9b624d5125Cited by top-tier papers9
- Systematically differentiating parametric discontinuitiesSai Praveen Bangaru, Jesse Michel, Kevin Mu, Gilbert Bernstein et al.SIGGRAPH 2021 ยท 30 citations
- Provably correct, asymptotically efficient, higher-order reverse-mode automatic differentiationFaustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis et al.POPL 2022 ยท 27 citations
- A dual number abstraction for static analysis of Clarke JacobiansJacob Laurel, Rem Yang, Gagandeep Singh, Sasa MisailovicPOPL 2022 ยท 17 citations
- ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic ProgramsAlexander K. Lew, Mathieu Huot, Sam Staton, Vikash K. MansinghkaPOPL 2023 ยท 16 citations
- A general construction for abstract interpretation of higher-order automatic differentiationJacob Laurel, Rem Yang, Shubham Ugare, Robert Nagel et al.OOPSLA 2022 ยท 9 citations
Builds on2
- On Solving Minimax Optimization Locally: A Follow-the-Ridge ApproachYuanhao Wang, Guodong Zhang, Jimmy BaICLR 2020 ยท 106 citations
- Differentiable Volumetric Rendering: Learning Implicit 3D Representations Without 3D SupervisionMichael Niemeyer, Lars M. Mescheder, Michael Oechsle, Andreas GeigerCVPR 2020
Related papers
- Distributions for Compositionally Differentiating Parametric DiscontinuitiesJesse Michel, Kevin Mu, Xuanda Yang, Sai Praveen Bangaru et al.OOPSLA 2024 ยท 7 citations
- ฯPAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable ProgramsMathieu Huot, Alexander K. Lew, Vikash K. Mansinghka, Sam StatonLICS 2023 ยท 5 citations
- Semantics of Integrating and Differentiating SingularitiesJesse Michel, Wonyeol Lee, Hongseok YangPLDI 2025
- On Correctness of Automatic Differentiation for Non-Differentiable FunctionsWonyeol Lee, Hangyeol Yu, Xavier Rival, Hongseok YangNeurIPS 2020 ยท 50 citations
- Backpropagation in the simply typed lambda-calculus with linear negationAloรฏs Brunel, Damiano Mazza, Michele PaganiPOPL 2020 ยท 24 citations
