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.

翻译：循环不变式是推理迭代算法正确性的基础。然而，推导合适的不变式仍然是一项具有挑战性且通常需要人工完成的任务，特别是对于复杂程序。本文提出BALI，一种分支感知框架，通过集成大语言模型（LLMs）来增强循环不变式的推断与验证。我们的方法将自动推理与分支感知的静态程序分析相结合，以提高精确性和可扩展性。具体而言，与先前仅依赖LLM的“猜测-验证”方法不同，BALI首先利用SMT验证分支序列级（路径级）子句，随后将其组合为程序级不变式。我们概述了其关键组件，展示了初步结果，并讨论了未来实现全自动不变式发现的研究方向。