Reviews: Provably Correct Automatic Sub-Differentiation for Qualified Programs

In this submission, the authors consider the problem of computing sub-differentiation for a class of non-smooth functions automatically and correctly. They give a very nice example that illustrates problems with current automated differentiation frameworks, such as tensorflow and pytorch. Then, the authors prove a chain rule for the one-sided directional derivative of a composite non-smooth function satisfying certain assumptions. Based on this rule, the authors derive a (randomized) algorithm for computing such a derivative for a particular kind of programs only with constant overhead. The algorithm is very similar to the one for back-ward automatic differentiation except that its forward computation is based on the newly-proved chain rule in the submission, rather than the standard chain rule for differentiation.