NL 2 TL : Transforming Natural Languages to Temporal Logics using Large Language Models (2023)

Abstract: Temporal Logic (TL) can be used to rigorously specify complex high-level specification for systems in many engineering applications. The translation between natural language (NL) and TL has been under-explored due to the lack of dataset and generalizable model across different application domains. In this paper, we propose an accurate and generalizable transformation framework of English instructions from NL to TL, exploring the use of Large Language Models (LLMs) at multiple stages. Our contributions are twofold. First, we develop a framework to create a dataset of NL-TL pairs combining LLMs and human annotation. We publish a dataset with 23K NL-TL pairs. Then, we finetune T5 models on the lifted versions (i.e., the specific Atomic Propositions (AP) are hidden) of the NL and TL. The enhanced generalizability originates from two aspects: 1) Usage of lifted NL-TL characterizes common logical structures, without constraints of specific domains. 2) Application of LLMs in dataset creation largely enhances corpus richness. We test the generalization of trained models on five varied domains. To achieve full NL-TL transformation, we either combine the lifted model with AP recognition task or do the further finetuning on each specific domain. During the further finetuning, our model achieves higher accuracy (> 95%) using only <10% training data, compared with the baseline sequence to sequence (Seq2Seq) model.

## introduction temporal logic (tl) has been widely used as a mathematically precise language to specify requirements in many engineering domains such as robotics @xcite , electronics design @xcite , autonomous driving @xcite . tl can capture the complex spatial, temporal, and logical requirements of both human languages and environmental constraints, and can be transformed into executable actions or control inputs for robots @xcite @xcite @xcite . unlike many robotics works that try to use endto-end black-box models to infer robotic behaviors directly from natural language (nl) @xcite , using structured tl as the intermediate has a twofold benefit -the tl can be used for direct planning, and the tl representation can be used to identify specific sources of failure and provide automatic feedback to a non-expert user @xcite . however, tl has a steep learning curve. communicating one's goals and constraints through nl is much more intuitive to a non-expert. therefore, a model able to transform nl instructions into tl is a missing but crucial component for interactive robots and engineering designs. currently, there is no general tool to perform automated translations between tl and nl that takes the following requirements into consideration: one big bottleneck in the nl-to-tl problem is the lack of data. although modern statistical methods can outperform rule-based methods (buzhinsky, 2019), they typically require a huge dataset. this data is expensive and difficult to collect since strong expertise of annotators is needed @xcite . as outlined above, constraining the domain or form of the nl instructions relieves the pressure of dataset, but also unavoidably undermines the generalizability @xcite . to supplement the data creation process and simultaneously overcome the need for a huge dataset, we propose to use pre-trained llms. we utilize gpt-3 @xcite to assist dataset creation and finetune t5 models @xcite to be specialized in nl-to-tl transformation. another aspect of our approach is to use 'lifted' versions of nl and tl for finetuning our model, which greatly enhances generalizability. in previous work, models trained on full nl-to-tl transformation often include converting specific individual actions into aps. for example, the ap "a response is created in slack" might be formalized as "cre-ate_slack". as a result, each work has to regularize its own content and style of aps, affecting generalization. instead of taking this approach, we hide all the aps in our data during finetuning, acquiring a lifted model on lifted nl-to-tl transformation. for the final ground application from full nl into full tl, two methods are proposed, either by combining the lifted model with ap recognition or further transfer learning in one specific domain. for further transfer learning into specific domains, we compare the models with/without pre-training on lifted nl-tl and show its significance. in this paper, we present two key contributions: gpt-4 @xcite comes out when approaching the end of this work. to compare the accuracy of direct gpt-4 few-shot end-to-end translation with our finetuned model, we did an adhoc test on chatgpt plus version with 100 samples in each domain. here we can not test on more samples since we do not have access to gpt-4 api and chatgpt plus version has access limitation per hour. the results show that gpt-4 achieves an accuracy of 77.7% over 300 samples, much lower than our model but higher than gpt-3. ## related work over decades, researchers have methods to translate english sentences into various tl formulae @xcite @xcite . however, to simplify the tasks, some previous work typically make strong assumptions to restrict the input text or the output formula, thus limiting the flexibility and generalizability. the first representative attempt is by @xcite al. (2010); tellex et al. (2011); howard et al. (2014) , where the traditional methods typically follow three steps: 1) pre-process given english input by extracting syntactical information, 2) identify patterns or rules for tl through classification, and 3) run an attribute grammar-based parser to derive a target logical format. these methods only work for restricted input nl @xcite . another category of approaches are learningbased. representative state-of-the-art works are @xcite ; @xcite ; @xcite . in @xcite the authors gather a dataset focusing on geometric ltl (gltl), in which the nl and gltl examples are all for the navigation of a car in the room. then seq2seq models with attention mechanism are trained. though the accuracy (93.45%) is satisfying, the used gltls are relatively simple with each gltl normally including one to three aps and the dataset also focuses on one confined task. in @xcite the authors choose to first translate a manually generated set of stl formulae into english sentences and train a semantic parser on the synthetic data. such synthetic data cannot represent general nl and therefore the trained parser only works well on the original stl formulae. in @xcite a semantic parser is built to learn the latent structure of nl commands for ground robots. the parser will provide (potentially incorrect) intermediate ltl representations to a motion planner, and the planner will give an executed trajectory as the feedback to see whether the robot's execution satisfies the english input. such approach has no guarantee on the correctness of the translated tl. in recent months, the work by fuggitti and chakraborti (2023) directly applies llms like gpt-3 to convert nl to ltl via few-shot learning. the prompts should be well designed and the model will fail once the nl and ltl structures are too complex (we will discuss it in section 7.1). hence, in the domain of nl-to-tl translation, data augmentation/synthesis has been done algorithmically in previous work, not using generative models. this constrains how natural the resulting 'nl' actually is. in recent years, starting from the attention mechanism @xcite , the rapid progression of pre-trained llms in nlp tends to unify many previous seemingly independent tasks into one large pre-trained model, especially the gpt series from openai @xcite , and t5 @xcite and palm @xcite from google. these models are pretrained with large amounts of natural sentences and codes, intrinsically encoding much world knowledge @xcite . the auto-regressive llms can naturally generate rich and meaningful corpus based on the given prompt. then many recent work propose to do the data augmentation with llms, such as generating medical dialogues @xcite and python codes @xcite via gpt-3. this inspires us the new opportunity in nl-to-tl task. ## approach there are 3 steps in our approach. first, generating lifted nl-stl dataset with llms. second, finetuning llms to get high accuracy on lifted nl-stl transformation. third, lifting the data and applying the lifted model. finally, we also consider the case where lifting is not possible and we must translate end to end by further finetuning the model. ## experimental results though the corrected data from navigation and circuit studies already provide multiple examples, these datasets only cover limited conditions and lack generalization. to show the necessity of the newly created data, the t5 models are finetuned with varied number of created nl-stl pairs, as shown in figure 5 . during training, all the data collected from navigation and circuit studies are used and the number of created data are varied among different models. the trained models are then tested with either the created data (referred as gpt-3-assisted data test) or the nl instructions collected from volunteers (referred as manual data test). since minor difference in stls can cause severe difference in the real meanings, we apply the binary accuracy as the metric, i.e., 100% right or not. we find that the top-1 testing accuracy increases greatly increasing the number of created pairs, with the highest accuracy 97.52% and 90.12% of gpt-3 assisted data and manual data testing, respectively. ## ablation studies human annotation to reveal the significance of human annotation, we train the model with the same amount of raw pairs created by gpt-3 and test them on corrected data. the results are shown in appendix h.1. we find that annotated dataset can improve the testing accuracy by around 10%. framework2 to reveal the significance of the data generated by framework2, we train the model with either the same amount of data from pure framework1 or the data combining two frameworks. utilizing both frameworks improves the accuracy by around 2% (appendix h.2). ## limitation in spoken language, coreference is quite common, such as "pick up the apple and then bring it to me". here "apple" and "it" refer to the same object. in the five datasets we collected and tested, the coreference problem is not severe since most nl do not have pronouns. for further work, the ner models specialized in resolving coreferences and converting them into normal aps are needed for more unbounded input sentences. during the synthesis of varied stls, here we use direct algorithm-based method to generate stl binary trees. to make the semantic meanings of stls closer to human spoken language, we add the extra nl-stl loop via gpt-3. however, another intuitive way is to fit the probable distribution of operators to be close to human spoken language. for instance, the probability of two continued 'negation' operators is nearly zero. in this work we only set some hard rules to specify the stl synthesis. further work can focus on the fitting of operator distributions and apply it into stl generation. the evaluation metric here is pure binary accuracy (fully correct or not). actually, it is quite difficult to judge the similarity or distance of two tls. simply calculating token matching or computing truth values both own drawbacks. a more effective metric is needed. the output of llms may sometimes generate incorrect tls. we build up rule-based methods to check syntactic correctness and correct errors like parentheses matching. further work can be added to improve output correctness by modifying training procedures and loss functions. ## conclusion we propose a framework to achieve nl-to-tl transformation with the assistance of llm, from aspects of both data generation and model training. one dataset with about 28k lifted nl-tl pairs is then constructed by which the t5 model is finetuned. two approaches are implemented to utilize the trained model into full nl-to-tl translation. experimental results on five varied domains display much better accuracy and generalizablity compared to original methods. the created dataset can be used to train future nl-to-tl models and serve as the benchmark. the proposed framework to finetune llms with lifted nl-tl pairs makes it possible for generalizable nl-to-tl translation without the constraints of domains and input instruction structures. although our framework is built on gpt-3, the rapid progression of llms can promote our framework. the strong semantic parsing ability of newly released gpt-4 will mitigate the burden of human annotations in our method. we find that gpt-4 generated stls/nls are closer to the correct answers, compared to gpt-3 generated stls/nls. as future work, we believe the model can be improved with larger dataset containing more diversified corpus with gpt-4 as the base model.