Synthesis modulo oracles

Add to your list(s) Download to your calendar using vCal

• Elizabeth Polgreen, University of Edinburgh
• Friday 16 February 2024, 14:00-15:00
• SS03, Computer Laboratory.

If you have a question about this talk, please contact Jamie Vicary.

In classic program synthesis algorithms, such as counterexample-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?

In this talk, I will present 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 by the synthesis problem. Upon receipt of a query, the oracle responds with 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.

I will also talk about how we are extending this work to incorporate oracles that we may not trust (for instance, large language models), and the challenges this entails.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• SS03, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.