Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library

DOI10.46298/LMCS-19(4:5)2023arXiv2112.07292MaRDI QIDQ6178671FDOQ6178671

Authors: Paulo Emílio de Vilhena, François Pottier 

Publication date: 16 January 2024

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/2112.07292

Recommendations

• Reverse AD at higher types: pure, principled and denotationally correct
• Correctness of automatic differentiation via diffeologies and categorical gluing
• On formal certification of AD transformations

zbMATH Keywords

program verificationseparation logicautomatic differentiationeffect handlers

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites Work

• Programming with algebraic effects and handlers
• Evaluating Derivatives
• Handlers of Algebraic Effects
• Title not available (Why is that?)
• An introduction to algebraic effects and handlers (invited tutorial paper)
• Modular verification of programs with effects and effects handlers
• Exception Handling in CLU
• Title not available (Why is that?)
• Beautiful differentiation
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Effect handlers via generalised continuations
• Shallow effect handlers
• There and back again
• Functional differentiation of computer programs
• Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
• Modular verification of programs with effects and effect handlers in Coq
• Typed Tagless Final Interpreters
• Title not available (Why is that?)
• Correctness of automatic differentiation via diffeologies and categorical gluing
• On the versatility of open logical relations. Continuity, automatic differentiation, and a containment theorem
• Reverse AD at higher types: pure, principled and denotationally correct
• Functional differentiation of computer programs
• Title not available (Why is that?)
• Koka: programming with row polymorphic effect types
• Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala
• Separation Logic Tutorial

This page was built for publication: Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6178671)