Abstract: Machine learning is set to fundamentally change computing — and, according to some, end programming as we know it — in the coming decade. On the one hand, many human-written algorithms spanning every layer of the software stack will likely be replaced by neural networks. On the other hand, learning-based code generators will take on an ever-larger share of software engineering.
These developments open up a tremendous opportunity for formal methods. Neural networks are notoriously brittle and opaque, and formal verification can be a valuable approach to inducing trust in systems that are neurally generated or have neural modules. However, to reach their full potential, such verification methods cannot just be post-hoc but must be tightly coupled with learning.
In this talk, I will describe a few forms that such a coupling could take. I will start by introducing a framework of certified sequential-decision-making agents that have access to a set of external proof-checking tools. I will then describe several instantiations of this framework, including a model-based reinforcement learning algorithm whose training procedure incorporates feedback from a formal verifier, a mechanism for safe exploration that uses formal program synthesis as a step within a mirror descent, and an in-context-learning agent that uses an external proof assistant to generate certifiably correct code.
Bio: Swarat Chaudhuri (http://www.cs.utexas.edu/~swarat) is a Professor of Computer Science and the director of the Trishul laboratory at UT Austin. 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.
