Personal statement
I am a 5th-year PhD candidate in CSE at UC San Diego, advised by Loris D'Antoni. My research focuses on scaling up formal reasoning through modularization and abstraction, specifically within program analysis, program synthesis, and proof search. I have also explored constrained decoding of Large Language Models (LLMs) as a method for ensuring reliable code generation.
Outside of work, I enjoy playing acoustic guitar and training for marathons.
Education & Certification
PhD in Computer Science and Engineering
UC San Diego (Transferred from UW-Madison)
Sep 2024 - Current
MS in Computer Science
Aug 2021 - May 2024
BS in Computer Science and Mathematics
Pohang University of Science and Technology
Summa Cum Laude, Engineering's Valedictorian
Feb 2015 - Feb 2021
Job Experiences
Research Fellow
Theorem
Mar 2026 - Current
Applied Scientist Intern
Amazon Web Services
Jun 2024 - Aug 2024
Applied Scientist Intern
Amazon Web Services
May 2023 - Sep 2023
Malware Analyst, Security Personnel
ROK Army Headquarter (Obligatory Military Service)
Aug 2018 - Mar 2020
Publications
Constrained Sampling for Language Models Should Be Easy:
An MCMC Perspective [arXiv]
Emmanuel Anaya Gonzalez*, Sairam Vaidya*, Kanghee Park, Ruyi Ji,
Taylor Berg-Kirkpatrick, Loris D'Antoni
*equal contribution
NeurIPS 2025
Flexible and Efficient Grammar-Constrained Decoding [arXiv] [Github]
Kanghee Park, Timothy Zhou, Loris D'Antoni
ICML 2025
LOUD: Synthesizing Strongest and Weakest Specifications [arXiv][Github]
Kanghee Park*, Xuanyu Peng*, Loris D'Antoni
*equal contribution
OOPSLA 2025
Grammar-Aligned Decoding [arXiv] [Github]
Kanghee Park*, Jiayu Wang*, Taylor Berg-Kirkpatric, Nadia Polikarpova, Loris D'Antoni
*equal contribution
NeurIPS 2024
Modular System Synthesis [arXiv]
Kanghee Park, Keith J.C. Johnson, Loris D'Antoni, Thomas Reps
FMCAD 2023
Teaching
TA for CS513 (Numerical Linear Algebra)
University of Wisconsin-Madison
2022 Spring
TA for CS240 (Discrete Mathematics)
University of Wisconsin-Madison
2021 Fall