![Theoretical Foundations of Computer Systems_hi-res logo](/sites/default/files/styles/workshop_banner_sm_1x/public/2023-03/Theoretical%20Foundations%20of%20Computer%20Systems_hi-res.png.jpg?itok=Xu9k2zci)
Abstract
A key principle in automated reasoning is the idea to alternate between a teacher and a learner. The learner forms hypotheses, which are incrementally refined using feedback given by the teacher. In this talk, I will discuss the importance of the vocabulary (and hence "bandwidth") of the feedback given by the teacher by looking at challenges faced by the well-known CEGIS algorithm. I will present an improved variant, called CEGIS-T, which uses expressive feedback on the syntax of potential solutions. This addresses a particular challenge for program synthesizers, namely the generation of programs that require non-trivial constants, which is out of reach for many state-of-the-art synthesizers. I will conclude with forward-looking ideas on how to elevate the syntactic feedback to semantic feedback.