1 citations · 1 across the 16 of their papers we have counts for
6 papers · 1 filter
Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs
Ning Zhang, Nongyu Di, Zenan Li +2
As AI-generated code proliferates, formal verification, particularly through interactive theorem provers such as Rocq and Isabelle, becomes increasingly important for ensuring soft…
Beyond Fail-to-Pass: Iterative Hardening of Co-Generated Bug Reproduction Tests and Fixes
Yuhao Tan, Zhibang Yang, Fangkai Yang +9
Large language models (LLMs) have made automated program repair (APR) increasingly practical for real-world bugs, but repairing directly from bug reports remains underconstrained.…
Synthesizing Inductive Invariants for Distributed Protocols via IC3 and Large Language Models
Weining Cao, Guangyuan Wu, Yuan Yao +3
Distributed protocols are notoriously difficult to verify correctly. Proving safety typically requires inductive invariants that both imply the desired property and are preserved b…
Task Abstention for Large Language Models in Code Generation
Yanke Zhou, Yuhao Tan, Senrong Xu +4
Large language models (LLMs) have revolutionized automated code generation. One serious concern, however, is the so-called ``hallucination'', i.e., LLMs may generate seemingly plau…
Uncertainty Quantification for LLM-based Code Generation
Senrong Xu, Yuhao Tan, Yanke Zhou +6
Prediction sets provide a theoretically grounded framework for quantifying uncertainty in machine learning models. Adapting them to structured generation tasks, in particular, larg…
Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set
Nongyu Di, Tianyu Chen, Shan Lu +6
Large Language Models (LLMs) are widely used for code generation. However, the correctness of code generated by LLMs remains a concern. A potential remedy to this concern is to hav…