Augmenting, Not Replacing: The Role of LLMs in Human-Centric Formal RE

Formal methods for requirements engineering have existed for decades; yet, these techniques are rarely used if not required by certification because they are challenging for non-experts (e.g., novices and non-technical stakeholders in multidisciplinary teams) to interpret and apply. To enable non-experts to participate in collaborative software teams, we envision using artificial intelligence (AI) to assist in interpreting formal notations. Our research project investigates how and to what extent generative AI with large language models (LLMs) can be used to assist non-experts in interpreting formal requirements. In this paper, we conduct an exploratory investigation of both generating translations and interpreting linear temporal logic (LTL) formulae. Specifically, we explore prompting LLMs with sufficient information for the task of generating LTL formula explanations. With our initial prompt, we complete a classroom study where students learn LTL and then interpret a series of LTL formulae with and without the LLM-generated descriptions. We then improve our approach based on insights from the classroom study, and evaluate the overall quality of our updated prompt and the explanations it generates.