Provably correct, asymptotically efficient, higher-order reverse-mode automatic differentiation
Faustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, T. M. R. Ellis, Richard A. Eisenberg, Andrew Fitzgibbon
Abstract
In this paper, we give a simple and efficient implementation of reverse-mode automatic differentiation, which both extends easily to higher-order functions, and has run time and memory consumption linear in the run time of the original program. In addition to a formal description of the translation, we also describe an implementation of this algorithm, and prove its correctness by means of a logical relations argument.
Topics & Concepts
CorrectnessComputer scienceAutomatic differentiationSimple (philosophy)Argument (complex analysis)Mode (computer interface)Translation (biology)AlgorithmConstruct (python library)Order (exchange)Theoretical computer scienceProgramming languagePhilosophyBiochemistryComputationChemistryFinanceOperating systemEpistemologyMessenger RNAEconomicsGeneAdvanced Control Systems OptimizationFormal Methods in VerificationNumerical Methods and Algorithms