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

arXiv: https://arxiv.org/abs/2305.07766 · HTML: https://mlsanity.com/paper/2305.07766/

## Key facts

- Cited by 59 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 37 references that are in the map.
- First posted on arXiv 12 May 2023.

## Builds on (most cited first, 11 of 11)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformer](https://mlsanity.com/paper/1910.10683/) (2019)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [PaLM: Scaling Language Modeling with Pathways](https://mlsanity.com/paper/2204.02311/) (2022)
- [Sparks of Artificial General Intelligence: Early experiments with GPT-4](https://mlsanity.com/paper/2303.12712/) (2023)
- [Selection-Inference: Exploiting Large Language Models for Interpretable Logical Reasoning](https://mlsanity.com/paper/2205.09712/) (2022)
- [Medically Aware GPT-3 as a Data Generator for Medical Dialogue Summarization](https://mlsanity.com/paper/2110.07356/) (2021)
- [Learning a natural-language to LTL executable semantic parser for grounded robotics](https://mlsanity.com/paper/2008.03277/) (2020)
- [DeepSTL -- From English Requirements to Signal Temporal Logic](https://mlsanity.com/paper/2109.10294/) (2021)
- [Generalizing to New Domains by Mapping Natural Language to Lifted LTL](https://mlsanity.com/paper/2110.05603/) (2021)

## Built on by (most cited first, 30 of 59)

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [AutoTAMP: Autoregressive Task and Motion Planning with LLMs as Translators and Checkers](https://mlsanity.com/paper/2306.06531/) (2023)
- [Plug in the Safety Chip: Enforcing Constraints for LLM-driven Robot Agents](https://mlsanity.com/paper/2309.09919/) (2023)
- [Safety Guardrails for LLM-Enabled Robots](https://mlsanity.com/paper/2503.07885/) (2025)
- [A Survey of Robotic Language Grounding: Tradeoffs between Symbols and Embeddings](https://mlsanity.com/paper/2405.13245/) (2024)
- [Conformal Temporal Logic Planning using Large Language Models](https://mlsanity.com/paper/2309.10092/) (2023)
- [SELP: Generating Safe and Efficient Task Plans for Robot Agents with Large Language Models](https://mlsanity.com/paper/2409.19471/) (2024)
- [SPINE: Online Semantic Planning for Missions with Incomplete Natural Language Specifications in Unstructured Environments](https://mlsanity.com/paper/2410.03035/) (2024)
- [A Survey on Large Language Models for Automated Planning](https://mlsanity.com/paper/2502.12435/) (2025)
- [Verifiably Following Complex Robot Instructions with Foundation Models](https://mlsanity.com/paper/2402.11498/) (2024)
- [ConformalNL2LTL: Translating Natural Language Instructions into Temporal Logic Formulas with Conformal Correctness Guarantees](https://mlsanity.com/paper/2504.21022/) (2025)
- [Air-Ground Collaboration for Language-Specified Missions in Unknown Environments](https://mlsanity.com/paper/2505.09108/) (2025)
- [We'll Fix it in Post: Improving Text-to-Video Generation with Neuro-Symbolic Feedback](https://mlsanity.com/paper/2504.17180/) (2025)
- [Distilling On-device Language Models for Robot Planning with Minimal Human Intervention](https://mlsanity.com/paper/2506.17486/) (2025)
- [Neuro-Symbolic Evaluation of Text-to-Video Models using Formal Verification](https://mlsanity.com/paper/2411.16718/) (2024)
- [Multi-Agent Reinforcement Learning Guided by Signal Temporal Logic Specifications](https://mlsanity.com/paper/2306.06808/) (2023)
- [Jailbreaking LLM-Controlled Robots](https://mlsanity.com/paper/2410.13691/) (2024)
- [HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement](https://mlsanity.com/paper/2505.15740/) (2025)
- [Towards Logically Sound Natural Language Reasoning with Logic-Enhanced Language Model Agents](https://mlsanity.com/paper/2408.16081/) (2024)
- [Generative Agents for Multi-Agent Autoformalization of Interaction Scenarios](https://mlsanity.com/paper/2412.08805/) (2024)
- [KUDA: Keypoints to Unify Dynamics Learning and Visual Prompting for Open-Vocabulary Robotic Manipulation](https://mlsanity.com/paper/2503.10546/) (2025)
- [LogicGuard: Improving Embodied LLM agents through Temporal Logic based Critics](https://mlsanity.com/paper/2507.03293/) (2025)
- [Ground-Compose-Reinforce: Grounding Language in Agentic Behaviours using Limited Data](https://mlsanity.com/paper/2507.10741/) (2025)
- [Logically Constrained Robotics Transformers for Enhanced Perception-Action Planning](https://mlsanity.com/paper/2408.05336/) (2024)
- [Verifiable Natural Language to Linear Temporal Logic Translation: A Benchmark Dataset and Evaluation Suite](https://mlsanity.com/paper/2507.00877/) (2025)
- [Contextual Safety Reasoning and Grounding for Open-World Robots](https://mlsanity.com/paper/2602.19983/) (2026)
- [Foundation Models to the Rescue: Deadlock Resolution in Connected Multi-Robot Systems](https://mlsanity.com/paper/2404.06413/) (2024)
- [Safe and Interpretable Multimodal Path Planning for Multi-Agent Cooperation](https://mlsanity.com/paper/2602.19304/) (2026)
- [Formal Methods Meet LLMs: Auditing, Monitoring, and Intervention for Compliance of Advanced AI Systems](https://mlsanity.com/paper/2605.16198/) (2026)
- [Overcoming Knowledge Barriers: Online Imitation Learning from Visual Observation with Pretrained World Models](https://mlsanity.com/paper/2404.18896/) (2024)

## Abstract (arXiv)

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.