News
[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.
[August 2023] Honored to receive the prestigious Early Research Scholarship!
[June 2023] We released LeanDojo, an open-source playground for LLMs to prove formal theorems in Lean.
[May 2023] I am officially joining Caltech Anima AI + Science Lab, working on neuro-symbolic reasoning and more!
|
Research
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.
|
|
Towards Large Language Models as Copilots for Theorem Proving in Lean
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.
|
|
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
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.
|
Awards
- Early Research Scholarship (2023)
- Caltech SURF Award (2023)
- UCSB Creative Studies Honors (2022)
|
Misc
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.
|
|