At Microsoft Research, I worked with Nikolaj Bjørner to design and implement a novel parallel framework for the Z3 SMT solver that uses feedback from active search to steer solving. Our approach dynamically builds a binary partition tree of the search space by sampling from workers’ VSIDS statistics during solving. We introduced a novel search-space pruning mechanism that harnesses the full power of core-based CDCL-style pruning to continuously shrink the partition tree. We further optimized our architecture by incorporating online backbone detection into worker threads, as well as a terminate-on-demand mechanism to eagerly eliminate work on pruned subproblems. The resulting algorithm is highly generalizable and scalable. The implementation can be found here and was released in z3-5.0.0.

At Microsoft Research, I contributed to the training pipeline (data augmentation + RL) for a 32B LLM specialized in program verification. I was responsible for preparing and augmenting Lean datasets for SFT and RL training, building a custom Dockerized Lean verification server, and evaluating model checkpoints.

In a class project, we adapted the constrained decoding algorithm Grid Beam Search (GBS) to impose lexical constraints on transformers. GBS was originally applied to stateful Neural Translation Models for seq2seq translation. We developed a new pipeline for generating structured outputs from a given prompt and set of lexical constraints that supports any pretrained autoregressive language model, which we chose to be GPT2. Then, we fine-tuned GPT-2 on a corpus of Chekhov’s stories. Our subjective analysis showed that GBS + fine-tuned GPT2 gave more interesting and meaningful domain-specific results than GBS + GPT2 alone.

I introduced a unified, hierarchical meta-representation of sequence data structure called the structural temporal graph (STG), a k-partite directed acyclic graph, and applied it to symbolic music. Then, I used simulated annealing to develop a measure of structural distance between two music pieces rooted in graph isomorphism. Finally, I combined the formal guarantees of SMT solvers with nested simulated annealing over structural distances to frame and solve the dually NP-hard combinatorial optimization problem of music structure summarization as an extension of the Generalized Median Graph problem.

Under the mentorship of Prof. Ben Wiedermann at Harvey Mudd College, I created MusAssist, a DSL for music notation bridging the abstraction gap between music theory and composition. MusAssist gives end-users the novel ability to describe musical templates, such as cadences, at precisely the abstraction level as the music theoretic structures they represent, which models what a composer would organically conceive when composing by hand. I designed MusAssist’s syntax using a participatory design approach, and then wrote a Haskell-based compiler that translates MusAssist to MusicXML, a lower-level language accepted by most music notation software, for further manual editing.

Under the mentorship of Prof. Mark Huber at Claremont McKenna College, I created a novel system of Markov chains using inverse transform sampling to rapidly generate musical sketches, giving end-users the ability to create custom-length music in the style of a desired piece.

Computer science students with physical disabilities struggle to interface with a keyboard and mouse, and thus write code. Voice-to-code technologies, such as Talon Voice, help alleviate this burden. However, to our knowledge, no existing voice-to-code software supports natural language commands, which further cognitively burdens the user. To that end, in a class project, we proposed and implemented an extension to Talon Voice that enables natural language dictation via an LLM-based interpreter.

In a class project, we examined the impact of GitHub Copilot on Test-First Development, a software development paradigm where tests are written before implementation. We conducted a between-subjects (no Copilot vs Copilot) pilot study, consisting of coding tasks and pre- and post-task surveys. Participants iterated between writing a comprehensive API and test suite for a problem, with or without Copilot. We found that while Copilot enhanced coding speed, it resulted in superficial problem comprehension and decreased scope of the test suites.

In order to perform genomic data analyses, bioinformaticians are frequently forced to do cubmersome pre-processing of their data. To addres these challenges, in a class project, we developed pgen-rs, a tool enabling end-users to write their data wrangling requirements in natural language enhanced by LLM suggestions. pgen-rs converts natural language to a DSL that is executed by out Rust-based high-performance genomic data processor enabled by the PLINK file format.

In a class project, we developed ProCon, a tool implementing continuous, rule-based enumeration for just-in-time bottom-up search in SyGuS problems. Programs are enumerated in order of continuous, nonrounded weights as determined by a probabilistic weighting function. ProCon thus leverages the full power of the probabilistic model since it does not round the probabilities to discrete weights as size-based enumeration does.

In an independent study during my undergrad, I assisted Prof. Christopher Raphael at Indiana University Bloomington on a project investigating audio algorithms for music score alignment. We developed a novel algorithm to synchronously assemble remotely recorded audio tracks without click tracks in order to address the need for remote media collaboration induced by the ongoing COVID pandemic.

In a class research project during my first year of undergrad, I created an original Python-based model to sonify genetic material by translating DNA to MIDI piano chords under the mentorshop of Prof. Zachary Dodds. By mapping nucleotides and codons to musical chords, my work introduced a novel and straightforward means of conceptualizing both the structure of a gene and the processes of biological splicing and translation that is accessible to users of all scientific backgrounds.