18 citations · 20 across the 14 of their papers we have counts for
8 papers · 1 filter
InvWeaver: Deductive Feedback for Invariant Synthesis in Interacting-Loop Programs
Guangyuan Wu, Weining Cao, Zehui Tan +4
Loop invariant inference is a fundamental yet challenging problem in program verification. Recent LLM-aided guess-and-check techniques have shown strong performance on single-loop…
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…
Fair Conformal Classification via Learning Representation-Based Groups
Senrong Xu, Yanke Zhou, Yuhao Tan +5
Conformal prediction methods provide statistically rigorous marginal coverage guarantees for machine learning models, but such guarantees fail to account for algorithmic biases, th…
CDS4RAG: Cyclic Dual-Sequential Hyperparameter Optimization for RAG
Pengzhou Chen, Tao Chen
Retrieval-Augmented Generation (RAG) is sensitive to the vast hyperparameters of the retriever and generator, yet optimizing them using given queries is a challenging task due to t…
LLMSYS-HPOBench: Hyperparameter Optimization Benchmark Suite for Real-World LLM Systems
Siyu Wu, Yulong Ye, Zezhen Xiang +3
Large Language Model (LLM) systems have been the frontier of AI in many application domains, leading to new challenges and opportunities for hyperparameter optimization (HPO) for t…
Neuro-Symbolic Proof Generation for Scaling Systems Software Verification
Baoding He, Zenan Li, Wei Sun +4
Formal verification via interactive theorem proving is increasingly used to ensure the correctness of critical systems, yet constructing large proof scripts remains highly manual a…