Peiyang Song

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.

宋沛洋  /  Email  /  CV  /  Bio  /  Google Scholar  /  GitHub  /  LinkedIn  /  X  /  IG  /  WeChat

[Oct 2026] Released LLM2Cert for agentic certificate synthesis and verification, together with the DynaCertBench benchmark.
[Oct 2026] Released Épi, a persistent, self-improving agent for autonomous research in math and beyond.
[Sep 2026] Excited to share that P³, Vero, and Rethinking Psychometric Evaluation of LLMs have all been accepted to NeurIPS 2026!
[Sep 2026] Gave a guest lecture for CS 4824 / ECE 4424: Machine Learning at Virginia Tech on Sep 14 (slides).
[Aug 2026] Released our new study on Human Agency in Initial Human-AI Proof Formalization Workflows (thread).

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.

Lyapunov functions and barrier certificates formally guarantee that dynamical systems are stable and safe, but solver-based pipelines scale poorly beyond low-dimensional polynomial systems. LLM2Cert has LLMs synthesize candidate certificates and routes each proof obligation to an SMT solver or a Lean proof-repair agent, verifying 77.1% of our new 105-instance DynaCertBench, a 17.1-point gain over one-shot proposal.

Long-horizon research outgrows any single model session. Épi is an autonomous research agent that persists across sessions through research history, hierarchical memory, branching, and independent review. It has set 120 records across 20 problem families and given a computer-assisted proof of a case of Tuza's conjecture, while its coding variant, Épi-turbo, beats Codex on FrontierOR at 64% of the model cost.

Verified code generation asks LLMs for both a program and a machine-checkable proof, yet the standard program-then-proof pipeline often yields code that is hard to verify. Inspired by Dijkstra, P³ plans the program and its proof jointly from the specification. On Verina, AlgoVeri, and our new repository-derived Lean4Commit0 benchmark, it achieves the highest solve rate in every setting while cutting API cost by up to 40%.

Can AI agents build software that is provably correct, not just plausibly so? Vero is the first benchmark for joint implementation and proof synthesis at the repository level, with 43 multi-module Lean 4 repositories drawn from real-world software, from cryptographic protocols to distributed systems. Even the strongest frontier agent fully solves only 27 of them.

Psychometric probes can anticipate LLM behavior only if self-reports actually predict it. Across 11 frontier LLMs and four behavioral tasks, we find that this coherence exists but is selective: within a conversation, the Theory of Planned Behavior reaches human-level coherence where Big 5 traits fall short, and persona prompting makes self-reports consistent without bringing behavior into line.

LLMs increasingly act over time through tools, environments, users, and other agents, yet evaluation still inherits assumptions from single-response benchmarks. We argue that interactive evaluation needs a design science, not just more agent benchmarks: we define it, propose a two-axis taxonomy, and derive design principles and reporting standards for evaluating interaction trajectories.

AI promises to transform how mathematicians formalize proofs, but how do people actually use it? Through a survey and a controlled user study, we find that people want AI assistance that preserves their control over proof discovery, and that participants formalize more accurately with AI than without, flexibly combining multiple tools despite their limitations.

Most activation steering methods rely on a single static direction per task, which breaks down when a task needs multiple coordinated capabilities. Steer2Adapt instead composes reusable steering vectors from a low-dimensional semantic subspace, adapting to new tasks from only a handful of examples and improving performance by 8.2% on average across 9 reasoning and safety tasks.

LLMs reason impressively, yet still fail in surprisingly simple scenarios. We present the first comprehensive survey of LLM reasoning failures, organizing them by reasoning type (embodied vs. non-embodied) and failure type (fundamental, application-specific, robustness), and analyzing the root causes and mitigations of each to guide more robust reasoning.

LLMs say they have personalities, but they don't act like it. Alignment stabilizes self-reported traits in human-like ways, yet these traits fail to predict behavior, and persona injection shifts self-reports with little effect on actions. Alignment today shapes language, not behavior, cautioning against equating coherent self-reports with cognitive depth.

We bring LLMs into Lean as copilots for human mathematicians. Lean Copilot runs LLM inference natively in Lean, powering tools that suggest proof steps, select premises, and search for complete proofs within users' workflows. On Mathematics in Lean, it automates 74.2% of proof steps, 85% more than Lean's rule-based automation (aesop).

What can you compute efficiently when a number is encoded as the arrival time of a signal edge? We introduce negative-logarithmic delay space arithmetic, a new approach to temporal computing that turns general-purpose arithmetic into “soft” versions of standard temporal operations while preserving all of their algebraic identities.

Mathematicians work across ever-evolving domains, while existing provers are trained on static datasets. LeanAgent learns continuously from expanding mathematical knowledge without forgetting, via curriculum learning, a dynamic knowledge database, and progressive training. It proved 155 theorems across 23 Lean repositories that previously lacked formal proofs, many in advanced mathematics.

LLM provers struggle with long proofs, partly because they have no sense of how close a proof is to completion. LeanProgress predicts the number of remaining proof steps with 75.8% accuracy and uses this signal to guide best-first search, improving the 41.4% ReProver baseline on Mathlib4 by 3.8%, with the largest gains on longer proofs.

As agents move beyond prompting, adaptation through post-training, memory, and skills has become central to their performance and reliability, yet research remains fragmented. We unify the field in a four-paradigm framework spanning agent adaptation (from tool-execution or agent-output signals) and tool adaptation (agent-agnostic or agent-supervised), and chart open problems ahead.

Why does supervised fine-tuning often narrow LLM capabilities while reinforcement learning tends to preserve them? We introduce a benchmark that decomposes reasoning into atomic skills such as calculation, fact retrieval, and simulation, and trace them through post-training: RL-tuned models keep stable skill profiles, while SFT models drift sharply and overfit to surface patterns.

Infants make A-not-B errors: they repeat a previously rewarded action even after conditions visibly change. In the first systematic evaluation of this inhibitory control in LLMs, models that excel with in-context learning lose up to 83.3% accuracy when the context changes trivially. Better pretraining mitigates these errors, but self-explanation fails to remove them.

East Asian idioms pack rich cultural context into a few characters, and compiling their translations demands much time and creativity even from experts. Using GPT-4, we identify Pareto-optimal prompting strategies for faithfulness and creativity that outperform Google and DeepL, producing far more high-quality translations per idiom than human translators at low cost.

We introduce energy-efficient convolution that improves the energy per pixel of each convolution frame by more than 2× compared to the state-of-the-art while improving the energy delay product by four orders of magnitude, by developing a new temporal arithmetic with a negative log transformation.

Can LLMs generate mathematical proofs that can be rigorously checked? LeanDojo removes the barriers of private code, data, and heavy compute with an open-source Lean playground of toolkits, data, models, and a 98,734-theorem benchmark. Its retrieval-augmented prover, ReProver, trains in one GPU-week and outperforms GPT-4, with no proprietary data.

I organize workshops and instruct tutorials, including:

• Lead Organizer, The 6th Workshop on Mathematical Reasoning and AI (MATH-AI) @ NeurIPS 2026
• Lead Instructor, Tutorial on Neuro-Symbolic Theorem Proving with Lean @ 3rd Neuro-Symbolic AI Summer School (NSSS)

My research has been covered by many media. Some representative ones include:

• Scientists Found AI's Fatal Flaw—The Most Advanced Models Are Failing Basic Logic Tests, Popular Mechanics, 2026
• 'Not how you build a digital mind': How reasoning failures are preventing AI models from achieving human-level intelligence, Live Science, 2026
• When AI gets the maths right but the model wrong, Doing The Math, 2026
• Researchers Discover "Personality Illusion" to Reveal a Profound Disconnect Between Language and Behavior in LLMs, MIT Technology Review China, 2025
• New Framework Simplifies the Complex Landscape of Agentic AI, VentureBeat, 2025
• This AI Paper Explains Why Most "Agentic AI" Systems Feel Impressive in Demos and then Completely Fall Apart in Real Use, MarkTechPost, 2025
• Mathematicians' Newest Assistants Are Artificially Intelligent, Scientific American, 2024
• LeanAgent: The First Life-Long Learning Agent for Formal Theorem Proving in Lean, MarkTechPost, 2024
• Lean Copilot: An AI Tool That Allows Large Language Models (LLMs) to Be Used in Lean for Proof Automation, MarkTechPost, 2024
• Can LLMs Generate Mathematical Proofs That Can Be Rigorously Checked?, MarkTechPost, 2023

• ICML CTB Workshop Best Paper Award (2026)
• EACL Outstanding Reviewer Award (2026)
• TMLR Survey Certification (2026)
• NeurIPS LAW Workshop Best Paper Honorable Mention Award (2025)
• ICLR Notable Reviewer Award (2025)
• George W. Housner Student Discovery Fund (2025)
• IEEE Micro Top Pick Award (2025)
• Caltech SURF Fellowship (2023)

• CS 4824 / ECE 4424: Machine Learning, Guest Lecturer @ Virginia Tech, Fall 2026
• CS 38/138: Algorithms, Teaching Assistant @ Caltech, Spring 2026
• ME/CS/EE 133B: Robotics - Planning, Teaching Assistant @ Caltech, Winter 2026
• ME/CS/EE 133A: Robotics - Kinematics, Teaching Assistant @ Caltech, Fall 2025

• Journal Reviewer @ ACM Computing Surveys, SPJ Intelligent Systems.
• Conference Reviewer @ NeurIPS, ICLR, COLM, ACL, EMNLP, NAACL, EACL, AACL, IJCNLP, etc.

I enjoy long walks, running, cycling, and badminton. I also love reading and writing, and sharing good meals with friends. When I'm on vacation, I like traveling, collecting fridge magnets, and doing nature photography — and I finally have time to dive into longer books.

Earlier on, I explored a range of spare-time activities, including math and algorithm contests, debate tournaments, and music production.

Last updated: October 2026. Website template credit: Jon Barron.