We apply program verification technology to the problem of specifying and verifying automatic differentiation (AD) algorithms. We focus on ``define-by-run'', a style of AD where the program that must be differentiated is executed and monitored by the automatic differentiation algorithm. We begin by asking, ``what is an implementation of AD?'' and ``what does it mean for an implementation of AD to be correct?'' We answer these questions both at an informal level, in precise English prose, and at a formal level, using types and logical assertions. After answering these broad questions, we focus on a specific implementation of AD, which involves a number of subtle programming language features, including dynamically allocated mutable state, first-class functions, and effect handlers. We present a machine-checked proof, expressed in a modern variant of Separation Logic, of its correctness. We view this result as an advanced exercise in program verification, with potential future applications to the verification of more realistic automatic differentiation systems and of other software components that exploit delimited control effects.
翻译:我们用程序核查技术来说明和核查自动区分算法的问题。 我们侧重于“ 逐项计算 ”, 这是一种AD的风格, 即必须区分的程序由自动区分算法执行和监测。 我们首先询问, “ 执行什么是AD? ” 和“ 执行AD正确意味着什么? ” 我们用准确的英文资料非正式地回答这些问题,并使用各种和合乎逻辑的说法正式地回答这些问题。 在回答这些广泛的问题之后, 我们侧重于AD的具体实施, 其中包括一些微妙的编程语言特征, 包括动态分配的变异状态、 一流功能和效果处理器。 我们提出了一个机器检查的证明, 以现代的“ 分离逻辑变式” 来表达其正确性。 我们认为这一结果是一种先进的程序核查工作, 在未来有可能应用到更现实的自动区分系统和其他软件的核查, 来利用限定的控制效果。