Computer Science Speaker Series Master Calendar

View Full Calendar

The End of Programming Is a New Beginning for Verification

Event Type
Seminar/Symposium
Sponsor
The Department of Computer Science, University of Illinois and FM/SE Seminar
Location
Siebel 2405
Virtual
wifi event
Date
Apr 26, 2024   2:00 pm  
Speaker
Prof. Swarat Chaudhuri, UT Austin
Contact
Isha Chaudhary
E-Mail
isha4@illinois.edu
Views
87
Originating Calendar
Computer Science Speakers Calendar

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.

link for robots only