Banghu Yin

Fully Automating Template Polyhedral Analysis by Leveraging LLMs

Path-Sensitive Loop Invariant Inference via Large Language Models and Abstract Interpretation

A path-sensitive loop invariant inference approach based on Large Language Models and abstract interpretation that constructs candidate invariants as disjunctions of clause conjunctions satisfied by counterexamples across loop paths and iteratively refines them using counterexamples generated by the SMT solver during v...

LLM-Based Invariant Generation for Multi-Loop Programs via Forward and Backward Iterative Refinement

Cloud computing infrastructure increasingly relies on cloud services where correctness is critical. Ensuring their correctness requires formal verification techniques grounded in rigorous mathematical reasoning. In practice, formal models of cloud services frequently exhibit multiple loop structures, and verifying such...

AdaRAG: Budget-Aware Adaptive Retrieval-Augmented Generation via Hierarchical Reinforcement Learning

Multi-turn retrieval-augmented generation (RAG) improves question answering by decomposing evidence seeking into iterative retrieval and reasoning steps. Existing multi-turn RAG methods usually optimize when and how to retrieve while fixing the number of retrieved documents per step. However, we discovered that this fi...