Abstract

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.