Grammar-Forced Translation of Natural Language to Temporal Logic using LLMs

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.

1. Writing and organization: Clear and well-structured writing with easy-to-follow organization [72U5]
2. Ease of implementation: The framework is conceptually simple yet effective, making it likely to be adopted by others [n686]
3. Advantage of Encoder only vs. CLM: Notable achievement in outperforming GPT-4o using only a BERT+T5 combination [72U5, JKCj]
4. 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.
5. 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.
6. 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.

Beginning of direct response to JKCj:

Q4: In Algorithm 1, how is the temporal logic grammar function (grammar.get_valid()) defined or implemented?

A4: 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.

Q5: Can the approach be extended to handle time intervals as in NL2TL?

A5: 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.

Additionally, we will address the minor typos pointed out in the comments and suggestions.

Before proceeding, please read our response addressed to all reviewers found in our rebuttal for reviewer JKCj.

Q1: I think some implementation details (e.g., hyperparameter selection, number of runs per experiment) could be better documented to ensure reproducibility.

A1: 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.

Q2: 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.

A2: 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:

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):

Q3:How does it differ from top-k sampling?

A3: 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.

Q4: The focus is primarily on improving accuracy rather than computational efficiency; it's unclear if GraFT introduces any additional computational overhead

A4: 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.

Q6:The figures could be improved for better readability, particularly Figures 3 and 4

A6: 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.

Before proceeding, please read our response addressed to all reviewers found in our rebuttal for reviewer JKCj.

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?

A1. 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.

We 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.

Q2: How are the grounded nouns utilized in the LTL formula? Could you provide an example?

A2: 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.

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.

A3: 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.

Q4: For data efficiency and accuracy results, it would be nice to compare against the NL2TL baseline.

A4: 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.

In 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.

Before proceeding, please read our response addressed to all reviewers found in our rebuttal for reviewer JKCj.

Q1: 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.

A1: 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.

(A)

Q2: 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

A2: 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.

Q3: The baseline models used for comparison (from 2023) may be outdated. More recent baselines should be considered to strengthen the comparative analysis

A3: 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.