Grammar-Forced Translation of Natural Language to Temporal Logic using LLMs
Authors: William H English
Dominic Simon
Sumit Kumar Jha
Rickard Ewetz
Venue: ICML 2025 poster (2025)
Keywords: Temporal Logic
Grammar Constrained Decoding
Sequence-to-Sequence
Primary area: applications->language_speech_and_dialog
TL;DR: We present a framework for translating natural language into TL that exploits improved grounding of atomic predicates, a grammar-forcing training protocol for seq2seq models, and a temporal logic based grammar constrained decoding strategy

Abstract: Translating natural language (NL) into a formal language such as temporal logic (TL) is integral for human communication with robots and autonomous systems. State-of-the-art approaches decompose the task into a grounding of atomic propositions (APs) phase and a translation phase. However, existing methods struggle with accurate grounding, the existence of co-references, and learning from limited data. In this paper, we propose a framework for NL to TL translation called Grammar Forced Translation (GraFT). The framework is based on the observation that previous work solves both the grounding and translation steps by letting a language model iteratively predict tokens from its full vocabulary. In contrast, GraFT reduces the complexity of both tasks by restricting the set of valid output tokens from the full vocabulary to only a handful in each step. The solution space reduction is obtained by exploiting the unique properties of each problem. We also provide a theoretical justification for why the solution space reduction leads to more efficient learning. We evaluate the effectiveness of GraFT using the CW, GLTL, and Navi benchmarks. Compared with state-of-the-art translation approaches, it can be observed that GraFT improves the end-to-end translation accuracy by 5.49% and out-of-domain translation accuracy by 14.06% on average.

Grammar-Forced Translation of Natural Language to Temporal Logic using LLMs
William English Dominic Simon
Sumit Kumar Jha? Rickard Ewetz
Abstract
ning (Tellex et al., 2011; Abdulla et al., 2004). Ensuring that the behavior of such systems is bound to set of known rules is essential to deploy them safely and reliably, especially when they are expected to operate without constant human supervision (Raman et al., 2013; Boteanu et al., 2016). Tem- poral Logics (TL) are group of powerful formalisms that constitute the basis of most formal specification languages, allowing expressive description of the behavior of dynamic systems over time (Konur, 2013; Madsen et al., 2018). How- ever, generating these specifications directly from natural language (NL) is an open problem, and achieving effective and efficient translation between NL and TL is an increas- ingly important task in advancing system automation (Chen et al., 2023; Fuggitti & Chakraborti, 2023; Cosler al., 2023).
Translating natural language (NI.) into a formal language such as temporal logic (TL) is integral for human communication with robots and au- tonomous systems. State-of-the-ar approaches decompose the task into grounding of atomic propositions (APs) phase and a translation phase. However, existing methods struggle with accurate grounding, the existence of co-references, and learning from limited data. In this paper, we pro- pose framework for NL to TL translation called Grammar Forced Translation (GraFT). The frame- work is based on the observation that previous work solves both the grounding and translation steps by letting a language model iteratively pre- dict tokens from its full vocabulary. contrast, GraFT reduces the complexity of both tasks by restricting the set of valid output tokens from the full vocabulary only handful in each step. The solution space reduction is obtained by exploiting the unique properties of each problem. We also provide a theoretical justification for why the solu- tion space reduction leads to more efficient learn- ing. We evaluate the effectiveness of GraFT using the CW, GLTL, and Navi benchmarks. Compared with state-of-te of-te-o-thh--ee art translation approaches, it can be observed that GraFT improves the end-to-end translation accuracy by 5.49% and out-of- translation accuracy by 14.06% on average.
Early work on NL to TL. translation focused on either on restricted natural language inputs (Raman et al., 2013) or template matching (Tellex et al., 2020). Although struc- tured inputs are easy to map into TL., they place an undue burden on the user who may not have a technical back- ground (Thistle & Wonham, 1986). On the other hand, template matching requires a substantial number of domain specific examples (Bombieri et al., 2023). More recently, NL to TL translation has been investigated using large lan- guage models (LLMs) (Cosler et al., 2023; Pan et al., 2023; Patel, 2019). This has involved approaches where LLMs are used to perform end-to-end translation. While such approaches can handle simple translations, the accuracy have been observed to be limited to 70% for more chal- lenging test cases (Xu et al., 2024). More recent studies decompose the translation into atomic propositions (APs) grounding phase and a translation phase. The two step ap- proach is motivated by that domain specific terms will be extracted during the grounding phase, which facilitates do- main agnostic translation (Fuggitti & Chakraborti, 2023). Existing works perform the grounding of APs using casual language model and few shot learning (Liu et al., 2023). The translation step is performed by fine-tuned sequence-to- sequence model, where one token of the TL. is predicted at the time (Chen et al., 2023). To boost the performance of the translation, studies have proposed to increase the size of the training data set using generative data augmentation (Chen et al., 2023). Unfortunately, it can be observed that
1. Introduction
Formal specifications play a crucial role in all systems that require autonomous reasoning, verification, or plan-
'Department of Electrical and Computer Engineering, Univer- sity of Florida, Gainesville, Florida Knightt Foundation School of Computing and Information Sciences, Florida International University, Miami, Florida. Correspondence to: William English <will.english @ edl...
Proceedings of the 42nd International Conference Machine Learning, Vancouver, Canada. PMLR 267, 2025. Copyright 2025 by the author(s).

---

Grammar-Foreed Translation of Natural Language to Temporal Logic using LLMS
isting AP grounding techniques struggle with consistently achieving high accuracy. In particular, for natural language inputs containing multiple references to the same AP, i.e., co-references. Moreover, the accuracy of the translation is highly dependent on the amount of available training data.
logic by introducing modalities that capture time-related aspects, such as "always."" "sometimes." " "eventually," and "until." This paper deals with temporal logic but the concepts can easily be extended to signal temporal logic (Madsen et al., 2018) or linear temporal logic (Zhu, 2021). Temporal logic formulas are defined recursively, as follows:
In this paper, we propose a framework for NL to TL trans- lation called Grammar Foreed Translation (GraFT). The framework is based on the observation that previous work solves both the grounding and translation steps by letting language model iteratively predict the next token from the full token library. In contrast, GraFT reduces the complexity of both tasks by restricting the number of valid output token from the full library to only a handful in each step. The main contributions of this paper can be summarized, as follows:
:- x1= A whp V w/o + v O p Opppul
where nt are the atomic predicates and both sp and to are temporal logic formula. 7, A, V, and + are the logical operators negation, and, or, and implies, respectively. O. Q D. U, are the temporal operators next, eventually, always, and until respectively.
A sample NL to TL translation problem would involve trans- lating the natural language sentence "Go to the red room and push the box into the green room." into (Frre room A green grren_room)).
1. The GraFT framework grounds the APs in the NL input using an masked language model (MLM). This both reduces the task complexity and restricts number of valid output tokens the set of integers.
2.2. Language Modeling
2. A fine-tuned sequence coreennceto-sequueee so-sequence model is used to translate the grounded NI. into TI.. GraFT exploits the known grammar of the TL language, to place restric- tions of the valid output tokens from the sequence-to- sequence model to handful.
In this section, we review popular language modeling ap- proaches such as masked language modeling, sequence-to- sequence modeling, and causal language modeling.
Masked Language Modeling (MLM)) Masked language modeling is a training approach used primarily in NLP where certain words in sentence are randomly masked or hidden, and the model is tasked with predicting these missing words based on the surrounding context (Devlin et al., 2019). This technique helps the model understand relationships between words and enhances its ability to gen- erate coherent and contextually relevant text. MLM the foundation for training of models like BERT (Devlin et al., 2019), DistilBERT (Sanh et al., 2020), and ROBERTA (Liu et al., 2019). MLMs have demonstrated excellent perfor- mance of tasks with bidirectional representations.
3. Mathematical justification are provided to explain why the restrictions the output tokens lead to more effi- cient learning. We provide proofs for lower (or equal) cross-entropy well as improved gradient alignment under grammar-forcing.
4. We evaluate the proposed framework on three natural language to temporal logic benchmarks- CW, GLTTL, and Navigation. Compared with state-of-the-art ap- proaches, we improve the accuracy of the end-to-end translation by 5.49% on average, by 14.06% on average in dut-o--distribution tests.
Sequence-to-Sequenee Language Modeling (Seq2Seq): Sequence to sequence modeling is a framework designed for tasks where input and output are both sequences, such as translation or summarization (Raffel al., 2020). In this architecture, two neural networks, typically encoder and decoder, work in tandem: the encoder processes the input sequence and compresses it into fixed-size context vector, while the decoder generates the output sequence from this representation. Seq2Seq has been used to train models such as T5 (Raffel et al., 2020), Bart (Lewis et al., 2019), and Pegasus (Zhang et al., 2020). The Seq2Seq approach works well for tasks that require understanding the entire input context before generating the output, enabling applications like machine translation, chat-bots, and text summarization.
The remainder of the paper is organized, as follows: Prelim- inaries are given in Section 2. The methodology is provided in Section 3 and experimental evaluation in Section 4. The paper concluded in Section 5
2. Background
In this section, we review preliminaries on temporal logic, language modeling, and related work.
2.1. Temporal Logic
Temporal logic is a formal framework used to reason about propositions qualified in terms of time, allowing for the expression of statements about the temporal ordering of events (Konur, 2013). It extends classical propositional
Causal Language Modeling (CLM) Causal language mod- cling, often associated with autoregressive models, focuses on predicting the next word in a sequence given the previ-
2

---

Grammar-Foreed Translation of Natural Language to Temporal Logic using LLMS
Approach
AP grounding
TL Translation Decoding Strategy
Model
Vocab Size
Model
Vocab Size
NL2LTL (Fuggitti & Chakraborti, 2023)
CLM
100,256
NL.2Spec (Cosler et al., 2023)
CLM
50,257
NL2TL (Chen et al., 2023)
CLM
100,256 6
Seq2Seq
32,182
GraFT (proposed)
MLM
Seq2Seq Grammar-Construinn
1 [V] - 20
Table 1: Contrast between the use of LLMs within the proposed translation and state-of-the of--the-rtt approaches. A '-' denotes that the step was not performed. GraFT's MIM vocab size is 6 due to the 6 labels relating to APs (0 for non-AP or 1-5), and between 1 and 20 for the translation- the minimum and maximum number of valid tokens at any given state.
ous words (Achiam et al., 2024). This method is inherently directional and processes the input in a left-to-right manner. Models that are trained using CLM include the prominent GPT family (Achiam et al., 2024). This approach effective for tasks that require coherent prompt-based text generation.
ing each of them independently was proposed in (Cosler et al., 2023). Several works have investigated fine-tuning sequence-to-sequemee models to perform translation (Pan et al., 2023; Patel, 2019; Chen et al., 2023). The perfor- mance improvements achieved through fine-tuning are often correlated with the amount of available training data. Data augmentation to generate training data using LLMs was proposed in (Pan et al., 2023). An alternative to data depen- dency is deploying the translation model in a reinforcement learning environment, using rewards for fine-tuning. How- ever, these methods overlook TL's structured, context-free grammar.
2.3. Related Work
In this section, we provide an overview of recent attempts translating natural language into formal language speci- fications and temporal logic using LLMs. The translation can be decomposed into two main steps: 1) grounding of atomic predicates and 2) NL to TL translation.
We observe that previous approaches to grounding and translation use language models without exploiting the unique properties of the problems to enhance learning. For both tasks, a language model is used to predict token from the models full token library. In the proposed GraFT framework, we propose reduce the complexity of both tasks by placing restrictions on the valid output tokens. In particular, the grounding is reformulated into a masked language modeling problem where the output tokens are restricted to integers, For the translation, the temporal logic grammar is used to dynamically reduce the number of valid output tokens to a handful. The main differences compared with previous work are shown in Table 1.
Proposed Method:
Atomic predicates (APs) are state variables or events that temporal logic reason over. While the logical statements are the same for different domains, the defini- tion of the atomic predicates can vary substantial between different applications. For example, the APs used to de- scribe the operation of traffic light are very different from the APs used to describe the operation of an autonomous robot. Therefore, it was proposed the atomic predicates within the NL should be extracted (or grounded) in a pre- processing step before the translation into TL (Chen al., 2023; Liu et al., 2023; Hsiung et al., 2021). The grounded NL would be more similar across domains and allow cross- domain adaptation with the use of less training data. This was performed by replacing each atomic predicate with prop_z variable in (Chen et al., 2023), descriptive single words in (Liu et al., 2023), and templates in (Hsiung et al., 2021). These grounding approaches improve downstream translations but can introduce errors, including hallucinated keywords and difficulties handling co-references, where different words refer to the same AP.
AP Grounding:
3. Methodology
In this section, we present the methodology of the GraFT framework that converts natural language into temporal logic. The framework consists of two steps: grounding of atomic predicates (APs) and grounded NL to TL transla- tion. The first step uses an MLM (BERT (Devlin al., 2019) identify the atomic predicates, which is detailed in Section 1.1. The second step uses Seq-2-Seq model (T5 (Raffel et al., 2020)) to translate the lifted natural language given in the previous step into lifted linear temporal logic, as outlined in Section 3.2. Finally, the lifted APs from step one are inserted into the lifted LTL, yielding the final translation result. An overview of the flow of the framework is shown in Figure 1.
The translation of natural language (or grounded natural language) using LLMs has been ex- plored in (Fuggitti & Chakraborti, 2023: Cosler et al., 2023; Chen et al., 2023). The most straightforward approach to NL to TL translations is to used an large off-the-shelf CLM (Chen et al., 2023). The accuracy of the approach can be enhanced if restrictions are placed on the NI descrip- tions and by providing examples with few shot prompting. Breaking down the problem into sentences and translat-
NL to TL Translation:
3

---

Grammar-Foreed Translation of Natural Language to Temporal Logic using LLMs
Grounding Phase
Translation Phase
Output Probabilttes
Solmai
Temporal Logic
Grammar
Input
Labels
Output (Temporal Logic Expression)
(Natural Language Sentence)
Encoder
Masked Language Model
(BERT)
Seqpence
Ispui Embedding
Output Entedding
Figure 1: An overview of the GraFT framework of end-to-end translation of NL to TL.
3.1. Grounding of Atomic Predicates
to sound more natural. For example, it is not surprising to observe that the causal model has slightly modified the input by dropping the word "eventually", which introduces an error in the subsequent translation, as is a key word for temporal logic. Moreover, the output the CLM must be parsed as it is not guaranteed follow the format shown in the few shot prompting examples. Conversely, masked language models (MLMs) are trained to predict labels the imput tokens, which we hypothesize is much more effective solution for solving this task. In the bottom of the figure, it can be observed that our proposed grounding approach only assigns an indicator variable to each the tokens in the input, i.c., the indicator variable determines a token part of AP not.
In this section, we describe how the GraFT framework ex- tracts the atomic predicates from the NL input. AP ground- ing is the process of substituting the atomic predicates (APs) within the NL input to obtain Grounded NL. Before we outline our approach, we examine the characteristics of per- forming the AP grounding using different types of language modeling.
We compare performing the AP grounding using CLM (GPT-4o) and MLM (BERT) in Figure 2. We first focus on performing the AP extraction using a CLM as in (Chen et al., 2023). Causal language models are trained perform next-word prediction rather than to predict masked tokens in a sequence. While CLMs regarded for their reasoning abilities, and are capable of extracting the APs as shown at the top of the figure, the sequence returned by the model is not 1-to-1 with the input sequence. While the CLMs may "understand" that is sup- posed to replicate the input sentence with the APs masked, is prone introducing errors by modifying the sentence
Failure Analysis of CLMs:
Proposed Grounding using MLM: The AP grounding in the GraFT framework is performed by fine-tuming a MLM. Using the fine-tuning process, we teach the MLM to assign an indicator variable I, to each token i of the input. The indicator variables 7 form list of integers. In integer grounding, each AP in the input string assigned integer ID, and tokens which are part of reference to that AP
Causal Language
Input NL:
" "Redirect the asset 24th avenue. Follow if it leaves there."
Model
Grounded NL:
[prop__1 [prop_2) [prop 3]. [prop_4) 4] if [prop_ 2] [prop_5] [prop_3]. []
(GPT)
Masked
Input NL:
"Redirect the asset near 24th avenue. Follow if it leaves there."
Language
Model
Integer Grounding:
[1,
2, 0, 3, 0,
2, 5, 3, 0]
(BERT)
Grounded NL:
[prop_1] the [prop_2] 2] near [prop_3]. [prop_4] [prop_2] 2] [prop_5] 5] [prop_3]
Integer Mapping: [prop "Redirect"
[prop "asset", "it"
[prop_3] 3] "24th avenue", "there"
[prop_4] "Follow"
[prop_5) "leaves
Figure 2: AP grounding using LLMs trained using different types of language modeling.

---

Grammar-Foreed Translation of Natural Language to Temporal Logic using LLMs
Output
Probabilities
Softmax
Linear
Grammar Mask
Softmax
Temporal
Model
Raw Logit
Grammar-Constrn Constrained Logit Scores
Logic
Vocabulary
Scores
Temporal Logic Grammar
Grammar
Linear
Sequence
Legal Tokens
If
-2..99
-00
-00
Stack State
finilyy
finally
-35.86
formula (
peop
+
Decoder
Previous Token
globally
the -14.74
-00
Encoder
org
and
prop
-83.91
-83.91
Input Embedding
Output Embedding
...
for -63.45
+00
Input
Output
Sequence
Sequence
Current
Decoded Token
Position
finally
and
Enaily
Figure 3: At each training step, prior to performing SoftMax on the output logits in preparation for computing L, we observe the label at position target sequence I.. Given this token and the current state of the TL. parsing stack, we can obtain a of valid token that may proceed that label. For each output logit Z, we set the score for all tokens outside of V, to -O0.
are labeled with the respective ID. An example of this AP grounding approach is given in Figure 2.
3.2.1. GRAMMAR CONSTRAINED DECODING
In order to exploit the grammatical structure of the target language, we construct a logits processor that ensures the sequence being decoded obeys the rules. Because of this, we can guarantee that sequences produced by GraFT are grammatically correct temporal logic expressions. Our im- plementation of the grammar-constraine logits processor is described in Algorithm 1.
0, Jn is not part an AP,
I; n, In is part of the Tigh AP.
(1)
The objective of the fine-tuning is to predict the indica- tor variables I. We use standard cross-entropy loss for the training using an annotated portion of the Navigation dataset (Wang al., 2021). Notably, each of the MLMS trained only the Navigation dataset demonstrate nearly perfect performance for other datasets. These results are presented in Table 3.
Algorithm effectively adjusts the logit scores returned by scquence-fo-seqqeecce models to decode logits during generation. The first token in the sequence is restricted to the known list of valid initial tokens, and so for that logit we apply mask that erases all tokens that can not follow from the initial state of the grammar. For all subsequent tokens,
the temporal logic grammar to determine which tokens may proceed the previously decoded token, as well as which tokens may occur given the current state of the temporal logic grammar. We now turn to further explanation of this training procedure.
3.2. Grounded NI. to TI Translation
In this section, we describe how the grounded NL is trans- lated into TL. The translation is performed using Seq2Seq model. The key idea is to impose the grammar of the TL when decoding the output from the model. particular, we introduce two grammar-based augmentations: a grammar- forcing strategy during training, and grammar-constraing decoding during inference. The details provided in Sec- tion 3.2.1. Lastly, the section is concluded with theoretical basis for the improved efficiency in learning. The details of the theoretical motivation are provided in Section 3.2.2. An overview of the proposed translation framework is shown in Figure? 3.
As previously stated, we apply grammar constrained decod- ing during training. However, rather than pass the previous token generated by the model, we pass the previous token in the target sequence. This technique is reminiscent of reacher-forcing (Hao et al., 2022), as we use ground truth labels to inform the model of how it may generate sequences during training. similar to the grammar-constrainet de- coding we use during inference, except we use the tokens of
5

---

Grammar-Foreed Translation of Natural Language to Temporal Logic using LLMS
the target sequence update the grammar state and retrieve valid tokens. We now turn to theoretical justification for this technique.
(1) Lower (or Equal) Cross- Cross-Entropy.
By construction,
3.2.2. THEORETICAL. BASIS FOR GRAMMAR-FORCAE
exp(zy)
L(z.y) y)
=
EvEn exp (zo)
We know intuitively that by zeroing-out known invalid to- kens from the output logits vector, we can reduce our cross- entropy loss. The following is a more formal argument for this claim. Firstly, we introduce our notation and propose that our approach provides some guaranteed improvements. We then explain how reach this conclusion in formal terms. We provide additional justification in Section A.4 of the Appendix.
exp(2y)
L'(z,y)
log
EneV, exp( (2u)
Since V. S V. we have
Σ
exp(zz)
S Σ exp(ze).
eEV.
VEV
Preliminaries: Let V be the vocabulary of the model p(0). At each decoding step L, the model returns vector of logits 2 (21, 22; ..., zn) where žn = (vi, U2, (()))) RR The standard softmax distribution over a single logit is
Thus
explzy)
exp(zy) Evey exp(2 (zu)
Ener. exp(2n)
exp(zr)
p Exevexp(22 exp(zu)*
V VEW V
which implies
the label at step / is E V. the cross-entropy loss is
exp(zy)
explay)
- log
S - S-log
EvEn, exp(zu)
EvEy exp(2e)
exp(zy)
L(z,y) log Σuev exp(zu)
Hence [z y) S L(z, v). Equality can occur if 2, = for all & V., which precisely the masking scenario.
Now suppose that at step t, only subset V/ C V contains grammatically valid tokens. We mask out all invalid tokens by setting their logits to -00. Define the transformed logits
(2) More Focused Gradient (Better Alignment).
4 =
if E Ve.
For standard cross-entropy, the gradient with respect to each logit 2 is:
-00, if $ V.
and the corresponding distribution
OL(z.)) v)
= =p(k) - 1[k = y).
Ozp
exp(zv) p'(u) Ener exp(2n)
if E Ve, i E Ve,
(2)
where p(k) exp(2x) / Evey exp(2x).
Under grammar-forcing,
The grammar-forved cross-entropy loss becomes
0L' aL' O25
D' p'()) 1 y).
exp(zy) Emer. exp(zu)
v' llogp'(v) = - -log
We also recall the probability distribution under grammar forcing 2 and observe that
assuming y E Vt.
aT' v) dzk
Masking Invalid Tokens Improves Optimization Let y Vú be the target, and let z be the logit vector in that position at some iteration of training. Then the grammar- forced cross-entropy I.' Tz(2.,) v) is never larger than the stan- dard cross-entropy L(z, y). Furthermore, the gradient of L' focuses updates only on valid tokens, thereby reducing the effective search space and often yielding faster or more stable convergence.
=0, V k $ V.
Recalling that E V., we observe that no gradient signal is wasted on tokens that can never be correct, allowing each update step to invest more effective capacity into discrimi- nating among valid tokens.
6

---

Grammar-Foreed Translation of Natural Language to Temporal Logic using LLMs
Approach
Data Quantity
AP Grounding
Translation Model
CW (%)
GLTL
Navi
Model
(%)
(%)
NL2LTL (Fuggitti Chakraborti, 2023)
None
GPT-4o-mini
69.90
74.40
65.30
NL22Spec (Cosler al., 2023)
None
GPT-44-mini
78.60
68.40
71.60
Ungrounded Seq2Seq
500
T5
59.60
46.80
43.40
NL2TL (Chen et al.. 2023)
500
GPT-4o-mini
T5
93.00
83.80
80.40
NL2TLL (Chen et al., 2023)
500
GPT4
T5 91.50
82.60
83.70
GraFT (proposed)
500
BERT
T5 97.70
91.50
85.00
Ungrounded Seq2Seq
2000
T5
68.10
55.90
56.30
NL2TL (Chen et al., 2023)
2000
GPT-4o-mini
T5
98.20
97.40
86.70
NL2TL (Chen al., 2023)
2000
GPT-4
T5
96.70
96.20
90.00
GraFT (proposed)
2000
BERT
T5
99.90
99.80
99.10
Table Performance comparison of different models for end-to-end translation with training data from each dataset. The BERT model used for AP Grounding is trained the same data used to train the translation model.
1.6
framework in Section 4.1. Next, we provide end-to-end translation results in Section 4.3.
T5
1.4
T5 + GraFT
Final Training Loss
1.2
4.1. Ablation Studies of GraFT
1.0
Model
Objective
CW (%)
GLTL
Navi
0.8
(%)
(%)
0.6
GPT-4o-mini
Causal
97.76
95.84
83.97
GPT-4o
Causal
95.02
93.53
86.08.
0.4
GPT-4
Causal
96.24
94.68
87.28
0.2
DistiBBERT
Masked
95.80
93.83
99.99
RoBERTa
Masked
98.34
96.96
99.99
0.0
BERT
Masked
98.58
97.35
99.99
100
400 Training Data Quantity
200
300
500
Table 3: The table evaluates the models' accuracy the AP Masking task using 1000 examples from the Navi dataset.
Figure 4: A comparison of training loss for T5 with without grammar-forcing during training.
The effectiveness of performing AP extraction using an MLM compared with CLM is evaluated in Table 3. For the AP Grounding evaluation, we use top-1 accuracy (fail/succeed) for each test. We use 1000 unseen examples from each dataset. We observe that GPT-4o-mini performs reasonably well on both CW and GLTL, but struggles with identifying APs from the Navi dataset. The performance of each of the BERT models is quite impressive across each do- main. All three models both achieve almost 100% accuracy unseen in-domain examples, with BERT and RoBERTa maintaining high performance on the out-of-domain datasets as well.
4. Experimental Evaluation
We conducted our evaluation on machine with one NVIDIA RTX 4070 Ti Super GPU, Intel 19-14900KF 32 Core CPU, and 64GB of RAM. Our evaluation datasets in- clude Navigation (Wang et al., 2021), GLTL (Gopalan et al., 2018), and CW (MacGlashan et al., 2015). Some statistics on these datasets are given in the appendix A. We evalu- ate performing the AP grounding using the MLMs BERT, RoBERTa, and DiST Each AP grounding model was trained for epochs learning rate of le-5, We also eval- uate performing the grounded NL to TL translation. Each translation model was trained for 3 epochs at learning rate of 2c-5, We perform our evaluation of the translation models and end-to-end approaches using 1000 examples from each dataset. We first perform ablation studies to eval- uate the impact of each of the different parts of the GraFT
4.2. Grounded Translation Results
In Figure 5, we compare the accuracy of three T5 models with respect to training data quantity. We use the T5 check- point provided at the HuggingFace- hosth repository (Raffel et al., 2020) as the base for each model. We then trained two versions of this model accordance with the two frame-

---

Grammar-Foreed Translation of Natural Language to Temporal Logic using LLMS
CW
GLTL
NAVI
100
100
100
80
80
80
Accuracy (%)
60
60
60
40
40
40
20
NL2TL
20
NL2TL
20
NL2TL
T5
T5
T5
GraFT
GraFT
GraFT
0
100
200
300
400
500
100
200
300
400
500
100
200
300
400
500
Training Data Quantity (#)
Figure 5: Accuracy results of three T5-based translation models. The T5 framework a baseline evaluated with ground truth lifted NL specifications as input. GraFT and NL2TL are evaluated using their respective lifting approaches. Each translation model is trained with LR= 2e-5 for 3 training epochs.
Approach
Training Data
CW
GLTL
Navi (%)
(%)
(%)
NL2TL (Chen et al., 2023)
GLTL+Navi
60.2
44.0
55.3
GraFT (proposed)
GLTL+Navi
63.2
48.3
73.0
NL2TL (Chen et al., 2023)
CW+Navi
21.2
23.1
51.6
GraFT (proposed)
CW+Navi
58.8
41.1
73.1
NL.TTL (Chen et al., 2023)
CW+GLTL
63.0
45.3
14.6
GraFT (proposed)
CW+GLTL
70.0
56.2
21.2
Table 4: Performance comparison of different models for end-to-end translation. Here, fine-tuning performed with respect to two of the datasets, and evaluation is performed using all three datasets.
works using their respective grounded natural language and temporal logic pairs. The NL2TL and T5 both use standard cross-entropy loss, which we compare against our grammar- forcing method described 3.2. The bascline T5 model uses the ground-truth lifted natural language, contributing to its high accuracy. Our first observation that approach yields greater accuracy at each training data quantity, most notably with smaller quantities of training data. Our second observation is that the GraFT model never suffers reduc- tion accuracy as result of additional training data, while the control model suffers heavily, particularly in the CW evaluation. We believe that less gradient noise during train- ing allows GraFT continue learning with the introduction of unseen training data, while the control model may be- come confused when exposed to new sequence pairs. We observe that grammar-forcing improves accuracy by 0.9% 10%
are trained on datasets containing examples from each do- main, and we specify the models used for translating natural language (NL) to TL and for identifying atomic proposi- tions (APs) where applicable. GraFT outperforms all com- pared approaches, achieving an average accuracy of 99.6% across the datasets. NL2LTL and NL2Spec under-perform GraFT by at least 12.8% to 21 21.24% on CW. GLTL, and Navigation datasets, respectively. These approaches do not perform AP grounding and rely solely on CLMs for transla- tion. GraFT demonstrates ~5% improvement over NI.2TI. when the data quantity is 500. This gap closes slightly when the data quantity is 2000, excepting the Navi dataset, where GraFT demonstrates an improvement of 12.40%. We attribute GraFT's superior performance its training ap- proach, which enhances domain transferability over stan- dard T5 models finettuned with cross-entropy loss.
Additionally, NL2TL's use of GPT for AP grounding under- performs on the Navi dataset. We evaluate performance on out-of-distribution data in Table GraFT achieves higher aceuracy on all out-of-distribution tests, demonstrating av-
4.3. End-to-end results We present the end-to-end results of GraFT and other tempo- ral logic (TL) translation approaches in Table 2. All methods
8

---

Grammar-Foreed Translation of Natural Language to Temporal Logic using LLMS
erage improvements by 8.33% on GLTL+NAVI, 25.7% on CW+NAVI, and 8.16% CW+GLTI The notable benefit observed in the CW+NAVI evaluation is NL2TL's failure to learn the CW distribution despite its inclusion in the train- ing set. On the other hand, GraFT was able to learn this distribution more successfully. This shows the potential for generalization if a modest pre-training dataset for NL to TL translation is available in the target domain.
descriptions linear temporal logic templates: an ap- plication in the surgical robotic domain. Applied In- telligence, 53(22) 10. 10.100776104489-023-4448222 URL https: /tt.//diiiii org/10. 1007 04889-04---0000 02000-23--200 0488220.
November 2023, doi:
Boteanu, A., Howard, T., Arkin, J., and Kress-Gazi H. model for verifiable grounding and execution of complex natural language instructions. In 2016 IEEE/RSJ Inter- national Conference Intelligent Robots and Systems (IROS), pp. 2649-2654, 2016. doi: 10.1 10.1109/ROOS.0 20019 7759412.
5. Conclusion
In this paper, we present GraFT, a framework for natural language to temporal logic translation. We demonstrate that grammar-forced training improves generalization and reduces Nomain--pecinf training data requirements. We also apply MLMs more cheaply and accurately perform AP grounding prior to translation. The combination of problem-specific training approach and AP grounding with BERT results in more robust and generalized natural lan- guage to temporal logic translation framework that preserves NL AP segments from the original input to provide the NL- AP mapping required to interpret the TL expression. Future work in this area will include collecting and synthesizing diverse NL.TTL datasets to further evaluate the transferability of translation models.
Bottou, L., Curtis, F. E., and Nocedal, Optimization methods for large-scale machine learning, 2016.
Chen, Y., Gandhi, R., Zhang, Y., and Fan, C. N1201: Trans- forming natural languages to temporal logics using large language models. Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, 2023.
Cosler, M., Hahn, C., Mendoza, D., Schmitt, F., and Trippel, C. nl2spec: Interactively translating unstructured natural language tonbsp:temporal logics withnbsp:large language models. In Computer Aided Verification: 35th Interna- tional Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II, pp. 383-396, Berlin, Heidel- berg, 2023. Periingr--Verlgg. ISBN 978-3-031-3777 doi: 10. 10.10077978----33-3777-------1 URL https:// 0dd.:org/00..107797------------0
Acknowledgements
This material part sponsored by UF startup funds and The views and conclusions contained herein are those of the thors and should not be interpreted as necessarily represent- ing the official policies or endorsements, either expressed or implied, of DARPA or the U.S. Government.
DARPA under agreement number
Devlin, J., Chang, M.-.,, Lee, K., and Toutanova, K. Bert: Pre-training of deep bidirectional transformers for lan- guage understanding, 2019. URL https://axxxv org/ ht//abs/100 abs.1110..000.. 04805.
Impact Statement
Fuggitti, and Chakraborti, T. N12Itl a python package for converting natural language (nl) instruc- tions to linear temporal logic (Itl) formulas. In AAAI Conference Artificial Intelligence, 2023. URL attps://apl https://api.smmmaiiicccttt CorpusID:25972677 wwwantisscoolar.com org/
This paper presents work whose goal advance the field of Machine Learning. There are many potential societal consequences of our work, none which we feel must be specifically highlighted here.
Gopalan, N., Arumugam, D., Wong, L. L. S., and
References
Tellex, S. Sequence-to-sequuecee language grounding of non-markovian task specifications. Robotics: Sci- ence and Systems XIV, 2018. URL https://api. semanticscholse org/ Co.ppsIDD:4699000
Abdulla, P. A., Jonsson, B., Nilsson, M., and Saksena, M. A survey of regular model checking. In Gardner, P. and Yoshida, N. (eds.), CONCUR 2004 Concurrency Theory, pp. 35-48, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. ISBN
Hao, Y., Liu, Y., and Mou, L. Teacher forcing recovers reward functions for text generation, 2022.
Achiam, J. al. Gpt-4 technical report, report, 2024. URL http:: //laxiivorr//aaaai...eea
08774.
Hsiung, E., Mehta, H. Chu. J. Liu, X., Patel,
R. Tellex S., and Konidaris, G. D. Generaliz- ing to new domains by mapping natural language to lifted Itl. 2022 International Conference on
Bombieri, M., Meli, D., Dall' Alba, D., Rospocher, M., and Fiorini, P. Mapping natural language procedures

---

Grammar-Foreed Translation of Natural Language to Temporal Logic using LLMs
Robotics and Automation (ICRA), pp. 3624-3630, 2021. URL https:// sew...issssmtttccclol.ll... org/CorpusII:2333 233853447
text-to-text transformer. Journal of Machine Learning Research, 21(140):1-67, 2020. URL http:// /ttt:://mmlr. orggpapers/v21// 074 1144.htm...
Konur, S. A survey on temporal logics for specifying and verifying real-time systems. Frontiers of Computer Sci- ence, 7(3):770, 2013. doi: 10.1007/5111044-13-222999 URL URL.tttss://jounnae hep. com. en/ fcs/ /EN/ shttssssllee......mmmmmm..m
Raman, V., Lignos, C.,, Finucane, C., Lee, K., Marcus, M., and Kress-Gazit, H. Sorry dave, i'm afraid i can't do that: Explaining unachievable robot tasks using natural language, 06 2013.
Sanh, V., Debut, I.., Chaumond, J., and Wolf, T. Distil- bert, distilled version of bert: smaller, faster, cheaper and lighter, 2020. URL https: / www.a.ooioggoa...aeeee..o..ooooa / 1910. 01108.
Lewis, M., Liu, Y. Goyal, N., Ghazvininejad, M., Mo- hamed, A., Levy, O., Stoyanov, V., and Zettlemoyer, L.. seneeneeto-sequene pre-training for natural language generation, translation, and comprehen- sion, 2019. TRLpttts:///akke wwtp:/ii..rr//boo.o a1900 13461.
Bart: Denoising
Tellex S., Kollar, T., Dickerson, S., Walter, M. R., Banerjee, A. G., Teller, S., and Roy, N. Approaching the symbol grounding problem with probabilis- tic graphical models. Al Magazine, 32(4):64-76, Dec. 2011. doi: 10.1609/aimag..2224.3386 https://ojs aaai wwt.:aa.......maaiii.i.//// indexx... php/a http://aammaaaaneeaarrrarcea///a
Liu, J. X., Yang, Z., Idrees, I., Liang. S., Schornstein, B., Tellex, S., and Shah, A. Grounding complex natural language commands for temporal tasks in unseen envi- ronments, 2023. URL /ttpps:///aaxivi org/ abs/ 2302.1164
URL
Tellex, S., Gooalan, N., Kress-Gazit, H., and Ma- tuszek, C. Robots that use language. Annual Review of Control, Robotics, and Autonomous Systems, 3(Volume 3. 2020):25-55, 2020. ISSN 2573-5144. doi: https:/ddo.org/10..1146 mmnnev--oontrd-1101199477222222 htt
Liu, Y., Ott, M., Goyal, N., Du, J., Joshi, M., Chen, D., Levy, O., Lewis, M., Zettlemoyer, L., and Stoyanov, V. Roberta: robustly optimized bert pretraining approach, 2019. URL https::tp/:: // wwrxiv..rrrgr..o.o... /ttbs///90.... 11692.
MacGlashan, J., Babes- Vroman, M., desJardins, M., Littman, M. L., Muresan, S., Squire, S., Tellex, S., Aru- mugam, D., and Yang, L. Grounding english commands to reward functions. In Robotics: Science and Systems, 2015. URL https: / /api. http:/appp.a.a.iiieeeeeeeee org/CozpusID: 11:005115.
hamnul/eeveees.oooooootteeee///e 1146/ htt4://mmuerrrcootrrr-11111----0
Thistle, J. G. and Wonham, W. M. Control problems in a temporal logic framework. International Jour- nal of Control, 44(4):943 976, 1986. doi: 10.1080/
00207 URL https: http://oi..oo// org/10. 1080 1080 (1800002071786083330
Madsen, C., Vaidyanathan, P., Sadraddini, S., Vasile, C.-I,, DeLateur, N. A., Weiss, R., Densmore, D., and Belta, C. Metries for signal temporal logic formulae. In 2018 IEEE Conference on Decision and Control (CDC), pp. 1542-1547, 2018.
Wang. C., Ross, C., Kuo, Y.-L., Katz, B., and Barbu, A. Learning a natural-language to executable semantic parser for grounded robotics. In Kober, Ramos, and Tomlin, C. (eds.), Proceedings of the 2020 Conference on Robot Learning, volume 155 of Proceedings of Machine Learning Research, pp. 1706- 1616.1718..0 PMLR, 16-18 Nov 2021. URL https: http:htttt:://oeeeeeeeeeee http///ppceeee...ee///// mlr. p.ress/ v155 / htt////agg2ggggg html.
doi: N0.1109/CDDC22218886199999
Pan, J., Chou, G., and Berenson, D. Data- efficient learning of natural language to linear tem- poral logic translators for robot task specifica- tion. 2023 IEEE International Conference on Robotics and Automation (ICRA), pp. 11554-11561, 2023, URL https: wtw.aappssmmmaiiccclssssseee att/CorppsID:23550447
Xu, Y., Feng. J., and Miao, W. Learning from failures: Translation of natural language requirements into linear temporal logic with large language models. In 2024 IEEE 24th International Conference on Software Quality, Reliability and Security (QRS), pp. 204-215, 2024. doi: 10. 10.1109/QR56778 2024.00029,
Patel, R. Learning to ground language to tem-
poral logical form. 2019. URL https:
//api. wwwanticcchoolar................ htt.s/sccccoaa..oo/oopossss..s 207980435.
Zhang, J., Zhao, Y., Salch, M., and Liu, P. J. Pegasus: Pre-training with extracted gap-sentences for abstractive summarization, 2020. URL https: // //aa/vivvv////////////a////aaavv org/ abs/1912.08777
Raffel, C., Shazeer, N., Roberts, A., Lee, K., Narang, S., Matena, M., Zhou, Y., Li, W. and Liu, P. J. Ex- ploring the limits of transfer learning with a unified
10

---

Grammar-Foreed Translation of Natural Language to Temporal Logic using LLMs
Zhu, W. Big data linear temporal logic formulas. In 2021 IEEE 4th Advanced Information Management, Com- municates, Electronic and Automation Control Confer- ence (IMCEC), volume 4, pp. 544-547, 2021. doi: 10.1 1A110//MCCS111132222222 .9482668.

---

Grammar-Foreed Translation of Natural Language to Temporal Logic using LLMs
A. Appendix
In this appendix, we provide supplementary results, analysis, and justification for our approach. We first provide quantitative information about the NL-LTL corpora used our experiments in Section A.I. In Section A.2, we provide our LTL logits processing algorithm and discuss its usage during training and inference. In Section A.3 provide an ablation of lifting models with various AP quantities. Lastly, in Section A.4, we provide extended theoretical support for our claims made in Section 3.2.2
A.1. Corpus Statistics
In this section, present diversity metrics for each corpora used in experiments. Each corpus is roughly comparable in terms of linguistic diversity. We also note that the CW corpus contains significantly fewer unique grounded LTL expressions.
Domain
NL
# LTL
Vocab
Navi (Wang et al., 2021)
7,079
142
139
GLTL (Gopalan et al., 2018)
11,153
188
203
CW (MacGlashan al., 2015)
2,130
39
196
Table 5: Statistics of NL-TL corpora used in our training and evaluation. The # NL column gives the number of unique NL input sentences, the LTL column gives the number of unique TL. expressions, and # Vocab gives the total number of unique words.
A.2. Algorithm 1: LTL Logits Processor
In this section, we present the algorithm used for our grammar-forced translation approach. During translation, the state variable tracks the current state of an LTL parser. As the logits decoded by the model, zero-out invalid token predictions, almost identical to our approach used in grammar-forced training, shown in 3. The only difference is that during training, we use the ground-truth token labels to maintain the state of the translation. During inference, we instead maintain the state based on the model's 's own outputs.
Algorithm Temporal Logic Logits Processor
Input: Input IDs Scores S
state gr ammar. init_inttttet state()
for i in range(/) do if i >0 then
last.token = 1i-1
state. upaaee (last token) end if
legal.tokens granmar.get.vallddsst.....
mask [1 in range [
mask mask[]ega.tokenn
s [(i mask] = 00
end for
Output: Scores S
12

---

Grammar-Foreed Translation of Natural Language to Temporal Logic using LLMs
A.3. Lifting Ablations
We evaluate four off the best-performing lifting models on lifting sequences with more than atomic predicates. To obtain these sequences, we concatenated existing entries that did not share APs and re-labeled the newly conjoined AP dictionaries. The results demonstrate promising scalability in MLM-based approaches, while the LLMs performance suffers rapid decline as AP quantities increase.
Model
Objective
CW CW(%) (%)
GLTL (%)
Navi (%)
GPT-4
Causal
81.88
80.41
83.02
DistilBERT
Masked
94.20
91.75
99.99
RoBERTa
Masked
96.37
95.66
99.99
BERT
Masked
97.10
96.52
99.99
Table 6: AP grounding results for 6-10 APs (Range B).
Model
Objective
CW (%)
GLTL (%)
Navi (%)
GPT-4
Causal
70.34
69.80
72.24
DistiBBER
Masked
92.86
90.63
98.54
RoBERTa
Masked
95.13
94.67
99.73
BERT
Masked
95.78
96.44
99.91
Table 7: AP grounding results for 11-15 APs (Range C).
A.4. Extended Theoretical Basis for Grammar-constrainet Optimization
Here, we outline an argument for our claim that imposing grammar constraints (that are not violated by the distribution of training data) during training can improve the convergence rate of stochastic gradient descent (SGD). Concretely, Theorem A.4 shows that there is a variance term M that appears in the rate. We proceed by showing that if applics a mask over token sequences that necessarily do not appear the distribution, this variance term decreases to M M, hence reducing the constant factor the ( VN bound, indicating faster convergence in practice, particularly when N is small. This section relies heavily on Theorem A.4, and we recommend reviewing section 4.3 of (Bottou et al., 2016) for a detailed proof of convergence bounds on SGD in the context of a non-convex objective function with non-diminishing stepsize.
Claim A.4
Let z():x)) and (( (r) be the cross-entropy loss of an unconstrained and constrained language model, respectively. Suppose both losses are differentiable in 9 and have bounded gradients.
V gla) (0.))1 < E[I[V((0.)11
Theorem: SGD Convergence Bounds (Nonconvex, Diminishing Stepsize) (Bottou et al., 2016) :
ar E
2(E[(((:)] - lins) +
LM 1
Σ ak
M
VN
where L is smoothness constant, / 0 is parameter related to descent conditions, à 0 is stepsize parameter, and M is uniform bound on the second moment (or variance) of the stochastic gradients (see Assumption A.4).
Definition (Unconstrained Language Model):
(o(
Mof
(3)
where 20(x)) R/V| is the logit vector for all tokens the full vocabulary V.
13

---

Grammar-Foreed Translation of Natural Language to Temporal Logic using LLMS
Definition 2 (Grammar-Constraaned Language Model):
if E Vi, otherwise.
Mr
(4)
p/ (z, (x)))
(o o M,)(ax),
(5)
Definition (Cross-Entropy Loss at Iteration n)) Let [21, ........ .r) be sequence drawn from data distribution D. At iteration the model parameters are On. Then we define the cross-entropy loss for single sequence æ as
((nii))
log pe,, (xt I<I). Σ
When averaging over all sequences in the data distribution D, obtain the expected cross-entropy loss iteration
T
L(O,) = EE>=D(((Pniz)) = - ED
log pe, (xe x21i]=
Assumption 1 (Correct Grammar) øy occurs in the data for prefix Iec then #t V2 C V. Therefore, grammar- masking does not affect tokens that actually appear.
Assumption (Bounded Variance of SG Estimation)
There exist constants m, my 0 such that
[[o(0,))] S m + m. [V((0 where a se D,
(6)
Proof of Claim A.4 : Consider a parameter vector and random sample x ~ D. For the unconstrained model (3), we observe
ove(O, [0(x<))(o]]
0 < R
Vu EV
by contrast, in the grammar-constrained model (4), we can observe
Vv (0,z)
E
AA0 & Vz.
ZΦ [u]
Hence, coordinate-wirt wise,
Vela (0:x) < [+((0=))[o] A4.
Therefore,
|| (0: 2) = || 2
Taking expectation over x ~ and any internal sampling noise, we obtain
E(IVe(5) < [[]
Defining
M(y) = sup V [[IIVEL)
M sup B[IVE(()))] 0
see MG) M. Striet inequality Mgg M arises whenever there is at least one token that the grammar forbids but the unconstrained model might otherwise assign non-negligible probability to. Hence the grammar-constraine model has strictly smaller variance constant in the sense used in Theorem A.4. By Theorem A.4, the asymptotic SGD bound in the sewoonww/ddmmiiisiinnsstppppsspe
scenario on the order O (M/vN). Since M < M, replacing M by M yields righter constants in the finite-time and asymptotic terms. Thus, grammar- constrained optimization accelerates convergence by reducing stochastic gradient variance.
14


Reviews:
[{"review_id": "3NfktKR8r7", "reviewer": "Reviewer_72U5", "summary": "This paper introduces a framework for translating natural language to temporal logic by restricting output token space during both grounding and translation phases. The framework employs a masked language model for atomic propositions grounding and a fine-tuned sequence-to-sequence model for translation. Using a BERT+T5 combination, GraFT demonstrates significant improvements in both end-to-end translation accuracy and out-of-domain scenarios compared to existing methods. The paper provides mathematical justification for token restriction benefits and evaluates the framework on CW, GLTL, and Navigation benchmarks.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "**Before proceeding, please read our response addressed to all reviewers found in our rebuttal for reviewer JKCj.**\n\nQ1: The method for obtaining grounded NL sequences for T5 training lacks clear explanation. The paper fails to justify whether these grounded NL sequences are suitable as learning objectives for CLMs.\n\nA1: In GraFT, the grounded sentences are obtained by passing the original NL sentences to BERT, which provides a mapping between the AP labels and segments of the sentence. The BERT model must be fine-tuned on labeled data, which is provided in the LTL datasets (these datasets include information on the span of APs in the NL sentences). In the NL2TL framework, an LLM is prompted to generate the AP labels and segments within the sentence, rather than directly labeling the tokens of the input as is done by BERT. In response to the question of whether grounding NL sequences is suitable as a learning objective for CLMs, we present the tables below. The tables contain AP grounding results for 3 ranges of AP quantities (1-5 (A), 6-10 (B), and 11-15 (C)) for an MLM and an off-the-shelf CLM. Our position is that CLMs are *not* an optimal choice for this learning objective.\n\n(A)\t\n| Model       | Objective | CW (%) | GLTL (%) | Navi (%) |\n|-------------|-----------|--------|----------|----------|\n| GPT-4o-mini | Causal    | 97.76  | 95.84    | 83.97    |\n| GPT-4o      | Causal    | 95.02  | 93.53    | 86.08    |\n| GPT-4       | Causal    | 96.24  | 94.68    | 87.28    |\n| DistilBERT  | Masked    | 95.80  | 93.83    | 99.99    |\n| RoBERTa     | Masked    | 98.34|  96.96     | 99.99|\n| BERT \t| Masked | 98.58  | 97.35    | 99.99    |\n(B)\n\n| Model      | Objective | CW (%) | GLTL (%) | Navi (%) |\n|-------------|-----------|--------|----------|----------|\n| GPT-4      | Causal    | 81.88  | 80.41    | 83.02    |\n| DistilBERT | Masked    | 94.20  | 91.75    | 99.99    |\n| RoBERTa    | Masked    | 96.37  | 95.66    | 99.99    |\n| BERT       | Masked    | 97.10  | 96.52    | 99.99    |\n(C)\n\n| Model      | Objective | CW (%) | GLTL (%) | Navi (%) |\n|-------------|-----------|--------|----------|----------|\n| GPT-4      | Causal    | 70.34  | 69.80    | 72.24    |\n| DistilBERT | Masked    | 92.86  | 90.63    | 98.54    |\n| RoBERTa    | Masked    | 95.13  | 94.67    | 99.73    |\n| BERT       | Masked    | 95.78  | 96.44    | 99.91    |\n\n\nQ2: The difference in output formats between CLM and MLM for grounded NL (Figure 2) requires clarification - the paper should explain whether this stems from fundamental architectural differences between the two models\n\nA2: The fundamental difference is that BERT classifies each token in the input as PROP_ID or 0, where the PROP_ID class is an integer that corresponds to an AP that appears one or more times in the sentence, and the 0 class indicates that a token is not part of any AP. In contrast, a CLM is *generative* and predicts (the next) future token, rather than classifying the tokens it received as input. Our evaluation results for MLM vs CLM AP grounding (provided above) support our position that the MLM training objective is better suited to the task of AP grounding than the CLM objective. \n\nQ3: The baseline models used for comparison (from 2023) may be outdated. More recent baselines should be considered to strengthen the comparative analysis\n\nA3: In our supplemental evaluation results provided in our response to reviewer **n686**, we include recently trained models including GPT-4 and GPT-4o, trained in 2024. To our knowledge, our evaluation compares against the current state-of-the-art temporal logic translation frameworks.", "claims_and_evidence": "Yes.", "methods_and_evaluation_criteria": "Yes.", "theoretical_claims": "No.", "experimental_designs_or_analyses": "Yes. See **Weaknesses** and **Strengths** below.", "relation_to_broader_scientific_literature": "GraFT's token space restriction approach bridges general NLP techniques with formal language translation tasks.", "essential_references_not_discussed": "No.", "other_strengths_and_weaknesses": "**Weaknesses:**\n- The method for obtaining grounded NL sequences for T5 training lacks clear explanation. The paper fails to justify whether these grounded NL sequences are suitable as learning objectives for CLMs. \n- The difference in output formats between CLM and MLM for grounded NL (Figure 2) requires clarification - the paper should explain whether this stems from fundamental architectural differences between the two models\n\n\n\n**Strengths:**\n- Clear and well-structured writing with easy-to-follow organization\n- Innovation points are well-articulated\n- Results are presented clearly and comprehensively\n- Notable achievement in outperforming GPT-4o using only a BERT+T5 combination", "other_comments_or_suggestions": "N/A", "questions_for_authors": "**Questions:**\n\n- The baseline models used for comparison (from 2023) may be outdated. More recent baselines should be considered to strengthen the comparative analysis", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "1YA9x3Petp", "reviewer": "Reviewer_VmqZ", "summary": "The authors propose GraFT, an innovative framework that employs masks to ensure the syntax correctness of generated LTL programs. The approach first utilizes BERT to extract atomic propositions (APs) and map them into a predefined set of equivalent classes for co-references. Then, it leverages T5 to learn the translation step. GraFT improves end-to-end translation accuracy by 5.49% and out-of-domain translation accuracy by 14.06% on average across three benchmarks.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "**Before proceeding, please read our response addressed to all reviewers found in our rebuttal for reviewer JKCj.**\n\nQ1. Why is the vocabulary size for atomic propositions (APs) limited to only 6? If the narration spans an entire movie lasting over two hours, wouldn’t it require significantly more atomic propositions?\n\nA1. This limitation was introduced by the existing datasets rather than by the authors. We choose a prop id space of 6 tokens because the sentences in our dataset have a maximum of 5 APs. Each token that is not part of these is assigned the 0-class, and any tokens which are part of an AP are assigned an integer ID corresponding to which AP it is a part of. However, our proposed approach can certainly be extended to handle more than 5 APs. **Please see our response to reviewer 72U5, where we have provided results for up to 15 APs.** For any number of APs, our approach of performing grounding using an encoder only model outperforms using CLMs.\n\nWe would also like to point out that in the “2 hour long narration” example, it seems that the reviewer is referring to a *trace* with a large number of AP's, rather than a temporal logic expression. The difference being a *trace* is a time-ordered sequence of states over which some specification can be checked (the specification being a temporal logic expression). For example, we may specify in natural language that “The identity of the culprit is not revealed until the film is in the third act.”, and we may check that specification against a trace (i.e, extended document that holds the dialogue). Moreover, we believe that the 5 AP maximum observed in the dataset reflects the general expectation that the input NL sentences to our framework are roughly equivalent to a single human query, which typically do not contain hundreds of APs. \n\nQ2: How are the grounded nouns utilized in the LTL formula? Could you provide an example? \n\nA2: The grounded AP's represent the parts of the sentence which will serve as atomic predicates in the resulting TL expression. An example NL input may be: \"When the apple falls from the tree, pick it up and eventually put it in the basket.\" The grounding system would label every token in the input with the AP it relates to. For the purposes of this example I will just label the words rather than the true subword tokens used by BERT. The output sequence from BERT may look like: [0,1,1,1,1,1,1,0,2,2,2,0,0,3,3,3,3,3], and we construct a new sentence based on this sequence: \"When the prop_1, prop_2 and eventually prop_3.\" And we store the corresponding tokens in a dictionary: {prop_1: \"the apple falls from the tree\", prop_2: \"pick it up\", prop_3: \"put it in the basket\"}. The purpose of this is to simplify the NL prior to translation without sacrificing altogether the semantic nuance and complexity of the original natural language; the relevant segments are stored in a dictionary so they can be used downstream to determine their truth values.\n\nQ3: The dataset descriptions are insufficiently explained. Regarding the GW dataset, I could not find details on its context, size, input, and output in either the main text or the supplementary material.\n\nA3: We do not reference any GW dataset - Is this question perhaps about CW or GLTL? If so, there is a table in the appendix (A1) with information on the datasets. The table contains the number of unique NL sentences, number of unique LTL sentences, and the number of unique words that appear in each dataset.\n\nQ4: For data efficiency and accuracy results, it would be nice to compare against the NL2TL baseline.\n\nA4: We have performed the requested evaluation and the results can be viewed using the link (https://docs.google.com/document/d/e/2PACX-1vTYbY_0G_5EUXs1sumgRB7q3zz_3gCQRU0g8OCFXGFvxH2thZ2NqFNzxXWujADzOTj1uBICDQxRCcFi/pub). The results show that our approach outperforms NL2TL with even more margin than the T5 baseline. This stems from the fact that our method of grounding the APs is superior to the method in NL2TL. We had originally used T5 to isolate the improvement from the training.\n\nIn regard to the missing essential reference: This does appear to be an essential reference which we should include in our discussion of the background work. While the authors approach to pruning the space of target programs appears similar to our proposed approach (GraFT), there is a key difference relating to how we obtain the grammatical state (or as the authors describe it on page 7, the “current context”). In the author’s approach, the syntax checker functions the same during both training and inference, establishing the current context using previously generated tokens. However in GraFT, the syntactic validity of tokens at position t is dependent on the label at position t-1, rather than the generated token at position t-1, as would be used in the author’s proposed method.", "claims_and_evidence": "The authors list four contributions; however, they primarily describe the framework rather than explicitly stating the key contributions.", "methods_and_evaluation_criteria": "I have several questions regarding the methodology:  \n\n**Q1.** Why is the vocabulary size for atomic propositions (APs) limited to only 6? If the narration spans an entire movie lasting over two hours, wouldn’t it require significantly more atomic propositions?  \n\n**Q2.** How are the grounded nouns utilized in the **LTL** formula? Could you provide an example?  \n\n**Q3.** The dataset descriptions are insufficiently explained. Regarding the **GW** dataset, I could not find details on its context, size, input, and output in either the main text or the supplementary material.", "theoretical_claims": "I have check the algorithm and it makes sense.", "experimental_designs_or_analyses": "See Methods And Evaluation Criteria", "relation_to_broader_scientific_literature": "This work is highly relevant to the syntax-guided program synthesis community. In fact, the masking strategy used to ensure program syntax correctness has been around for quite some time. See Essential References Not Discussed for further reference.", "essential_references_not_discussed": "[1] Bunel, Rudy, et al. \"Leveraging grammar and reinforcement learning for neural program synthesis.\" arXiv preprint arXiv:1805.04276 (2018).\n\n[2] Netz, Lukas, Jan Reimer, and Bernhard Rumpe. \"Using grammar masking to ensure syntactic validity in llm-based modeling tasks.\" Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems. 2024.", "other_strengths_and_weaknesses": "My main concern with this work is how it differentiates itself from existing literature in the program synthesis community.", "other_comments_or_suggestions": "For data efficiency and accuracy results, it would be nice to compare against the NL2TL baseline.", "questions_for_authors": "See Methods And Evaluation Criteria, and Other Strengths And Weaknesses", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "7Ehw12d1N8", "reviewer": "Reviewer_n686", "summary": "This paper introduces Grammar-Forced Translation (GraFT), a framework to translate natural language (NL) into temporal logic (TL) using large language models (LLMs).", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "**Before proceeding, please read our response addressed to all reviewers found in our rebuttal for reviewer JKCj.**\n\nQ1: I think some implementation details (e.g., hyperparameter selection, number of runs per experiment) could be better documented to ensure reproducibility.\n\nA1: We have included training scripts for the models that should allow for our results to be reproduced. This was provided in the supplementary materials zip file. For the sake of clarity, we are happy to provide the exact hyperparameters used for training. BERT and T5 were both trained for 3 epochs with an LR of 2e-5. T5 was given |training data|/3 * 0.075 warm up steps. Identical hyperparameters were used for training T5 used in NL2TL and GraFT. \n\nQ2: I would like to see more empirical results with different LLM other than gpt4-o-mini. If the author can show this, I will raise my score.\n\nA2: We have performed an evaluation of NL2TL with GPT4o and GPT-4 as the grounding model, an end-to-end evaluation that uses GPT-4 as the grounding model, and an end-to-end evaluation of an T5 without an AP grounding model. These new results are presented below:\n\n**End-to-End Evaluation of NL2TL with more models (Updated with 4 new entries: ungrounded seq2seq trained on 500 and 2000 examples, NL2TL with GPT-4 each trained on 500 and 2000 examples):**\n\n| Approach           | Data Quantity | AP Grounding Model | Translation Model | CW    | GLTL  | Navi  |\n|--------------------|---------------|--------------------|-------------------|-------|-------|-------|\n| Ungrounded Seq2Seq | 500           | -                  | T5           | 59.60 | 46.80 | 43.40 |\n| NL2TL              | 500 | GPT-4o-mini | T5                              | 93.00 | 83.80 | 80.40 |\n| NL2TL              | 500           | GPT-4              | T5                | 91.50 | 82.60 | 83.70 |\n| GraFT              | 500           | BERT               | T5                | 97.70 | 91.50 | 85.00 |\n| Ungrounded Seq2Seq | 2000          | -                  | T5        | 68.10 | 55.90 | 56.30 |\n| NL2TL \t   | 2000              | GPT-4o-mini        | T5        | 98.20 | 97.40 | 86.70 |\n| NL2TL              | 2000          | GPT-4              | T5                | 96.70 | 96.20 | 90.00 |\n| GraFT              | 2000          | BERT               | T5                | 99.90 | 99.80 | 99.10 |\n\n\nQ3:How does it differ from top-k sampling?\n\nA3: In top-k sampling, we direct generation using the K highest scoring the tokens at each step. In Grammar-forced Training (GraFT), we first outright eliminate all of the grammatically incorrect tokens (based on the previous LABEL token, not previous PREDICTED token) before computing the loss. Likewise during inference with GraFT, we perform this same operation, but based on the previous predicted token, because of course labels are not available during evaluation. In top-k sampling, the model may still be informed by a list of tokens that includes grammatically invalid options. We eliminate that possibility altogether using grammar-forcing.\n\nQ4: The focus is primarily on improving accuracy rather than computational efficiency; it's unclear if GraFT introduces any additional computational overhead \n\nA4: Experimentally, we have observed that GraFT training requires 15-20% more time than ordinary training with T5. We will provide a figure that displays the computational overhead for GraFT vs T5 during training and inference, to be placed in the appendix of our final submission.\n\nQ6:The figures could be improved for better readability, particularly Figures 3 and 4\n\nA6: We can improve the readability by increasing the font size and reducing the presence of less-relevant details of the T5 architecture. These changes should bring the relevant details of our framework into focus. We will address these concerns in the final version of the paper- but we are unable to make changes to our submission PDF during the review period.", "claims_and_evidence": "The claims regarding the performance improvements and complexity reduction of GraFT are convincingly supported by empirical evidence.", "methods_and_evaluation_criteria": "Seems to make sense", "theoretical_claims": "I check the section 3.2.2, and it seems to make sense", "experimental_designs_or_analyses": "I think some implementation details (e.g., hyperparameter selection, number of runs per experiment) could be better documented to ensure reproducibility.", "relation_to_broader_scientific_literature": "The paper builds upon and extends prior work in NL-to-TL translation in several ways. The work connects to broader research on structured prediction, grammar-guided generation, and efficient fine-tuning of language models.", "essential_references_not_discussed": "n/a", "other_strengths_and_weaknesses": "1. The framework is conceptually simple yet effective, making it likely to be adopted by others\n2. The approach is data-efficient, performing well even with limited training examples\n\n3.The focus is primarily on improving accuracy rather than computational efficiency; it's unclear if GraFT introduces any additional computational overhead\n4.While the approach reduces the need for domain-specific training data, it still requires a modest amount of in-domain data for optimal performance\n\n\nI would like to see more empirical result with different LLM other than gpt4-o-mini. If the author can show this, I will raise my score.", "other_comments_or_suggestions": "The figures could be improved for better readability, particularly Figures 3 and 4", "questions_for_authors": "How does it differ from top-k sampling?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "8i31IeQ3HL", "reviewer": "Reviewer_JKCj", "summary": "The paper introduces Grammar Forced Translation (GraFT), a framework for translating natural language into temporal logic. GraFT simplifies the translation process by restricting the output tokens to a limited set, using the unique properties of each task and exploiting the known grammar of temporal logic during training and inference. This approach improves end-to-end translation accuracy and out-of-domain accuracy compared to state-of-the-art methods.\n\n## update after rebuttal\n\nI have no further comments and maintain the initial assessment of the paper.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "**Remarks for all reviewers:** We would like to thank all reviewers for their time and detailed feedback. With two weak accepts and two weak rejects (with one weak reject indicating that they would consider raising their score if provided additional experimental results), the paper is on the borderline to be accepted. In this overall response, we summarize the strengths of the paper and how we have addressed the reviewers' concerns.  \n\n1. **Writing and organization**: Clear and well-structured writing with easy-to-follow organization [72U5]\n2. **Ease of implementation**: The framework is conceptually simple yet effective, making it likely to be adopted by others [n686]\n3. **Advantage of Encoder only vs. CLM**: Notable achievement in outperforming GPT-4o using only a BERT+T5 combination [72U5, JKCj]\n4. **Limited number of APs during grounding** [VmqZ]: The AP grounding with BERT used a maximum of 5 APs per input sequence. To address this, we conducted an additional evaluation of BERT and GPT-4 on the AP grounding task (presented in our response to reviewer 72U5). Our new evaluation shows results on sequences with 6-10 APs and 11-15 APs, in addition to the original 1-5 AP examples used in the original evaluation. We believe that the original benchmarks only contained up to 5 APs, as humans typically struggle to reason about a larger number of entities simultaneously.\n5. **Limited number of CLMs are used in the evaluation** [n686]. Our original  experimental evaluation only compared with one state-of-the-art CLM, GPT-4o-mini. To address this limitation, we performed multiple additional evaluations. In particular, we conducted two evaluations of AP grounding using Gpt-4 and GPT-4o. In addition, we conducted an evaluation of end-to-end translation with NL2TL using Gpt-4 grounded inputs. The results of these evaluations are presented in our response to reviewer n686.\n6. **How does our work distinguish itself from existing work in the program synthesis community** [VmqZ, n686 ]: To the best of our knowledge, this is the first time that several of the concepts in our submission have been applied to NL-to-TL translation, which is a contribution itself. Moreover, we do not simply present an off the shelf implementation of existing techniques (i.e grammar constrained decoding). We contribute a novel approach to training seq2seq models for the NL-to-TL task, outlined in section 3.2. Lines 278-288 of our submission describes a key difference in our training approach when compared against existing grammar-based techniques. Additionally, the use of BERT for AP grounding appears to be an entirely novel application that yields significant benefits over the standard CLM-based approach.\n\n**Beginning of direct response to JKCj**:\n\nQ4: In Algorithm 1, how is the temporal logic grammar function (grammar.get_valid()) defined or implemented?\n\nA4: The grammar.get\\_valid(state) function takes the current parser state for the sequence, which is maintained per sequence and is updated when each new token is processed using the grammar.update\\_state(state, token\\_id) function, where state is the current state and token_id is the token that we've just parsed. The grammar state holds a list of tasks that need to be completed before parsing ends. When a \"(\" token is parsed, we push a \"(\" element to the state stack for the sequence. For example, the state of a sequence may be [\"formula\", \"(\", \"prop\"] and the token we are parsing is \"\\_\". When we call grammar.update\\_state(state, \"\\_\"), the new state is [\"formula\", \"(\", \"prop\\_\"]. Now we must parse the next token. We will call grammar.get\\_valid(state), which will return a set of valid token ID's {1, 2, 3, 4, 5}, because we know that \"prop_\" can only be followed by a digit 1-5 (based on our dataset; if we expected more props we would have increased this to include all potential prop IDs). The full implementation of our grammar is provided in the reproducibility zip file in /TIME/TemporalLogicGrammar.py.\n\nQ5: Can the approach be extended to handle time intervals as in NL2TL? \n\nA5:   Yes, this is absolutely possible. The only requirement for extending GraFT to other temporal logic formalism is the adaptation of the chosen formalism from terminal-based into token-based. We decided to limit the considered temporal logics to LTL in order to keep the paper more streamlined. However, we will consider extensions to time-bounded LTL and STL in our future work.\n\nAdditionally, we will address the minor typos pointed out in the comments and suggestions.", "claims_and_evidence": "Intuitively, the benefits of focusing on valid grammer states for a more focused gradient are readily apparent. The shortcomings of a Causal Language Modelling (CLM)-based approach in AP Grounding  with respect to a Masked Language Modeling (MLM)-based approach are sensible and results support the hypothesis.\n\nIn other literature, Temporal Logic (TL) describes a more general logic over time and subsumes Linear Temporal Logic (LTL). It is unclear how the logic operators defined in the Sec. 2.1 differ from standard LTL and the paper could replace all references to                               TL with LTL (or $\\texttt{LTL}_f$).", "methods_and_evaluation_criteria": "The datasets used are off-the-shelf and provided from previous work. Comparisons made for performance as well as performance on training with a limited subset of the data are reasonable and provide suitable evidence that GraFT is more data efficient and robust than other CLM-based models.", "theoretical_claims": "The theory provides an intuition to the effectiveness of grammar constraints and appears valid.", "experimental_designs_or_analyses": "Table 4 compares NL2TL with the proposed method (GraFT) which does not consider time intervals in the temporal logic. Are the comparisons fair given than NL2TL contains the added ability to handle these time intervals (as a part of Signal Temporal Logic)?", "relation_to_broader_scientific_literature": "The proposed method makes advances in generating Temporal Logic specs from Natural Language which can be used as a step in various pipelines that require a formal language as input [1, 2]. A high accuracy in this translation could generalize various methods to accepting natural language as input (and not just an expression in formal logic). The method does not consider grounding predicates in other modalities like vision/images [3].", "essential_references_not_discussed": "References using Temporal Logic:\n\n[1] Robust Counterexample-guided Optimization for Planning from Differentiable Temporal Logic, Dawson & Fan, IROS 2022\n\n[2] Co-learning Planning and Control Policies Constrained by Differentiable Logic Specifications, Xiong et al, ICRA 2024\n\n[3] Lang2LTL-2: Grounding Spatiotemporal Navigation Commands Using Large Language and Vision-Language Models, Liu et al, 2024", "other_strengths_and_weaknesses": "N/A", "other_comments_or_suggestions": "- The double quotes should be fixed for LaTeX e.g. P2L67C2 “go to the red room → Use `` instead of \"\n- Minor typos:\n    - P6L287C1 - “We know turn”", "questions_for_authors": "1. In Algorithm 1, how is the temporal logic grammar function (`grammar.get_valid()`) defined or implemented?\n2. Can the approach be extended to handle time intervals as in NL2TL?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: The paper proposes a framework for converting natural language to temporal logic specifications (such as LTL). This is achieved by restricting the output token space during grounding (where a masked language model is used) and a during translation (using a fine-tuned seq-to-seq model). Results demonstrate that the framework - a combination of BERT + T5 - outperforms existing baselines, including LLMs. 

Reviewers were generally positive about the paper, which provided theoretical intuition and a convincing set of experiments, outperforming more modern LLMs. The authors provided clear responses in their rebuttal, including clarification of finer details, context for the work within the program synthesis space, and additional experiments comparing to other large language models. These additions result in a stronger paper that is highly relevant to the community, and could see wide adoption due to its relative simplicity and excellent performance.
Decision: Accept (poster)