40 citations · 47 across the 9 of their papers we have counts for
4 papers · 1 filter
P: Joint Program-and-Proof Planning for Verified Code Generation
Zenan Li, Ziran Yang, Peiyang Song +2
Verified code generation asks a large language model (LLM) to generate both an executable program and a machine-checkable proof that the program meets a formal specification, promi…
The Personality Illusion: Revealing Dissociation Between Self-Reports & Behavior in LLMs
Pengrui Han, Rafal Kocielnik, Peiyang Song +4
Personality traits have long been studied as predictors of human behavior. Recent advances in Large Language Models (LLMs) suggest similar patterns may emerge in artificial systems…
LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction
Robert Joseph George, Suozhi Huang, Peiyang Song +1
Mathematical reasoning remains a significant challenge for Large Language Models (LLMs) due to hallucinations. When combined with formal proof assistants like Lean, these hallucina…
Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
Peiyang Song, Kaiyu Yang, Anima Anandkumar
Neural theorem proving combines large language models (LLMs) with proof assistants such as Lean, where the correctness of formal proofs can be rigorously verified, leaving no room…