Advised by Prof. Sean Welleck

• Developed the miniCTX benchmark to evaluate large language models in formal mathematics, focusing on real-world proof generation using context information.
• Fine-tuned deepseek-coder-1.3B model using file-tuning data, which incorporates context information alongside traditional state-tactic pairs, outperforming larger models like Llemma-7B and GPT-4o.
• Developed a Python wrapper for Lean REPL, simplifying interactions with Lean and enhancing usability.
• Published the first-author paper “miniCTX: Neural Theorem Proving with (Long-)Contexts”.
• Planning to extend the benchmark to areas beyond math, such as program verification, and to evaluate premise selection methods.

Advised by Prof. Paul Liang and Prof. Louis-Philippe Morency

• Developed a real-time multitasking framework for Open Face 3.0, supporting comprehensive facial behavior analysis including landmark detection, action unit detection, facial expression recognition, and gaze estimation.
• Enhanced toolkit accessibility by developing Python bindings that support both Open Face 2.0 and Open Face 3.0, enabling more flexible integration into computer vision applications.
• Implemented generative models for data augmentation, specifically targeting non-frontal face images, to enhance facial landmark detection and emotion recognition accuracy.

Advised by Prof. Pengfei Liu

• Developed and refined step-by-step math problem prompts for training data based on error cases, enhancing the reasoning capabilities and output readability of Llama2, resulting in a 10% performance increase on the GSM8K dataset.
• Explored methods to integrate supplementary datasets with the primary dataset for supervised fine-tuning to address specific shortcomings, such as arithmetic calculations in main mathematical tasks.
• Created and executed a variety of supervised fine-tuning experiments to understand responses from large language models.
• Contributed to the development of Abel model and “Reformatted Alignment” paper.

Advised by Prof. Oana Carja

• Investigated the effects of spatial structures, as characterized by graph properties, on evolutionary dynamics.
• Explored the relationship between phylogenetic tree structures and graph properties, focusing on tree balance metrics.
• Utilized statistical tools to discern patterns of clonal evolutionary dynamics within complex graphs.
• Developed simulation programs to validate mathematical models.
• Conducted research into applications of these principles in network theory and biology.

Advised by Prof. Giovanni Leoni

• Investigated various properties, including bounded variation and absolute continuity, of decreasing rearrangement functions in Sobolev space.
• Collaborated with a small group to write research paper and presented at Mathematics Undergraduate Research Symposium (slides).