Automated Analyses for Continuous Computations

Abstract

Computer science increasingly uses continuous computations in many applications ranging from neutral networks to scientific computing. To express these computations, powerful domain-specific languages have emerged, namely differentiable and probabilistic programming languages. However, programmers must ensure the programs written in these languages are efficient and robust. But without advanced mathematical training, programmers may lack the expertise needed to provide these assurances.

To address these challenges, I develop automated program analyses for continuous computations in both differentiable and probabilistic programming languages. This talk will focus on my work which built the first systematic framework for enabling general, precise, and scalable analyses of differentiable programs. This systematic framework combines abstract interpretation with differentiable programming and automatic differentiation (AD). I show how this combination allows one to cleanly, formally, and compositionally reason about both a function (e.g., DNN, scientific model, or optimization objective) and its derivatives in a sound manner. Specifically, I will show how to leverage the structure of AD computations to optimally synthesize AD abstractions for the chain rule, product rule, and quotient rule, thus optimizing the precision of the abstract interpretation while simultaneously scaling to large convolutional neural networks (OOPSLA’23). I next show how to extend this reasoning to abstractly interpret derivatives even in the face of non-differentiability (POPL’22). I lastly show how this framework can be generalized to higher-order derivatives and instantiated with more expressive abstract domains to further improve the generality and precision (OOPSLA’22).

This talk also touches upon my work which built the first compiler for generated fixed-point arithmetic probabilistic programs on embedded devices (DAC’21, DATE’23). To conclude, I will discuss future applications and how I aim to bridge the gap between the capabilities of yesterday’s program analyses and the needs of tomorrow’s programmers.

Bio:

Jacob Laurel is a Computer Science PhD Candidate at the University of Illinois Urbana-Champaign advised by Prof. Sasa Misailovic. His research interests center upon applying insights from continuous mathematics to build program analyses for differentiable and probabilistic programming. His current research focuses on building precise, general, and scalable static analyses for Automatic Differentiation. He has published in conferences including POPL, OOPSLA, ESOP, DAC, DATE, CVPR, and ICLR. He received a Sloan UCEM Scholarship as well as a Mavis Future Faculty Fellowship for his contributions. He earned bachelors degrees in both Electrical Engineering and Applied Mathematics (Scientific Computation Track) at the University of Alabama at Birmingham.