The last 15 years have witnessed a remarkable revolution in program synthesis, starting with symbolic and enumerative methods that generate programs that provably satisfy formal user-given specifications, and progressing to the rise of large language models (LLMs), which generate code that often aligns with informal user intent. These two approaches are quite different in how they generate programs, in what specifications they support, and in the types of guarantees they provide about whether the produced program is actually a “good” one. However, both approaches can greatly benefit from applying one key principle: avoiding programs that are provably bad/incorrect.

This talk will present techniques for proving unrealizability, i.e., to prove whether a set of programs only contains bad/incorrect programs that can safely be discarded by a synthesizer. I will also dive into recent work on constraining the output of LLMs to follow user-given intents and show how unrealizability can act as a bridge between formal methods and LLM-based code generation. This connection presents an exciting opportunity for programming language researchers to shape the future of AI-assisted programming.

Loris D’Antoni is an Associate Professor in the Department of Computer Science and Engineering at UCSD. His research helps people write code they can trust. He has won the Phillip R. Certain-Gary D. Sandefur Letters & Science Distinguished Faculty Award, an NSF CAREER Award, the Microsoft Research Faculty Fellowship, Google and Facebook Faculty Awards, and the Morris and Dorothy Rubinoff Dissertation Award. Loris received his Bachelor and master’s in computer science from the University of Torino in 2008 and 2010, respectively, and his PhD in Computer Science from the University of Pennsylvania in 2015.