Probabilistic Programming and Generative Models for Formal Mathematics

Wednesday, February 10, 2021 - 13:00
Daniel Huang

In this talk, I'll describe my research on probabilistic programming and generative models for formal mathematics, two areas that combine probabilistic and symbolic techniques. Probabilistic programming uses programming language technology to simplify the task of probabilistic inference. I'll present my work on compiling probabilistic programming languages to improve the efficiency and variety of probabilistic inference algorithms supported in a probabilistic programming language. I'll also describe some work on a model that learns to predict proof steps given examples of human proofs constructed in a proof assistant.


Daniel Huang is currently a postdoctoral fellowship at Boston College after spending some time at an academic startup spinoff working on AI for printed circuit board layout. He received his PhD from Harvard University and completed a postdoctoral fellowship at UC Berkeley. In a previous life, he was an electrical engineer.