The Power of Reframing: Using LLMs in Synthesizing RV Monitors

Applying formal methods to a system typically involves ex- pressing the requirements in terms of the native formalism of the used tool. In RV, this is often temporal logic. There is a potential gap between requirements expressed in natural language (NL, e.g., English), in which design and requirement documents are written, and their translation to the formalism. The latter is often rigid, including a small number of pre- defined temporal constructs. Our focus is the translation of descriptions written in NL to monitors. This poses several challenges. First, an NL description may be far removed from the basic constructs of the temporal logic, making the gap too big, resulting in an unreliable translation. Sec- ond, the description may go beyond the expressiveness of the temporal logic. Finally, the description may include ambiguities that may result in a mismatch between the intended meaning and the formal specifica- tion. We present a method and an interactive tool using an LLM that implements new temporal constructs defined during interaction with a user, minimizing the gap between NL and formalism. It uses the LLM capability to reframe temporal descriptions given in NL in order to learn the correct desired interpretation of the new constructs and then au- tomatically translate them to code. After learning new constructs, the system is capable of reliably synthesizing monitors in the enriched spec- ification language from NL descriptions. The tool can also just be seen as an assistant in implementing a monitoring logic.