Talk: Automated Analyses for Continuous Computations

LIVE STREAM: https://uwmadison.zoom.us/j/91319900678?pwd=TEdocGg2cGs3aVlVN3JlUUJwNWp6QT09

Abstract: Computer science increasingly uses continuous computations in many applications ranging from machine learning 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. First, I show how the inherent structure of AD computations and the use of continuous optimization enables one to synthesize AD abstractions for the chain rule, product rule, and quotient rule. In addition to optimizing the precision of the abstract interpretation of AD, this technique scalably analyzes large convolutional neural networks and their derivatives (OOPSLA’23). Next, I will show how to extend this reasoning to abstractly interpret derivatives 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 fixed-point arithmetic probabilistic programming on embedded systems (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 Sasa Misailovic. His research interests center upon applying insights from continuous mathematics to build program analyses for differentiable and probabilistic programming languages. His current research focuses on building general, precise, and scalable static analyses for Automatic Differentiation. He has published in multiple 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.