Open Collections

Soundness for automatic differentiation via string diagrams

Banff International Research Station for Mathematical Innovation and Discovery

Reverse-mode automatic differentiation, especially in the presence of complex language features, is notoriously hard to implement correctly, and most implementations focus on differentiating straight-line imperative first-order code. Generalisations exist, however, that can tackle more advanced features; for example, the algorithm described by Pearlmutter and Siskind in their 2008 paper can differentiate (pure) code containing closures. We show that AD algorithms can benefit enormously from being translated into the language of string diagrams in two steps: first, we rephrase Pearlmutter and Siskind's algorithm as a set of rules for transforming hierarchical graphs; rules which can -and indeed have been- be implemented correctly and efficiently in a non-trivial language. Then, we sketch a proof of soundness for it by reducing its transformations to the axioms of Cartesian reverse differential categories, expressed as string diagrams.

Mathematics; Category Theory; Homological Algebra; Algebraic Topology; Algebraic Structures

video/mp4

Author affiliation: Huawei Research

2023-10-28

Attribution-NonCommercial-NoDerivatives 4.0 International

http://hdl.handle.net/2429/86372

Unreviewed

http://creativecommons.org/licenses/by-nc-nd/4.0/