We thank the reviewer for their insightful feedback.

Response to "Reasons To Reject":

Point 1: We agree that the RAG model can potentially overfit to the retrieved constructs in the lexicon seen during training time. However, our experimental evidence shows this is not the case. Firstly, open-vocabulary constructs are by definition those not seen before. Our evaluations duly reflect this as gains are all seen using unseen constructs in feedback during inference. Secondly, the difference in performance between the validation and test sets is quite small indicating there is very little overfitting. For instance, for the Code-T5 base model trained via RoLex, the difference in BLEU performance between validation and test performances is a mere 0.2 BLEU score! For the NL2LTL domain, note that the training set is synthetic and has no overlap with the test set. The overall large gains in all of the settings indicate that the overfitting, if any, is small.

Response to "Questions to Authors":

Some of these questions are addressed in the paper’s Appendix, which the reviewer may read for further clarification. To take each question in turn:

• The lexicon is built using small snippets of text/documentation describing the construct. For each evaluation testbed, the lexicons are constructed differently. Please see Appendix Section 8.3 for further details.
• All of the lexicons in our testbeds are OOV compared to the training sets. This is accomplished by explicitly making sure that none of the test OVCs are seen in training examples.
• Our retriever is designed to retrieve the top-k relevant lexicon entries (k=10 in our experiments). If a parse requires multiple lexicon entries, our fine-tuned retriever is trained to retrieve all of them within the top-k. Our generator is fine-tuned and conditioned upon the retrieval such that it identifies all of the relevant lexicon entries and uses them during generation. This is accomplished through specific training strategies during fine-tuning, such as teaching the models to learn to extract relevant lexicons first and then teaching them to do the semantic parsing task. These training strategies are highlighted in Section 4.3 of the paper.

We will add discussions about reviewer's points in the final camera-ready version of the paper.

We thank the reviewer for their constructive feedback.

Response to "Reasons to Reject":

Point 1: We agree that the problem setting is not typical in open-domain NLP problems, including standard semantic parsing application areas such as Text-to-SQL or Knowledge-based QA.

However, as we argue in the paper (beginning paragraph of Section 3), the setting we introduce is especially well-suited for formal verification, where there are a large number of problem domains in which translating text specifications to formal statements is a serious burden preventing progress in verification and slowing the development of protocol implementations. For example, there are thousands of RFCs out there and, for each of them, the expert needs to parse the specification to formal language manually. Also, this project and associated datasets were developed from collaborations with formal verification researchers who want to verify Network File Systems but are unable to do so due to the difficulty of parsing specifications into formal models. Hence, their difficulty further necessitates the need for our solution.

We will add text to the paper to better highlight this motivation and the broader potential for impact in the final version.

Response to "Questions to Author":

We thank the reviewers for pointing out these typos/errors. We will fix them in the final camera-ready version of the paper.

We thank the reviewer for their constructive feedback and related work suggestions.

Reponse to "Reasons to Reject":

Point 1: Approaches in referred papers have similarities (using RAG to model feedback) but differs in tasks and training methods.

• (Mishra et. al 2022) , while using the concept of dynamically growing feedback database, differs in downstream domain task (QA vs Semantic Parsing). They also utilize free-form feedback compared to our lexicon-based feedback, which is more efficient for addressing constructs ( Table 4(b) ). We also train our retrievers for domain adaptation, compared to using off-the-shelf retrievers like them, due to the non-generalizability of our domains. Secondly, they use a trick called ``forced generation’’ which generates multiple inputs with each retrieved feedback using off-the-shelf generators. We propose different unique training schemes that teach the model to use feedback effectively (Section 4.2 for details).
• (Das et. al 2021) uses training examples/cases as feedback and have a static database of such examples. Whereas, our feedback is designed as a dynamic database of lexicons growing with each inference parse.

Point 2: We agree that actual HIL experiments can showcase practical considerations ( HCI aspects etc.). However, semantic parsing problems we consider require domain knowledge and trained users. Hence, testing using such expert users can be difficult and expensive. This is especially true for our NL2LTL setting, in Network File Systems domain, where the target formalism is niche and our test set required many iterations and months of input from formal verification experts. Hence, we settled for the middle ground of using simulated environments common across the literature.

We assume “deriving data synthetically” refers to how human feedback data was simulated and not test datasets themselves, as all of them are real-world datasets.

Point 3: Fine-tuning retrievers can affect generalizability. However, our test domains are specialized and models require domain-specific knowledge. Hence, fine-tuning, compared to off-the-shelf RAG, yields significant performance gains, as shown in results in Table 3(b) and 7. Building generalized retrievers that can work across domains (e.g. from NL2LTL to the NL2Code domains) can be interesting future work in this space.

In the final camera-ready version of the paper, we will add discussions to these points.