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 models depends on the ability to automatically generate sufficient and accurate loop invariants. In this paper, we present an LLM-based invariant generation method for multi-loop programs via forward and backward iterative refinement. The approach is built upon the recent generate-combine-check framework. First, we employ a multiloop structure-guided strategy to instruct the LLM to produce clause expressions without logical connectives, which are then combined via counterexample-driven refinement to form candidate invariants. After that, we use a backward iterative refinement mechanism to adjust the invariants in reverse order, that is, from post-condition at the end of the program, to the inter-loop invariants, and finally to the pre-condition at the beginning of the program. We implemented a prototype tool named MultiInvGen. Evaluation results show that, MultiInvGen successfully solves 71 tasks (65.7%) on a benchmark of 108 C programs, significantly outperforming the state-of-the-art LLMbased and Multi-loop invariant generation tool.
Wenyu Zhang, Guangsheng Fan, Dengping Wei et al.· Fall Joint Computer Conferen...· 0 citations
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 fixed-TopK design is suboptimal: single-hop questions tend to benefit from fewer retrieval rounds with larger per-round evidence sets, whereas multi-hop questions require more retrieval rounds with smaller evidence sets to support stepwise reasoning. To bridge this gap, we introduce AdaRAG, a budget-aware adaptive RAG framework that learns how to retrieve under a hard document budget, including how many retrieval rounds to perform, how many documents to retrieve in each round, and which retrieval source to use. AdaRAG implements this idea with a two-level policy architecture. ModeHead, a lightweight retrieval-mode classifier, selects passage retrieval, graph retrieval, or answer generation; TopkHead, a budget-aware document-allocation classifier, selects a legal TopK after query generation according to the remaining budget. These discrete policy heads are decoupled from language-model token generation, enabling direct reinforcement-learning optimization through hierarchical GRPO after supervised action-format learning. Our experiments across five QA benchmarks demonstrate AdaRAG's good generalization performance under constrained document budgets. In detailed comparisons on HotpotQA, it surpasses the strongest baselines by an average of 10.8 percentage points in Exact Match (EM) and F1 score.
Jia-Nan Sun, Miao Zhang, Chen Chen et al.· Fall Joint Computer Conferen...· 0 citations
