Skip to content (access key 's')
Logo of Technion
Logo of CS Department
Events

The Taub Faculty of Computer Science Events and Talks

SCOOPY: Enhancing Program Synthesis with Hierarchical Example Specifications
event speaker icon
Tomer Katz (M.Sc. Thesis Seminar)
event date icon
Monday, 17.03.2025, 13:30
event location icon
Taub 601 & Zoom
event speaker icon
Advisor: Dr. Hila Peleg

As program synthesizers become integrated into IDEs, programmers combine synthesized code and manually written code within the same project. We therefore built a Programming-by-Example (PBE) synthesizer that documents the example specifications provided to it alongside the result snippet that satisfies them.

We also modified the IDE to treat these example scopes as localized tests for the code they surround, in case they or the code are edited. Unless strict limitations are imposed on how users can edit example scopes, and where they can call the synthesizer, scopes of example-specified code can wind up encompassing others.

The programmer can decide to send such a hierarchical scope to the synthesizer, to refactor the code, to automatically correct manually-written code, or simply to fix a mistake found in an example. State of the art PBE synthesizers cannot handle this hierarchical specification: synthesis will only consider the outer-most block, discarding the user intention contained in inner scopes. This can lead to undesired, overfitted programs.

To address this information loss we propose Spec Scooping, a syntax-guided technique to “scoop” out and preserve the intent from inner example scopes. We accompany Spec Scooping with a host of IDE features to help programmers edit example scopes and the code inside them, including an identification of when specifications contradict each other. Since Spec Scooping enriches the specifications sent to the synthesizer, it also requires modifications to the bottom-up Observational Equivalence synthesis algorithm.

We implement Spec Scooping in a tool ScooPy, including a development environment that supports scooping and an extended synthesizer.We evaluate ScooPy on 33 benchmarks based on SyGuS competition benchmarks.

Our results show that hierarchical specifications are generally more expressive, and that, compared to nonhierarchical specifications at the same level of expressiveness, scooping can provide a performance boost. We also performed two small-scale qualitative studies of ScooPy to gauge the benefits of attaching the specifications to a synthesis result and of users’ interaction with ScooPy’s development environment.