ACL2 Workshop 2025
Abstracts

Formal methods for system engineering have traditionally faced two fundamental barriers to adoption: formal specifications are hard to write, and formal proofs are hard to automate at scale. In this talk, I will argue that recent progress in machine learning offers a historic opportunity to overcome these problems. Specifically, I will summarize recent progress in the emerging field of AI for formal mathematics, including developments in automatic formalization, proof synthesis, and the acceleration of formal reasoning with informal methods. I will show that these techniques have immediate applications in software and hardware verification and that conversely, formal system engineering tasks raise interesting foundational questions in AI for math. I will end the talk by highlighting some productive ways in which the formal methods and AI communities can work together in this research area.

Bio: Swarat Chaudhuri (http://www.cs.utexas.edu/~swarat) is a Professor of Computer Science at UT Austin and a Research Scientist at Google Deepmind. He is known for his work at the interface of machine learning and automated reasoning, including program synthesis, neurosymbolic reasoning, and certified learning. Prof. Chaudhuri has received the NSF CAREER award, the ACM SIGPLAN John Reynolds Dissertation award, Meta and Google Research awards, several ACM SIGPLAN and SIGSOFT distinguished paper awards, and an Op-Ed Project Fellowship. He has served on the program committees of most of the prominent venues in formal methods, machine learning, and programming languages and has been a Program Chair for the CAV and ICLR conferences.