Project Ideas

Here are some project ideas, roughly in the order of increasing difficulty / scope. For all projects that involve applying synthesis in a new domain, the default is to use an existing synthesis framework such as Sketch, Rosette, or PROSE, but you can also implement a synthesizer from scratch if you feel up to task. You can also take a look at the completed projects and implement an alternative solution for one of them. Please talk to us before deciding on your project topic.

• Reproduce experimental results from any paper we read.
• CEGIS: Re-implement a symbolic program synthesizer based on a CEGIS loop. Your synthesizer must accept input in the Sygus format.
• Grammar reduction: In lecture 3, we talked about how a grammar can be reduced so that it doesn't generate redundant expressions in the first place. Implement a tool that generates a reduced grammar from a set of equivalences or rewrite rules. Compare it with a tool a-la Smith&Albarghouthi that checks generated programs for normality.
• Extending Probe: Probe is a SyGus solver that performs weighted bottom-up search with weights learned on the fly, from partial solutions. You can consider extending Probe in several ways:
  • Add conditionals: Currently Probe has no specific optimizations for learning conditionals, hence it performs poorly on conditional-rich Euphony benchmarks. The idea would be to add EU-Solver style condition abduction to Probe.
• Synthesis with ASP There is some recent work on using Answer-Set Programming (ASP) to synthesize Datalog programs. The goal of this project would be to apply ASP to a different relational domain, e.g. synthesizing context-free grammars (or tree grammars).
• Extending LEAP: LEAP is a tool we developed that combines an LLM with Live Programming to help programmers validate AI's code suggestions. You can consider extending LEAP in several ways:
  • Currently the programmer needs to invoke the function on a concrete input in order to see its behavior with Live Programming. You will modify LEAP to use the LLM to generate informative inputs
  • Integrate LEAP with either human-written or automatically-generated assertions/tests (perhaps following the ideas in this paper) to filter out irrelevant suggestions
  • Different AI suggestions are often semantically similar (even if syntactically not identical). You could extend LEAP to analyze program traces in order to filter out semantically equivalent programs.