ML for formal reasoning
I am a UW second-year undergraduate studying CS and Math and doing research into neural theorem proving.
ICLR 2026
Talk to me about my research, neural theorem proving, or today's invited talk.
The VerifAI-2 workshop runs April 26 in Room 208. If you are also there, please pay me a visit.
About
I am early in my research career, and looking to explore new directions. My current interests are in RL methods for proof discovery, formal verification using AI, and autoformalization.
At UW, I am especially interested in the loop between theorem provers, diagnostics, data generation, and language models. I like work that treats proofs as more than a sequence of tokens.
Publication
ICLR VerifAI Workshop, 2026
With Evan Wang, Daniel Lee, Siyuan Ge, Ajit Mallavarapu, Jarod Alper, and Vasily Ilin.
The paper introduces APRIL, a dataset for learning Lean proof repair from erroneous proofs, compiler diagnostics, repaired proofs, and feedback-grounded explanations.
Research
What makes one proof an erroneous version of another? How do we train models to go from one to the other? I find these questions fascinating.
How can we trust vibe-coded applications? How can we build secure systems in the face of the generational bug-finding tools to come? I increasingly believe that massive formal verification aided by AI is the answer.
What do we need to produce verification that stands up to real-life threats? Do we need to formalize all the way down to the physics underlying the hardware before we can properly verify software, or can we start in the middle? These questions are inherently important to the way we work going forward.
Connect