English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Temporal Logic (TL) can be used to rigorously specify complex high-levelspecification for systems in many engineering applications. The translationbetween natural language (NL) and TL has been under-explored due to the lack ofdataset and generalizable model across different application domains. In thispaper, we propose an accurate and generalizable transformation framework ofEnglish instructions from NL to TL, exploring the use of Large Language Models(LLMs) at multiple stages. Our contributions are twofold. First, we develop aframework to create a dataset of NL-TL pairs combining LLMs and humanannotation. We publish a dataset with 28K NL-TL pairs. Then, we finetune T5models on the lifted versions (i.e., the specific Atomic Propositions (AP) arehidden) of the NL and TL. The enhanced generalizability originates from twoaspects: 1) Usage of lifted NL-TL characterizes common logical structures,without constraints of specific domains. 2) Application of LLMs in datasetcreation largely enhances corpus richness. We test the generalization oftrained models on five varied domains. To achieve full NL-TL transformation, weeither combine the lifted model with AP recognition task or do the furtherfinetuning on each specific domain. During the further finetuning, our modelachieves higher accuracy (>95%) using only <10% training data, compared withthe baseline sequence to sequence (Seq2Seq) model.

NL2TL: Transforming Natural Languages to Temporal Logics using Large Language Models