5 papers
FLARE: Fine-Grained Diagnostic Feedback for LLM Code Refinement
Yinsheng Yao, Hongxiang Zhang, Weixi Tong +1
Large language models often generate code with bugs. Existing methods rely on feedback signals such as test failures and self-critiques to iteratively refine the generated code. Su…
Adaptive Proof Refinement with LLM-Guided Strategy Selection
Minghai Lu, Zhe Zhou, Danning Xie +3
Formal verification via theorem proving enables the expressive specification and rigorous proof of software correctness, but it is difficult to scale due to the significant manual…
Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Ruixin Wang, Zhongkai Zhao, Le Fang +4
Automated Program Repair (APR) holds the promise of alleviating the burden of debugging and fixing software bugs. Despite this, developers still need to manually inspect each patch…
Proof Automation with Large Language Models
Minghai Lu, Benjamin Delaware, Tianyi Zhang
Interactive theorem provers such as Coq are powerful tools to formally guarantee the correctness of software. However, using these tools requires significant manual effort and expe…
Automated Deep Learning Optimization via DSL-Based Source Code Transformation
Ruixin Wang, Minghai Lu, Cody Hao Yu +2
As deep learning models become increasingly bigger and more complex, it is critical to improve model training and inference efficiency. Though a variety of highly optimized librari…