Emily First
About me
I am a postdoctoral researcher at UC San Diego working with Sorin Lerner (but I work remotely from NYC). In May 2023, I completed my PhD in Computer Science at UMass Amherst, where I worked with Yuriy Brun in the Laboratory for Software Engineering Research (LASER). My research is at the intersection of software engineering, programming languages, and machine learning. Specifically, I focus on creating tools to automatically generate proofs of software correctness in Coq and Isabelle/HOL. In May 2017, I received a BS in Math and Computer Science from Harvey Mudd College.
Research and Publications
CoqPyt: Proof Navigation in Python in the Era of LLMs
Pedro Carrott, Nuno Saavedra, Kyle Thompson, Sorin Lerner, João F. Ferreira, Emily First
To appear at FSE 2024 (Demo Track)
demo video, github
Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving
Chenyang An, Zhibo Chen, Qihao Ye, Emily First, Letian Peng, Jiayun Zhang, Zihan Wang, Sorin Lerner, Jingbo Shang
To appear at ACL 2024
arXiv
Getting More out of Large Language Models for Proofs
Shizhuo Dylan Zhang, Emily First, Talia Ringer
AITP 2023
arXiv
Baldur: Whole-Proof Generation and Repair with Large Language Models
Emily First, Markus N. Rabe, Talia Ringer, Yuriy Brun
ESEC/FSE 2023
ACM SIGSOFT Distinguished Paper Award
arXiv
Passport: Improving Automated Formal Verification Using Identifiers
Alex Sanchez-Stern*, Emily First*, Timothy Zhou, Zhanna Kaufman, Yuriy Brun, Talia Ringer
TOPLAS 2023 (presented at PLDI 2023)
arXiv github (* Co-first authors)
Proofster: Automated Formal Verification
Arpan Agrawal, Emily First, Zhanna Kaufman, Tom Reichel, Shizhuo Zhang, Timothy Zhou, Alex Sanchez-Stern, Talia Ringer, Yuriy Brun
ICSE 2023 (demo track)
preprint, tool
Diversity-Driven Automated Formal Verification
Emily First, Yuriy Brun
ICSE 2022
ACM SIGSOFT Distinguished Paper Award
video, doi, github, VM
TacTok: Semantics-Aware Proof Synthesis
Emily First, Yuriy Brun, Arjun Guha
OOPSLA 2020
video, doi, github, VM