BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Synthesis modulo oracles - Elizabeth Polgreen\, University of Edin
 burgh
DTSTART:20240216T140000Z
DTEND:20240216T150000Z
UID:TALK212239@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:In classic program synthesis algorithms\, such as counterexamp
 le-guided inductive synthesis (CEGIS)\, the algorithms alternate between a
  synthesis phase and an oracle (verification) phase. Many (most) synthesis
  algorithms use a white-box oracle based on satisfiability modulo theory (
 SMT) solvers to provide counterexamples. But what if a white-box oracle is
  either not available or not easy to work with?\n\nIn this talk\, I will p
 resent a framework for solving a general class of oracle-guided synthesis 
 problems which we term synthesis modulo oracles (SyMO). In this setting\, 
 semantic oracles are black boxes with a query-response interface defined b
 y the synthesis problem. Upon receipt of a query\, the oracle responds wit
 h some meaningful piece of information about the semantic behaviour of the
  desired program. This allows us to lift synthesis to domains where using 
 an SMT solver as a verifier is not practical\, for instance\, synthesizing
  controllers for linear time invariant systems. \n\nI will also talk about
  how we are extending this work to incorporate oracles that we may not tru
 st (for instance\, large language models)\, and the challenges this entail
 s.
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR