About me

I am a PhD candidate in CS at George Mason University, advised by Prof. ThanhVu Nguyen. My current research focuses on formal methods for reliable AI and software, particularly program verification, automated theorem proving, and autoformalization in Lean 4. I investigate how to translate informal mathematics and C programs into formal representations with strong correctness guarantees. I am also interested in combining formal verification with LLM generation to produce outputs that are faithful to specifications and mechanically checked.

Prior to my PhD, I obtained my B.E. from Hanoi University of Science and Technology in Hà Nội, Việt Nam. My undergraduate research, under the guidance of Prof. Huynh Thi Thanh Binh, focused on combining Evolutionary Algorithms and Deep Learning for solving combinatorial optimization problems. I also spent two years at VinAI Research as an AI Resident working with my mentor Dr. Dat Quoc Nguyen on Vietnamese-English machine translation.