LLM-guided Predicate Discovery and Data Augmentation for Learning Likely Program Invariants

Abstract

Security protocols, protocols to achieve consensus, those for maintaining memory consistency and coherence, distributed ledgers, multi-party computation, and many similar software systems are examples of distributed message-passing based computation. Ensuring correctness of such distributed systems is a challenging problem for many automatic verification approaches. The deductive verification approach for reasoning about such systems involves computing a program invariant, i.e., an expression evaluates to true for every reachable program state. Several approaches for synthesizing invariants are dynamic, i.e., runs of the program and ancillary information such as target safety properties are used to learn an invariant expression. However, most existing approaches invoke a model checker (or a theorem prover) within the synthesis loop, which makes these approaches depend on the scalability of the verification tools. In this paper, we propose a counterexample-guided inductive synthesis approach called RunVS which learns invariant expressions from program runs, but without information such as target safety properties, and without invoking a model checker/theorem prover for validation. The synthesis approach pairs a decision-tree (DT) based method with a data augmentation technique: DT-learning provides an expression that classifies observed states from augmented states that are speculated to be unreachable. Validation of the learned invariant is performed by sampling program runs and states; any run that invalidates the invariant results in counterexamples used to revises the invariant. As there is no formal proof that the learned artifact is a true invariant, we call such an expression a likely invariant. An important user input to synthesis is often the set of predicates that comprise the invariant expression; we use a novel integration with a large language model (LLM) and prompt it to provide likely predicates to be used. We show empirical results of our approach on several distributed protocols implemented in the Promela modeling language.