5 papers
Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis
Anjiang Wei, Tianran Sun, Tarun Suresh +3
Program verification relies on loop invariants, yet automatically discovering strong invariants remains a long-standing challenge. We investigate whether large language models (LLM…
Astra: A Multi-Agent System for GPU Kernel Performance Optimization
Anjiang Wei, Tianran Sun, Yogesh Seenichamy +5
GPU kernel optimization has long been a central challenge at the intersection of high-performance computing and machine learning. Efficient kernels are crucial for accelerating lar…
Translating Large-Scale C Repositories to Idiomatic Rust
Saman Dehghan, Tianran Sun, Tianxiang Wu +2
Existing C to Rust translation techniques fail to balance quality and scalability: transpilation-based approaches scale to large projects but produce code with poor safety, idiomat…
Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcity
Dylan Zhang, Justin Wang, Tianran Sun
Existing LMs struggle with proof-oriented programming due to data scarcity, which manifest in two key ways: (1) a lack of sufficient corpora for proof-oriented programming language…
Curator Attack: When Blackbox Differential Privacy Auditing Loses Its Power
Shiming Wang, Liyao Xiang, Bowei Cheng +3
A surge in data-driven applications enhances everyday life but also raises serious concerns about private information leakage. Hence many privacy auditing tools are emerging for ch…