POPL 2022 (series) / POPL Research Papers / Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation
Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic DifferentiationRemote
Thu 20 Jan 2022 10:45 - 11:10 at Salon I - Foundation and Verification of Machine-Learning Systems Chair(s): Gilbert Bernstein
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.
Thu 20 JanDisplayed time zone: Eastern Time (US & Canada) change
Thu 20 Jan
Displayed time zone: Eastern Time (US & Canada) change
10:20 - 12:00 | Foundation and Verification of Machine-Learning SystemsPOPL at Salon I Chair(s): Gilbert Bernstein University of California at Berkeley | ||
10:20 25mResearch paper | A Dual Number Abstraction for Static Analysis of Clarke JacobiansInPerson POPL Jacob Laurel University of Illinois at Urbana-Champaign, Rem Yang University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware, Sasa Misailovic University of Illinois at Urbana-Champaign DOI Media Attached | ||
10:45 25mResearch paper | Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic DifferentiationRemote POPL Faustyna Krawiec University of Cambridge, Simon Peyton Jones Microsoft Research, Neel Krishnaswami University of Cambridge, Tom Ellis Microsoft Research, Richard A. Eisenberg Tweag, Andrew Fitzgibbon Graphcore DOI Media Attached | ||
11:10 25mResearch paper | Interval Universal Approximation for Neural NetworksInPerson POPL Zi Wang University of Wisconsin-Madison, Aws Albarghouthi University of Wisconsin-Madison, Gautam Prakriya Chinese University of Hong Kong, Somesh Jha University of Wisconsin DOI Media Attached | ||
11:35 25mResearch paper | PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull ApproximationsInPerson POPL Mark Niklas Müller ETH Zurich, Gleb Makarchuk ETH Zurich, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware, Markus Püschel ETH Zurich, Martin Vechev ETH Zurich DOI Media Attached | ||