Formal Specifications from Natural Language
Authors: Christopher Hahn
Frederik Schmitt
Julia Janice Tillman
Niklas Metzger
Julian Siber
Bernd Finkbeiner
Venue: Submitted to ICLR 2023 (2023)
Keywords: language models
natural language
formal specifications
first-order logic
temporal logic
regular expressions

Abstract: We study the generalization abilities of language models when translating natural language into formal specifications with complex semantics. In particular, we fine-tune language models on three datasets consisting of English sentences and their corresponding formal representation: 1) regular expressions (regex), frequently used in programming and search; 2) First-order logic (FOL), commonly used in software verification and theorem proving; and 3) linear-time temporal logic (LTL), which forms the basis for industrial hardware specification languages. Our experiments show that, in these diverse domains, the language models maintain their generalization capabilities from pre-trained knowledge of natural language to generalize, e.g., to new variable names or operator descriptions. Additionally, they achieve competitive performance, and even outperform the state-of-the-art for translating into regular expressions, with the benefits of being easy to access, efficient to fine-tune, and without a particular need for domain-specific reasoning.

Under review as a conference paper at ICLR 2023
FORMAL SPECIFICATIONS FROM NATURAL LANGUAGE
Anonymous authors
Paper under double-blind review
ABSTRACT
We study the generalization abilities of language models when translating natural language into formal specifications with complex semantics. In particular, we fine- tune language models on three datasets consisting of English sentences and their corresponding formal representation: 1) regular expressions (regex), frequently used in programming and search; 2) First-order logic (FOL), commonly used in software verification and theorem proving; and 3) linear-time temporal logic (LTL), which forms the basis for industrial hardware specification languages. Our experiments show that, in these diverse domains, the language models maintain their generalization capabilities from pre-trained knowledge of natural language generalize, e.g., to new variable names operator descriptions. Additionally, they achieve competitive performance, and even outperform the state-of-the -frtherr- for translating into regular expressions, with the benefits of being easy to access, efficient to fine-tune, and without a particular need for domain-specific reasoning.
INTRODUCTION
Translating natural language into formal languages is long-standing goal of artificial intelligence research dating back to the 1960s (e.g.. Weizenbaum (1966); Winograd (1971). )) Due to recent
progress in deep learning (especially Vaswani al. (2017) and the development of language models (LMs), the field has seen significant improvements, for instance, in the translation from natural
language into coding languages formal mathematics (e.g.. Le..LLee et al. (2022); Chowdhery et al. (2022); Chen et al. (2021): Wu et al.] (2022). In this paper, we study the generalization abilities of a pre-trained LM when translating natural language into formal specification languages.
Formal specification languages are used in various computer science fields to describe system's ss desired behavior, including fields such as systems design, requirements analysis, and automated reasoning. Examples include specification languages based on logics, such as Alloy (Jackson) 2002) and LTL (Pnuelil 1977), system specification languages based on state charts, such SDL (Fonseca i Casas et al. 2013), ) or text processing specifications based on regular languages, omega-regular languages, and automata theory (Aho 1991] Thomas 1990). Compared to natural language, the benefit of a formal specification language is its unambiguous semantics making it accessible for algorithmic work that relies on a specification as input. Examples are high Segh-performance SAT and
SMT solvers (e.g., [Sorensson & Hen (2005): Biere et al. (2013); Audemard & Simon 2018): Moura & Björner (2008); (Barrett et (201 1), planning tools La Valle 2006), model checkers (e.g.. Cimatri
al. (2002); Holzmann] ( (1977): Behrmann et al. (2006)), hardware synthesis tools (e.g.. Bohy
(e.g..Boohy et al.
(2012) Faymonvilee et al. (2017) Meyer et al. (2118). or automatic theorem provers (c.g., Bertot
& Castéran (2013); Nipkow et al. (2002)). Despite their benefits and various application areas, formal specification languages are still almost exclusively used by domain experts as their application requires significant domain- domain-specifee knowledge and extensive manual work. With the success of LMs,
the goal of making the techniques mentioned above available to broader user base to increase the correctness, trust, and assurance in computer systems is finally getting closer.
So far, efforts in utilizing deep learning to translate natural language into formal specifications have relied on training (often over-engineered) neural networks from scratch (e.g.,Singh et al. (2020); ; He et al.) )2022)). ) Such approaches are naturally limited in their generalization capabilities. The natural questions arise: 1) Can off- the-shelf LMs achieve competitive performance when fine-tuned on this challenging translation task? 2) How well will they generalize with their pre- pre-trained knowledge of natural language? In this work, we initiate a study on this topic by fine-tuning the open-source transformer language model T5 (Raffel et al. 2020). The transformer architecture (Vaswani et al.

---

Under review as a conference paper at ICLR 2023
natural language (ID)
lines having a character and the string 'dog" in them
regex prediction (correct)
(()&(dog)).
natural language (OOD)
lines with words with a letter before the string "eye" or the string "time"
regex prediction (cnrrect)
([A-7a-z])*' (eye) (time) ).*
natural language (ID)
Globally it is the case that if a holds then eventually and b hold.
LTL prediction (correct)
Mia + Oa A b))
natural language (OOD)
Whenever does hold, 09 eventually hold.
L.T. predictii (correct)
O 69
An ID example of a regex model trained solely on the noun "dog", tested OOD new nouns "eye" and "time"; and an ID example of an LTL model trained on variables in to i4 and on to 04, tested OOD on new variables and operator descriptions (bottom). OOD fragments are highlighted.
Figure I:
2017) has proven itself to be the most powerful general-purpose model at the moment of writing, setting new standards in many application domains such as computer vision (e.g., Dosovitskky et al. Dong et al. (2018)), and, especially, natural language processing (e.g., Brown et al. (2020)). Additionally, T5 is open-source and the trained models are easily accessible a broad audience.
(2020), ) speech recognition
We have picked three common yet diverse formal representations used widely in software and hardware domains: 1) regular expressions, frequently used in programming and text manipulation, 2) First-order logic, which is standard formalism used in software domains, such as theorem proving, and 3) Lincar-time temporal logic, which is used in hardware domains, such as model checking of sequential circuits. Regular expressions (regex), introduced by Kleene et al. (1956), are sequences commonly used for text manipulation. For example, (a lb) * reads as "all sequences with no symbols other than a and b, including the empty string". First-order logic (FOL) extends propositional logic with predicates and quantification. With the foundations developed independently by Goutoo Frege and Charles Peirce (Peirce 1933). FOL is formal system of high importance in mathematics, computer science, and linguistics. For example, the formula Vx...y.-1. = y) denotes that for every x, there is y. which is not equal x. Linear-time temporal logic (LTL) (Pnueli] 1977) is a hardware specification language widely used by the verification community. It forms the basis for industrial specification languages like the IEEE standard PSL. CLEEE-Comiision et al. 2005). LTL extends propositional logic with temporal operators, specifying behavior over time. For example, when considering a controller for a shared resource, the formula [(r + Og) denotes that it is "always the case that request is eventually followed by grant g".
Our experiments show that the fine-tuned LM achieves competitive performance on all tasks and even improves state-of-the-art performance in translating natural language to regex by 6 percentage points. Additionally, the models can utilize pre-trained knowledge of natural language. For example, Figure I shows hand-picked in-distribution (ID) and out-of-distribution (OOD) examples for models trained on translating natural language to regex and LTL, respectively. The regex model generalizes to new nouns that were not present during fineituning. The LTL model was fine-tuned on "globally" and "always" as the translation of the LTL operator D. on "implies" and "if then" as the translation of the implication ->, and on variables in i4 and on 04. It generalized to new variable names and operator descriptions, recognizing x and 09 as variables, "whenever" as synonym for "globally", and a simple comma as synonym for "implies". We provide detailed experiments in Section showing, for example, that the regex model achieves the same accuracy on a held-out test set (>> 88%) when being trained on only four out of 16 occurring nouns in the test set (c.f., Figure 2 in Section
In summary, we make the following contributions. We provide the first fine-tuned off-the-shed language models for translating natural language into formal specifications, including a new state-of- the-art model for translating into regular expressions. We contribute two novel datasets for translating natural language into FOL and two for translating natural language into LTT. Furthermore, we analyze the generalization capabilities of the pre- rre-trained language models by conducting generaliza- tion experiments on new variables, nouns, and operator descriptions, as well as out- out-of-diisribution instances.
'The datasets, models, and code will be published once the double-blind reviewing process ends.
2

---

Under review as a conference paper at ICLR 2023
2
RELATED WORK
Natural language to regex. Similarly to FOL, there were early rule-based techniques for regex translation (Ranta 1998). The regex datasets have been made more amenable to translation using semantic parsing for decomposition (Kushman & Barzilay 2013). Training has been guided towards semantically equivalent (Zhong et al. (0188) or approximately equivalent regular expressions (Park) (et al., 2019); the natural language descriptions have been enriched by paraphrases generated by crowdsoureing (Locascio et al., 2016). The latter work is the most closely related to ours, it also does not use comain--peciffe reasoning such as, c.g., semantic equivalence. Ye et al. (2000) have proposed to solely learn generation of regex sketches, and to relegate the construction of the final, correct regular expression to a program synthesis procedure; their dataset is not publically available.
Natural language to FOL. The task of translating natural language into logics, for example with rule-based (e.g., Loggsonoosoo|/ ( 1984); Woods (173); [Thompoon et al. (1969); [altz (1978); Hendrix et al.
(1978); Templeton & Burger ( (983)) statistical approaches (Zelle & Mooney 1996]] Thompson
2003 Zettlemoyer & Collins, [0077] [012 Kwiatkowksi et al.] 2010). and recently also neural
2017 Liu al. 2018 Li et al. 2018) has been studied extensively in the past in the area of semantic parsing Kamath & Das (20 8)
methods (Kočiský al. 6 Buys & Blunsom 2017 2
In this work, we rely on the FOL translation (Kamp & Reyle 2013) of boxer's output (Bos) 2015
Closest to our work on FOL translations is the first approach of translating natural language to FOL presented by Singh et al. (2020). They construct a dataset using semantic parsing, but clean up the representation of boxer's is FOL output, and train a highly specialized LSTM-based architecture. At the time of writing, no code or dataset are publically available for a direct comparison. Hann et al.] (2022) independently developed few-shot learning approach using very large language models, achieving a similar accuracy on novel datasets.
Natural language to LTL. Other approaches to the problem of translating from natural language to LTL focus on the robotics domain, such as temporal aspects in grounded robotics (Wang et al. 2020) and planning (Patel et al. (2019). A survey of earlier research beyond neural approaches is provided by |Brunello et al. (2019). Grammar-based approaches to translate L.T. into structured natural language (Konrad & Cheng 2005 Grunske 2008) inspired the design of our grammar for constructing the dataset. Gavran et al. (2020) present an interactive method for translating into LTL specifications from example traces by combining SMT solving and semantic parsing. Cherukuri et al. (2022) consider the inverse direction: translating from LTL formulas to natural language.
Deep Learning in formal reasoning tasks. The term autoformalization (Wang et al.) 2018 Szegedy 2020: Wu et al., (2022) has been coined for tasks of translating between natural language and formal mathematics. Deep learning approaches were able to handle symbolic representations such as logical formulas in SAT-solving (Selsam et al. 2019: [Selsam & Björner 2019). expressions in mathematics (Lample & Charton 2020). formalization
in theorem proving (Polu & Sutskever 2020), specifications in hardware synthesis (Hahn et al.) 2020) 2021), even code in software generation (Li ct al. 2022 Chen et al. 202T). Transformer models have succesfully been trained on
programming language translation (Roziere et al. 2020), source code to learn representations of programs (Hellendoorn et al.) 2020), and on code synthesis (Li al., 2022] Chen et al. [ kamp
al. (202)) | all lacking training for formal representation of their specifications. [Saxton et al. (2019);
Schlag et al. (2019) study to solve math problems given in natural language. Transformers were also trained on symbolic integration and solving differential equations (Lample & Charton 2020).
Transformers have been applied to formal mathematics (Rabe et al. 2020).
3
DATA SETS
We consider three formal specification domains: 1) regular expressions (regex) frequently used in programming or search, 2) First-order logic (FOL), which is a standard formalism used in software domains, such as theorem proving, and 3) Linear-time Temporal Logic (LTL), which used in verification, such as hardware model checking. We train six datasets, two for each considered domain (see Ta the appendix for an overview). For regular expressions, we used the existing benchmark sets Regex-synthetln contributions. In the following, we give background on the respective domains and describe the existing datasets and our data generation methods in detail.
and Regex-turk. The FOL and LTL datasets are new
3

---

Under review as a conference paper at ICLR 2023
3.1 NATURAL LANGUAGE AND REGEX PAIRS
Regular expressions (regex) are sequences that describe a search pattern for natural language text. They are commonly used in programming. for example, for string-searching or ind-and-replace operations. They have been introduced by Kleene et al. (1956) and are used extensively in text editors, and are even supported natively in many programming languages. For example, (a (b) * reads as "all sequences with no symbols other than and b, including the empty string". We follow the regex representation defined in previous work (see Figure S in the appendix).
The Regex- Regex-synthne het ic dataset was synthetically generated by Locascio et al. (2016). They used a manually-crafted grammar based on the smaller dataset from Kushman & Barzilay (2013). Two randomly drawn samples from this dataset are "lines with number or the string 'dog' zero more times" paired with ( ([0-91) (dog) ) * and "lines not starting with a character, 2 or more times" paired with (.)) (.+) ), Regex-turk is a dataset that Locascio et al. (2016) generated based on paraphrases of the natural language descriptions in
collected through crowdsourcing at Amazon Mechanical Turk. Two randomly drawn samples from this dataset are "a let- ter appears before a number in the lines" paired with ( [A- -z]) ([0- .)).*.......>>> .*.. and "lines do not start with the string 'dog' nor the string 'truck" paired with ( (dog) (. )))) & (truck) )
3.2 NATURAL LANGUAGE AND FOL FORMULA PAIRS
First-order logic (FOL) extends propositional logic with predicates and quantification. With the foundations being developed independently by Gottlob Frege and Charles Peirce (Peirce 1933), FOL a formal system of high importance in mathematics, computer science, and linguistics. First-order terms and formulas are defined relative to given signature. A first-order signature is pair of disjoint sets F and P of function and predicate symbols, respectively, as well as an arity function FUP + N. Given a signature, the FOL alphabet consists of the elements of J and P as well as standard logical connectives (7, V, A, -, T, L), quantifiers Y and 3, the equality symbol =, and an infite set of variables { 22,,.... The syntax of well-defined formula is given as follows:
1. ||| f(1,.... (n) a : Q P(I....... 6.)) = (21, I -ax an A A Ir.o
where æ is a variable, e is a constant, f is an n-ary function, Q is a nullary predicate and P an 1 S n-ary predicate. The boolean connectives V, ->, and ++ as well as the quantifier Y can be derived. For example, the formula Vr.By.- = (x. y) denotes that forall z, there is y, which is not equal to x.
We generated FOL formulas from natural language sentences using the cande (Clark & Curran 2004) and boxer (Bos] 2015) toolchain. cande is a wide-coverage Combinatory Categorial Grammar (CCG) parser. CCG (Steedman) 200T) a lexicalized grammar where every word in sentence is assigned an elementary syntactic structure. A derivation of this CCG is then given to boxer, which provides a semantic framework to output various formal derivations of the input sentence, e.g., in first-order logic. Both datasets FOL-mnli and FOL CoL-codesc are generated using this toolchain. The dataset FOL-mnl i consists of small sentences taken from the hypothesis predictions of the glue/mnli dataset (Williams et al. 2018). Two randomly drawn examples are "The fans do not bring any support." and "No one will ever understand how continental plates form.". The dataset FOL-codessC consists of pairs of natural language sentences of java code snippets and their first-order translations. We sampled the pairs from the recently published Codese (Hasan et al. 202T) dataset consisting of 4.2M datapoints. We cut off the natural language descriptions after the first sentence and translated them into an FOL formula with the candc- boxer toolchain. This results in highly challenging dataset, which we believe to be close to practical applications. For example, two randomly drawn instances are "deletes a certificate from specified key vault" and "sets the base dir for the volume".
3.3 NATURAL LANGUAGE AND LTL FORMULA PAIRS
is a temporal logic for the verification of hardware systems. LTL extends propositional logic with temporal operators, specifying behavior over time. LTL formulas are defined over a set of variables AP called atomic propositions. The alphabet consists of elements of A AP, standard logical connectives (-, V,,, -,,,,TT, 1), and temporal operators O (next)
Linear-time temporal logic (LTL) Pnueli 1977
4

---

Under review as a conference paper at ICLR 2023
and U (until). The syntax of an LTL formula is given as follows:
; -pp (P1 V P22 Oip 91
where p E AP is an atomic proposition and Oşp means that the subformula yp holds in the next timestep or cycle and Φp l Φ2 means that ş holds until 42 holds. We additionally use the derived operaters eventually O p Tud yp and globally Op - -p. For example, when considering controller for shared resource, the formula (r O g) denotes that "it is always the case that a grant to the resource g eventually follows process' request r".
We generated pairs of natural language sentences and LTL formulas with two different methods. In the first data generation method LUTL-patterie we utilized these specification patterns commonly defined in the literature (Dwyer et al. 1998 Etessami & Holzmann] 2000 Holeček et al., [2004] Pelánek 2007), which are provided by the spot library (Duret-Lutz et al., 2016). For example, the specification pattern ( + b) states that at every timestep, whenever holds, b has to hold as well and the specification pattern [Q a states that a has hold infinitely often. Since an LTL specification typically consists of a conjunction of such patterns, we followed the approach in the literature and conjoined up to patterns and their translations (Li al. (003). In the second dataset, constructed pairs of natural language sentences and formulas using straight-forward grammar with minimal domain-specific knowledge (Konrad & Cheng 2005 Grunske 2008) (see Appendix D in the appendix). The grammar restricts formulas only contain negations directly in front of atomic propositions, which is dictated by the structure of the English language, as verbs follow a different conjugation depending on whether they are used in positive a negated case. For instance, a is translated to "Globally a holds" and D ma is translated to "Globally a does not hold". To translate L.L formulas automatically, we used natural language grammar that is structurally the same as the LTL grammar. The interested reader can find the grammar and a detailed explanation in Appendix D The dataset LTL- synthesis consists of pairs of natural language translation with our grammar (see Appendix D) and their LTL. hardware synthesis specification. These hardware synthesis specifications are taken from a recently published dataset, where the authors trained Transformer to predict hardware circuits directly from LTL specifications (Schmitt et al. 2021). The synthesis specifications consist an LTL formula expressing the assumptions posed on the environment and an LTL formula expressing the desired guarantees of the system. They can be combined into single LTL formula by implication.
EXPERIMENTS
We fine-tuned the base version of the open-source language model T5 Raffel et al. (2020) with 220 million parameters on an NVIDIA DGX A100 system for around hour each run with a learning rate of 0.001. We needed use the small 1 version for our bascline experiments on an untrained T5 model to achieve stable training. We use Py PyTorch (Paszke et al.) 2019) and the huggingface transformers library (Wolf et al.) 2020) to fine-tune the models. We report accuracy of the best- pest-performin models (see Appendix A for ablations). In general, achieving stable training for the baseline T5 model was challenging and required much more engineering effort compared to the pre-trained version of T5 (c.f Figure 3) We split the data into 90% training. 5% validation, and 5% test data. Table I summarizes the test results. We used the following prompt, respectively: "translate natural language regular expression):
to (FOL I LTL
4.1 REGULAR EXPRESSIONS
New state-of-the-ari by semantic generalization. The fine-tuned language model achieves a new state-of-the-art in translating natural language regular expressions both datasets. This even holds true when comparing against state-of-the-arr reinforcement learning approaches (Zhong et al.) 2018, Park et al. 2019); indicated in Table by (RL). A natural language sentence has multiple correct translations into a regular expression. For example, the following prediction is correct, yet different from the training target:
natural language description model prediction (correct)
lines starting with character followed by vowel, 7 or more times ((.. (.*"AAEOUaeioo) +)
training target
((. (A.'(AEEOUeeioou) (), (77,))
5

---

Under review as a conference paper at ICLR 2023
To account for such predictions, the accuracy of the regex models is evaluated with equivalence check, called semantic accuracy Locascio et al. (2016). On the synthetically generated dataset Regex-syythheiic the LM achieves 94.01% semantic accuracy; the Regex-turk dataset, the language model achieves 64.20% semantic accuracy. Due to the model's generalization to the semantic, its performance increased from 90.62% to 94.01% and 47.00% 64.20%, respectively, being the decisive factor in beating the state-of-the-art. This is exceptionally substantial on the Regex- dataset. Figure (top left) depicts the accuracy per sequence of the best performing models during training. While the baseline model achieves the same accuracy (with longer training) on Regex-synthet
the pre-trained model outperformes the baseline on Regex-tuz by significant margin. Note that we incorporate no additional training objective in contrast to previous work (Zhong et al. 2018: Park et al. 2019).
Generalization to new nouns. The high accuracy of the fine-tuned LM on this task poses the question the model does "forget" its knowledge of the natural language during fine-tuning (see, e-g.. He et al. (221I). In this experiment, we tested the models generalization English nouns that were not present during fine-tuning, but certainly during pre-training. Figure 2 shows the results this experiment for the pre-trained T5 model (left) and the baseline T5 model (right). The first three nouns are the ones present in the datasets, i.e., "dog", "truck", and "ring". When minettunigg on only four nouns, by adding another commonly used noun, namely "time", the model generalizes seamlessly to 16 nouns. The additional nouns were drawn from the 25 most common English nouns. Unsurprisingly, the baseline T5 model shows limited generalization capabilities to novel nouns and the pre-trained model consistently performs better, also for less nouns during training. Figure 3 (bottom right) shows the accuracies on the respective validation set. A similar observation can be made when testing on numbers that were not present during fine-tuning:
natural language description lines with the string 'dog' or letter, 9 or more times model prediction (correct) ((dog))(AA77a-7)))
OOD-testing across datasets. As a final experiment in the regex domain, we cross-tested the models on the regex datasets. Such -iitt--distriuutinn (OOD) tests are known to be challenging for neural networks. It is especially interesting if a model trained on Regex-synthet hetic, ic, which is purely synthetic, can translate instances of Regex- trained on the syntactic data achieved a semantic accuracy of 49.4992200 49.20%, which is only 15 percentage points behind the models accuracy that was trained on this dataset, and only percentage points behind the previous state-of-the-art. Interestingly, the model can interpret ambiguous natural language sentences differently than its human counterpart and even corrects buggy targets, probably due to being trained on slightly diffeernnt dataset. For example:
which constructed by humans. The model
natural language description
lines with number that comes before a letter, and a vowel, and the string 'dog' ([0-9]). (IZTAAAAZZZZIIKKAAAAUUUUUUOOOOOO ((AEEIO (X00))))((((oo00(0000000")""))1) ([A-Za-z]).
model prediction ("incorrect") training target
In the "easier" direction, the model trained on Regex-turk achieved an accuracy of 83.83% falling only 10 percentage points short behind the model trained on this dataset and percentage points
Table I:
Accuracy of the best runs for fine-tuned T5 language models on held-out test sets, where steps denote the number of training steps; accuracy is reported as the accuracy per sequence.
dataset
previous SOTA
baseline T5 (steps)
fine-tuned T5 (steps)
Regex-synthetic.
88.7 91.6 (RL)
94.01 (5K)
94.01 (IK)
Regex-turk
58.2 62.8 (RL)
58.0 (5K)
64.20 (IK)
FOL-mnli
56.10 (estimated)
46.87 (10K)
53.91 (5K)
FOL-codesc
58.59 (10K)
58.98 (3K)
LTL-pattern
100.00 (5K)
100.00 (1K)
LTL-synthesis
87.50 (5K)
87.90 (IK)

---

Under review as a conference paper at ICLR 2023
40.12
$3.00
21.86
91-82
18,
3192
40:31
60:43
39.12
50.30
50:12
45.71
63
25.00
89:22
90.42
43.91
$5.29
20.46
$7.22
59:02
85
Anoonss
69.66
92.42
91.62
37.02
61
18-03
10.60
15
88
180
85
20.02
16
#nouns in training data
Amouns in training data
Figure 2: Syntactic accuracy of pre-trained T5 regex models (left) and baseline T5 regex models (right) trained on variations of Regex Regex-synthet. ic with proper subsets of nouns.
behind the previous state-of-the-art. However, it is only fair to note that T5 was trained internet corpus, making it likely that the model has seen regular expressions during pre-training, which probably contributes to the model's high accuracy. In the next sections, will consider FOL and LTTL, where it is much more unlikely that the network has seen many instances during pre-training.
4.2 FIRST-ORDER LOGIC (FOL)
Comparability the state-of-the-art (Singh al. (2020) achieved an estimated semantic accuracy of 56.10% on their 138K large dataset with a specialized architecture and an array of optimizations. Their dataset is similarly constructed as 150K large dataset FoL-mnli, but they heuristically estimate their semantic accuracy with a matching algorithm. For best reprodueibility, we thus only report on the syntactic accuracy of T5 in this paper as, the time of writing, their dataset and code were not publically available. Their FOL formulas are represented as reduced mapping of the candc-boxer output while we train on the raw output end-to-end in this work. On held- out dataset, the fine-tuned LM achieved a syntactic accuracy of 53.91% %, falling only percentage points short of the semantically estimated state-of-the-ee constructed to mimic code snippets, our best model achieved an accuracy of 58.98% (see 3 right). will be interesting to see how specialized approaches perform on this new dataset. Since this is a newly contributed dataset, we provide two randomly sampled successful and failed translation attempts while evaluating the best model on held-out test set of FOL-
On the FOL-codes dataset, which was
natural language description model prediction (correct)
choose an available port fol(1, (A,D). ( and(rl Actor and(al aaailallvailbbl(1] Oato0://a.aaaeaaooooooo/ooaaaaaa
natural language description model prediction (incorrect)
show start page fol(1,some( (-soaeeeesssseCeCaaooooaaCCaaaaa and(n (ataaaatt(A,n.nddii http://awwccaccc//aaaaaaooaaaaaa
OOD-testing across datasets. We experiment again with cross-testing in the FOL domain to report the performance model trained on everyday natural language (FOL-mnli) to the specialized domain of code (POL-codesc) Note that, compared to the regex experiment, the domains considered in these datasets are much more different. model trained on FOL-mnli achieved an accuracy of 31.25% when tested on the code comment examples from FOL-codesc. Vice versa, model achieved an accuracy of 10.55%. This accuracy decreases drastically for the baseline model, achieving only 19.92% and 0%, respectively. Our experiments indicate that pre-trained language models used for code generation can translate its input into formal specifications, which formally represent their language understanding. They thus remove ambiguity and automatically formalize their input. Our long-term vision is that this additional output can be used to increase the trust in the code model's output. With the FOL-codess dataset, we aim make the first contribution toward this goal.
7

---

Under review as a conference paper at ICLR 2023
Accuracy per sequence
Accuracy per sequence
Regex-tur turk baseline Rygex-syythetic baseline
FOL-mii baseline
FOL JoL-nn11
FOL-codesc baseline
Regex synthetic Regex-ture turk
Fod-cc
0.8
0.6
0.5
Ayply www.mna
0.6
M Pale
0.1
Step
Step
0
1k
2k
4k
5k
2k
6k
8k
10k
Accuracy per sequence
Accuracy per sequence
LTT syntthest baseline
TT -synthesss
nouns baseline
nouns nouns basel noun basellee Line 1 noun
LTL ppattert baseline
LT) -pattorn
nouns
0.6
0.6
0.4
0.4
0.2
Step
Step
1k
2k 3k
4k
5k
1k
2k
3k
4k
5k
Figure 3: Respective accuracy per sequence validation sets during training of the best performing models reported in Table | sequence for the new nouns experiment (bottom right).
Regex (top left), FOL (top right), LTL (bottom left); and the accuracy per
4.3 LINEAR-TIME TEMPORAL LOGIC (LTL)
New baseline and challenging datasets for L.7.. The language model performed well on the task of translating natural language into LTL specifications as it seems to benefit from the models generalization capabilities from pre-trained knowledge on natural language (see Figure bottom left). The LTL SELL-pateern dataset serves baseline, where the language model achieves accuracy of 100.00% by probably learning the underlying grammar. The LTL-synthes dataset, however, is designed to be more challenging. It contains combination of practical specifications to automatically synthesize hardware circuits Schmitt et al. (202T). For example:
FigureBbottom
natural language description
Globally it is the case that if o4 holds and in the next step i0 does not hold then in the next step holds and ol does not hold until il does not hold or globally ol does not hold and globally o3 holds. ((((())) A (O( ((o))) - (O(o)))))
model prediction (correct)
(o ((()))) ((T(0))))
On these large instances, the language model achieves an accuracy of 87.50% Failed translation attempts are, in general, due to the large size of the instances often overshooting the size limit of our language models. This experiment is especially interesting, since combining our approach with the approach of (Schmitt et al. (2021) would enable the developement of tool that synthesizes sequential hardware eircuits automatically out natural language. Final circuit predictions can then be model-checked or tested against the intermediate LTL formalization of the natural language.
Generalization to new variable names. We observed that the models are also able to process new variable names. Altough the models were fine-tuned a fixed set of variables (io....,f 14 and Og.... O2 for LTL-synthess to correct translations. A model trained on LT--pattern achieved accuracy of 95.00% when being tested on held-out instances where all variables were replaced with random letters from the alphabet. See Figure T in the introduction and the following example:
and c...., e for LTL-pat eenn using other variables also led
8

---

Under review as a conference paper at ICLR 2023
natural language (ID)
Globally it is the case that a holds then eventually a and b hold.
model prediction (correct)
[ + (a A 6))
natural language (OOD)
If holds infinitely often then y holds infinitely often.
model prediction (correct)
y
OOD-testing across datasets. We OOD cross-tested on the LTL datasets. Interestingly, only one of the directions showed generalization. We tested a model, trained on LTL LTL-pattern, on large instances from the synthesis specifications in LTI LTI-synthesis direction achieved an accuracy of 3. 3.12%. However, in the other direction, i.e., model trained on LTttsyythesi s and tested on LTL-pattern achieved an accuracy of 17.11%. we conduct the same experiment with the baseline model, the accuracy drops to 0% and 7.81%, respectively.
model trained and tested in this
Generalizution to new operator descriptions. Lastly, we quantitatively measured the generalization of L.TL models to new operator descriptions, which were kindly provided by uninvolved experts, by adding them to our translation grammar. We build two grammars, one with the additional operator descriptions and one without them (see Appendix D). Translations are then randomly chosen. A model trained on the grammar only consisting of single translation for each operator achieved an accuracy of 53% when being tested on instances generated with the enriched grammar. For example:
natural language description
Always it is the case that if o2 holds then always il does not hold.
model prediction (correct)
(o2) - O (-(1)))))
An additional example is the test instance hand-crafted by expert shown in Figure T Section 1 where the model recognizes "whenever" as the L--oprrator and the comma as the very subtle repre- sentation of implication, both of which are not even captured by our enriched grammar. A possible use-case in this domain is the automatic formalization of software and hardware requirements from natural language to formal LTL specifications.
5 LIMITATIONS AND CONCLUSION
A limiting factor is that our approach still requires GPU with enough memory to fit the language model, which detracts from its general accessibility. We set out to demonstrate the applicability of language models to wide variety of formal domains. Nevertheless, many interesting domains are of this work's scope but still viable targets for our approach. These include theorem proving, SQL translations, logical programming, SAT, and SMT. Another limitation is the focus on one particular class of language models. A possible further research direction is to explore the capabilities of decoder-only models such as the GPT-2 model family. Many datasets considered in this work are purely synthetic (which is only natural for the considered domains). Hence, a practical next step is encouraging experts contribute open-source data in their respective domains. A final limitation is the unfeasibility of proper comparisons with existing works, e.g., due to unavailable datasets. With this work, we contribute an open-source gathering of existing datasets to conduct further research.
To conclude, we conducted the first study on the generalization capabilities of fine-tuned language models to translate natural language into formal specifications, resulting in a new state-of-the-ar for translating natural language into regular expressions. The benefits of fine-tuning an open-source language model are that they are easily accessible and cheap train. We contributed two new datasets for translating natural language into First-order Logic and two new datasets for translating natural language into Linear-time Temporal Logic. We provided experiments on the generalization capabilities of the pre-trained language model T5, which serves baseline for further research. Our experimental results show that off-the-shelf language models can outperform approaches on existing datasets and perform well on new datasets. The language models prove themselves to be highly versatile. A unique selling point is their capability of generalizing from pre-trained knowledge of natural language, such as handling other variable names, new nouns, and new operator descriptions. We believe that the generalization capabilities of language models can be crucial in making real- world problems of translating natural language formal specifications tractable.

---

Under review as a conference paper at ICLR 2023
6 REPRODUCIBILITY STATEMENT
The code, datasets, models, and notebooks for reproducing the experiments will be made publicly available once the double-blind reviewing process ends. One of the main goals of this work was to study a translation approach that is as accessible as possible. Consequently, we have used an off-the-shelf language model that is both open-source and requires significantly less memory than very large language models. Additionally, we found that, compared to training an LM from scratch, fine-tuning has been proven robust, making this approach prriddduiibbitt--rrendi
REFERENCES
Alfred V Aho. Algorithms for finding patterns in strings, handbook of theoretical computer science (vol. a): algorithms and complexity, 1991.
Gilles Audemard and Laurent Simon. On the glucose sat solver. International Journal on Artificial Intelligence Tools, 27(01):1840001, 2018.
Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. Cvc4. In International Conference on Computer Aided Verification, pp. 171-177. Springer, 2011.
Gerd Behrmann, Alexandre David, Kim Guldstrand Larsen, John Häkansson, Paul Pettersson, Wang Yi, and Martijn Hendriks. Uppaal 4.0. 2006.
Yves Bertot and Pierre Castéran. Interactive theorem proving and program development: Coq Art: the calculus of inductive constructions. Springer Science & Business Media, 2013.
Armin Biere et al. Lingeling, plingeling and treengeling entering the sat competition 2013. Proceed- ings of SAT competition, 2013:1, 2013.
Aaron Bohy, Véronique Bruyere, Emmanuel Filiot, Naiyong Jin, and Gean-François Raskin. Acaciat, a tool for LTL synthesis. In International Conference on Computer Aided Verification, pp. 652-657, Springer, 2012.
Johan Bos. Open-domain semantic parsing with boxer. Proceedings of the 20th nordic conference of computational linguistics (NODALIDA 2015), pp. 301-304, 2015.
Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neclakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. Language models are few-shot learners. Advances in neural information processing systems, 33:1877-1901, 2020.
Andrea Brunello, Angelo Montanari, and Mark Reynolds. Synthesis of Itl formulas from natural language texts: State of the art and research directions. In 26th International Symposium on Temporal Representation and Reasoning (TIME 20/9). Schloss Dagsuhh-LeibmizzzZennn fuer Informatik, 2019.
Jan Buys and Phil Blunsom. Robust incremental neural semantic graph parsing. arXiv preprint arXiv: 07092, 2017.
Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al. Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374 2021.
Jianeeng Cheng, Siva Reddy, Vijay Saraswat, and Mirella Lapata. Learning structured natural
language representations for semantic parsing, arXiv preprint arXiv: 2017.
Himaja Cherukuri, Alessio Ferrari, and Paola Spoletini. Towards explainable formal methods: From Itl to natural language with neural machine translation. In International Working Conference on Requirements Engineering: Foundation for Software Quality, pp. 79-86. Springer, 2022.
Aakanksha Chowdhery, Sharan Narang, Jacob Devlin, Maarten Bosma, Gaurav Mishra, Adam Roberts, Paul Barham, Hyung Won Chung, Charles Sutton, Sebastian Gehrmann, et al. Palm: Scaling language modeling with pathways. arXiv preprint arXiv:2204.02311 2022.
10

---

Under review as a conference paper at ICLR 2023
Alessandro Cimatti, Edmund Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiami, and Armando Tacchella. Nusmv 2: An opensource tool for symbolic model checking. In International conference computer aided verification, pp. 359-364. Springer, 2002.
Stephen Clark and James R Curran. Parsing the wsj using cog and log-linear models. Proceedings of the 42nd Annual Meeting of the Association for Computational Linguistics (ACL-04), pp. 103-110, 2004.
Linhao Dong, Shuang Xu, and Bo Xu. Speech-transformer:: a no-recurrence sequence-to-sequenee model for speech recognition. In 2018 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP), pp.
IEEE, 2018
Alexey Dosovitskiy, Lucas Beyer, Alexander Kolesnikov, Dirk Weissenborn, Xiaohua Zhai, Thomas Unterthiner, Mostafa Dehghani, Matthias Minderer, Georg Heigold, Sylvain Gelly, et al. An image is worth 16x16 words: Transformers for image recognition at scale. arXiv preprint arXiv:2010.11929, 2020.
Alexandre Duret-Luiz, Alexandre Lewkowiez, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Laurent Xu. Spot 2.0 a framework for LTL and w-automata manipulation. Proceedings of the 14th International Symposium Automated Technology for Verification and Analysis (ATVA' 16), volume 9938 of Lecture Notes in Computer Science, pp. 122-129, Springer, October 2016. doi: 10.1007/978-33 3-788---339---88 3--11-46552-333
Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Property specification patterns for finite-state verification. Proceedings of the Second Workshop on Formal Methods in Software Practice, March 4-5, 1998, Clearwater Beach, Florida, USA, pp. 7-15. ACM, 1998. doi: 10.1145/298595.298855
Kousha Etessami and Gerard Holzmann. Optimizing büchi automata. In Catuscia Palamidessi (ed.), CONCUR 2000 Concurrency Theory, 11th International Conference, University Park, PA. USA, August 22-25, 2000, Proceedings, volume 1877 of Lecture Notes Computer Science, pp. 153- Springer, 2000. doi: 10.1007/3-540-44618 13. URL http:::///oi.orooggooo 4007/3-540-4468-11
Peter Faymonville, Bernd Finkbeiner, and Leander Tentrup. BoSy: An experimentation framework for bounded synthesis. In International Conference Computer Aided Verification, pp. 325-332.
Springer, 2017.
Pau Fonseca
Casas, Xavier Pi, Josep Casanovas, and Jordi Jové. Definition of virtual reality simulation models using specification and description language diagrams. In International SDL Forum, pp. 258-274. Springer, 2013.
Ivan Gavran, Eva Darulova, and Rupak Majumdar. Interactive synthesis of temporal specifications from examples and natural language. Proceedings of the ACM on Programming Languages, (00PSLA)):1266, 2020.
Lars Grunske. Specification patterns for probabilistic quality properties. In 2008 ACM/IEEE 30th International Conference Software Engineering, pp. 31-40. IEFE, 2008.
Christopher Hahn, Frederik Schmitt, Jens U, Kreber, Markus N. Rabe, and Bernd Finkbeiner. Deeplti, 2020. URL
systaacrrieeessteeeeeeeeeee wwstemsstttsssssee /eepltt
Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus N. Rabe, and Bernd Finkbeiner. Teach- ing temporal logics to neural networks. International Conference on Learning Representations, ICLR, 2021.
Simeng Han, Hailey Schoelkopf. Yilun Zhao, Zhenting Qi, Martin Riddell, Luke Benson, Lucy Sun, Ekaterina Zubova, Yujic Qiao, Matthew Burtell, et al. Folio: Natural language reasoning with first-order logic. arXiv preprint arXiv:2209.00880 00840. 2022.

---

Under review as a conference paper at ICLR 2023
Masum Hasan, Tanveer Muttaqueen, Abdullah Al Ishtiaq, Kazi Sajeed Mehrab, Md. Mahim Anjum Haque, Tahmid Hasan, Wasi Ahmad, Anindya lqbal, and Rifat Shahriyar. CoDesc: large dederdesciiition parallel dataset. In Findings of the Association for Computational Linguistics: ACI-IJCNILP 2021, pp- 210-218, Online, August 2021. Association for Computational Linguis- http://///0......nnnnaaaa.l//// URL ptttps:/acclannthol..g 00002220 2021
tics. doi: 10.18653/v1/200
Findings saccings-ac.118
Jie He, Ezio Bartocci, Dejan Ničković, Haris Isakovic, and Radu Grosu. Deepstl-from english requirements to signal temporal logic. In 44th International Conference on Software Engineering (ICSE 2022), 2022.
Tianxing He, Jun Liu, Kyunghyun Cho, Myle Ott, Bing Liu, James Glass, and Fuchun Peng. Analyz- ing the forgetting problem in pretrain finetuiiinn of open- open-domain dialogue response models. In Proceedings of the 16th Conference of the European Chapter of the Association for Computational Linguistics: Main Volume, pp. 1121-1133, 2021.
Vincent J. Hellendoorn, Charles Sutton, Rishabh Singh, Petros Maniatis, and David Bieber. Global relational models source code. 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net, 2020. URL https:
//openreview net. fattt//oormmiddBBe
Gary G Hendrix, Earl D Sacerdoti, Daniel Sagalowicz, and Jonathan Slocum. Developing a natural language interface to complex data. ACM Transactions on Database Systems (TODS), 3(2): 105-147, 1978.
Jan Holečck, Tomáš Kratochvila, Vojtëch Rehák, David Šafránek, Pavel Šimečck, et al. Verification results in Liberouter project, 2004.
Gerard J. Holzmann. The model checker spin. IEEE Transactions on software engineering, 23(5): 279-295, 1997.
SEEE-Commission et al. IEEE standard for property specification language (PSL). IEEE Std 1850-2005, 2005.
Daniel Jackson. Alloy: lightweight object modelling notation. ACM Transactions on software engineering and methodology (TOSEM), 11(2):256-290 2002.
Tim Johnson. Natural language computing: the commercial applications. The Knowledge Engineering Review, 1(3):11-23, 1984.
Aishwarya Kamath and Rajarshi Das. A survey on semantic parsing, arXiv preprint arXiv:1812.00977. 2018.
Hans Kamp and Uwe Reyle. From discourse to logic: Introduction to modeltheoretic semantics of natural language, formal logic and discourse representation theory, volume 42. Springer Science & Business Media, 2013.
Stephen C Kleene et al. Representation of events in nerve nets and finite automata. Automata studies, 34:3-41, 1956.
Tomáš Kočiský, Gábor Melis, Edward Grefenstette, Chris Dyer, Wang Ling, Phil Blunsom, and Karl Moritz Hermann. Semantic parsing with semi-supervised sequential autoencoders. arXiv preprint 16Xiv:1609.000
2016.
Sascha Konrad and Betty HC Cheng. Real-time specification patterns. In Proceedings of the 27th international conference on Software engineering, pp. 372-381, 2005.
Nate Kushman and Regina Barzilay. Using semantic unification to generate regular expressions from natural language. In Lucy Vanderwende, Hal Daumé III, and Katrin Kirchhoff (eds.), Human Language Technologies: Conference of the North American Chapter of the Association of Computational Linguistics, Proceedings, June 9-14. 2013, Westin Peachtree Plaza Hotel, Atlanta, Georgia, USA, pp. 826-836. The Association for Computational Linguistics, 2013. URL ott.ol//1.o11/11110010000
12

---

Under review as a conference paper at ICLR 2023
Tom Kwiatkowksi, Luke Zettlemoyer, Sharon Goldwater, and Mark Steedman. Inducing probabilistic oeg grammars from logical form with higher- order unification. In Proceedings of the 2010 conference on empirical methods in natural language processing. pp. 1223 2223-133, 2010.
Guillaume Lample and François Charton. Deep learning for symbolic mathematics. In 8th Interna- tional Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net, 2020.
Steven Lalalee. Planning algorithms. Cambridge university press, 2006.
Aitor Lewkowyez, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Ra- masesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, et al. Solving quantitative reasoning problems with language models. arXiv preprint arXiv: 14858, 2022.
Jianwen Li, Lijun Zhang, Geguang Pu, Moshe Y. Vardi, and Jifeng He. LTL satisfiability checking revisited. In César Sánchez, Kristen Brent Venable, and Esteban Zimányi (eds.), 2013 20th Inter- national Symposium on Temporal Representation and Reasoning, Pensacola, FL, USA, September 26-28, 2013, pp. 91-98. IEEE Computer Society, 2013. doi: 10.1109/1IE:2203..119 URL https:///oii http:///aa....1.100..1111111111. 200109991...213..15.
2013.19
Yujia Li, David Choi, Junyoung Chung, Nate Kushman, Julian Schrittwieser, Rémi Leblond, Tom Eccles, James Keeling, Felix Gimeno, Agustin Dal Lago, et al. Competition-level code generation with alphacode. arXiv preprint arXiv:2203. 078114 2022.
Zuchao Li, Jiaxun Cai, Shexia He, and Hai Zhao. Seq2seq dependency parsing. In Proceedings of the 27th International Conference on Computational Linguistics, pp. 3203-3214, 2018.
Jangminn Liu, Shay Cohen, and Mirella Lapata. Discourse representation structure parsing. In Proceedings of the 56th Anmual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 429-439 2018
Nicholas Locascio, Karthik Narasimhan, Eduardo Del Nate Kushman, and Regina Barzilay. Neural generation of regular expressions from natural language with minimal domain knowledge. In Jian Su, Xavier Carreras, and Kevin Duh (eds.), Proceedings of the 2016 Conference Empirical Methods in Natural Language Processing, EMNLP 2016, Austin, Texas, USA, November 144, 2016, pp. 1918 1923. The Association for Computational Linguistics, 2016. doi: 10. 111865//11dd1--1199 URL https: //oi: wtt.a/o..........1///////////...
Philipp J. Meyer, Salomon Sickert, and Michael Luttenberger. Strix: Explicit reactive synthesis strikes back! In Computer Aided Verification 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford. UK, July 14-17, 2018, Proceedings, Part I, volume 10981 of Lecture Notes in Computer Science, pp. 578-586. Springer, 2018. doi: 10. 11100779778-3319-611444
Leonardo de Moura and Nikolaj Björner. 73: An efficient smi solver. In International conference on Tools and Algorithums for the Construction and Analysis Systems, pp. 337-340. Springer, 2008
Erik Nijkamp, Bo Pang, Hiroaki Hayashi, Lifu Tu, Huan Wang, Yingbo Zhou, Silvio Savarese. and Caiming Xiong. A conversational paradigm for program synthesis. arXiv preprins 1xXi::2203.13474 2022.
Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. Isabelle/HOL: a proof assistant for higher-order logic. Springer, 2002.
Jun-U. Park, Sang-Ki Ki Ko, Marco Cognetta, and Yo-Sub Han. Softregex: Generating regex from natural language descriptions using softened regex equivalence. In Kentaro Inui, Jing Jiang, Vincent Ng. and Xiaojun Wan (eds.), Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference on Natural Language Processing. EMNLP-IJCNLP 2019, Hong Kong. China, November 3-7, 2019, pp. 6424 6430. Association for Computational Linguistics, 2019. doi: 10.18653//1/DI1-16617 URL https: 1ttp://0001116/////1/11111111111
13

---

Under review as a conference paper at ICLR 2023
Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Kopf, Edward Yang. Zachary Vito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang. Junjie Bai, and Soumith Chintala. Pytorch: An imperative style, high-performance deep learning library. In H. Wallach, H. Larochelle, A. Beygelzimer, F. d' d'Alché-Bil E. Fox, and R. Garnett (eds.), Advances in Neural Information Processing Systems 32, pp. 8024-8035. Curran Associates, Inc., 2019.
Roma Patel, Roma Pavlick, and Stefanie Tellex. Learning ground language to temporal logical form. NAACL, 2019.
Charles S. Peirce. The Collected Pupers of Charles Sanders Peirce, Vol. IV: The Simplest Mathematics. Harvard University Press, Cambridge, 1933.
Radek Pelánek. BEEM:
benchmarks for explicit model checkers. In Dragan Bosnacki and Stefan Edelkamp (eds.), Model Checking Software, 14th International SPIN Workshop, Berlin, Germany, July 1-3, 2007, Proceedings, volume 4595 of Lecture Notes in Computer Science, pp. 263 Springer, 2007. doi: 10. 0007/998--3540-733770000 17. URL 0rtp://///ooi..//11.00000.0 1978 3- 0-40-7337--6 6
Amir Pnueli.
The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October- 1 November 1977, pp. 46-57. IEEE Computer Society, 1977. doi: 10. 10.11099SFCS.1177..2 URL
1109/ /T.9//FCS... 1977.32
Stanislas Polu and Ila Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020.
Markus N. Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical reasoning via self-supervised skip-tree training. 2020.
Colin Raffel, Noam Shazeer, Adam Roberts, Katherine Lee, Sharan Narang, Michael Matena, Yanqi Zhou, Wei Li, and Peter J. Liu. Exploring the limits of transfer learning with unified text-to- text transformer. J. Mach. Learn. Res., 21:140:1-140ss 2020. URL
papers/v21/20 074 html
Aarne Ranta. A multilingual natural- -anguual- interface regular expressions. In Finite State Methods in Natural Language Processing, 1998. | /atp::/aallaaaa ///aaaaaanthhooooo org/w98 1108
Baptiste Roziere, Marie-Ama Lachaux. Lowik Chanussot, and Guillaume Lample. Unsupervised translation of programming languages. Advances in Neural Information Processing Systems, 33: 20601-20611, 2020.
David Saxton, Edward Grefenstette, Felix Hill, and Pushmeet Kohli. Analysing mathematical reasoning abilities of neural models. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA. May 6-9, 2019. OpenReview.net, 2019. |
Imanol Schlag, Paul Smolensky, Roland Fernandez, Nebojsa Jojic, Jürgen Schmidhuber, and Jianfeng Gao. Enhancing the transformer with explicit relational encoding for math problem solving. arXiv preprint
1, 2019.
Frederik Schmitt, Christopher Hahn, Markus N. Rabe, and Bernd Finkbeiner. Neural circuit synthesis from specification patterns. In Mare' Aurelio Ranzato, Alina Beygelzimer, Yann N. Dauphin, Percy Liang, and Jennifer Wortman Vaughan (eds.), Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurlPS 2021, December 6-14, 2021, viriual, pp. 1 15408 15420, 2021. URL. htRp:ttttppss/prreeeeemmg i neur ps. cc/ httee/hhhhhaaae 82 3 30bea 7d5 220.0eee00.3ad001114444553311110 -ww.:aas--bbbttttto .tt.raacchmmllll
Daniel Selsam and Nikolaj Bjørner. Guiding pirf-performance SAT solvers with unsat-core pre- dictions. In Theory and Applications of Satisfiability Testing SAT 2019 22nd International Conference, SAT 2019. Lisbon, Portugal, July 9-12, 2019, Proceedings, volume 11628 of Lecture Notes in Computer Science, pp. 236-353. Springer, 2019. doi: 10. 111110079978--000-244
14

---

Under review as a conference paper at ICLR 2023
Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. Learning a SAT solver from single-bit bit supervision. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019.
Hrituraj Singh, Milan Aggrawal, and Balaji Krishnamurthy. Exploring neural models for parsing natural language into first-order logic. arXiv preprint wxXiv2202.06554. 2020.
Niklas Sorensson and Niklas Een. Minisat vl. 13-a sat solver with conflict-clause minimization. SAT, 2005(53):1-2, 2005.
Mark Steedman. The syntactic process. MIT press, 2001.
Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. In International Conference on Intelligent Computer Mathematics, pp. 3-20. Springer, 2020.
Marjorie Templeton and John F Burger. Problems in natural-language interface to dbms with examples from eufid. In First Conference on Applied Natural Language Processing, pp. 3-16, 1983.
Wolfgang Thomas. Automata on infinite objects. In Formal Models and Semantics, pp. 133-191. Elsevier, 1990.
Cynthia Thompson.
Acquiring word-meaning mappings for natural language interfaces. Journal of Artificial Intelligence Research, 18:1-44, 2003.
Frederick Thompson, Peter Lockemann, B Dostert, and RS Deverill. Rel: A rapidly extensible language system. In Proceedings of the 1969 24th national conference, pp. 319-399-117 499,417,55 1969.
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett (eds.), Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, pp. 5998-6008, 2017. URL httph: htttpp://poocceediigg www.diinnnnnnnnnnneoeeeeemm neurips waaascc/ppae cc/paper/20177 2017hhash/ / Abst Absttaaaatbbaaaaaattttt......... html
David L Waltz. An english language question answering system for a large relational database. Communications of the ACM, 2177):226-33, 1978.
Christopher Wang, Candace Ross, Yen-Ling Kuo, Boris Katz, and Andrei Barbu. Learning a natural- language to Itl executable semantic parser for grounded robotics. arXiv preprint arXiv:2008.03277, 2020.
Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. First experiments with neural translation of informal formal mathematies. In International Conference Intelligent Computer Mathematics, pp. 255-270. Springer, 2018.
Joseph Weizenbaum. Eliza computer program for the study of natural language communication between man and machine. Communications of the ACM, 9(1):36 45, 1966.
Adina Williams, Nikita Nangia, and Samuel R. Bowman. A broad-coverage challenge corpus for sentence understanding through inference. In Marilyn A. Walker, Heng Ji, and Amanda Stent (eds.), Proceedings of the 2018 Conference of the North American Chapter of the As- sociation for Computational Linguistics: Human Language Technologies, NAACL-HLT 2018, New Orleans, Louisiana, USA, June 1-6, 2018, Volume (Long Papers), pp. 1112-1122. As- sociation for Computational Linguistics, 2018. doi: 10.18653/v1/118-1100. URL https?
moooi.org/10.oo http://...1653//1//ea/ -1001
Temy Winograd. Procedures representation for data in computer program for understanding nat- ural language. Technical report, MASSACHUSETTS INST OF TECH CAMBRIDGE PROJECT
MAC, 1971.
15

---

Under review as a conference paper at ICLR 2023
Thomas Wolf, Lysandre Debut, Victor Sanh, Julien Chaumond, Clement Delangue, Anthony Moi, Pierric Cistac, Tim Rault, Remi Louf, Morgan Funtowicz, Joe Davison, Sam Shleifer, Patrick von Platen, Clara Ma, Yacine Jernite. Julien Plu, Canwen Xu, Teven Le Scao, Sylvain Gug- ger, Mariama Drame, Quentin Lhoest, and Alexander Rush. Transformers: State-of-the-art natural language processing. In Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing: System Demonstrations, pp. 38-45, Online, October 2020. Association for Computational Linguistics. doi: 10. 10.118633/v 11203/0000220.m.p-eeeeeee. https: aclaalann http:///aaaattthogoocooo org/ 2020. wmw.eedemss........mmommmm
URL
William A Woods. Progress in natural language understanding: an application to lunar geology. In Proceedings of the June 4-8, 1973, national computer conference and exposition, pp. 441-450, 1973.
Yuhuai Wu, Albert Q Jiang. Wenda Li, Markus N Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. arXiv preprint arXiv:2205. 12615, 2022.
Xi Ye, Qiaochu Chen, Xinyu Wang, Isil Dillig, and Greg Durrett. Sketch- regular expression generation from natural language and examples. Trans. Assoc. Comput. Linguistics, 8:679- 694, 2020. URLhtttp http::ss///raaaac/ .rgg o o ndex. 2135
ew
John M Zelle and Raymond J Mooney. Learning to parse database queries using inductive logic programming. In Proceedings of the national conference artificial intelligence, pp. 1050-1055, 1996.
Luke Zettlemoyer and Michael Collins. Online learning of relaxed ecg grammars for parsing to logical form. In Proceedings of the 2007 Joint Conference on Empirical Methods in Natural Language Processing and Computational Natural Language Learning (EMNLP-CoNLA) pp. 678-687, 2007.
Luke S Zettlemoyer and Michael Collins. Learning to map sentences to logical form: Structured classification with probabilistic categorial grammars. arXiv preprint arXiv: I2rXiv:207.... 1420, 2012.
Zexuan Zhong, Jiaqi Guo, Wei Yang, Jian Peng, Tao Xie, Jian-Guang Lou, Ting Liu, and Dongmei Zhang. Semregex: A mamantics-based approach for generating regular expressions from natural language specifications. In Ellen Riloff, David Chiang, Julia Hockenmaier, and Jun 'ichi Tsujii (eds.), Proceedings of the 2018 Conference on Empirical Methods Natural Language Processing, Brussels, Belgium, October 31 November 4, 2018, pp. 1608-1618, Association for Computational Linguistics, 2018. doi: 1//11///////1-/.../ 189. URL https: //doi org /10. 1tt.//.0..111//// d18-1189
16

---

Under review as a conference paper at ICLR 2023
A ABLATIONS
We reported only a selected number of trained models and conducted experiments. We tried to avoid the report of duplications, where the model shows similar behavior across all domains (such as the generalizaion to new nouns), with the exception being the OOD cross-testing, which is an interesting insight for all considered domains. The code as well as the datasets will be made publically available. We did several ablation studies while looking for the best performing models and performed hyperparameter search for every reported model. The most influential hyperparameter for the baseline models is the learning rate. In Figure we show the influence of different learning schedules on the accuracy per sequence for the FOL- codesc dataset. When finetuning T5 models we used constant learning rate of 0.001. We also experimented with larger and smaller models, since pretrained T5 models are available in different sizes. In general, the base model with 220 million parameters performed best when finetuning. Furthermore, when finetuning for longer than a few thousand steps (depending on the size of the dataset between 1K to 3K steps), which takes around 3 hours of training experimented with prompting. We observed a significant (around 3% 5%) decrease in performance when omitting the prompt. Additional experiments with the prompt, for example prompting with "Translate the following English sentence to lead to no significant increases or decreases in performance.
observed significant increase in performance
A100 for each run. Additionally,
Accuracy per sequence
c- 1-33-5u-114 14
c-3-t5u-13
c-3-t5u-12
- c-3-t5u-11
c-3-t5u-10
c-3-t5u-9
c-3-t5u-7
c-3-t5u-6
c-3-t5u-5
c-3-t5u-4
0.4
0.3
0.2
0.1
Step
0
1k
2k
3k
4k
5k
Learning rate
c-3-t5u-1 14
- c-33-55-13
c-3-t5u-12 - c-3-t5u-11
c-3-t5u-10
c-3-t5u-9 c-3-t5u-7
c-3-t5u-6
c-3-t5u-5
c-3-t5u-4
0.002
0.0015
0.001
0.0005
Step
0
1k.
2k
3k
4k
5k
Figure 4: Sensitivity to learning rate schedule of baseline model on FOL-codesc dataset.
17

---

Under review as a conference paper at ICLR 2023
B DATASETS OVERVIEW
In Table we give an overview of the datasets used in this work and their corresponding data source and size.
Table 2: The datasets used in this work for training and evaluation of the language models.
Dataset
Data source
Size
sygtx-sy
synthesized regex Locascio al. (2016)
10K
Regex-turk
regex using amazon turk Locasció et al. 2016
10K
FOL FOL-mnli FOL-codesc
cande & boxer translation of mnli hypothesis
150K
cande boxer translation codesc
600K
LTL LTL-pattern
grammar translation of specification patterns
200K
LTL syn-syy
grammar translation of synthesis specifications
100K
C REGEX DEFINITION
In Figure we show the regex formalism used by Locascio et al. (2016) for creating datasets
Regex synthetic and beogex-aynther
Non- Termieinnnls
+ x and y
y - y * I contains X
+ not
T. y followed by y
x, N more times I11, - x, at most N times
N,N,
x & y & + x and and
1/ 2 >x or or
I.* + starts with
x + ends with x
1b lb words with x only
(x)+ X, at least once
(x)**
x, zero more times
Terminals
[AEIOU] - vowel
0
number
word - the string 'word'
A-Z] + an uppercase letter
aa- z. + lowercase letter
- a character
Figure 5: Regex syntax used in the considered datasets; taken from Locascio et al. (0016)
D NATURAL LANGUAGE GRAMMARS
In this section, we present the grammars that used construct the LTL datasets. On the highest level a formula can be, e.g., an implication, a conjunction, an equivalence or an atomic proposition. Atomic propositions well as negated atomic propositions are represented by an e_p. which stands for "simple pattern".. Every other subcomponent that is not an or a negated ap is represented by c_p, which stands for "complex pattern".. Binary operators like conjunction have operands that can be either easy or complex, represented by the e_or_ category. If the formula is complex, we need parentheses to clarify operator precedence. For instance (a means that globally both and b hold. However if we translate it directly and say "Globally holds and b holds", we loose the meaning of the parentheses. This natural sentence could as well represent the formula (L)) A b. To model parentheses by using the phrase "Globally it is the case that" followed
avoid this ambiguity, by whatever the subformula is. This way it clear that the scope of the operator extends to the entire translation of the subformula and not only the very next part. The same principle is applied the other unary operators such as finally and next, however not to negation as we only have negations followed by easy patterns.
The grammar with minimal domain-knowe knowledge for a 1:1 translation beween LTL formulas and natural language is the following:
18

---

Under review as a conference paper at ICLR 2023
formula
highest_level
highest_level
universality existence implication on equivalence
conjunction disjunction until next e_p
universality
"L"epp " "L("c_p")"
existence
+ eepp "O("c_p"))
implication
e_or_c" "_oor_
equivalence
__er__""""________ c_oo
conjunction
___or_c"""e_or_
disjunction
= _
until
=e_or_c'W''_orr
release
=e_or_c"R"e_or__
next
"0""_pp"""""""pp""""""""""""""""
c_p
= highest_level
e_or_e
e_p 1 "("'""""""""""
e_p
ap "P
formula
highest_level
highest_level
universality existence implication lequivalence
conjunction disjunction until| next e__
universality
"Globally"e e_p
"Globally it is the case that" c_p
existence
"Eventually" e_p
"Eventually it is the case that" c_p
implication
"if" "_oo__"thhhn" e_oore
equivalence
e_ of and only ef __
conjunction
= e_or_c "and"e "_o_""_or_c
disjunction
e __or__correee e_o_c_
until
= e e_ "it_c""utilee_oo____ __or__
release
e_ or holls until" "_iill__o____ or_or__" for forever"
next
"in the next step" "in the next step it is the case that" c_p
c_p
highest_level
e_or_c
e_p c_p
e_p
ap "oolds" ap "does not hold"
19

---

Under review as a conference paper at ICLR 2023
In second step, replaced the operator descriptions with additional variations:
formula
highest_level
highest_level
universality existence implication equivalence
conjunction disjunction until next e__p
infinitely_often
"[Ko(""_rr""")
eventually_Forever
= "\(α""_or_c"")
universality
"0"e_pl "[""__"""
existence
= "O"e_pl " "O("cp"))
implication
-_or_ -
equivalence
= "
conjunction
=__or_c A
disjunction
= __o
until
= ___or_c'f'e_or__
release
e_or_c"R"' R_or_
next
"O"e_pl 4(" """"""""""""""""""""""""""""""""
CLp
highest_level
e_or_c
= e_p "("__p""" c_p [cp
e_p
= ap "Pa
formula
highest_level
highest_level
= universality exxsteence iimpl
equivalence conjunction disjunction until next
e_p infinitelyyoftenn weeetaaaleeeeoreeeeeeeeee
infinitely_often
Infinitely often" e_p "Infinitely often is the case that" c_p
eventually_forewe
= "Eventually forever" e_p
"Eventually it is the case that forever" cLP
universality
("Globally" "Always") e_pl
GGlobblly it is the case that"
"Always it the case that") c_p
existence
("Eeetuuall"" "Finally") e_p! ( "Eventually it is the case that" "Finally it the case that") c_p
implication
"if e_or_
equivalence
or "if and only if" e_or_c
conjunction
= e_or_ "and" e_or_c
disjunction
= e_o "or" e_or__
until
"until" e_or_c
release
e_ __ "holds until" e_or_c "or forever"
next
"in the next step" e_p "in the next step it is the case that" c_p
c_p
= highest_level
__or_c
e_p e_p|c_p
e_p
= ap "holds" ap "does not hold"
20


Reviews:
[{"review_id": "tRontlF9CdR", "reviewer": "Reviewer_i1Lj", "summary": "", "questions": "", "limitations": "", "rating": 3, "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": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "The ability of language models to translate from natural language into formal languages is studied. Concretely, regular expressions, first-order logic and linear-time temporal logic are considered as target languages. Four new synthetic datasets are created to measure success on the latter two languages.\nExperiments indicate that off-the-shelf fine-tuned Transformer models can handle the chosen tasks reasonably well. Some efforts are made to consider some axes of generalization in the experiments.\n", "summary_of_the_review": "It is unclear what insights the reader should take away here, and the authors do not outline future work. Overall, the contribution is limited to running experiments on four new datasets that are all problematic in their own ways, and are not connected to pre-existing tasks. Hence, I do not think this paper is of substantial interest to the ICLR community and would hence recommend rejection. It may be better suited for a workshop more focused on neural models for formal languages.", "strength_and_weaknesses": "* (+) Evaluating the ability to translate natural language into formal languages is important for better human/computer interfaces.\n* (-) The generated datasets are unrepresentative of _natural_ language. (see the examples in Sect 4.2 and 4.3)\n", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "1: The contributions are neither significant nor novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "rrqC5ixTWaR", "reviewer": "Reviewer_NwtW", "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": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "The authors propose a generalizable architecture using large language models as a backbone to translate the natural language into formal specifications.\nContributions: \n1. First off-the-shelf fine-tuned language model for natural language to formal specification.\n2. New datasets for translating natural language into FOL and LTL\n3. Generalizability capacity", "summary_of_the_review": "The authors propose a generalizable architecture using large language models as a backbone to translate the natural language into formal specifications. However, this work heavily relies on the previous literature and does not include enough innovative ideas. ", "strength_and_weaknesses": "Strengths:\n1. The study is performed on multiple formal languages, including Regex, FOL, and LTL. This demonstrates that the model can adapt to different formal languages with a similar pipeline.\n2. The examples for Regex and FOL show the mapping is non-trivial.\n\nWeakness:\nTwo aspects can be taken to view the weakness. \nAspect 1: Consider this paper as a dataset paper. Both FOL-mnli and FOL-codesc are generated using previous techniques; the LTL-pattern and LTL-synthesis are also not well addressed for their difference from the literature. Further, the natural language part of LTL-synthesis is quite synthetic and template based. \nAspect 2: Consider this paper as a methodology paper. The methodology is not that deep and does not contain deep technical contributions. One word that the authors compare to is folio, which the authors claim they adopt a similar methodology as theirs. However, the folio work is indeed a dataset paper, and all the few-shot GPT tasks are simply baselines for demonstration purposes. \n", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "1: The contributions are neither significant nor novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "PhjhXtp-tV", "reviewer": "Reviewer_xRr1", "summary": "", "questions": "", "limitations": "", "rating": 5, "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": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "The paper focuses on the problem of translating natural language into formal specifications, in particular, regular expressions (regex), first order logic (FOL), and linear temporal logical (LTL). Instead of training deep models from scratch for this problem, the authors investigate whether fine-tuning pretrained language models achieves similar performance, and how well it generalizes to for example new variable names or operator descriptions. The authors consider six datasets in their work, two for each domain: they use existing benchmark datasets Regex-synthetic and Regex-turk, and synthetically generate the datasets for FOL (FOL-mnli and FOL-codesc) and LTL (LTL-pattern and LTL-synthesis) which are also contributions of the paper. \n\nThe authors use the T5 model and compare training from scratch to fine-tuning pretrained T5 model for their experiments. On the regex datasets, they report a 6% improvement over SOTA results on both synthetic and turk datasets when fine-tuning the T5 model. On FOL-mnli, they also show a 7% improvement when fine-tuning compared to training from scratch. On LTL datasets, training from scratch and fine-tuning gives similar results. They evaluate generalization by considering nouns that were not present during fine-tuning for regex, new variable names and operator descriptions for LTL. They also conduct cross testing, where they train on one dataset for a domain and evaluate on the other dataset. They show that while the models have acceptable performance for regex, their performance drastically decreases for FOL and LTL datasets.", "summary_of_the_review": "The problem investigated is interesting. However, given the questions raised above, and parts of the evaluation being limited, I don't believe the paper is ready as is. ", "strength_and_weaknesses": "The paper is well written and well motivated, the authors clearly describe the problem and the approach for data generation and evaluation. However, the experimental section is a bit limited and the authors seem to draw strong conclusions from experiments on small datasets (see questions below).\n- The small version of T5 model is used for the baseline experiments, but the base version is used for fine-tuning experiments. Is the comparison fair? How do the baseline experiments compare to fine-tuning the small version?\n- The generalization test for regex is investigated on a very small set, what can really be inferred from this experiments? Similarly for investigating the generalization to new operator descriptions for LTL, the set of alternatives is very small.\n- For generalization to new operator descriptions for LTL, the performance of the model goes from 100% to 53%. Where does it fail? ", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "JSEdgGrfwoL", "reviewer": "Reviewer_AR6P", "summary": "", "questions": "", "limitations": "", "rating": 5, "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": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "The paper investigates the application of language models to translation from statements in natural language to formal languages including regular expressions, first order logic and linear temporal logic. The authors fine-tuned a pre-trained language model (T5) on three groups of datasets, each corresponding to the problem of translation from natural language to one formal language, and reported that the fine-tuned model outperforms the SOTA of translation to regular expressions. The authors also observed that the model could generalize to out-of-distribution instances to some extent, as well as instances where changes are made to variable names, nouns and operator descriptions.\n ", "summary_of_the_review": "The authors presented an interesting observation that language models are capable of translating natural languages to formal languages when fine-tuned on target problems. However, I think the other contributions claimed in the paper need to be supported by more content before the paper can be accepted.", "strength_and_weaknesses": "Strength\n\n+ The empirical evaluation validates the approach showing that the performance compares favorably to that of previous approaches, though limited to the problem of tranlation from natural language to regular expressions.\n\n+  The study of out-of-distribution performance by having two categories of datasets for each problem is nice to have, which helps understand the capability of LLMs on logic tasks.\n\nWeakness\n\n- While I appreciate the claimed SOTA (of 2% lead) on translation to regex, the overall contribution of the paper seems a bit pale. The paper claimed two new datasets being part of the contribution, but did not provide proper experiments justifying the fairness of them.\n\n- The analysis of generalizability is limited. It is not that surprising that language models had no problems recognizing new nouns and variable names, as well as equivalent descriptions of operators, since they have seen enough on the internet (which could also contain some problems in the experiments.) What would be interesting to see, for example, could be the performance with respect to the complexity of a formula (e.g., the number of logical connectives). \n\n- It is unclear how the accuracies used for FOL and LTL are defined. It is understandable that semantic equivalence for FOL is difficult, but how is syntactic accuracy done in the paper? Do you simply count an exact match as correct? \n\n- More baselines could have been added to support the claim of the paper. For example, have you tried few-shot learning with T5? If few-shot learning (with reasonably good example prompts) works, then it probably means that the language model has already seen enough translation examples during training. ", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "2: Several of the paper’s claims are incorrect or not well-supported.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}]

Author rebuttal:

Decision: Reject