Deductive verifcation is an approach where the user expends effort in constructing a program invariant manually, or learns this invariant from program traces, and subsequently uses the program invariant for safety verifcation tasks.Most existing invariant synthesis tools still rely on model checking methods to certify invariants, use enumerative search to identify and refne candidate invariants, and user insights to start with a set of candidate predicates that may appear in the fnal (learned) invariant.On the other hand, pre-trained large language models (LLMs) have recently attracted considerable attention in various tasks related to generating program code (e.g., from natural language).There have been recent efforts at applying LLMs to the program verifcation context.In this paper, we investigate the capabilities of LLMs to synthesize program invariants by creating a specialized set of prompts.When LLM invariant synthesis with direct prompting fails, we introduce two revision frameworks for incorporating LLM calls.In the frst framework PSyn, the LLM suggests atomic predicates based on counterexamples for reconstructing the invariants.The second framework ISyn adopts the LLM to generate invariants by itself within a revision process.We tested our methods on 8 distributed systems modeled in Promela and invariants are verifed with Spin.Our results show that the state-of-the-art model GPT-o3, when it is used to generate invariants directly, is less effective than the symbolic invariant synthesis method RunVS.However, our integrated approach PSyn, which employs the LLM as a predicate prompter, signifcantly outperforms GPT-o3 and ISyn and has comparable performance with RunVS.This integrated technique also produces higher-quality invariants in general.Because we focus on runtime monitoring frameworks, we primarily consider system traces and hence likely invariants.However, our revision frameworks can also learn true invariants by using model checkers in the revision frameworks.
Xia et al. (Wed,) studied this question.