{"ID":2823650,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2601.00882","arxiv_id":"2601.00882","title":"BALI: Branch-Aware Loop Invariant Inference with Large Language Models","abstract":"Loop invariants are fundamental for reasoning about the correctness of iterative algorithms. However, deriving suitable invariants remains a challenging and often manual task, particularly for complex programs. In this paper, we introduce BALI, a branch-aware framework that integrates large language models (LLMs) to enhance the inference and verification of loop invariants. Our approach combines automated reasoning with branch-aware static program analysis to improve both precision and scalability. Specifically, unlike prior LLM-only guess-and-check methods, BALI first verifies branch-sequence-level (path-level) clauses with SMT and then composes them into program-level invariants. We outline its key components, present preliminary results, and discuss future directions toward fully automated invariant discovery.","short_abstract":"Loop invariants are fundamental for reasoning about the correctness of iterative algorithms. However, deriving suitable invariants remains a challenging and often manual task, particularly for complex programs. In this paper, we introduce BALI, a branch-aware framework that integrates large language models (LLMs) to en...","url_abs":"https://arxiv.org/abs/2601.00882","url_pdf":"https://arxiv.org/pdf/2601.00882v1","authors":"[\"Mingxiu Wang\",\"Jiawei Wang\",\"Xiao Cheng\"]","published":"2025-12-31T07:13:42Z","proceeding":"cs.PL","tasks":"[\"cs.PL\"]","methods":"[\"Large Language Model\",\"Language Model\"]","has_code":false}