Final Project
The final project is a significant component of this course, worth 35% of your grade. It provides an opportunity to explore advanced topics in machine programming and apply the concepts learned throughout the semester.
Project Overview
Students will pick a research problem in program synthesis, analysis, or related areas. We provide a list of project ideas below, but you are encouraged to propose your own ideas based on your interests and background. The project can be theoretical, experimental, or a combination of both.
Working in a team
The project should be completed with at most 3 students. In the proposal, you should describe the project idea, the team members, and the division of labor.
Project Requirements
- Proposal (5%): A 2 page document outlining your project idea, methodology, and expected outcomes
- Implementation (20%): Working code and/or theoretical development
- Report (5%): A comprehensive written report describing your work
- Presentation (5%): A 10-minute presentation to the class
Project Timeline
- TBD: Project proposal due
- TBD: Final project presentations (during the final exam period, Dec 15–23; time and location TBD)
- TBD: Final report due (via Grade-scope)
Presentation Details
The final project presentations will take place on a date TBD during the final exam period (Dec 15–23); the time and location are also TBD. Each group will have 10 minutes for presentation followed by 5 minutes for Q&A. Please make sure your slides are well-prepared and that you stay within time so everyone gets a fair slot.
Final Write-Up Requirements
The final project report/write-up is due TBD and should be submitted via Grade-scope.
Formatting Requirements
Please typeset your write-up professionally using LaTeX or Typst. For this class, we will use the NeurIPS 2026 template:
Note: If you do not know Typst yet, please look it up as it may be a good replacement of LaTeX.
Content Requirements
Your write-up must be at least 4 pages in length (not counting the references) and must include the following sections:
- Abstract
- Introduction
- Related Works
- Conclusion & Future Works
The sections in between may include things like "Methodology", "Evaluation", "Benchmark", "Framework", "Case Study", or anything that is key to your project. Please cite the related works professionally.
Project Ideas
Here are some example project areas to consider:
- Build a mid-to-large-scale dataset for a particular programming language or domain, whether by hand, by crawling, or with existing models.
- Pick a low-resource language (Haskell, Prolog, Datalog, Scallop, CodeQL, LEAN, Coq, Z3, Racket, Clojure, LaTeX, TikZ, Processing, PDDL) and build a small-scale dataset to measure how well LLMs synthesize programs in it.
- Pick a high-resource language but a narrow domain — kernel drivers in C, CUDA, Unreal Engine in C++, neural network modules in Python/PyTorch/JAX — and evaluate LLMs there.
- Design a small domain-specific language for robot control, games, theorem proving, databases, mathematics, logic, visualization, or animation, and show how well LLMs generate programs in it.
- Build a conversational coding agent that carries out edits and feature requests on a codebase.
- Build a downstream application that relies on program synthesis.
- Use LLMs to synthesize formal specifications for existing programs, and evaluate the generated specifications rigorously.
- Identify security vulnerabilities in LLM-generated programs.
- Reimplement a technique from the literature (see Readings).
Note: These are suggestions only. You are encouraged to propose your own ideas based on your interests and background.
Turning into a Research Project
You are strongly encouraged to do so. If you have an interest in turning your final project into an academic research paper, please come to the instructor as early in the semester as possible.
In Fall 2025, a few course projects were later turned into research papers that are currently under submission:
- Yuming Feng et al., Theory-Scale Auto-Formalization of Logics for Computer Science
- Tadd Mao et al., Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs
- Zhiming Chang et al., BODHI: Precise OS Kernel Specification Inference