|
I am an Honors CS undergrad in College of Creative Studies (CCS), UC Santa Barbara, co-advised by Professor Richert Wang and Professor Phill Conrad. I am a SURF fellow in the Computing + Mathematical Sciences (CMS) Department at Caltech, advised by Professor Anima Anandkumar and co-advised by Dr. Kaiyu Yang. I am also a researcher at UCSB ArchLab, working with Professor Tim Sherwood and Dr. Jeremy Lau (Google). 宋沛洋 / Email / CV / Google Scholar / GitHub / LinkedIn / Twitter |
|
|
[September 2023] Our paper LeanDojo is accepted to NeurIPS Datasets and Benchmarks Track as an Oral Presentation.
[September 2023] We released LeanInfer for running neural networks directly in Lean. |
|
My research interest is in Machine Learning (ML), from its applications in Natural Language Processing (NLP) and Computer Vision (CV), to its foundation in Systems and Programming Languages (PL). My recent research works are mainly in two directions: 1) neuro-symbolic reasoning and AI4Math combining Large Language Models (LLMs) with Interactive Theorem Provers (ITPs); 2) energy-efficient machine learning with temporal logic and other novel designs. |
|
Peiyang Song, Kaiyu Yang†, and Anima Anandkumar† († Equal advising) NeurIPS MATH-AI Workshop, 2023 code We introduce a framework for running neural network inference directly in Lean. It enables programmers to build various LLM-based proof automation tools that integrate seamlessly into the workflow of Lean users, including tools for suggesting proof steps and completing intermediate proof goals using LLMs. |
|
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar Neural Information Processing Systems (NeurIPS) Datasets and Benchmarks Track, 2023, Oral presentation arXiv / project / code / media 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. |
|
|
I was a computer science, mathematics, and physics competitor. I took part in multiple international contests and won lots of prestigious awards during those days. These experiences have undoubtedly shaped who I am, and they are still among the most important memories of my academic journey. |
|
|