PhD Candidate @ UC San Diego, Research Fellow @ Theorem
transformers-GAD. [NeurIPS'24] Grammar-Aligned Decoding: An algorithm to constrain LLMs' outputs without distorting its original distribution
28aspire. A solver of loud framework, for synthesizing strongest over-approximation and weakest under-approximation
6spyro. Synthesizer for provably sound, and most-precise specifications
4sapience. Library Learning Modulo Theory with Automated Rule Deduction
1oopsla23-artifact. Dafny
1