I am a first-year Ph.D. student at Carnegie Mellon University (CMU), affiliated with the Language Technologies Institute (LTI) in the School of Computer Science (SCS), and the Institute for Computer-Aided Reasoning in Mathematics (ICARM). I am fortunate to be advised by Prof. Sean Welleck and working closely with Prof. Jeremy Avigad.

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, 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], and further toward persistent agents that refine their methods across long-horizon, verifier-checked research [Épi]. I also extend this line of work from mathematics to other formalizable domains, such as verified code generation [P³] [Vero] and certificate synthesis for dynamical systems [LLM2Cert].

(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 inherently harder to pursue in the absence of symbolic verifiers or reliable reward signals. To fundamentally alleviate this challenge, one way forward is to develop meaningful agent-centered evaluations that elicit and capture rich behavioral signals across diverse real-world scenarios [Interactive Evaluation] [Personality Illusion] [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: October 2026]