Several faculty members are considering working with students this summer. The last section of this document contains some further information. Please contact them directly if you are interested and would like more information.
- Greg Anderson (link to apply)
Probabilistic programs are a structured way to model probability distributions that arise in certain computational problems, especially in machine learning. Alternatively, we can view probabilistic programs as programs which sample from some set of probability distributions. The structure of a probabilistic program gives rise to some interesting avenues for analyzing its behavior, building on existing work in the analysis of deterministic programs. In this work, we aim to automatically search for proofs of correctness for certain classes of properties of systems described by probabilistic programs. This project will require thinking carefully about proof techniques and engaging with some of the details of probability theory and programming language semantics. You can think of it as a "meta-proving" project; we don't just want to prove that particular programs work, we want to come up with a mechanized way to search for proofs given an arbitrary program and correctness specification in some language.
Since this project is heavily reliant on proof techniques and automation, it'll be important to be comfortable with basic proof strategies (MATH 112 and 113) as well as some coding (CSCI 121, MATH/STAT 141, or similar). The particular strategies I plan to look at also draw somewhat heavily from linear algebra (MATH 201). Beyond those, there are a number of other classes which might be helpful for this research, but I would encourage you to consider it even if you haven't taken these classes:
- MATH 202 (Vector Calculus)
- MATH 391 (Probability)
- CSCI 382 (Algorithms and Data Structures)
- CSCI 384 (Programming Languages)
- Erica Blum (consensus algorithms, more information here)
- Harper Knittel
This summer, we will select and study a problem in graph algorithms. This is a broad field of study, including topics like matching (e.g., matching with your tinder date), shortest path (e.g., getting to your tinder date), clustering (e.g., determining who is in your tinder filter radius), and more! Work will be predominantly theory-oriented (proofs of near/optimality, runtime, and hardness), but may include other areas like problem modeling, human experiments, and implementation. - Charles McGuffey
- Anna Ritz (computational biology & graph algorithms - looking for two students interested in developing software - see this github). Apply through the Biology Department by March 5 - email Anna to develop a proposal.
- Lenny Wainstein (statistics)