SemanDiff · Semantically correct automatic differentiation
Horizon 2020 — Marie Skłodowska-Curie Actions
- Duration
- 2020-03-15 → 2022-03-14
- EU contribution
- €187,572
- Participants
- 1
- Scheme
- MSCA-IF
Lines connect the coordinator with its partners.
Results in brief
Semantically correct automatic differentiation
> What is the problem/issue being addressed? The problem my project addresses is how to calculate derivatives of functions implemented by piece of computer code in a way that is simultaneously correct, efficient and generally applicable. > Why is it important for society? Such derivative calculations are used in practically every machine learning/AI/computational statistics application, as they are needed to use gradient based optimization (e.g. gradient descent) and integration techniques (e.g. Hamiltonian Monte Carlo). > What are the overall objectives? The overarching objectives of this action are (I) To develop operational and denotational semantic foundations for differential programming. (II) To use this semantics both to prove correct existing differential programming techniques and to inform how to extend them soundly to cope with richer language features. (III) To produce a reference implementation of an AD system to which these correctness proofs apply. > Conclusion The project objectives were realised. I developed various semantically grounded AD techniques, together with an implementation and correctness proof. A key insight during this project was that AD code transformations can be uniquely characterised as certain homomorphic functors on the syntax of programming languages. This homomorphism property is the key to their correctness and to their application to expressive programming languages.
Data: CORDIS, © European Union
Project objective
Many recent advances in machine learning and computational statistics rely on algorithms that calculate derivatives. This use of derivatives has motivated the creation of domain specific modelling languages in which each program can be differentiated automatically, by the compiler. This technique is known as automatic differentiation (AD). AD is typically implemented through source-code-transformations, either directly or indirectly via operator overloading. These transformations become intricate in languages with expressive language features like algebraic data types and higher-order functions. Meanwhile, traditional calculus and differential geometry do not suffice to prove their correctness or even give them meaning, as ordinary differential geometry cannot support higher-order functions. Indeed, such formal correctness proofs have never been published.This project will use the mathematical foundations of diffeological spaces, a conservative extension of traditional differential geometry to higher-order types, to give precisely such correctness proofs. In particular, it will give appropriate source-code transformations for both the forward mode and reverse mode techniques of AD on a language with specified semantics in diffeological spaces. Next, it will prove that these source-code transformations correctly implement the canonical semantic notion of differentiation, as given by the diffeological spaces semantics. It will perform this analysis for a higher-order language with tuples and variant types. These formal descriptions and correctness proofs of AD for expressive languages will be accompanied by closely matching implementations, built on top of the Accelerate framework for purely functional GPU programming.
Original text from CORDIS.
Participants
- UNIVERSITEIT UTRECHT · UtrechtCoordinatorNetherlands
Links
Data: CORDIS, © European Union