NL2CTL: Automatic Generation of Formal Requirements Specifications via Large Language Models

Reducing the gap between natural language requirements and precise formal specifications is a critical task in requirements engineering. In recent years, requirement engineering is becoming increasingly complex alongside the growing intricacy of system engineering. Most requirements are expressed in natural language, which can be incomplete and ambiguous. However, formal languages with strict semantics can accurately represent certain temporal logic properties and allow for automated verification and analysis. This often limits the application of verification techniques, as writing formal specifications is a manual, error-prone, and time-consuming task. To address this, this paper proposes a framework that leverages Large Language Models (LLMs) to achieve automated conversion of natural language requirements to Computation Tree Logic (CTL). To address the issue of dataset scarcity, we leveraged the interactive and generative capabilities of LLMs. By constructing a random generation algorithm and utilizing prompt engineering, we generated an NL-CTL dataset using LLMs. The generated dataset was then used to fine-tune the T5-Large model, enhancing its generative capacity. To improve generalization, this paper proposes the use of the GPT-3.5 Atomic Proposition (AP) Recognition method, which eliminates the constraints of using the framework across different domains. A series of experimental evaluations showed that the fine-tuned LLM achieved an accuracy of 46.4%, whereas the LLM with few-shot learning using only prompt engineering achieved only 2% accuracy, demonstrating the feasibility of this approach.