between the correctness of autodiff systems and that of applications (e.g., gradient descent) built upon autodiff systems?

We thank the reviewers for their constructive and inspiring feedback. As we cannot see R2 (i.e., Reviewer #2), we respond to the reviews by R1, R3, and R4 only. The correctness of autodiff systems defined in the paper could be misleading to practitioners. We agree with the reviewers' points that (i) the correctness of the applications built upon autodiff systems is as important Also, we do not claim that our correctness condition is "the" Rather we are just suggesting "a" correctness condition that can serve as a reasonable (possibly minimal) We will clarify this limitation in the revised version of the paper. Here are detailed responses to the point (ii) on the applications mentioned in the reviews.