Grounding Complex Natural Language Commands for Temporal Tasks in Unseen Environments
Authors: Jason Xinyu Liu
Ziyi Yang
Ifrah Idrees
Sam Liang
Benjamin Schornstein
Stefanie Tellex
Ankit Shah
Venue: CoRL 2023 Poster (2023)
Keywords: language grounding
temporal reasoning
robot navigation
formal methods

Abstract: Grounding navigational commands to linear temporal logic (LTL) leverages its unambiguous semantics for reasoning about long-horizon tasks and verifying the satisfaction of temporal constraints. Existing approaches require training data from the specific environment and landmarks that will be used in natural language to understand commands in those environments. We propose Lang2LTL, a modular system and a software package that leverages large language models (LLMs) to ground temporal navigational commands to LTL specifications in environments without prior language data. We comprehensively evaluate Lang2LTL for five well-defined generalization behaviors.
Lang2LTL demonstrates the state-of-the-art ability of a single model to ground navigational commands to diverse temporal specifications in 21 city-scaled environments. Finally, we demonstrate a physical robot using Lang2LTL can follow 52 semantically diverse navigational commands in two indoor environments.

Grounding Complex Natural Language Commands for Temporal Tasks in Unseen Environments
Jason Xinyu Liu"l, Ziyi Yang" Ifrah Idrees', Sam Liang", Benjamin Schornstein Stefanie Tellex', Ankit Shah
Department of Computer Science, Brown University, United States Department of Computer Science, Princeton University, United States
Abstract: Grounding navigational commands to linear temporal logic (LTL) leverages its unambiguous semantics for reasoning about long-horizon tasks and verifying the satisfaction of temporal constraints. Existing approaches require training data from the specific environment and landmarks that will be used natural language to understand commands those environments. We propose Lang2LTL, modular system and software package that leverages large language models (LLMs) ground temporal navigational commands LTL specifications environments without prior language data. We comprchensively evaluate Lang2LTL for five well-defined generalization behaviors. Lang2I.TL. demonstrates the state- of-the-art ability of a single model to ground navigational commands to diverse temporal specifications in 21 city-scaled env environments. Finally, we demonstrate a physical robot using Lang2LTL can follow 52 semantically diverse navigational commands in two indoor environments.
Keywords: language grounding, robot navigation, formal methods
Indoor Environments
York City
Visit the brown wooden desk least twice, acdition do woodan dook before the bookshel!
Fleane keep whittig the Boston Common and South Station
central Bridge
yooou
Figure 1: Lang2LTL. can ground complex navigational commands household and city-scaled environments without retraining.
Introduction
Natural language enables humans to express complex temporal tasks, like "Go the grocery store on Main Street at least twice, but only after the bank, and always avoid the First Street under construction." Such commands contain goal specifications and temporal constraints. A robot executing this command must identify the bank as its first subgoal, followed by two separate visits to the grocery store, and visiting First Street is prohibited throughout the task execution. Linear temporal logic [1] provides an unambiguous target representation for grounding a wide variety of temporal commands.
Prior work of grounding natural language commands LTL expressions for robotic tasks covered limited of LTT. formulas with short lengths and required retraining for every environment 3, 4, 5]. In contrast, some recent approaches proposed leveraging LLMs to directly generate robot
"Equal contribution 'Code, datasets and videos https: wwt.lll.itttuuiii.
7th Conference Robot Learning 2023), Atlanta, USA.

---

policies [6, 8,8, 9]. The LLM output is itself a formal language that must be interpreted by an external user-defined program. Such approaches cannot solve many complex temporal tasks considered in this work. Another advantage of using formal language like LTL is that existing work on automated planning with LTL specifications provides strong soundness guarantees.
In this paper, propose Lang2LTL, system capable of translating language commands to grounded LTL expressions that are compatible with range of planning and reinforcement learning tools [10, 11, 12, 13, 14]. Lang2LTL is modular system that separately tackles referring expression recognition, grounding these expressions to real-world landmarks, and translating a lifted version of the command to obtain the grounded LTL specification. This modular design allows Lang2LTL to transfer to novel environments without retraining, provided with a semantic map.
We formally define five generalization behaviors that learned language grounding model must exhibit and comprehensively evaluate Lang2LTL's generalization performance on novel dataset containing 2, 1.5 semantically unique LTL formulas corresponding to 47 LTL formula templates. Lang2LTL showed the sate-of-theeart capabilities of grounding navigational commands in 21 cities using semantic information from a map database a zero-shot fashion. Finally, we demonstrated that a physical robot equipped with Lang2LTL was able follow 52 semantically diverse language commands in two different indoor environments provided with semantic maps.
2 Preliminaries
Large Language Models: Autoregressive large language models (LLMs) are producing SoTA results on a variety of language-basee tasks due to their ceneral-purpons language modeling capa- bilities. LLMs are large-scale transformers [15] pretrained to predict the next token given context window [16, 17J. In this work, we used the GPT series models [18, 19] and the T5-Base model [20].
Temporal Task Specification: Linear temporal logic (LTL) [1] has been the formalism of choice for expressing temporal tasks for variety of applications, including planning and reinforcement learning [10, 21, 22, 11, 23, 14], specification elicitation [3, 24, 25, 26, 2], and assessment of robot actions [27]. The grammar of LTI. extends propositional logic with a set of temporal operators defined as follows:
3 : -i (P
V22
X
U 92
An LTL formula yp is interpreted over discrete-time trace of Boolean propositions, AP that maps environment state to Boolean value. (p, (f1, i22 any valid LTL formulas. The operators (not) and V (or) are identical to propositional logic operators. The temporal operator X (next) defines the property that Xpp holds if yp holds at the next time step. The binary operator U (until) specifies an ordering constraint between its two operands. The formula øo U y22 holds if y1 holds at least until ø2 first holds, which must happen at the current or a future time. In addition, we use the following abbreviated operators, A (and), (finally or eventually), and G (globally or always), that are derived from the base operators. Fyp specifies that the formula & must hold at least once in the future, while Gyp specifies that yp must always hold.
We developed Lang2I.TL based on a subset of specification patterns commonly occurring in robotics [28]. Appendix Table 4 lists the specification patterns and their interpretations.
Planning with Temporal Task Specification: Every LTL formula can be represented as a Büchi automaton [29, 30] thus providing sufficient memory states to track the task progress. The agent policy can be computed by any MDP planning algorithm on the product MDP of the automaton and the environment [10, 21, 22, 11, 12, 13]. Lang2LTL is compatible with any planning or reinforcement learning algorithm that accepts an LTL formula as task specification.
3 Related Work
language-guided guided robot task execution focused on using semantic parsers to ground language commands into abstract representations capable of
Natural Language Robotic Navigation: Early work of language-

---

informing robot actions [31, 32, 33, 34, 35]. Recent work leverages large pretrained models to directly generate task plans, either as code [7, 6] or through text [36, 9]. The LLM output is formal language that must be interpreted by an external procedure. Thus the external interpreters need to be expressive and competent for the success of these approaches. contrast, planners for LTL offer asymptotic guarantees on the soundness of the resulting robot policies. Finally, LM-Nav [8] is modular system that computes navigational policy by using LLM to parse landmarks from command, then vision-language model in conjunction with graph search algorithm to plan over pre-constructed semantic map. Note that LM-Nav can only ground commands of the Sequence Visit category as defined by Menghi et al. [28], while Lang2LTL can interpret 15 temporal tasks.
Translating Language Formal Specification: Prior approaches are tied to the domain they were trained on and require retraining with large amount of data to deploy in novel domain. Gopalan al. [3] relied commands paired with LTL formulas in a synthetic domain called Cleanlip World. Patel et al. [4] and Wang et al. [5] developed weakly supervised approach that requires natural language descriptions along with satisfying trajectory.
Leveraging LLM to facilitate translation into LTL is an emerging research direction [37, 38, 39, 40]. These approaches relied on string transformations to transform referring expressions in a command into propositions. In contrast, Lang2ITL. explicitly grounds the referring expression propositional concepts in the physical environment through grounding module.
The closest approach to ours, proposed by Berg et al. [2]. uses CopyNet [41] architecture to generate LTL formula structures followed by explicitly replacing the appropriate propositions. We demonstrate a significant performance improvement over Berg et al. [2]'s s approach by leveraging L.LMs as well as training and evaluating on a semantically diverse dataset.
4 Problem Definition
We frame the problem as users providing natural language command u to robotic system that performs navigational tasks in an environment M = (S, A, T",, where S and A represent the states and actions of the robot, and T describes the transition dynamics of the environment, Our proposed language grounding system, Lang2LTL, translates the language command to its equivalent LTL formula yp and grounds its propositions to real-world landmarks. We assume the robot has access to its state information S and semantic database of propositions D = {k= (z, f) structured as key-value pairs. The key & is a unique string identifier for each proposition, and æ contains semantic information about the landmark stored serialized format (e JSON). For example, in a street map domain, the semantic information includes landmark names, street addresses, amenities, etc. f:S - {0, 1} is Boolean valued function that evaluates the truth value of the proposition in given state Appendix B shows example entry of this semantic database. Finally, we assume that the robot has access to automated planner that accepts an LTT. formula and a semantic map as input and generates a plan over the semantic map as output. We used AP-MDP [12] for this paper.
Consider the example of drone following a given command within an urban environment depicted in Figure 2. The environment M encodes the position and the dynamics of the drone. The semantic database D = { (2, f)} includes the landmark identifiers, their semantic information, and proximity function.
5 Lang2LTL: Natural Language Grounding
Lang2LTL is a modular system that leverages LLMs to solve the grounding problem by solving the following subproblems,
1. Referring Expression Recognition: We identify the set of substrings, {ra), J. in the command u that refer to Boolean propositions. In this case, fra } { the store Main Street", "the bank").
3

---

Referring Expression Recognition
Referring Expression Grounding
Import
Refering Exprentions
RE Erinndinge
Erdosld
Thraet Vullust mistmorrt
Proest LLM
L
Coa Sinstarty
Fabert
chase L-B.))
lepa
AB Propociiion on and Symsul Maps Patance crase in
Cart
Lifted Translation
Uiad Farmuta
buyy sharilling
Faxm Ulb
eeeatt wwttunu dEaM
Figure 2: Lang2LTL system overview: Green blocks are pretrained or finetuned LLM models. Yellow blocks are the input or output of the system.
2. Referring Expression Grounding: Each referring expression is mapped to of the proposition identifier strings, k E ', which yields map (r: - k). Each proposition is also bijectively mapped to a placeholder symbol / from a fixed vocabulary 3 = {"AA, "B", ...} by {Ar ++ 3). In the example described above, the phrases "the store on Main Street" and "the bank" refer to the proposition identifiers walmart and chase, which are in turn mapped to the placeholder symbols "A" and "B".
3. Lifted Translation: After substituting the referring expressions {ri} by placeholder symbols 3 using the map frr - B}, we obtain the lifted utterance, "Go to A, but only after visiting B.". The lifted translation module then translates this lifted utterance into a lifted LTT. formula, Sp = (A) A (-AU B).
Finally, we substitute placeholder symbols "A" and "B" by grounded propositions walmart and chase using the bijection {k: (3) to construct the output L.T.. formula depicted in Figure 2.
We hypothesized that the benefit of solving the translation problem in the lifted domain is two-fold. First, the output vocabulary size is significantly reduced. Secondly, the lifted formula data can be sourced from multiple domains, thus providing access to a larger training dataset. Once accurately translated in the lifted domain, the formulas can be grounded to unseen landmarks in novel domains, a task at which LLMs excel. We examine the efficacy of this modularization in Section 6.
5.1 Referring Expression Recognition (RER)
Referring expressions are noun phrases, pronouns, and proper names that refer to some individual objects [42]. In this work, only consider the task of recognizing noun phrases and proper names. Referring expressions are entire substrings that refer to single entity, therefore, they are superset of named entities. For example, "the store on Main Street" is the referring expression, but it contains two named entities, "store" and "Main Street.
Referring expression recognition generally challenging to all existing pretrained name entity recognition models, especially without adequate examples for finetuning. We demonstrate high performance on the RER task by adapting the GPT-4 prompted with task description and examples to enable in-context learning. Details of the prompting approach are provided in Appendix D.
5.2 Referring Expression Grounding (REG)
Due to the diversity of natural language, a user can refer to landmark using many possible referring expressions. Grounding these expressions into the correct propositions is challenging. We propose using the embeddings computed by an LLM for measuring similarity. LLMs have been shown to map semantically similar texts to similar embedding values [43].
Let Gembed + R" represent the function that computes an n-dimensional embedding of a text string using the parameters of the LLM. Following Berg et al. [44], match the referring expressions {re} to the proposition tokens k's by matching their respective embeddings using cosine similarity.

---

The embedding of proposition token, k, is computed by encoding the semantic information, of its corresponding landmark, e.g., street name and amenity. This process is represented formally as follows,
gembed (r:) gembed (2)
k argmax [k:E) gembed (ri) gembed (z)l
(2)
5.3 Lifted Translation
Our lifted translation module operates with much smaller vocabulary than the number of landmarks within any given navigation domain. It can also be trained with navigational commands from wider variety of data sources. In designing our lifted translation module, we followed the Gopalan et al. [3] and Patel et al. [4] and represented the prediction target LTL. formulas the prefix format instead of infix format. This allows us to unambiguously parse the formulas without requiring parenthesis matching and shorten the output.
The lifted translation module accepts lifted utterance input and generates lifted LTL formula with an output vocabulary of up to 10 operators and five lifted propositions. We evaluated the following model classes for lifted translation. The implementation details are provided in Appendix
Finetumed LLM: We finetuned L.MSs using supervised learning following [16]. We tested two LLMs with supervised finetuning, namely, T5-Base (220M) [20] (using the Hugging Face Transformer library [45]. and the text-davinvi-003 version of GPT-3 using the OpenAI APL. The target was exact token-wise match of the ground-truth LTL. formula.
Prompt LLM: We evaluated prompting the pre-trained GPT-3 [18] and GPT-4 [19] models using the OpenAl API. We did not vary the prompts throughout given test set.
Seq2Seq Transformers: We trained an encoder-decoder model based on the transformer architecture [15] to optimize the per-token cross entropy loss with respect to the ground-truth LTL formula, together with a token embedding layer to transform the sequence of input tokens into sequence of high-dimensional vectors.
Evaluation of Language Grounding
We tested the performance of Lang2LTL towards five definitions of generalizing temporal command interpretation as informed by formal methods in Section 6.1. We evaluated the performance of each module described in Section in isolation in addition to demonstration of the integrated system. Lang2LTL achieved state-of-the-an performance in grounding diverse temporal commands in 21 novel OpenStreetMap regions [46].
6.1 Generalization in Temporal Command Understanding
Utilizing formal language, such LTL, to encode temporal task specifications allows us to formally define five types of generalizing behaviors.
Consider two utterances, 41 =" Go chase", and ut "Visst chase," describing the same temporal formula F chase. If the system has only seen #1 at training time, but correctly interprets u2 test time, it is said to demonstrate robustness to paraphrasing. This the most common test of generalization for robotics. A test-train split of the dataset is adequate for testing robustness to paraphrasing, and we refer to such test sets as ullerance holdout. Most prior works [3, 2, 40, 37, 5, 4] demonstrate robustness to paraphrasing.
Robustness Paraphrasing:
observe prior works following language commands
Robustness to Substitutions: Assume the system has been trained interpret the command corresponding chase, and G -walmart training time but has not been trained command corresponding to Fwalmart. If the system correctly interprets the command corresponding to
5

---

F Fwalmart, it is said to demonstrate robustness to substitution. To test for robustness to substitutions, any formula the test set must not have a semantically equivalent formula in the training set. [3] demonstrated limited robustness to substitutions. The lifted translation approach followed by Berg al. [2], NL2TL [40], and Lang2LTL demonstrates robustness to substitutions
Robustness to Vocabulary Shift: Assume the system has been trained to interpret commands corresponding to Fchase at training time but has never seen any command containing the propositions walmart. If the system correctly interprets F Fwalmart at test time, the system is said to be robust to vocabulary shift. To test for robustness to vocabulary shift, we identify the set of unique propositions occurring in every formula in the test and training set. The training set and test set vocabularies should have an empty intersection in addition to the non-equivalence of every test formula with respect the training formula. Methods that explicitly rely lifted representations show robustness to vocabulary shifts by design [44, 8, 40]. Our full system evaluations demonstrated robustness to novel vocabularies in Section 6.5.
Robustness to Unseen Formulas: Assume that all formulas the training set are transformed by substituting the propositions in pre-defined canonical order, e.g., both F chase, and F walmart are transformed to F a. We refer to these transformed formulas the formula skeleton. To test for robustness unseen formulas, the test set must not share any semantically equivalent formula skeleton with the training set. We used the built-in equivalency checker from the Spot LTL library [47].
Robustness to Unseen Template Instances: We define this as special case of robustness to unseen formulas. If all the formulas in the test and training set are derived from template- based generator using a library of pre-defined templates [28, 48], model may exhibit generalization to different semantically distinct formula skeletons of the same template; such a model displays robustness to unseen templates. We refer the test set whose skeletons vary only as instantiations of templates during training a formula holdout test set. If the unseen formulas in the test set do not correspond to any patterns, we refer to it as type holdout test set.
None of the prior works have evaluated proposed models for robustness to unseen formulas. We evaluated the lifted translation module of Lang2LTL on both formula and type holdout test sets. Lang2LTL experienced degradation of performance expected, indicating that robustness to unseen formulas is still open challenge.
Lifted Translation
Grounded Translation: OSM
10
1.0
Model
Frntused TSawe
Finetned pIT
hempt GFT4
0-6
Soutbe
0.85
0.2
0.2m
Uttorance
Formula Test Type
Type
Lang2CT.
Copyhet Model
Promett GPT44
(b)
Figure 3: Figure 3a depicts the average accuracies of six lifted translation models on the three holdout sets over five-fold volss-valiation. Figure 3b depicts the average accuracies of the grounded translation task in the OSM domain.
Table 2: Cross-Domain Evaluation. for Zero-Shot
Table Proposition Grounding Evaluation
OSM [44]
CleanUp [3]
Component
Accuracy
Lang2LTL
49.40 + 15.49%
78.28 + 1.73%
RE Recognition
98.01 2.08%
CopyNet [44]
45.91 + 12.70%
2.57%*
RE Grounding
98.20 + 2.30%
RNN-Att [3]
NA
95.51 + 0.11%

---

6.2 Lifted Dataset
We first collected a new parallel corpus of 1,156 natural language commands in English and L.TL formulas with propositional symbols to train and evaluate the lifted translation module. We included 15 LTL templates identified by Menghi et al. [28] and generated 47 unique lifted LTL formula templates by varying the number of propositions from
when applicable.
To improve the lifted translation module's Robustness to Substitutions, permuted the propositions in utterances and corresponding formulas. The lifted dataset after permutation contains 2,125 unique LTL formulas and 49,655 English utterances describing them. For detailed description of the dataset, please refer to Appendix H.
6.3 Grounded Dataset
Generating Diverse REs: We used GPT-4 paraphrase landmark names from an open-source map database, OpenStreetMap (OSM) [46], more diverse forms of referring expressions (REs) by providing the semantic information. The prompt used for generating diverse REs is in Appendix C.
We then substituted the symbols in the lifted dataset (Section 6.2) by diverse REs on 100 randomly sampled lifted utterances for each of the 21 OSM cities. For a list of example commands, please see Appendix Table 5.
6.4 Component-win wisse Evaluation
Proposition Grounding: We evaluated the RER and REG modules the grounded OSM dataset with 2,100 utterances across 21 cities. The average accuracy and the standard error across the cities for these modules are depicted in Table 1. The accuracy of RER decreased slightly, and REG performed uniformly well as we varied the complexity commands and REs, respectively (Appendix Figure 6).
Lifted Translation: We evaluated the six models presented in Section 5.3 for lifted translation through five-fold cross-validation ufterance, formula and type holdout tests. Figure 3a depicts the average accuracy and the standard deviation across the folds. We note that the two finetuned LLM models demonstrate the best performance on utterance holdout. We also noted degradation of performance on formula and type holdout tests, with the latter being the most challenging across all models. Finetuned LLM models suffered the worst degradation of performance. Finally, the addition of type-constrained decoding to T5 significantly improved its performance on the more challenging formula and type holdout. Due the lower cost of inference, and the ability to implement type-constrained decoding to prevent syntax errors, chose the finetuned T5 model for lifted translation in our full-system evaluation.
6.5 System Evaluation
We compared the translation accuracy of the full Lang2LTL system on the grounded datasets with the CopyNet- based translation model [2] and Prompt GPT-4. We retrained CopyNet with an identical data budget as the Lang2LTL lifted translation model. For Prompt GPT-4, we ensured that there was least one example from each formula skeleton in the dataset included in the prompt. Figure 3b depicts Lang2LTL outperforming both the basclines by significant margin. Note that due to the high cost of inference, Prompt GPT-4 was only evaluated on smaller subset of the test set.
6.6 Cross-Domain Evaluation
We further tested the zero-shot generalization capability of Lang2LTL on two different crowd-sourced datasets from prior work; the Cleanup World [3] on an analog indoor environment; and the OSM dataset [2] collected via Amazon Mechanical Turk. Table 2 shows the translation accuracies of Lang2LTL without any fine-tuning on the target datasets. Note that Lang2LTL outperforms CopyNet results reported by Berg et al. [2]. We further note that the CleanUp World dataset contains 6 unique
7

---

formula skeletons, out of which some were not a part of our lifted dataset. The degraded performance expected when the model needs to generalize to unseen formulas.
7 Robot Demonstration
To demonstrate Lang2LTIL's ability to directly execute language commands by interfacing with automated planning algorithms, we deployed a quadruped module robot, Spot [49] with the AP- MDP planner [12] in two novel indoor environments. Each environment had eight landmarks (e.g.. bookshelf, desks, couches, elevators, tables, etc.). We ensured that each environment had multiple objects of the same type but different attributes. We used Spot's GraphNay framework to compute semantic map of the environment. The AP-MDP [12] planner can directly plan over this semantic map, given an LTL task specification. Please refer to Appendix J for complete description of the task environments.
As proof-of-concepl we further finetuned the lifted translation module on 120,000 lifted utterances and formulas formed by sampling pairwise compositions from the lifted database and composed using conjunctions and disjunctions.
We compared Lang2LTL to Code-as-Policee (CaP) [6]. a prominent example of directly grounding language instructions to robot plans expressed as Python code. We provided aoliics-Po with interface functions to input the semantic map and a helper function to automatically navigate between nodes while having the ability to avoid certain regions. Thus CaP had access actions at much higher level of abstraction than system. Note that AP-MDP only interfaced with primitive actions defined as movement between any two neighboring nodes.
Lang2LTL was able to correctly ground 52 commands (40 satisfiable and 12 unsatisfiable commands). The failure cases were due to incorrect lifted translations. The formal guarantees of the AP-MDP planner assured that the robot execution was aborted when facing an unsatisfiable specification. By contrast, CaP only able generate acceptable executions for 23 of 52 commands and did explicitly recognize the unsatisfiable commands. CaP demonstrated more robustness to paraphrasing than our system, which failed on some compositional patterns not in the augmented lifted dataset.
8 Limitations
We observed that Lang2LTL fails at grounding language commands with certain utterance structures, which suggests that the lifted translation model overfits some training utterances. A list of incorrect groundings shown Appendix Table and Table 3. Finetuning models with larger capacities, e.g., T5-Large, may help. In this work, we only consider the task of recognizing noun phrases and proper names as referring expressions, not pronouns. We can tackle the coreference resolution problem by first prompting an LLM using an off- the-the-shelf model map pronouns to their corresponding noun phrases proper names before the RER module. If there are multiple landmarks of the same semantic features present in the environment, e.g., two Starbucks, Lang2LTL cannot distinguish the two and selects one at random. To resolve this ambiguity, the robot needs to actively query the human user via dialog when necessary.
Conclusion
We propose Lang2LTL, a modular system using large language models to ground complex navi- gational commands for temporal tasks in novel environments of household and city scale without retraining and generalization tests for language grounding systems. Lang2I.TI. achieves grounding accuracy of 81.83% 21 unseen cities and outperforms the previous SoTA and end-to-end prompt GPT-4 baseline. Any robotic system equipped with position- capability and semantic map with landmarks labeled with free-form text utilize Lang2LTL to interpret natural language from human users without additional training.

---

Acknowledgments
The authors would like to thank Charles Lovering for his feedback that helped improve the draft, Peilin Yu and Mingxi Jia for helping edit the videos, and Alyssa Sun for developing the web demonstration. This work is supported by ONR under grant numbers 1:0014-22-1-2992 and N00014-21-1-2584 AFOSR under grant number 1-9550-21-1-02111 NSF under grant number CNS-2038897, and with support from Echo Labs and Amazon Robotics.
References
[1] A. Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (sfes 1977), pages 46-57. icec, 1977.
[2] M. Berg, D. Bayazit, R. Mathew, A. Rotter-Aboyoun, E. Pavlick, and S. Tellex. Grounding Language to Landmarks in Arbitrary Outdoor Environments. In IEEE International Conference on Robotics and Automation (ICRA), 2020.
[3] N. Gopalan, D. Arumugam, L.. Wong, and S. Tellex. Sequence-to-Sequee Language Ground- ing of Non-Markovian Task Specifications. In Proceedings of Robotics: Science and Systems, Pittsburgh, Pennsylvania, 2018. doi:10.15607/RSS 2018.XIV.067.
[4] R. Patel, Pavlick, and S. Tellex. Grounding language to non-markovian tasks with no supervision task specifications. Robolics: Science and Systems, 2020.
[5] C. Wang. C. Ross, Y.-L. Kuo, B. Katz, and A. Barbu. Learning a natural-language to Itl executable semantic parser for grounded robotics. In Conference on Robot Learning, pages 1706-1718, PMLR, 2021.
[6] Liang, Huang, Xia, P. Xu, K. Hausman, B. Ichter, Florence, and A. Zeng. Code as policies: Language model programs for embodied control. In arXiv preprint urXiv:2209.07553, 2022.
[7] Singh, V. Blukis, A. Mousavian, A. Goyal, D. Xu, J. Tremblay, D. Fox, J. Thomason, and A. Garg. Progprompt: Generating situated robot task plans using large language models. arXiv preprint arXiv:2209. 11302 2022.
[8] D. Shah, Osiński, S. Levine, al. Lm-nav: Robotic navigation with large pre-trained models of language, vision, and action. In Conference on Robot Learning, pages 492-504. PMLR, 2022.
[9] S. S. Raman, V. Cohen, E. Rosen, I. Idrees, D. Paulius, and S. Tellex. Planning with large language models via corrective re-prompting. arXiv preprint arXiv:2211.09955 2022.
[10] M. L. Littman, U. Topeu, Fu, C. Isbell, M. Wen, and J. MacGlashan, Environment-indepeedee. task specifications via glti, arXiv preprint arXiv: 7704.034444 2017.
[11] A. Camacho, R. T. Icarte, T. Q. Klassen, R. A. Valenzano, and S. A. Mellraith. Ltl and beyond: Formal languages for reward function specification reinforcement learning. In IJCAI, volume 19, pages 6065-6075 2019.
[12] Y. Oh, Patel, Nguyen, B. Huang, Pavlick, and S. Tellex. Planning with State Abstractions for Mon-Markovian Task Specifications. In Proceedings of Robotics: Science and Systems, Freiburg, Germany, June 2019.
[13] R. T. Icarte, T. Q. Klassen, Valenzano, and S. A. Mcllraith. Reward machines: Exploiting reward function structure in reinforcement learning. Journal Artificial Intelligence Research, 2022.
[14] X. Liu, A. Shah, E. Rosen, M. Jia, G. Konidaris, and S. Tellex. Skill transfer for temporally- extended task specifications. arXiv preprint 220.:2206.000900 2022.

---

[15] A. Vaswani, N. Shazeer, N. Parmar, J. Uszkoreit, L. Jones, A. N. Gomez, L. Kaiser, and
I. Polosukhin. Attention is all you need, Advances in neural information processing systems, 30, 2017.
[16] A. Radford, K. Narasimhan, T. Salimans, I. Sutskever, et al. Improving language understanding by generative pre-training. 2018.
[17] A. Radford, J. Wu, R. Child, D. Luan, D. Amodei, I. Sutskever, al. Language models are unsupervised multitask learners. OpenAl blog, 1(8):9, 2019.
[18] T. Brown, B. Mann, N. Ryder, M. Subbiah, D. Kaplan, P. Dhariwal, Neelakantan, P. Shyam, G. Sastry, A. Askell, S. Agarwal, A. Herhert- Voss,, G. Krueger, T. Henighan, R. Child, A. Ramesh, D. Ziegler, J. Wu, C. Winter, C. Hesse, M. Chen, E. Sigler, M. Litwin, S. Gray, B. Chess, J. Clark, C. Berner, S. McCandlish, A. Radford, I. Sutskever, and D. Amodei. Lan- guage models are few-shot learners. In H. Larochelle, M. Ranzato, R. Hadsell, M. Balcan, and H. Lin, editors, Advances in Neural Information Processing Systems, volume 33, pages 1877- 1901. Curran Associates, Inc., 2020, URL https::/ neurips. cc/paper- .pf.
file files/ http:///.....e.eeeeee//.eee66ee.
[19] OpenAI. Gpt-4 technical report, 2023.
[20] C. Raffel, N. Shazeer, A. Roberts, K. Lee, S. Narang, M. Matena, Zhou, W. Li, and J. Liu. Exploring the limits transfer learning with unified text-to-text transformer. Journal of Machine Learning Research, 21(140): 2020. URL http://ttmmm /tttp://jmmrreee http://jjnooooo//peeeeeee org/papers/v2// 20-074. html.
[21] R. T. Icarte, T. Klassen, R. Valenzano, and S. Mcllraith. Using reward machines for high-level task specification and decomposition in reinforcement learning. In International Conference on Machine Learning, pages 2107-2116. PMLR, 2018.
[22] G. De Giacomo, L. Iocchi, M. Favorito, and F. Patrizi. Foundations for restraining bolts: Rein- forcement learning with ltlf/ldlf restraining specifications. In Proceedings of the international conference on automated planning and scheduling, volume 29, pages 128-136, 2019.
[23] A. Shah, Li, and J. Shah. Planning with uncertain specifications (puns). IEEE Robotics and Automation Letters, 5(2):3414 2020.
[24] A. Shah, Kamath, A. Shah, and S. Li. Bayesian inference of temporal task specifications from demonstrations. Advances Neural Information Processing Systems, 31, 2018.
[25] M. Vazquez-Chanlatte Jha, A. Tiwari, M. K. Ho. and S. Seshia. Learning task specifications from demonstrations. In Advances in Neural Information Processing Systems 31, pages 5368-
5378. 2018.
[26] J. Kim, C. Muise, A. Shah, S. Agarwal, and J. Shah. Bayesian inference of linear temporal logic specifications for contrastive explanations. In IJCAI, 2019.
[27] A. Shah, S. Wadhwania, and J. Shah. Interactive robot training for non-markov tasks. arXiv preprint arXiv:2003.00233. 2020.
[28] C. Menghi, C. Tsigkanos, P. Pelliccione, C. Ghezzi, and T. Berger. Specification patterns for robotic missions. IEEE Transactions on Software Engineering, 47(10):228-223 -2244, oct 2021. ISSN 1939-3520. 100/:S0.109// 29445999.
[29] M. Y. Vardi. An automata-theoretic approach to linear temporal logic. Logics for concurrency, pages 238-266. 1996.
[30] R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Protocol Specification, Testing and Verification XV: Proceedings of the Fifteenth IFIP WG6. I International Symposium Protocol Specification, Testing and Verification, Warsaw, Poland, June 1995, pages 3-18. Springer, 1996.
10

---

[31] M. Macmahon. Marco: A modular architecture for following route instructions. AAAI Workshop Technical Report, 01 2005.
[32] M. MacMahon, B. Stankiewicz, and B. Kuipers. Walk the talk: Connecting language, knowledge, and action in route instructions. In Proceedings of the 21st National Conference Artificial Intelligence Volume 2, AAAI'66, page 1475-1482. AAAI Press, 2006. ISBN 9781577352815.
[33] D. Chen and Mooney. Learning to interpret natural language navigation instructions from observations. In Proceedings of the Twenty-Fifth AAAI Conference on Artificial Intelligence, AAAI 11, page 559-865.420 AAAI Press, 2011.
[34] J. Kim and R. Mooney. Unsupervised PCFG induction for grounded language learning with highly ambiguous supervision. Proceedings of the 2012 Joint Conference on Empirical Methods in Natural Language Processing and Computational Natural Language Learning, pages 433 444, Jeju Island, Korea, July 2012. Association for Computational Linguistics. URL https: acl anthology org/D12-1040.
[35] Y. Artzi and I.. Zettlemoyer. Weakly supervised learning of semantic parsers for mapping instructions actions. Transactions of the Association for Computational Linguistics, 1:49-62, 2013. doi: 11..1162/aacc.... a 00209. URL https: pttttp:://acaanntolllso
org//13-11 1005.
[36] M. Ahn, A. Brohan, N. Brown, Y. Chebotar, O. Cortes, B. David, C. Finn, K. Gopalakrishnan, K. Hausman, A. Herzog, et al. Do as can, not as say: Grounding language in robotic affordances. arXiv preprint arXiv:2244006691, 2022.
[37] J. Pan, G. Chou, and D. Berenson. Data-efficient learning of natural language to linear temporal logic translators for robot task specification. arXiv preprint arXiv:2303. 2023.
[38] M. Cosler, C. Hahn, D. Mendoza, F. Schmitt, and C. Trippel. nl2spec: Interactively translating unstructured natural language to temporal logics with large language models. arXiv preprint arXiv:2303.04864 2023.
[39] Fuggitti and T. Chakraborti. NL2LTL python package for converting natural language (NL) instructions linear temporal logic (LTL) formulas. In AAAI, 2023. System Demonstration.
[40] Y. Chen, R. Gandhi, Zhang, and C. Fan. N12tl: Transforming natural languages to temporal logics using large language models. arXiv preprint arXiv:2305.07766, 2023.
[41] J. Gu, Z. Lu. H. Li, and V. O. Li. Incorporating copying mechanism in sequence-to- sequence learning. In Proceedings of the 54th Annual Meeting of the Association for Computationnl Linguistics (Volume 1: Long Papers), pages 1631-1640, Berlin, Germany, Aug. 2016. Association for Computational Linguistics. 1oi:10.18653/v 16531/1111111111154 URL tttps://aalantholege. org/P16-
[42] J. Lyons. Semantics: Volume 2, volume 2. Cambridge university press, 1977.
[43] A. Neelakantan, T. Xu, R. Puri, A. Radford, M. Han, Tworek, Q. Yuan, N. Tezak, J. W. Kim, C. Hallacy, et al. Text and code embeddings by contrastive pre-training, arXiv preprint arXiv:2201. 10005, 2022.
[44] M. Berg, D. Bayazit, Mathew, Rotter-Aboyoun, E. Pavlick, and Tellex. Grounding Language to Landmarks in Arbitrary Outdoor Environments. In IEEE International Conference on Robotics and Automation (ICRA), 2020.
[45] T. Wolf, L. Debut, V. Sanh, J. Chaumond,
C. Delangue, A. Moi, P. Cistac, T. Rault, R. Louf, M. Funtowicz, J. Davison, S. Shleifer, von Platen, C. Ma, Jernite, J. Plu, C. Xu, T. Scao, S. Gugger, M. Drame, Q. Lhoest, and A. M. Rush. Transformers: State-of-the-art natural language processing. In Proceedings of the 2020 Conference Empirical Methods in Natural Language Processing: System Demonstrations, pages 38-45, Online, Oct. 2020.

---

Association for Computational Linguistics. URL https::/ww..acle aclweb...wbbb...... www.aw.......anooooo.o.oooooo org/anthology/ 2020. emnlp-demos.c
[46] OpenStreenMap contributors. Planet dump retrieved from http::/planne..sm.orgg https:
/www: www.oppensteetm.p.... org, 2017.
[47] A. Duret-Lutz, E. Renault, M. Colange, F. Renkin, A. Aisse, Schlehuber-Caiis Medioni, A. Martin, Dubois, C. Gillard, and H. Lauko. From Spot 2.0 Spot 20: What's new? In Proceedings of the 34th International Conference on Computer Aided Verifica- tion (CAV'22), volume 13372 of Lecture Notes in Computer Science, pages 174-187. Springer, Aug. 2022. doi: N00:1001007/988 3-001-13188-22
[48] M. B. Dwyer, G. Avrunin, and C. Corbett. Patterns in property specifications for finite-state verification. In Proceedings the 2t international conference on Software engineering, pages 111-420, 1999.
[49] Boston Dynamies. Spot@ the agile mobile robot. https///www.betttoymmmcc....com products/spot.
12

---

Appendix A Specification Patterns
We developed Lang2LTL to ground navigational commands to LTL formulas. We started with the catalog of robotic mission-relevant LTL patterns for robotic missions by Menghi et al. [28]. We adopted 15 templates that are relevant to robot navigation and modified some of their patterns to semantically match our requirements. The complete list of pattern descriptions and the corresponding LTL templates is in Table 4. Note that we use some additional abbreviated temporal operators, specifically "Weak until" W, and the "Strong release" M in terms of standard operators, i.c.,
W b a U (b V Ga), and a M b = b U (a A b).
Appendix B Semantic Information from OpenStreetMap Database
We show example entry of the semantic dataset as follows.
Jiaho supermarket": { housenubuussss "692",
"shop": "supermarket", "opening_hours": "Mo-Su 08:00- 08:00-20:00", "phone": "6173389788",
"addr: "addr:postcode" "02111", "atdr:street": "Washington Street"
},
Appendix C Implementation Details about Referring Expression Generation
We prompt the GPT-4 model for paraphrasing landmarks with corresponding OSM databases. For each landmark, three referring expressions generated. The prompt for generating referring expressions by paraphrasing is as follows.
13

---

Use natural language to describe the landmark provided in python dictionary form in a short phrase.
Landmark dictionary:
Fortuna Cafe": { h'addr.housenumbrr::: "711', 'cuisine"; 'chinese', 'amenity": 'restaurant', "addr:city":
'Seattle', 'addr:poscoode:: "98104', 'source": 'King County GiS,data.scattle.oor 'addr:tteett:
'South King Street' }
Natural language:
Chinese cafe on South King Street
Landmark dictionary:
'Seoul Tofu House & Korean BBQ': ('addrrhousemumber"" '516', 'cuisine': 'korean',
"amenity": 'restaurant', "addr:city": "Seattle", 'addr:postcode": '98104', "source': 'King
County "lS,data.seattle.oo// 'addr:street': '6th Avenue South')
Natural language:
Scoul Tofu House
Landmark dictionary:
'II Video': { ''shop'''electroniicss
"electronics') }
Natural language:
AI Video selling electronics
Landmark dictionary:
"Dochi": { ('addr.housenumber': '604', "cuisine": "donut,, 'amenity': 'cafe') }
Natural language:
cafe selling donut named Dochi
Landmark dictionary:
AVA Theater District': ("addr.housenumber'. '45', "building": 'residential', 'building:levels:: '30")
Natural language:
AVA residential building
Landmark dictionary:
'HI Boston': : ("operator': 'Hosteling International', 'smoking': 'no", 'wheelchair': 'yes", 'tourism':
'hostel'}
Natural language:
HI Boston
Landmark dictionary:
Appendix D Implementation Details about Referring Expression Recognition
The prompt for referring expression recognition is as follows,
14

---

Your task is to repeat exact strings from the given utterance which possibly refer to certain propositions.
Utterance:
move to red room Propositions: red room
Utterance: visit Cutler Majestic Theater Propositions: Cutler Majestic Theater
Utterance: robot e move to big red room and then move to green area Propositions: big red room green area
Utterance: you have visit Panera Bread Beacon Street, four more than four times
Propositions: Panera Bread on Beacon Street
Utterance: go to Cutler Majestic Theater at Emerson College on Tremont Street, exactly
three times
Propositions: Cutler Majestic Theater at Emerson College on Tremont Street
Utterance: make sure you never visit St. James Church, Christian place of worship on Harrison Avenue, Dunkin' Donuts, Thai restaurant Montien, New Saigon Sandwich, Stuart St Tremont St
Propositions: St. James Church, a Christian place worship on Harrison Avenue Dunkin' Donuts Thai restaurant Montien New Saigon Sandwich Stuart St @ Tremont St
Utterance: move the robot through yellow region
small red room and then to large green
room
Propositions: yellow region| small red room
large green room
Utterance:
The results using this prompt to recognize referring expressions with spatial relations are shown in Table
Appendix E
Implementation Details about Lifted Translation
E.1 Fintuned T5-Base
For finetuning the T5-Base model, set the batch size to 40, the learning rate to 10-4, and the weight decay to 10-2 We ran training for 10 epochs and picked the best-performing one for reporting results.
E.2 Finetuned GPT-3
The per specification type accuracies and the accuracies for varying number of propositions in the formula while testing the finetuned GPT-3 model on the utterance holdout is depicted in Figure The finetuned GPT-3 model achieves high accuracies across formula types and varying numbers of propositions. It shows the benefit of having a large high-quality dataset of natural language commands representing diverse LTL formulas. All previous works also used utterance holdout their testing methodology, but their training and test sets contain significantly fewer unique LTL formulas.
15

---

E.3
Prompt GPT-4
The prompt for end-to-end GPT-4 is as follows,
Your task translate English utterances into linear temporal logic (LTLL) formulas.
Utterance: visit b LTL: F.b
Utterance: eventually reach and LTL: & F F
Utterance: go to h a and b
LTL: & Fh Fab
Utterance: proceed to reach h at the next time instant only and only if you see b LTL: b
Utterance: wait b till you see LTL: U h
Utterance: to h in the very next time instant whenever you see b LTL: Gib h
Utterance:
E.4
Prompt GPT-3
The prompt for end-to-end GPT-3 is the same as the one we used for Prompt GPT-4.
E.5 Seq2Seq Transformer
We constructed and trained transformer model following [15]. More specifically, built the model's s encoder with three attention layers and decoder with three layers, and used 512 the embedding size and 8 as the number of attention heads. For training, adapted batched training with batch size equal to 128, learning rate equal to 10 and dropout ratio equal to 0.1; the training process runs for 10 epochs, and we picked the best-performing checkpoint for baseline comparison.
E.6 Type Constrained Decoding (TCD)
Constrained decoding has been used in generating formal specifications for eliminating syntactically invalid outputs. Due to the sampling nature of NN-based models, generated tokens from the output layer can result in syntactical errors that can be detected on the fly, and type-constrained decoding solves it by forcing the model only generate tokens following the correct grammar rule. By eliminating syntax errors, it also improves the overall performance of the system.
In practice, type-constrained decoding is implemented at each step of the decoding loop: first checking the validity of the output token, then appending the valid token or masking the invalid, and e--generating new token according the probability distribution after masking. In addition, we design an algorithm simultaneously enforce the length limitation and syntactical rule by parsing partial formulas into binary trees. Beyond given maximum height of the tree, the model is forced only to generate propositions but not operators.
16

---

Appendix Implementation Details about Code as Policies
We designed two prompts for reproducing Code as Policies: one for code generation and the other for parsing landmarks. The code generation prompt is expected to generate an executable Python script that calls the goto_locy function for traversing through the environment and psrse case_loc() function ground referring expressions to landmarks, where the landmark resolution prompt is used. The code generation prompt for graph search is as follows,
Python 2D robot navigation script
import random from utils import goto_loc, parse_loe
# make the robot go to wooden desk. target loc parse. loc( woodenn desk") goto lottalectt loc)
go to brown desk and then white desk. target_loc_ parse_loce oooobr desk')
target_loc loc 2 = parse loc("ohin white desk")
target locs [target loc target. loc 2]
lorget_locs--o for target_loc in target_locs:
# head to doorway, but visit white kitchen counter before that.
target parse parse_loc(" loc('white kitchen counter')
larget_loc 2 = parse_ parse_loc("s (oo('doowayy))
target_locs = [target.loc.1] loc.et
for larget_loc in target_locs:
goto loc(target_
# avoid white table while going to grey door.
target loc parse loc(' grey door')
avoid_loc parse_loc(" conne_loo('white white table")
target_locs = [target_loc]
avoid_locs [avoid_loc]
for loc in target.locs:
goto_loc(los
locs)
either go to steel gate or doorway larget_loc__1 porse_loc('stes gate') )
target loc parse loc('doorwe) ddorwayy) target locs [target loc target loc 2] target loc random.chee www.:ccoocctttgegeee locs)
coto_loc((arget_loc)
go to doorway three times target_loc locs ('ooooowy)y)) for in range(3):
goto loc(target loc)
random loc = target loc
while random_loc = target_loc:
random_le www.om.choiceeeeee.mo..... sandom.choice(locaions))
goto_loc(randmm_lc))
17

---

The landmark resolution prompt is as follows.
# Python parsing phrases to locations script
locations ['bookshelf", 'desk A', 'table', 'desk B', 'doorway', kkichhen counter', 'couch', "door"]
semantic_info {
"bookshelf": ""material"; "wood", "color": "brown") }
"desk A"; ("material": "wood", "color": "brown"),
"desk B": ("material"" "metal", 'color': "white"),
"doorway": 0.
"kitchen counter": ("color": "white"),
"couch": ("color": "blue", "brand": "IKEA"],
"door": ("material": "steel", "color"; "grey"),
"table": ("color": "white"].
wooden brown bookshelf
ret.val 'bookshelf'
locations ['bookshelf", 'desk A,, 'table', 'desk B', 'doorway', 'kitchen counter', 'couch', 'door']
semantic info {
"bookshelf": {" ("material":: "wood", "color": "brown"),
"desk A": ("material"": "wood", "color": "brown"),
"desk B": ("material":: "metal", 'color': "white"),
"doorway": 0.
"kitchen counter": ("color": "white"),
"couch": ("color": "blue", "brand": "IKEA"),
"door": ("material": "steel", "color": "grey"),
"table": (""color:: "white"),
blue IKEA couch
ret val 'couch"
Appendix G Implementation Details about Grounded Translation
G.1 CopyNet
For reproducing [44], trained the CopyNet baseline with our grounded dataset preprocessed as its required format. To make fair comparison generalization ability, the CopyNet model has only seen utterance-formula pairs from the Boston subset, and the evaluation is run on grounded datasets of the rest 21 cities. For training CopyNet, we followed closely the instructions of the original paper and used the exact same LSTM model structure and pre-computed glove embedding for landmark resolution. On the hyperparameters, we set the embedding size to 128, the hidden size to 256, the learning rate 10-3, and the batch size to 100.
G.2 Prompt GPT-4
The prompt for end-to-end GPT-4 is as follows. While tried including landmark list in the prompt, it removed in the final version because we observed empirically that Prompt GPT-
18

---

Table 1: Dataset Comparison
Lang2LTL Lifted
CleanUp World
NL2TL
Wang et al. [5]
Number of datapoints
49,655
3,382
39,367
6,556
Unique formula skeletons
47
4
605
45
#Propositions (min, max, mean)
(1, 3.79)
(1, 3. 1.85)
(), 2.86)
(1, 2.01)
Formula Length (min, max, mean)
(2, 67, 18.89)
(2, 7, 4.77)
(1, 13, 5.98)
(3, 7, 4.48)
4 accieved better performance without explicitly giving a list of landmarks during prompt engineering.
Your task is to first find referred landmarks from a given list then use them as propositions to translate English utterances to linear temporal logic (LTL) formulas.
Utterance: visit Panera Bread sandwich fast food on Stuart Street LTL: F panera_bread
Utterance: eventually reach Wang Theater, and The Kensington apartments LTL: & F wang_theater the kensininnn
Utterance: make sure that you have exactly three separate visits Seybolt Park LTL: M & seybolt.park F & seybolt park F & syybolt_park. F & seybolt. park F seybolt. park seybolt park seybolt park G seybolt park seybolt. park G seybolt park G seybolt, park G seybolt_park
Utterance:
Appendix H Dataset Details
H.1
Quantifying diversity of temporal commands
We quantify the diversity of the temporal commands system is tested using the temporal formula skeletons in the evaluation corpus of commands. We propose that each novel dataset should be characterized along the following dimensions, and as example, we provide the respective values for the 2ang dataset (lifted and grounded OSM dataset) described in Section 6,4 of the main paper.
1. Number of semantically unique formulas: 47
2. Number of propositions per formula: minimum: 1, maximum: 5, average: 3.79
3. Length of formulas: minimum: maximum: 67. average: 18.89
4. Vocabulary size (for grounded datasets): 1757
5. Linguistic diversity of utterances: self-BLEU score: 0.85
Table 1 compares our proposed lifted dataset and other datasets proposed in prior work.
Appendix I
Detailed Result Analysis on Lifted Translation
We further analyzed the results for each model and holdout type for the lifted translation problem. In particular, we computed the accuracies per each formula type and the number of unique propositions required to construct the target formula. This analysis provides insights into the sensitivity of the models to particular templates and formula lengths.
The accuracies of each model and holdout type categorized by formula types are depicted in Figure 1. We observe that for both the finetuned models (Finetuned T5 and Finetuned GPT-3), the model
19

---

achieves high accuracies across various formula types for Utterance Holdout. Note that the perfor- mance across types is more uniform for the Finetuned GPT-3 than the Finetumed TS-Base model. Next, we note that Prompt GPT-4 achieves better accuracies as compared to Prompt GPT-3 across all evaluations.
We observe that the performance of the finetumed models is more unbalanced across differrnt formula types for the Formula Holdout test case. In comparison, Prompt GPT models achieve non-zero accuracies across all formula types. Once again, Prompt GPT-4 outperforms Prompt GPT-3. We note that adding type-constrained decoding to Finetuned T3-Base during inference only marginally improved Utterance Holdout, but significantly improved Formula and Type Holdout, which implies Finetuned T5-Base model is more likely to produce syntactically incorrect output when the grounding formula instance or type have not seen during training.
Finally, we note that only the prompt GPT models achieve meaningful accuracies in the Type Holdout scenarios. However, even in Type Holdout, the accuracies are concentrated on formula types that only had short lengths or shared subformulas with types seen during training. We can conclude that Formula and Type Holdout remain challenging paradigms of generation and an open problem for automated translation of language commands into formal specifications.
0000
Figure I: The accuracies per grounding formula types of six lifted translation models
Next, we repeated the above analysis but categorized accuracies by the number of unique propositions that appear within a formula. The results are depicted in Figure 2.
Figure 2: The accuracies per number of unique propositions of six lifted translation models
Here we note that in the Utterance Holdout test, the finetuned models demonstrated balanced perfor- mance across the dataset, whereas both prompt GPT models demonstrated degraded performance when the number of unique propositions the formula was increasing. Subsequently, the degraded performance on longer formulas was apparent even within the Formula and Type holdout domains. In contrast, the three finetuned models performed better for longer formulas in Formula Holdout. We hypothesize that this is because the finetuned models were more able generalize to different formula lengths of the same template (in particular, the templates that required temporal ordering
20

---

constraints to be encoded) as compared to the prompt completion-based approaches. In addition, there are more samples in the training set for longer formulas due to permutations of propositions.
As finetuning an LLM on the target task produced the best results for Utterance Holdout, we further analyzed the cause of errors for the instances where the lifted translation incorrect. We categorize the errors follows:
1. Syntax Errors: The formula returned by the lifted translation module was not valid LTL formula.
2. Misclassifed formula type: The lifted translation module returns an identifiable incor- rect formula type that did correspond to the input command.
3. Incorrect propositions: The returned formula was of the correct formula type but had the incorrect number of propositions.
4. Incorrect permutation:
The formula was of the correct template class and had the right number of propositions. but the propositions were in the wrong location within the formula.
5. Unknown template The returned formula was a valid LTL formula but did not belong to any known formula types.
Figure 3 to Figure depict the relative frequencies of the error cases as a pie chart for the three finetuned models. Note that returning unknown formula templates with the correct syntax was the most common cause of error in the lifted translation based on all finetuned models.
Pockissded eepatt
Incemect Procohtors
Figure Error frequencies of Figure 4: Error frequencies of Figure 5: Error frequencies of Finetuned T5-Base with TCD Finetuned T5-Base
Finetuned GPT-3
Since Finetumed GPT-3 achieves the best generalization across formula types, and sype-constrained decoding (TCD) during inference significantly improves the translation accuracies for unseen formula instances and types, the combination of large language models and TCD is by far the best approach for grounding language commands for temporal tasks.
Appendix J Robot Demonstration
J.1 Indoor Enviromment #1
The semantic information of landmarks in the first household environment is follows,
"bookshllf;;
"material"; "wood",
"color": "brown"
}, desk A":f "material": "wood", "color": "brown"
}.
" ddes B": {
"material"; "setal", "color": "white"
},
21

---

"doorway": 0
"k "kitchen counter": "color": "white"
},
"couch": { "color": "blue", "brand": "IKEA"
},
"doo": { "material"; "steel", "color"; "grey"
}. "table": "color": "shite"
Natural language commands used to test our system Lang2ITTL and Code as Polices [6] are shown in Table
J.2
Indoor Environment #2
The semantic information of landmarks in the second household environment is as follows,
"hallway A": { "decoration": "painting"
}. "hallway B": "decoration"; "none"
},
"table A": {
"location": "kitchen", "material"; "zetal", "color": "blue"
},
"table B": {
"location"; "atrium", "material"; "metal", "color": "shite"
}, "classroom": "door": ["glass", "grey"]
}, "elevator"; { "color": "purple"
"staircase": 0, "front deak": 0, "office": {
"door": ["wood", "yellow"]
}
Natural language commands used to test system Lang2LTL and Code Polices [6] are shown in
Table 3.
22

---

1.0
0.8
Accuracy
0.6-
Accurac)
0.0-
650
100
Propositions
RE Length
(a) RER Accuracy vs. Command Complexity
(b) REG Accuracy vs. Complexity
Figure 6: Figure 6a shows the accuracies of the referring expression recognition (RER) module as the complexity of commands (measured by the number referring expressions the command) increases. Figure 6b shows the accuracy of the referring expression grounding (REG) module the complexity of REs (measured by string length) increases.
23

---

Table 2: Commands for Robot Demonstration in Indoor Environment #1
Navigational Command
Lang2LTL Result
Codc as Policics Result
1. brown bookshelf, metal desk, wooden desk, kitchen counter, and couch in any order
SU00S5S
SUCOSSS
2. move to grey door, then bookrack, then brown desk, dosk
SUODESS
brown wooden
only after hookshelf
SUCDESS
the
4. go from brown booksbelf to white metal desk and only visit each landmark time
missundersiand the task
wooden desk exactly once and do not visit brown desk before bookshell'
go
SUOCESS
inexecutable
6. go white desk at least three times
SUODSSS
incrocutable
7. go wonden bookshelf least live times
bookshell's most
SUODESS
SUCDENS
9. counter most times
SUCDESS
SUCCESS
10. go to wooden desk exactly three times
SUOCeSS
misundersiand the task
move to brown wooden desk exactly 5 times
SUCCOSS
inexecutable
12. go doorway exactly two times, addition always avoid the table
SU00ESS
SUCCSSS
13. go to brown desk only after visiting bookshelf, addition go hrown desk only after visiting white desk
misunderstand the task
14, wnoden desk exactly in addition do not go wooden desk before bookrack
SUOD0SS
inerocurable
15. visit wooden desk least times, in addition do not go to wooden desk before bookshelf
SUcCess
inexecutable
16. visit the blue IKEA couch. in addition never go hig
SUCOESS
success
17, visit white kitchen counter then go brown desk, addition never visil white lable
18. go grey door, and only go bookshellf, in addition always avoid the table
SUCCESS
misunderstand the task
19. go kitehen counter then weoden desk, in addition after going to counter, you must avoid white table
SUccess
misunderstand the task
20. Go to bookshelf, alternatively go to metal desk
SUccess
misunderstand the task misunderstand the task stop execution correctly
21. counter, alternativlyy go metal desk
22. Go to the counter, but never visit the counter
unsatisliable. aboet correctly
23. do not go the woeden desk until booksheir, and do not go to bookshelf until wooden desk
unsutisliable. abort correcily
stup execution currectly
24, go to brown desk exactly once, addition go brown desk least twice
unsatisfiable. abort correctly
misunderstand the task
countes, addition avoid doorway
unsatisfiable. correctly
stop execution coreetlly
26. move to couch exacily twice, addition pass by counter
unsatisfiall. about correctly
stop execution correctly
navigate to counter then in addition after guing to the counter, you must avoid dueeway
unsatisfiable. abort correctly
misunderstand the task
28. Visit the counter least times and at times incorret grounding. OOD
inesecutable
29. visit least six times
incerrect grounding, OOD
go bookshell' then or go
grounding.
the task

---

Table 3: Commands for Robot Demonstration in Indoor Environment #2
Navigational Command
Lang21 .TI. Resalt
Code as Policcees Result
1. navigate to the office with the wooden dour, the classroom with glass
the atrium, kitchen counter, and the blue couch in any order
SICC0SS
SU00055
2. go down hallway decorated with paintings. then find the kitchen table, then front desk, then stairease
SUCCESS
SUCDESS
3. navigate to classroom but do not visit classroom before the
SUCCeSS
misunderstand
4. only visit classroom once, and do not visit classroom until you visit elevator first
5. Go the staircase, front desk and white table in that exact order. You are not permitted to revisit any of these locations.
SUCCESS
inexecutable
6. go the purple clevator at least live times
incxecutable
7. visit kitchen table most three times
SUccess
success
8. navigate the classrom exactly four times
inexecutable
9. go the front desk then the yellow office door. addition
visit classroom with glass door
SUO02SS
10. go stairs
front dosk.
addition avoid purple elevator
SUCCESS
elevator then front desk,
in addition avoid staircase
SUCCeSS
SUO005S
12. go front desk exactly two times, addition avoid clevator
SUCOESS
incxecutable
13. Go to elevator, allernatively go to staincase
SUCEESS
misundersiand the task
14, to the front desk least two different occasions, in addition you are only parmitted to visit the staircase at most once
SUCCeSS
misunderstand the task
15. Visit the clevator exactly once, in addition visit the front desk on at least separate occasions
SUCCess
incxecutable
16. Go to the office, in addition avoid visiting the elevator and the classraam
SUCCeSS
SUC025S
17, Visit the front desk, in addition
you are not permitted to visit clevator and staircase
Success
SUCO2SS
18. Visit the purple door clevator, then the front desk and then go to the kitchen table. addition you
go the elevator
the front desk
inexecutable
white table, addition you visit the staircase you must avoid the elevator after that
19. Visit the front desk
success
inexecutable
20. Go to the classmom with glass donr, but never visit the classroom with glass dour
unstisfiablle abort correctly
slop execution correctly
21. do not go to the white table until classroom, and go the
until white table
unsatisfiable. abort correctly
stop exccution correctly
exactly once, in addition kitchen table at least twice
go
unsatisfiable. abort correctly
misunderstand the task
23. find the office, addirion avoid visiting the front desk and the classroom and the table in atrium
unsatisfiable. abort correctly
stop exccution correctly
24, move to the kiichen table exactly twice. pass by hallway decorated by paintings most once
unsatisfibble. abort correctly
misunderstand
25, navigate to the kitchen tahle then front desk, addition after going to the kitchen table, you must avoid hallway docorated with paintings
unsatisfiable. abort correctly
misundcrstand the task
26. Go to the front desk least 4 different occasions, additionally, you only permitted to staircase most once
incomrect grounding.
inexecurable
27. Visit the front desk, additionally illy you visit the elevator you must visit the office after that
incomeet grounding, OOD
SUC0255
28. Visit the front desk, additionally you visit the oflice after
you the white table and the classmom
inzemeet grounding. OOD
misunderstand the task
25

---

Table 4: Specification Patterns for Lang2LTL
Specification Type
Explanation
Formala
Visit
Visit of waypoints {PI.P2 ... Pr } in any order
A Fr
Sequence
Visit set of waypoints (P1: Pa .... Pri J. ensure that Pa is visited at least once after visiting and so on
F(P1 F(P2 P........ FFr.))
Ordered
Visit set of waypoints (P1: P2 .... Pu... J. but ensure that Pa is never visited before visiting P1
F(P.) (-P(1 Up)
Strictly Ordered
Visit set of waypoints (P1: P2 .... Pr.. but ensure that pa is never visited before visiting additionally. ensure that ps is only visited on a single distinct visit before completing the of the task
F(Pa)
MEI P.)
NET C
pe U (pi U Upeel)))))
Patrolling
Visit set wwaypoints (P1: Pa ...... ................................ p.) infinitely often
N GFp,
Bound Delay
and only if the proposition is ever observed, then the proposition must hold at the very next time slep
G X6)
Delayed Reaction
If the proposition a is ever observed, then its response is ensure the proposition future
Ga - Fb]
some point in
Prompt Reaction
If the proposition must hold at the very next time step
observed, then the proposition
G X6)
Wait
The proposition a must hold till the proposition b bevomes true, & may never hold
W
Past Avoidance
The proposition a must not become true until the proposi- tion holds first. may hold
ma W
Future Avoidance
Once proposition observed be propo- sition 6 must never be allowed to become true from that point onwards.
G(a XG-b)
Global Avoidance
The set of propositions {P1, PP. must never be allowed become true
N G(-p.)
Upper Restricted Avoidance
waypoint can be visited on most separate
n P(a A (a U (-a A (-a (
n (<e UF (a
Pa
(e U
Lower Restricted Avaidance
The waypoint must be visited least separate visits
For
Fa forn 2, 2. A (a U (-0 (
Exact Restricted Avoidance
The waypoint must be visited on exactly n separate visits
= 1,
G(a v G-a))
Rorn 2. G(-a Gla G-a))))
Table 5: Example Commands from OpenStreetMap Dataset
LTL Type
Command (with two referring expressions)
Visit
move Thai hot pot restaurant Kneeland Street, and Vietnamse restaurant Washington Street visit Subway sandwich shop on The Plaza, Tollowed by Zada Jane's Cafe on Central Avenue
Sequence Visit
Ordered Visit
find Local Goods Chicago gift shop. not until find Currency exchange hurzan, first reach Citibank branch, and then Curler Majestic Theater on Tremont Street, in that exact order without repetitions Avenue, Kanellos Shoe Repair shop
Strictly Ordered Visit
Patrolling
keep visiting US Post Office West
Bound Delay
you must go to Purple Lot parking area. immeddatelly after you visit Royal Nails & Spa on South Main Street, and you can not go to Purple Lot parking area, any other time
Delayed Reaction
you must visit Peruvian restaurant immediately after you go to Beachside Resortwear clothing store, you must go to Walgreens Pharmacy
Virginia Avenue. once visit PNC Bank
Prompt Reaction
Wait
not go other place from Publix supermarket, unless you Reaches Museum
Past Avoidance
avoid visiting IES Test Prep school. till you observe bookstore on Elizabeth Street
Aveidance
never go to Commercial building make sure to never reach either Citbank, or Seybolt Purk go Cocktail bar. at most twice you have visit Main Branch of CoGo Bike Share Library for bicycle rental. two than two times navigate to Art shop on Bannock Street, exactly twice
Avenue, you go to Metro
Global Avoidance
Upper Restricted Avoidance
Lower Restricted Avoidance
Exact Restricted Aveidance
26

---

Table 6: Results of Recognizing Referring Expression with Spatial Relations
Navigational Command
Referring Expression(s)
Correctness
1. go back of Common Market always avoid entrance Litle Sugar
back of Common Market
correct
right Little Sugar
Litle
Sugar Creek left and right Little Sugar Creek
3. Intersection of Thayer street and Waterman street
intersection of Thayer street and Waternan street south of Edgehrank Coffee Ship
4. forward the south of Edgebrook Coffee Ship
go of Chinatown, then front of New Saigon Sandwich, withour visiting rear of Dumpling Cafe, then go rear of Dumpling Cafe, without visiting north Emerson College- Little Building. linally go south Emerson College Little Building, while only visiting each location
visiting west Saigon Sandwich,
of Chinatown | west of New Saigon Sandwich
front New Saigon Sand- wich rear of Dumpling Dumpling
north of Emerson College-
Littl Building south Eaner-
College Little Building big blue hox
6. go around big blue box
incorret
go of blue through between red and blue
exit of blue red
blue one
go CVS stay bridge
bridge
9. go right of Dairy Queen to left of Harris Teeter, end at entrance Wells Fargo
Dairy Queen Harris Tecter
incorrect
Wells Fargo
10. My Sister's Closet and stop close bus stop Ace Hardware
Sister's Closet bus stop near Ace Hardware
incurrect
27


Reviews:
[{"review_id": "xX2mD7T7yrH", "reviewer": "Reviewer_qzh3", "summary": "", "questions": "", "limitations": "", "rating": 4, "confidence": 3, "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": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "This paper tackles the problem of grounding complex natural language commands into formal linear temporal logic (LTL) specifications for robotic navigation tasks. This is important because LTL provides unambiguous semantics for reasoning about long-horizon tasks and verifying the satisfaction of temporal constraints given in the instruction. Existing approaches require training data from specific environments and landmarks, limiting generalization. The authors propose Lang2LTL, a modular system using LLMs to ground commands to LTL without prior language data from the target environment. Generalization experiments evaluated Lang2LTL on 5 generalization criteria on a new dataset with 2125 unique LTL formulas corresponding to 47 task templates. In system-level evaluations, Lang2LTL outperformed the baseline Code as Policies approach, which does not leverage LTL.", "summary_of_recommendation": "The paper is well-motivated and clearly written. The proposed method is a great example of connecting the open-world reasoning capabilities of LLMs with more precise task representations and planners. I recommend acceptance as the paper has convincing experiments, and the method should be easily adoptable by others in the field.", "technical_quality": "Very Good:  Convincing.", "clarity_of_presentation": "Excellent: Enjoyable to read.", "potential_impact": "", "robotics_focus": "Sufficient demonstration on hardware", "quality_of_limitations": "Limitations are addressed clearly", "questions_for_rebuttal": "See feedback section.", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "Strengths\n- The problem is well motivated and the approach is well justified.\n- Extensive discussion on generalization in understanding temporal navigation commands.\n- The claims are generally well supported by experimental results across multiple datasets and task types.\n- The paper is clearly written and well structured. The problem setup and proposed approach are easy to understand. \n- Detailed experiments across different LLMs.\n- Experiments used k-fold validation to report standard deviations\n- The limitations section acknowledges overfitting by the lifted translation model and the inability to distinguish between landmarks with the same features. The authors suggest using larger models and dialog for disambiguation. \n\nWeaknesses / Feedback\n1) Including some example commands used in the actual experiments would make the experiment clearer. In addition, the authors should provide an analysis of how the recognition and grounding modules perform relative to command/description complexity.\n2) A more detailed failure mode analysis for the real robot experiments would make the paper stronger. What proportion of translation errors is due to failures in the grounding vs. lifted translation modules?\n3) Are the symbolic formulae unique in LTL notation? If not, what happens when the symbolic translation LLM outputs a different but functionally identical LTL formula?\n4) It would be beneficial, from a user experience standpoint, to have an additional LLM that translates the final output formula back into natural language, where the user can preview how the planner understood the instruction and give corrective feedback if necessary. \n5) I urge the authors to release code and finetuned models so that the method can be easily reproduced by other researchers.\n", "extra_scores": {"impact": "4: The work contains interesting new ideas that will potentially have major impact in robotics or machine learning."}, "extra_text": {}}, {"review_id": "e2tsxgaXTxH", "reviewer": "Reviewer_o4yc", "summary": "", "questions": "", "limitations": "", "rating": 2, "confidence": 4, "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": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "The aim of this work is to translate natural language commands for navigation into LTL for execution on multiple platforms.  In this case a quadcopter and the Boston Dynamics Spot. The work extends Berg 2020 by \"leveraging LLMs and training and evaluating on a semantically diverse dataset\".  The key insights include the factorization of the problem for handling referring expressions versus grounding.  Lifted representations allow for a more general template to be learned where command structure is separated from arguments.", "summary_of_recommendation": "The work explores different language models and extends prior work on OSM to also include the Spot robot.  However, it's not clear that the evaluation/domain is truly diverse, the learning problem novel, nor the insights broader than another application of \"larger LM is better at symbol manipulation\"", "technical_quality": "Fair: Significant additional evidence required to support the claims.", "clarity_of_presentation": "Fair: Major revision needed to improve organization or clarity.", "potential_impact": "", "robotics_focus": "Sufficient demonstration on hardware", "quality_of_limitations": "Additional details required", "questions_for_rebuttal": "1. Am I correct in understanding that referring expression here is not the traditional notion in computer vision or manipulation that includes spatial references like \"left of\" but instead only prepositions like \"on ___ street\"? \n2. How were the 10 operators, propositions, and templates chosen? 47 templates feels surprisingly small given size and richness of the models being deployed? While most current work does not use LTL which brings it's own benefits and restrictions, this feels like it might be a very constrained semantic space?\n3. Related question about the definition of diversity.  Diverse is used to describe the work several times (e.g. \"semantically diverse language\") but comparisons to exist work on navigation, for example by reading the appendix, leave me worried that the language and object category space is much smaller than traditional navigation datasets instead most of the diversity being due to business names which would reduce the problem to one of pure linguistic KB knowledge.\n4. General request for more explanation of why which models are used where.  The intro/conclusions focus on GPT-4, it's unclear if that's the right takeaway from Fig 3a or how the fine-tuned models would do if used in 3b.  Discussing why GPT-4 is the best choice would be appreciated here.", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This work tackles multiple hardware platforms (unlike prior work), it also investigates the role of several LMs both closed models accessed via prompting and those that can be fine-tuned. I believe there are likely several important contributions in this work but it can be difficult to tease them apart and verify next to prior work.  The crux of my concerns are around the definition of diversity and clarity of presentation. ", "extra_scores": {"impact": "2: Unsure, difficult to assess."}, "extra_text": {}}, {"review_id": "BIB6BRrhmx", "reviewer": "Reviewer_y8dy", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": 3, "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": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "The paper presents a system based on LLMs for translating free form language navigation instructions into a structured command (based on linear temporal logic) that can be interpreted by off-the-shelf planners. The paper claims the method is state-of-the-art on this task.", "summary_of_recommendation": "Evaluation needs to be more thorough or better documented.", "technical_quality": "Good: Generally convincing, but some additional experiments or analyses needed.", "clarity_of_presentation": "Good: Minor revision needed to improve organization or clarity.", "potential_impact": "", "robotics_focus": "Sufficient demonstration on hardware", "quality_of_limitations": "Limitations are addressed clearly", "questions_for_rebuttal": "See the \"Review\" section.", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The explanation of the proposed system is easy to follow. However the evaluation is less clear. In particular, the authors claim that \"Lang2LTL achieved state-of-the-art performance in grounding diverse temporal commands in 21 novel OpenStreetMap regions\" but I have hard time finding evidence for this in the paper. The only prior work shown in Fig. 3 is the CopyNet model which has 0 accuracy and hence cannot be considered a reasonable baseline. In Table 2, the accuracy of Lang2LTL is either not significantly larger than prior accuracy (in the statistical sense), or is worse than prior accuracy. I'm happy to improve my score if the authors clarify the comparison to baselines (I do appreciate the comparison to code-as-policies).", "extra_scores": {"impact": "4: The work contains interesting new ideas that will potentially have major impact in robotics or machine learning."}, "extra_text": {}}, {"review_id": "-CqL7wGYQ3F", "reviewer": "Reviewer_UUsu", "summary": "", "questions": "", "limitations": "", "rating": 4, "confidence": 4, "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": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "The paper introduces Lang2LTL, a modular system and software package that utilizes large language models (LLMs) to ground navigational commands to linear temporal logic (LTL) specifications in novel environments without requiring retraining, as long as it is provided with a semantic map. Lang2LTL addresses three distinct tasks: referring expression recognition, grounding expressions to real-world landmarks, and translating the lifted command to obtain a grounded linear temporal logic (LTL) specification. This approach demonstrates state-of-the-art performance in grounding navigational commands to diverse temporal specifications in 21 city-scaled environments. The system achieves an 81.83% grounding accuracy in unseen cities, outperforming previous state-of-the-art methods and an end-to-end prompt GPT-4 baseline. The paper also showcases a physical robot successfully following 52 semantically diverse navigational commands in two indoor environments using Lang2LTL.", "summary_of_recommendation": "The paper presents a novel and significant contribution to the field of natural language understanding for robotic navigation tasks. By proposing Lang2LTL, the paper addresses the challenges of grounding navigational commands to linear temporal logic (LTL) without the need for re-training in novel environments. The comprehensive evaluation of Lang2LTL showcases impressive results in diverse city-scaled environments, demonstrating its state-of-the-art ability as Lang2LTL outperforms previous state-of-the-art methods, including an end-to-end prompt GPT-4 baseline. The successful demonstration of a physical robot following 52 semantically diverse navigational commands further validates the practicality and effectiveness of the proposed approach. The paper deserves acceptance given its novelty, significant contributions, and impressive results.", "technical_quality": "Excellent: Very convincing and thorough.", "clarity_of_presentation": "Excellent: Enjoyable to read.", "potential_impact": "", "robotics_focus": "Sufficient demonstration on hardware", "quality_of_limitations": "Additional details required", "questions_for_rebuttal": "1. Please clarify the first point of the weaknesses above. Can Lang2LTL handle pronouns and indirect references to landmarks? If not, can you propose a high-level solution that could be a direction for future work to make this approach more robust?\n2. Kindly recheck the above-pointed typos and referencing errors and address them.\n", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "**Strengths**\n1. Clarity: The paper's language is lucid, brief, and captivating, ensuring that readers can grasp the concepts effortlessly. The information flows logically, maintaining cohesion throughout the document.\n2. Originality: The work is very original, and the proposed approach is novel with promising results. \n3. Real-robot results: The paper also showcases results on a physical robot that successfully follows 52 semantically diverse navigational commands in two indoor environments using Lang2LTL.\n4. A reasonably complete comparative study of Lang2LTL performance with strong state-of-the-art baselines like Code-as-policies (CaP), CopyNet-based translation model, Prompt GPT-4, etc.\n5. Well-organized and informative appendix giving details on data collection, implementation details, and relevant examples as and when needed. \n6. Promising results supported by quantitive and qualitative analysis of the proposed system.\n\n**Weaknesses / Issues**\n\n1. Line 136 of the paper (section 5.1) mentions that the currently proposed method is limited to processing language instructions containing noun phrases and proper names. However, it cannot effectively handle indirect references and pronoun phrases like \"Go to the post office. Go to 'it' via the tall bridge.\" This limitation of Lang2LTL is not explicitly addressed elsewhere in the paper.\n2. In line 242, what is the Table “6.4” referenced here?\n3. In Figure 2, the yellow box for “Symbolic Formula” has an error - It should be “F a & ! a U b” instead of “F b & !a U b”.\n4. Line 261 has a typo - “crown-sourced” \n5. Line 295 - Appendix Table 1 and Table 2 should be Tables 2 and 3 instead.\n", "extra_scores": {"impact": "4: The work contains interesting new ideas that will potentially have major impact in robotics or machine learning."}, "extra_text": {}}]

Author rebuttal:

Meta-review: The authors present an approach for grounding navigation commands into linear temporal logic via an LLM. They evaluate this system in several domains, over various behaviors, and with different language model approaches.

Though the reviews were not fully in concensus, primarily as the result is not too surprising, they find that the work is an interesting and thorough investigation of how language models can translate into executable LTL instructions, and thus I recommend acceptance. 

Though likely out of scope, the paper could be further improved by showing LTL constraints beyond the navigation domain. Some of the results in the appendix could also be moved to the main body to highlight the breadth of results and Figure 1’s clarity could be improved, e.g., by detailing the method and LTL constraints.
Decision: Accept (Poster)