Final Project Ideas and Examples

Final Projects that have been done in similar courses

• Synthesizing Smart Contracts. Link. As the use of cryptocurrencies has increased in popularity, so too has the use of smart contracts based on blockchain. However, smart contracts are typically written by non-programmers who do not pay attention to best-practices. As a result, there have been several “heists” of millions of dollars. Can we apply program synthesis for auto-programming smart contracts?

• Directing Program Synthesis by Extracting Image Features for Refinement Types. Link. Current machine-learning techniques are data-hungry or specification-hungry. Program synthesis matters in solving problems with less data or specifications. Refinement-types perform well to reduce the searching space. The current application domain of refinement-types-directed search only lies in real values and simple programs. Can we apply such synthesis techniques for image processing?

• Program Synthesis in Continuous Domains Link. Most existing program-synthesis techniques are based on discrete search (such as top-down and bottom-up enumeration). However, programs do contain continuous real-valued parameters. Can we improve existing synthesis techniques for "enumerating" a large number of continuous parameter values? Similarly, can we apply continuous optimization methods for solving sketch-based program synthesis problems? Link

• Program Synthesis for Coarse-Grained Spatial Architectures Link. Coarse-grained spatial architectures are currently a popular hardware accelerator design because of their massive parallelism and energy efficiency. Coarse-grained designs consist of an array of Processing Elements (PEs). However, industrial hardware design tools do not offer functionality to map complex operations to systolic architectures, designers rely on manual solutions. Can we apply program synthesis to speed up this process?

• Syntax Evolution through Augmenting Topologies Link. Program synthesis relies on hand-crafted grammar rules (productions). The degree of flexibility of grammar rules can affect the efficiency of synthesis. Can we "synthesize" grammar rules as well?

• Neural Program Synthesis with Soft Actor-Critic Link. In a programming-by-example (PBE) framework, supervised learning has shown to be promising. However, supervised learning only optimizes for exact program matches, ignoring that a program could have a large amount of syntactically different but semantically equivalent counterparts. Can we apply reinforcement learning instead to improve the consistency of PBE?

• Implementing Conflict-Driven Learning on SyGuS Link. Program synthesis can be developed as an instance of Conflict-Driven Clause Learning (CDCL). This method takes inspiration from CDCL in SAT solvers, allowing the synthesizer to learn from past mistakes, and find a large number of other candidate programs that fail for similar reasons. Thus, the synthesizer can prune a large number of programs per step instead of just one as done in SyGuS. Can we demonstrate the effectiveness of this idea on the massive SyGuS benchmarks?

• Program Refinement from Data structure Integrity Constraints Link. Programmers add auxiliary data structures to optimize app performance i.e. cache. To maintain correctness, the updated program needs to satisfy a data structure integrity constraint that relates the state of the new data structures to the original structures. Manually updating the application to satisfy the integrity constraint is time-consuming and error-prone. Can we apply program synthesis to automate such a tedious procedure?

• Interpretable Neural Program Induction Link. Neural program induction seeks to induce a latent program representation, using a neural network to simulate the program to synthesize. Can we combine neural program induction and classic enumerative synthesis approaches to induce interpretable programs?

• Synthesizing Safe Multi-Agent Environments Link. Model-based Reinforcement learning seeks to optimize control policies based on environment models inferred from data. Environment model inference is, however, challenging. Can we apply program synthesis to learn Environment models as programs to capture both state-transition dynamics as well as rewards and specifications such as what can or cannot happen in an environment?

• Bottom-up Euphony Euphony (see lecture 4) guides top-down enumeration with a probabilistic model. Can use the same model to guide bottom-up search (roughly: expand the program bank in the order of probabilities rather than in the order of height)? Another idea: as we discover programs that solve some subsets of the examples, can we adjust the probabilities of the model encouraging it to use those subprograms?

• Synthesis for Pyret Pyret is a programming language designed for teaching. In Pyret, students are encouraged to write tests before they implement a function. In this project, you would add a synthesizer to Pyret that can generate a program satisfying the student-written tests. The synthesis results can be used both to help the student arrive at the solution and to show them where their tests are insufficient.