18 citations · 20 across the 14 of their papers we have counts for
14 papers
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…
Conformal Correction for Efficiency May be at Odds with Entropy
Senrong Xu, Tianyu Wang, Zenan Li +4
Conformal prediction (CP) provides a comprehensive framework to produce statistically rigorous uncertainty sets for black-box machine learning models. To further improve the effici…
FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory
Xiao-Wen Yang, Zihao Zhang, Jianuo Cao +7
Large language models (LLMs) have recently demonstrated remarkable progress in formal theorem proving. Yet their ability to serve as practical assistants for mathematicians, fillin…
LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation
Junyu Lai, Jiakun Zhang, Shuo Xu +6
Recent advancements in large language models (LLMs) have sparked considerable interest in automated theorem proving and a prominent line of research integrates stepwise LLM-based p…
Neuro-symbolic Learning Yielding Logical Constraints
Zenan Li, Yunpeng Huang, Zhaoyu Li +5
Neuro-symbolic systems combine the abilities of neural perception and logical reasoning. However, end-to-end learning of neuro-symbolic systems is still an unsolved challenge. This…
LASER: Script Execution by Autonomous Agents for On-demand Traffic Simulation
Hao Gao, Jingyue Wang, Wenyang Fang +4
Autonomous Driving Systems (ADS) require diverse and safety-critical traffic scenarios for effective training and testing, but the existing data generation methods struggle to prov…
Advancing Transformer Architecture in Long-Context Large Language Models: A Comprehensive Survey
Yunpeng Huang, Jingwei Xu, Junyu Lai +9
Transformer-based Large Language Models (LLMs) have been applied in diverse areas such as knowledge bases, human interfaces, and dynamic agents, and marking a stride towards achiev…