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.

翻译：时序逻辑（Temporal Logic，TL）能够严格地规范许多工程应用中系统的复杂高层规范。由于缺乏数据集以及跨不同应用领域的通用模型，自然语言（Natural Language，NL）与TL之间的转换研究尚不充分。本文提出一种准确且通用的从英文自然语言到时序逻辑的转换框架，探索了在多个阶段使用大型语言模型（LLMs）。我们的贡献有两方面：首先，我们开发了一种结合LLMs与人工标注来构建NL-TL对数据集的框架，并发布了一个包含28K个NL-TL对的数据集。然后，我们在NL与TL的抽象版本（即隐藏特定原子命题AP）上微调T5模型。增强的通用性源于两个方面：1）使用抽象的NL-TL对能够刻画常见的逻辑结构，不受特定领域约束；2）在数据集构建中应用LLMs极大地丰富了语料库的多样性。我们在五个不同领域上测试了训练模型的泛化能力。为实现完整的NL-TL转换，我们可将抽象模型与原子命题识别任务相结合，或在每个特定领域上进行进一步微调。在进一步微调中，与基线序列到序列（Seq2Seq）模型相比，我们的模型仅使用不到10%的训练数据即可达到高于95%的准确率。