PoP Seminar Talk

Searching for good programs, by avoiding bad ones

Jinwoo Kim, Ph.D. Student, Computer Science and Engineering
Tuesday, 10 November, 2026; 3:00pm
GHC 8102
Host: Jan Hoffmann

Abstract

Search (e.g. searching for a program, structured output, etc.) is a nearly universal component in solutions to modern problems. For many formal objects (such as code or proofs)—including those driven by LLMs—search algorithms rely on a loop where we first generate a candidate, check its correctness using a set of rules, and if the candidate is incorrect, iterate the process until the solution is found. This talk asks the question: instead of reasoning about the correctness of generated candidates individually, can we characterize the behavior of entire sets or distributions of outputs, so they can be avoided by the search algorithm and make search more efficient?

In this talk, I will present an overview of my work on this problem and how it can be used to empower both symbolic and neural search. I will first focus on unrealizability logic, a proof system for characterizing the semantics of sets of programs for symbolic program synthesis. Then I will discuss some of my work on applying this line of thought towards neural search via generative AI, with a focus on preserving the advantages of neural search while applying symbolic constraints via conditioning the distributions generated by LLMs.

Bio

Jinwoo Kim is a fifth-year Ph.D. student at UC San Diego, working in the intersection of formal methods and machine learning with Loris D’Antoni. His current research focuses on applying formal methods to make search procedures such as generative AI more reliable, efficient, and understandable. Prior to his focus on neural synthesis, his primary research was in formal program semantics and synthesis, leading to projects such as Semantics-Guided Synthesis and Unrealizability Logic.