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

1 Introduction

• Structured TL can support direct planning and help identify failure sources while providing feedback to non-experts.The paper motivates NL-to-TL translation as a way to make the formal representation more accessible to non-experts.Source: §1 · p. 1
• NL-to-TL research faces costly data collection and a trade-off between narrowing instruction domains or forms and generalizability.Expert annotation is needed, while domain or form constraints ease data demands but undermine generalization.Source: §1 · pp. 1–2
• The framework uses GPT-3 to assist dataset creation and fine-tunes T5 for NL-to-TL transformation.It trains on lifted NL and TL, hiding specific atomic propositions, then proposes AP recognition or domain-specific transfer for full translation.Source: §1 · p. 2
• The published dataset contains 28K lifted NL-TL pairs, including 15K newly generated pairs and 13K adapted from earlier datasets.The authors report that newly created data are indispensable because training only on collected data fails across domains.Source: §1 · p. 2
• Above 95% accuracy across five domains with less than 10% of the training data, compared with Seq2Seq baselines.The paper also reports comparing against direct few-shot GPT-3 learning.Source: §1 · p. 2

2.1 STL Syntax

• STL supports real-time constraints and is the paper’s representative formal language, with formulas built from predicates, logical operators, and bounded-time temporal operators.The paper also states that its framework is based on STL and performs well on datasets and tasks using LTL.Source: §2.1 · pp. 2–3

2.2 Lifted STL and Lifted NL

• In lifted NL and STL, specific atomic propositions are hidden by replacing each with a prop_i placeholder.This lets training focus on instruction context regardless of the specific propositions.Source: §2.2 · p. 3

2.3 STL Expression Formats

• In-order STL expressions with operators written as words achieve much better accuracy than the other three tested formats.The paper frames the expressions as linearizations of an STL binary tree.Source: §2.3 · p. 3

3 Related Work

• Traditional pipelines preprocess English, classify patterns or rules, and use attribute grammars, but work only for restricted input NL.The paper cites Finucane et al. (2010), Tellex et al. (2011), and Howard et al. (2014) as representative attempts.Source: §3 · p. 3
• Learning-based systems include domain-focused GLTL and synthetic-data parsers, while reported limitations include simple formulas or narrow coverage (He et al., 2022).Gopalan et al. report 93.45% accuracy on a confined navigation task with typically one to three atomic propositions.Source: §3 · p. 3
• Robot-feedback parsing lacks a correctness guarantee, while direct few-shot GPT-3 translation can fail on complex NL and LTL structures (Wang et al., 2021).The paper contrasts these approaches with LLM-assisted data augmentation, which can generate varied corpus from prompts.Source: §3 · pp. 3–4
• Earlier algorithmic data synthesis constrains how natural generated NL is, motivating the paper’s use of generative models for augmentation.The paper notes GPT-3’s capacity to generate corpus from prompts.Source: §3 · p. 4

4 Approach

• The approach has three stages: generate a lifted NL-STL dataset, fine-tune a model for lifted transformation, and apply it through lifting or further domain-specific fine-tuning.The latter route addresses cases where lifting is not possible.Source: §4 · p. 4

4.1 Data Generation

• Framework1 prompts GPT-3 with varied STL expressions to generate NL, then human annotators correct the NL; Framework2 adds an extra NL-STL loop to filter or modify difficult formulas.Prompts are randomly selected to diversify vocabulary and sentence structure, and 100 volunteer instructions are reserved for manual testing.Source: §4.1 · pp. 4–5
• The authors create 15,108 lifted pairs in about 150 person-hours and combine them with 5K Navigation and 8K Circuit pairs for a dataset of about 28K.Framework2 yields about 120 annotated pairs per person-hour, versus about 80 with Framework1.Source: §4.1 · p. 5

4.2 Model Finetuning

• The paper fine-tunes T5-base (220M) and T5-large (770M) on the same data to study whether model size affects performance.The supplied passage describes the model-size comparison setup.Source: §4.2 · p. 5

5 Experimental Results

• Top-1 accuracy reaches 97.52% on GPT-3-assisted data and 90.12% on Manual data as the number of created pairs increases.Training uses the Navigation and Circuit data alongside varying amounts of created data; accuracy is binary.Source: §5 · pp. 5–6
• In-order target expressions with operators replaced by words improve performance, matching natural sentence structure and easing LLM finetuning.This differs from prior Seq2Seq findings favoring pre-order expressions to avoid parentheses-matching issues (Wang et al., 2021).Source: §5 · p. 6, Table 1 · p. 6

Human Annotation

• Annotated data improves testing accuracy by around 10% over raw GPT-3-generated pairs.The models use the same amount of raw pairs for training and are tested on corrected data.Source: §6 · p. 6

Framework2

• Combining data from Framework1 and Framework2 improves accuracy by around 2% over using the same amount from Framework1 alone.The comparison tests the contribution of Framework2-generated data.Source: §6 · p. 6

Model Capacity of T5

• Finetuning T5 improves accuracy by around 14.5% compared with a Seq2Seq model trained on the same lifted NL-STL dataset.The comparison is used to assess T5’s model capacity.Source: §6 · p. 6

7 Application

• When AP representation rules are known, GPT-3 can identify and hide APs before the lifted model predicts the logical structure and the APs are restored.The second application route is direct domain-specific finetuning when only full NL-STL pairs are available.Source: §7.1 · p. 7, §7.2 · p. 7

7.1 Lifted Model + GPT-3 AP Recognition

• Combining the finetuned lifted model with GPT-3 AP recognition yields over 95% full-task accuracy across three domains.The tested domains are Circuit, Navigation, and Office email; Table 2 reports full NL-to-STL accuracy by grounding model.Source: §7.1 · p. 7, Table 2 · p. 7
• GPT-3 AP detection is described as easier than direct NL-to-STL translation, making task decomposition more data-efficient and flexible than an end-to-end approach.Table 3 reports GPT-3 AP-recognition accuracy by domain.Source: §7.1 · p. 7, Table 3 · p. 7

7.2 Transfer Learning

• Further finetuning adapts the lifted model to a domain’s AP formatting while retaining its learned semantic logical relations.This route is presented for settings without known hard-coded AP representation rules.Source: §7.2 · p. 7
• Near 95% accuracy is achieved in Circuit, Navigation, and GLTL with 200 to 500 full NL-STL examples, about one magnitude fewer than Seq2Seq baselines.T5-large with lifted NL-STL pretraining performs better than T5-base and the original Seq2Seq models.Source: §7.2 · p. 8, Figure 6 · p. 8
• On the CW dataset, finetuned LLMs outperform the original baseline when tested on LTLs unseen during training.CW contains 36 distinct LTLs, with an average of 50 NL descriptions per LTL.Source: §7.2 · p. 8, Figure 7 · p. 8

• Coreference is not severe in the five tested datasets, where most instructions lack pronouns, but more unbounded inputs need specialized NER for resolution and AP conversion.Source: §8 · p. 9
• STL synthesis uses algorithm-generated binary trees and hard rules, while fitting operator distributions to human language is left for future work.Source: §8 · p. 9
• Evaluation uses fully correct-or-not binary accuracy, but judging TL similarity is difficult and token matching or truth-value comparisons each have drawbacks.Source: §8 · p. 9
• LLM outputs may contain incorrect TLs; rule-based checks address syntactic issues such as unmatched parentheses, while further correctness improvements are left for future work.Source: §8 · p. 9

9 Conclusion

• The framework combines LLM-assisted data creation and lifted NL-TL finetuning; experiments across five domains report higher accuracy and generalizability than prior methods.The conclusion says the dataset contains about 28K lifted pairs and that the trained model is used for full NL-to-TL translation through two approaches.Source: §9 · p. 9

B Full algorithm to synthesize multiple STLs

• The STL synthesis algorithm builds formulas by randomly dividing propositions into sublists, adding operators, then joining the sub-STLs with binary operators.The generated formulas are syntactically correct but may have semantic flaws; preset rules avoid unreasonable cases such as consecutive negations.Source: B Full algorithm to synthesize… · p. 13

C.1 Prompt example from in-order STL to NL via GPT-3

• The STL-to-NL prompt uses in-order expressions with operators replaced by words and contains 20 pairs randomly selected from 100 examples.The selected pairs change during data creation.Source: §C.1 · p. 14

C.2 Prompt example from NL to pre-order STL via GPT-3

• The NL-to-STL prompt produces pre-order expressions, and GPT-3 performs similarly with pre-order and in-order formats.Source: §C.2 · p. 15

C.3 Prompt example for AP recognition via GPT-3

• The AP-recognition prompt asks GPT-3 to detect APs in natural-language sentences; the example uses the Navigation domain.Source: §C.3 · p. 16

D Number of NL-STL pairs in GPT-3 prompts

• GPT-3 is prompted with 20 randomly selected NL-STL pairs from a pool of 100, and accuracy plateaus when prompts contain more than 20 pairs.The prompt-pair test uses instructions whose target STLs contain two or three APs.Source: D Number of NL-STL pairs in GPT-3… · p. 17

E Example annotations of lifted NL-STL pairs

• The appendix includes example annotations connecting synthesized STLs to raw and then annotated natural-language sentences.Source: Table 5 · p. 18

F Process of human annotation

• Human annotation involved formal-methods and robot-planning researchers, with cross-checking by another annotator and a final author review.Annotators initially labeled 50 pairs each and received guidance and example pairs.Source: F Process of human annotation · p. 18

G Example full NL-STL pairs of each specialized dataset

• The appendix provides examples of full NL-STL pairs from specialized domains.Source: G Example full NL-STL pairs of each… · p. 18, Table 6 · p. 19

H.1 Significance of Human Annotation

• T5-large reaches 87.3% on the GPT-3-assisted data test and 79.4% on the Manual data test using only GPT-3-synthesized raw training data.Models trained on annotated data achieve about 10% higher accuracy than models trained on raw data.Source: §H.1 · p. 20, Figure 12 · p. 20

H.2 Significance of Framework2

• Annotated data improves model performance, and combining Framework1 and Framework2 data outperforms the same amount of Framework1-only data.Source: Table 7 · p. 20

I Model Capacity

• T5-large performs much better than Seq2Seq when both train on the same lifted dataset.The cited Figure 13 caption reports highest accuracies of 97.5% for T5-large and 83% for Seq2Seq.Source: Figure 13 · p. 21, I Model Capacity · p. 21

J.1 Statistics of lifted NL-STL dataset

• Table 8 summarizes lifted STL formulas by AP count and operator count, while Table 9 reports lifted-sentence and vocabulary statistics.Source: Table 8 · p. 22, Table 9 · p. 22

J.2 Statistics of corpus richness

• The synthesized dataset has more unique STLs and vocabulary than previously collected datasets, indicating greater corpus richness.Source: Table 10 · p. 22

K Accuracy evolution with AP number

• Finetuned T5-large remains accurate across increasing AP counts, while GPT-3 end-to-end accuracy drops rapidly.The section treats AP count as a proxy for sentence complexity.Source: K Accuracy evolution with AP number · p. 23, Figure 14 · p. 23

L Details of implementation

• Finetuning uses a 2e-5 learning rate, batch size 16, weight decay 0.01, and 20 epochs; lifted-model data are split 90% for training and 10% for testing.Average runs take 3 hours for T5-base and 10 hours for T5-large on one Nvidia RTX 8000 GPU.Source: L Details of implementation · p. 23
• Figure 15 illustrates full STL conversion by combining the trained model with AP recognition.Source: Figure 15 · p. 24