NL2STL: Transformation from Logic Natural Language to Signal Temporal Logics using Llama2

Signal Temporal Logic (STL) is a formal language used for specifying and reasoning about the temporal properties of signals in a system. It provides a framework for expressing complex temporal behaviors and requirements in a concise and expressive manner. However, the main limitation of the current use of STL languages for describing machine tasks is that the construction of STL languages is still stuck on manual generation. Therefore, in this paper, we build a model for transforming logic natural language to STL formulas with a substantial increase in accuracy and inference speed, compared to the previous translation approach. Firstly, we pre-train a large language model (llama2) for logical ability, then we archive unsupervised learning with randomly generated STL language as a dataset and instruction fine-tuning on NL-STL pairs. Finally, we achieve an excellent result comparing to the work before.