We show how the basic Combinatory Homomorphic Automatic Differentiation (CHAD) algorithm can be optimised, using well-known methods, to yield a simple and generally applicable reverse-mode automatic differentiation (AD) technique that has the correct computational complexity that we would expect of a reverse AD algorithm. Specifically, we show that the standard optimisations of sparse vectors and state-passing style code (as well as defunctionalisation/closure conversion, for higher-order languages) give us a purely functional algorithm that is most of the way to the correct complexity, with (functional) mutable updates taking care of the final log-factors. We provide an Agda formalisation of our complexity proof. Finally, we discuss how the techniques apply to differentiating parallel functional programs: the key observations are 1) that all required mutability is (commutative, associative) accumulation, which lets us preserve task-parallelism and 2) that we can write down data-parallel derivatives for most data-parallel array primitives.
Fri 19 JanDisplayed time zone: London change
15:10 - 16:30 | Machine and Automata LearningPOPL at Kelvin Lecture Chair(s): Steven Holtzen Northeastern University | ||
15:10 20mTalk | Efficient CHAD POPL | ||
15:30 20mTalk | ReLU Hull Approximation POPL Zhongkui Ma The University of Queensland, Jiaying LI Microsoft, Guangdong Bai The University of Queensland | ||
15:50 20mTalk | On Learning Polynomial Recursive Programs POPL Alex Buna-Marginean University of Oxford, Vincent Cheval Inria Paris, Mahsa Shirmohammadi CNRS & IRIF, Paris, James Worrell University of Oxford | ||
16:10 20mTalk | Programming-by-Demonstration for Long-Horizon Robot Tasks POPL Noah Patton The University of Texas at Austin, Kia Rahmani The University of Texas at Austin, Meghana Missula The University of Texas at Austin, Joydeep Biswas The University of Texas at Austin, Işıl Dillig University of Texas at Austin | ||