I am an incoming Ph.D. student at Carnegie Mellon University (CMU), affiliated with the Language Technologies Institute (LTI) in the School of Computer Science (SCS), and the newly founded Institute for Computer-Aided Reasoning in Mathematics (ICARM). I am working on verifiable reasoning agents at Apodex, mentored by Dr. Kaiyu Yang.

I received my B.S. in Computer Science from California Institute of Technology (Caltech), with a minor in Robotics, advised by Prof. Steven Low and Prof. Günter Niemeyer.

I study machine reasoning, in both formal and informal worlds: how AI systems can derive conclusions, act on them, evolve as tasks drift, and remain reliable when settings become complex.

(1) Formal reasoning. In mathematics, code, and other formalizable domains, verifiability gives us a rare foundation for building dependable reasoning systems. I develop models and infrastructure [LeanDojo] [Lean Copilot] that form a bidirectional loop between formal environments and ML systems, enabling efficient human-AI collaboration in theorem proving [Human-AI Formalization]. Building on this loop, I move beyond static models toward adaptive agents that evolve with growing libraries [LeanAgent] and expanding contexts [LeanProgress].

(2) Informal reasoning. In open-ended natural-language settings, I continue to study how agents adapt [Adaptation] [Steer2Adapt] and generalize [Generalization] [Idiom]. These goals, however, become harder to pursue with a lack of symbolic verifiers or reliable reward signals. One way forward is to develop agentic evaluations that provide rich behavioral signals while remaining meaningful across diverse scenarios [Interactive Evaluation] [Personality Illusion] [Rethinking Psychometrics]. Then at runtime, the complementary challenge is to equip reasoning systems to identify, mitigate, and resist failures as they inevitably arise [Reasoning Failures] [A-Not-B].

Earlier, I also worked on making reasoning systems more efficient through novel architecture design [Delay Space] [DelayNet].

My long-term research goal is to build AI systems whose reasoning is as creative as human intuition and as dependable as formal logic.

You can find more about me and my work from my Personal Website and Google Scholar Profile.

Should we share any common interest, feel free to email me at psong2@andrew.cmu.edu.

[Last Updated: June 2026]