Click here to flash read.
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 28K 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.
