Peiyang Song

I am a 4th-year undergrad majoring in Computer Science at California Institute of Technology (Caltech), advised by Prof. Steven Low, with a minor in Robotics advised by Prof. Günter Niemeyer. I am a researcher in Berkeley AI Research (BAIR) Lab, working with Prof. Dawn Song and Dr. Jingxuan He. I am also part of Stanford AI Lab (SAIL), advised by Prof. Noah Goodman and Dr. Gabriel Poesia. I am fortunate to have worked with Prof. Anima Anandkumar (Caltech), Dr. Kaiyu Yang (Meta), Prof. Tim Sherwood (UC Santa Barbara), and Dr. Jeremy Lau (Google) during my undergrad.

I am currently applying for 26Fall PhD positions in Computer Science. Please feel free to explore my research interest and work below. Would love to connect if you see potential fits!

宋沛洋  /  Email  /  CV  /  Bio  /  Google Scholar  /  GitHub  /  LinkedIn  /  Twitter

[Sep 2025] We released our work discovering The Personality Illusion: LLMs do not have personalities in the way humans do.
[Jul 2025] Our paper on Delay Space Arithmetic and Architecture is awarded IEEE Micro Top Picks.
[Jul 2025] I will be at the Agentic AI Summit 2025 on August 2 in UC Berkeley. Register here. Excited to catch up there!
[Jul 2025] Our paper on LLM Reasoning Failures is accepted to ICML AI for Math Workshop. Stay tuned for our full release!
[Jun 2025] Our paper on Human-Like Traits in LLMs is accepted to ICML MoFA Workshop. Stay tuned for our full release!

My research centers on LLM reasoning, especially for formal math and verifiable code, through neuro-symbolic approaches combining LLMs with formal systems such as Lean. This agenda unfolds along three interconnected directions:

• LLMs for proving formal math and generating verifiable code [LeanDojo], in a practical [Lean Copilot], predictable [LeanProgress], and extendable [LeanAgent] manner.
• Trustworthy LLM (informal) reasoning in natural languages, motivated by cognitive principles [Personality Illusion] and limitation studies [A-Not-B] [LLMRF].
• The application of neuro-symbolic approaches to fundamental challenges, such as energy-efficient inference [Delay Space] [DelayNet] and idiom translation [Idioms].

If any of this resonates with your interests, feel free to reach out and let's connect/collaborate!

We present the first comprehensive survey dedicated to reasoning failures in LLMs. By unifying fragmented research efforts, our survey provides a structured perspective on systemic weaknesses in LLM reasoning, offering valuable insights and guiding future research towards building stronger, more reliable, and robust reasoning capabilities.

LLMs say they have personalities, but they don’t act like it. Alignment today shapes language, not behavior. This linguistic–behavioral dissociation cautions against equating coherent self-reports with cognitive depth.

What operations can you perform efficiently when you use the “time of arrival” of a signal’s edge to represent a number? We present negative-logarithmic delay space arithmetic as a completely new approach to temporal coding. Under this approach, general purpose arithmetic is transformed to a “soft” version of the standard temporal operations in such a way that preserves all of the algebraic identities.

LLMs struggling with long proofs? We present LeanProgress, which uses a novel critic model where “distance” to the goal state acts as a key signal for step prediction, boosting performance on neural theorem proving in Lean. Our method achieves 75.1% prediction accuracy, with a 3.8% gain in proof search with step prediction.

LeanAgent continuously learns and improves on ever-expanding mathematical knowledge without forgetting what it learned before. It has a curriculum learning strategy that optimizes the learning trajectory in terms of mathematical difficulty, a dynamic database for efficient management of evolving mathematical knowledge, and progressive training to balance stability and plasticity.

We introduce Lean Copilot, a framework for running neural network inference directly in Lean. It enables various LLM-based proof automation tools that integrate seamlessly into the workflow of Lean users, including tools for suggesting proof steps (tactics), selecting premises, and searching for complete proofs using LLMs.

To compile a dictionary of East Asian idiom translations demands much time and creativity even for expert translators. To alleviate such burden, we automate high-quality data generation with GPT-4, and discover Pareto-optimal prompting strategies on both faithfulness and creativity, outperforming existing translation engines and human baseline.

Motivated by the crucial cognitive phenomenon of A-not-B errors, we present the first systematic evaluation on the surprisingly vulnerable inhibitory control abilities of LLMs. We reveal that this weakness undermines LLMs' trustworthy reasoning capabilities across diverse domains, and introduce various mitigations.

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? We release LeanDojo: an open-source playground consisting of toolkits, benchmarks, and models for LLMs to prove formal theorems in the Lean proof assistant.

My works have been covered by many media. Some representative ones include:

• 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

• ICLR Notable Reviewer Award (2025)
• George W. Housner Student Discovery Fund (2025)
• IEEE Micro Top Pick Award (2025)
• Early Research Scholarship (2023)
• Caltech SURF Award (2023)

• ME/CS/EE 133A: Robotics - Kinematics, California Institute of Technology, Fall 2025

• Reviewer @ NeurIPS, ICLR, ARR, ACL, EMNLP, IJCNLP, AACL, etc.
• Admissions Ambassador @ Undergraduate Admissions Office, Caltech.
• First-Year Caltech Connector (FCC) @ Student & Family Engagement Office, Caltech.
• Organizing Staff @ Agentic AI Summit 2025, UC Berkeley.

Last updated: Sep. 2025. Website template credit: Jon Barron.