Enhancing Transformation from Natural Language to Signal Temporal Logic Using LLM s with Diverse External Knowledge (2025)

Abstract: Temporal Logic (TL), especially Signal Temporal Logic (STL), enables precise formal specification, making it widely used in cyber-physical systems such as autonomous driving and robotics. Automatically transforming NL into STL is an attractive approach to overcome the limitations of manual transformation, which is time-consuming and error-prone. However, due to the lack of datasets, automatic transformation currently faces significant challenges and has not been fully explored. In this paper, we propose a NL-STL dataset named STL-Diversity-Enhanced (STL-DivEn), comprising 16,000 samples enriched with diverse patterns. To develop the dataset, we first manually create a small-scale seed set of NL-STL pairs. Next, representative examples are identified through clustering and used to guide large language models (LLMs) in generating additional NL-STL pairs. Finally, diversity and accuracy are ensured through rigorous rule-based filters and human validation. Furthermore, we introduce the Knowledge-Guided STL Transformation (KGST) framework, a novel approach for transforming natural language into STL, involving a generate-then-refine process based on external knowledge. Statistical analysis shows that the STL-DivEn dataset exhibits more diversity than the existing NL-STL dataset. Moreover, both metric-based and human evaluations indicate that our KGST approach outperforms baseline models in transformation accuracy on STL-DivEn and DeepSTL datasets.

## introduction signal temporal logic (stl) @xcite provides a flexible and precise framework for specifying requirements in safety-critical cyberphysical systems. extending temporal logic (tl) @xcite by introducing real-time and real-valued constraints, stl can describe not only discrete temporal events but also continuous-time and real-valued dynamic changes. therefore, stl, as a powerful expression tool for system design, offers valuable guidance in cyber-physical systems, such as autonomous driving @xcite and robot control @xcite . but one of the main challenges in leveraging the stl specification is the need to accurately transform the potentially ambiguous and complex constraints expressed in natural language into precise stl logical expressions, as shown in the following example: writing accurate stl formulas directly is a huge burden for domain experts, as it is both timeconsuming and error-prone. with the development of natural language processing (nlp) technology, researchers have been experimenting with utilizing nlp technology to transform natural language into tl and stl expressions, aiming to improve its automation and accuracy. for example, @xcite ; @xcite use predefined pattern formulas to transform natural language sentences into an intermediate representation. subsequently, by applying a set of predefined rules manually, the intermediate representation is mapped to temporal logic formulas. these approaches require extensive domain expertise and involve a steep learning curve @xcite . specifically, they can only be applied to very restrictive structured natural language expressions that match the given patterns. in recent years, the remarkable success of deep learning and large language models (llms) has spurred growing interest in leveraging them to address the transformation problem from natural language to stl. for example, deepstl @xcite introduces a grammar-based synthetic data generation technique and trains an attentional translator of english to stl using a transformerbased neural translation technique. nl2tl @xcite uses llms to help create the natural language-temporal logic dataset, which is then applied to fine-tune the t5 models. however, the proposed transformation methods also face challenges in accurately transforming complex natural language into signal temporal logic. to address these challenges, our efforts focus on the following two aspects. firstly, aiming at developing high-quality and expressively diverse nl-stl datasets to deal with the scarcity of nl-stl datasets, we explore utilizing llms to synthesize nl-stl pairs under the guidance of prompts. however, nl-stl pairs generated by llms often closely resemble the examples in the prompts. to ensure diversity and comprehensiveness, we introduce a method for constructing the stl-diversity-enhanced (stl-diven) dataset. we start by handcrafting a seed set of 120 nl-stl pairs, covering both basic and nested logic to serve as the foundation for data augmentation. next, a clustering algorithm is employed to select representative samples from the seed set. these exemplars are used to guide llms in generating new nl-stl pairs, which are then refined using rule-based filters and human validation to ensure diversity and precision. finally, the qualified nl-stl pairs expand the seed set and are stored in the stl-diven dataset. secondly, transformer-based models perform poorly when handling complex natural language transformation tasks. transforming nl sentences into stl formulas remains a challenging task due to the complexity of temporal constraints in the requirements of cyber-physical systems, including nested semantics @xcite . even many advanced models, such as gpt-4 @xcite and deepseek @xcite , while excelling at text generation tasks, still face limitations in transforming nl into stl. to address this limitation, we propose a novel transforming framework called knowledge-guided stl transformation (kgst). this framework operates in two steps: first, we fine-tune an llm on nl-stl dataset (e.g., stl-diven) and use the finetuned llm to generate a preliminary stl formula from the natural language input; second, the top k similar nl-stl pairs are retrieved from the dataset, and these pairs are referenced as external knowledge; then, gpt-4 is used to evaluate and refine the preliminary stl with the external knowledge to generate the refined stl. experimental results demonstrate that the kgst framework significantly outperforms existing baseline models in both quantitative and human evaluation metrics, showcasing its advantages in stl transformation tasks. in general, our contributions are as follows: ## related work from natural language to tl and stl. many researchers have tried to transform natural language sentences into temporal logic formulas @xcite @xcite @xcite . for example, @xcite transform the properties which are specified by controlled english to tl formulas using syntax and grammatical dependency parsing techniques. @xcite also define a controlled natural language to specify how a system model interacts with its environment, and sentences in this controlled language are automatically transformed into tl using predefined rules. nl2spec @xcite derives formal formulas from unstructured natural language using llms combined with human corrections. however, these tl-specific approaches cannot be directly applied to stl, as stl involves real-time and real-valued constraints that exceed the expressiveness of tl. as stl is widely used in academia and industry @xcite , several efforts have been made to transform natural languages into stl @xcite @xcite . for instance, deepstl @xcite utilizes grammar-based techniques to synthesize data, which is then used to train transformer models for transformation. nl2tl @xcite fine-tunes t5, trained on lifted natural language-temporal logic (nl-tl) datasets created by llms to perform transformation. however, synthetic data generated from specific templates do not capture the full diversity of the real-world language. in addition, dia-loguestl @xcite transforms natural language task descriptions into accurate stl formulas through user interaction and reinforcement learning, but relies on user feedback, increasing the complexity of usage. to address the insufficient dataset and inefficiencies in transformation, we introduce a new comprehensive dataset and propose a framework to improve the transformation from natural languages to stl. ## signal temporal logic stl is widely adopted as a specification formalism for cyber-physical systems. for example, au-tomatic transmission (at), a widely-used benchmark @xcite @xcite , is a transmission controller of automotive systems. it continuously outputs the gear, speed and rpm of the vehicle. one of its safety requirements is as follows: in the following 27 time units, whenever the speed is higher than 50, the rpm should be below 3000 in three time units. stl can represent such real-time and real-valued constraints. let r denote the set of real numbers. @xmath0, respectively. let n + be the set of positive integer numbers. let @xmath1, and let @xmath2. a d-dimensional signal is a function v : [0, t ] → r d , where t is called the time horizon of v. given an arbitrary time instant @xmath3, t ], v(t) is a d-dimensional real vector; each dimension concerns a signal variable that has a certain physical meaning, e.g., speed, rpm, acceleration, etc. in this paper, we fix a set x of variables and, without ambiguity, we call a variable a signal (1-dimensional signal). definition 1 (stl syntax). in stl, atomic formulas α and formulas φ are inductively defined as follows: the boolean semantics of an stl formula can be described in a satisfaction relation (v, t) |= φ, which represents the signal v that satisfies an stl formula φ at time t: now, we can formally specify the above at safety requirement by the following stl formula: note that nested stl formula refers to an stl formula where temporal operators are applied within the scope of other temporal operators. ## approach in this section, we first present our approach for constructing the stl-diversity-enhanced (stl-diven) dataset, which combines manual annotation and llms to generate diverse, high-quality data. second, we introduce the knowledge-guided stl transformation (kgst) framework to further enhance performance in stl transformation. ## experiments in this section, we conduct experiments on our proposed dataset and the existing benchmark proposed @xcite to evaluate our methods. ## conclusion in this work, we present a new dataset, stl-diven, which features nl-stl pairs with enhanced diversity. additionally, we introduce the kgst framework, a novel approach for transforming natural languages into stl. results from both metricbased evaluations and human evaluations demonstrate that our approach significantly improves transformation capabilities across two datasets. our approach facilitates the automatic extraction of temporal and continuous constraints in cyberphysical systems, supporting efficient and reliable modeling to ensure the safety and robustness.