Teaching Temporal Logics to Neural Networks
Authors: Christopher Hahn
Frederik Schmitt
Jens U. Kreber
Markus Norman Rabe
Bernd Finkbeiner
Venue: ICLR 2021 Poster (2021)
Keywords: Logic
Verification
Transformer

Abstract: We study two fundamental questions in neuro-symbolic computing: can deep learning tackle challenging problems in logics end-to-end, and can neural networks learn the semantics of logics. In this work we focus on linear-time temporal logic (LTL), as it is widely used in verification. We train a Transformer on the problem to directly predict a solution, i.e. a trace, to a given LTL formula. The training data is generated with classical solvers, which, however, only provide one of many possible solutions to each formula. We demonstrate that it is sufficient to train on those particular solutions to formulas, and that Transformers can predict solutions even to formulas from benchmarks from the literature on which the classical solver timed out. Transformers also generalize to the semantics of the logics: while they often deviate from the solutions found by the classical solvers, they still predict correct solutions to most formulas.

Published as a conference paper at ICLR 2021
TEACHING TEMPORAL LOGICS TO NEURAL NET- WORKS *
Christopher Hahn
Frederik Schmitt
CISPA Helmholtz Center for Information Security Saarbrücken, 66123 Saarland, Germany christophar hahn@ c spa. de
CISPA Helmholtz Center for Information Security Saarbrücken, 66123 Saarland, Germany frederi k. schmi t steecisp.de
Jens U. Kreber
Markus N. Rabe Google Research Mountain View, CA, USA mr mrabe@google.com
Saarland University
Saarbrücken, 66123 Saarland, Germany kreberêreact. uni- saar 1 land.
Bernd Finkbeiner
CISPA Helmholtz Center for Information Security Saarbrücken, 66123 Saarland, Germany
warkbeiner@cisppe
ABSTRACT
We study two fundamental questions in neuro-symbolic computing: can deep learning tackle challenging problems in logics end-to-end, and can neural net- works learn the semantics of logics. In this work we focus on linear-time tempo- ral logic (LTL), as it is widely used in verification. We train Transformer on the problem to directly predict a solution, i.c. a trace, to a given LTL formula. The training data is generated with classical solvers, which, however, only provide one of many possible solutions to each formula. We demonstrate that it is sufficient to train on those particular solutions to formulas, and that Transformers dict solutions even to formulas from benchmarks from the literature on which the classical solver timed out. Transformers also generalize to the semantics of the logics: while they often deviate from the solutions found by the classical solvers, they still predict correct solutions most formulas.
pre-
INTRODUCTION
Machine learning has revolutionized several areas of computer science, such as image recogni- tion (He et al. 2015), face recognition (Taigman al.) 2014). translation (Wu et al. 2016), and board games (Moravcík et al. 2017; Silver et al. 2017). For complex tasks that involve symbolic reasoning, however, deep learning techniques are still considered as insufficient. Applications of deep learning in logical reasoning problems have therefore focused on sub-problent
within larger logical frameworks, such as computing heuristics in solvers (Lederman et al.) [2020) [Balunovic al,, 2018
Selsam & Bjørner 2019) predicting individual proof steps (Loos et al.
Gauthier et al.,
2018
Bansal et al.] 2019 Huang et al. 2018). Recently, however, the assumption that deep learning ready to tackle hard logical questions was drawn into question. Lample & Charton (2020) demonstrated that Transformer models (Vaswani et al. (017) perform surprisingly well on symbolic integration, |Rabe al. (2020) demonstrated that self-supervised training leads to mathematical rea- soning abilities, and Broon et al. (2020) demonstrated that large-enough language models learn basic arithmetic despite being trained on mostly natural language sources.
This poses the question if other problems that are thought to require symbolic reasoning lend them- selves a direct learning approach. We study the application of Transformer models challenging
" Partialll supported by the Furopean Research Council (ERC) Grant OSARES (No. 683300) and the Col- laborative Research Center "Foundations of Perspicuous Software Systems" (TRR 248, 389792660).

---

Published as a conference paper at ICLR 2021
150 120
Figure 1: Performance of our best models trained on practical pattern formulas. The x-axis shows the formula size. Syntactic aceuracy, i.e., where the Transformer agrees with the generator are displayed in dark green. Instances where the Transformer deviates from the generators output but still provides correct output are displayed in light green; incorrect predictions in orange.
logical problems in verification. We thus consider linear-time temporal logic (LTL)
Pnuull
1977
which is widely used in the academic verification community (Dwyer et al. 1998 Li et al. 2013
Duret-Lutz et al. 2016 Rozier& & Vardi 2007 |Schuppan & Darmawan 2011 Li et al. 2013
2014
Schwendimann 1998) and is the basis for industrial hardware specification languages like the IEEE standard PSL
al.) 2005). LTL specifies infinite sequences and is typically used to describe system behaviors. For example, LTL can specify that some proposition P must hold at every point in time (O P) or that P must hold at some future point of time (O P). By combining these operators, one can specify that P must occur infinitely often P).
In this work, we apply a direct learning approach the fundamental problem of LTL to find satisfying trace to a formula. In applications, solutions to LTL formulas can represent (counter) examples for a specified system behavior, and over the last decades, generations of advanced algo- rithms have been developed to solve this question automatically. We start from the standard bench- mark distribution of LTL formulas, consisting of conjunctions of patterns typically encountered in practice (Dwyer et al., 1998). We then use classical algorithms, notably spot by Duret-Lutz et al. (206)), that implement competitive classical algorithm, to generate solutions to formulas from this distribution and train Transformer model to predict these solutions directly.
Relatively small Transformers perform very well on this task and we predict correct solutions to 96.8% of the formulas from held-out test set (see Figure [.. Impressive enough, Transformers hold up pretty well and predict correct solutions in 83% of the cases, even when we focus on formulas on which spot timed out. This means that, already today, direct machine learning approaches may be useful to augment classical algorithms in logical reasoning tasks.
We also study generalization properties of the Transformer architecture, important logical problems: We present detailed analyses on the generalization to longer formulas. It turns out that transformers trained with tree-positional encodings (Shiv & Quirk 2019) generalize much longer formulas than they were trained on, while Transformers trained with the standard positional encod- ing (as expected) do not generalize to longer formulas. The second generalization property studied here is the question whether Transformers learn to imitate the generator of the training data, or whether they learn to solve the formulas according the semantics of the logics. This is possible, as for most formulas there are many possible satisfying traces. In Figure [ we highlight the fact that our models often predicted traces that satisfy the formulas, but predict different traces than the one found by the classical algorithm with which we generated the data. Especially when testing the models -iittrriiitiitttinn we observed that almost no predicted trace equals the solution proposed by the classical solver.
To demonstrate that these generalization behaviors are not specific to the benchmark set of LTL formulas, also present experimental results random LTL formulas. Further, exclude that spot, the tool with which we generate example traces, is responsible for these behaviors, by repeat- ing the experiments on propositional formulas for which we generate the solutions by SAT solvers.
2

---

Published as a conference paper at ICLR 2021
The remainder of this paper is structured follows. We give overview over related work in We describe the problem definitions and present our data generation in Section 33 Our experimental setup is described in Section 4 and our findings in Section [S] before concluding in Section 0
Section 2
2 RELATED WORK
Datasets for mathematical reasoning. While we focus on a classical task from verification, other works have studied datasets derived from automated theorem provers (Blanchette et al. 2016 Loos
et al.
2017 Gauthier et al. 2018), interactive theorem provers (Kaliszyk et | 7017]
[00
Bansal et al.
2019
Huang al. 2018 Yang Deng 2019
Polu & Sutskever [020] Wu et al. 2020;] Li et al.
2020
Lee et al., 2020 Urban & Jakubuv 2020 Rabe et al. 2020). symbolic mathematics (Lample
Charton 2020), , and mathematical problems in natural language (Saxton al. 2019 Schlag et a
2019). Probably the closest work to this paper are the applications of Transformers to directly solve differential equations (Lample & Charton 2020) and directly predict missing assumptions and types of formal mathematical statements (Rabe et al., 2020 We focus different problem domain, verification, and demonstrate that Transformers are roughly competitive with classical algorithms in that domain on their dataset. Learning has been applied to mathematics long before the rise of deep learning. Earlier works focused on ranking premises or clauses Caims| (2004) | Urban (2004 2007);
Urban al. (2008): Meng & Paulson (2009; Schulz (2013) Kaliszyk & Urban (2014).
Neural architectures for logical reasoning. PPliwall et al. 2020) demonstrate significant im- provements theorem proving through the use of graph neural networks to represent higher-order logic terms. Selsam et al. (2019) presented NeuroSAT, graph neural network (Scarselli et al. 2008 Li et al. 2017| et al. 2017: et al. 2019) for solving the propositional satisfiability problem. In contrast, we apply generic
to-reneee--- model to predict the solutions to formulas, not only whether there is a solution. This allows us to apply the approach to a wider set of logics (logics without CNF). A simplified NeuroSAT AT architecture
trained for unsat-core predictions (Selsam & Bjørner 2019). Lederman et al. (2020) have used graph neural networks on CNF to learn better heuristics for 2QBF solver. Evans et al. (2018) study the problem of logical entailment in propositional logic using tree-RNNs. Entailment is a subproblem of satisfiability and (besides being a classification problem) could be encoded the same form as our propositional formulas. The formulas considered in their dataset are much smaller than in this work.
Language models applied to programs. Transformers have also been applied to programs for tasks such as summarizing code (Fernandes et al. 2018) variable naming and misuse (Hellen- doorn et al. 2020). Other works focused on recurrent neural networks or graph neural networks for
code analysis, e.g. (Piech et al., 2015; Gupta et al. 2017 Bhatia al. 2018: Wang et al. 2018 Allamanis et al. 2017). Another area in the intersection of formal methods and machine learning is the verification of neural networks (Seshia & Sadigh 2016, [Seshia et al., 2018 Siinhh et al., 2019
Gehr et al. 2018 Huang et al. Dreosis et al. 2019).
3 DATASETS
To demonstrate the generalization properties of the Transformer on logical tasks, we generated sev- eral datasets in three different fashions. We will describe the underlying logical problems and our data generation in the following.
3.1 TRACE GENERATION FOR LINEAR-TIME TEMPORAL LOGIC
Linear-time temporal logic (LTL. Pnueli 1977) combines propositional connectives with temporal operators such as the Next operator O and the Until operator U. O4p means that y holds in the next position of a sequence; spi 2 (22 means that 1 holds until 222 holds. For example, the LTL formula (bl a) A (cll-a states that has to hold along the trace until a holds and c has to hold until a does not hold anymore. There also exist derived operators. For example, consider the following specifi- cation of an arbiter: O(request + Qgrant) states that, at every point in time (O-operator). there is request signal, then grant signal must follow at some future point in time (ooperatoo).
3

---

Published as a conference paper at ICLR 2021
The full semanties and an explanation of the operators can be found in Appendix A infinite sequences, that are finitely represented in the form of a "lasso" ue where u, called pre- fix, and u, called period, are finite sequences of propositional formulas. We call such sequences (symbolic) fraces. For example, the symbolic trace (a A b)4 defines the infinite sequence where and b evaluate to true on every position. Symbolic traces allow us underspecify propositions when they do not matter. For example, the LTL formula a is satisfied by the symbolic trace: true true (a)², which allow for any combination of propositions on the first two positions.
We consider
Our datasets consist of pairs of satisfiable LTL formulas and satisfying symbolic traces generated with tools and automata constructions from the spot framework (Duret-Lutz et al. 2016). We use a compact syntax for ultimately periodic symbolic traces: Each position in the trace is separated by the delimiter " True and False are represented by "1" and "0", respectively. The beginning of the period v is signaled by the character "(" and analogously its end by ")". For example, the ultimately periodic symbolic trace denoted by a; a; a {b), describes all infinite traces where on the first 3 positions a must hold followed by an infinite period on which b must hold on every position.
Given a satisfiable LTL formula yp, our trace generator constructs Büchi automaton Ag that accepts exactly the language defined by the LTL formula, i.e., [(Aa) = L(z)). From this automaton, we construct an arbitrary accepted symbolic trace, by searching for an accepting run in Ap.
3.1.1 SPECIFICATION PATTERN
Our main dataset is constructed from formulas following 55 LTL specification patterns identified by the literature (Dwyer et al. 1998). For example, the arbiter property (Opp) - (pi U Po). stating that if Po is scheduled at some point in time, p1 is scheduled until this point. The largest specification pattern is of size 40 consisting of 6 atomic propositions. It has been shown that conjunctions of such patterns are challenging for LTL satisfiability tools that rely on classical methods, such as automata constructions (Li et al. 2013). They start coming to their limits when more than pattern formulas are conjoined. We decided to build our dataset in similar way from these patterns only to allow for a better comparison.
We conjoined random specification patterns with randomly chosen variables (from supply of 6 variables) until one of the following four conditions are met: 1) the formula size succeeds 126, 2) more than 8 formulas would be conjoined, 3) our automaton-based generator timed out (> 1s) while computing the solution trace, or 4) the formula would become unsatisfiable. total, we generated 1664487 formula-trace pairs in 24 hours on 20 CPUs. While generating, approximately 41% of the instances ran into the first termination condition, 21% into the second, 37% into the third and 1% into the fourth. We split this set into an 80% training set, 10% validation set, and 10% test set. The size distribution of the dataset can be found in Appendix B
For studying how the Transformer performs longer specification patterns, we accumulated pattern formulas where spot timed out (> 60s) while searching for a satisfying trace. We call this dataset L.TLUnsolved254 We capped the maximum length at 254, which is twice large as the formulas the model saw during training. The size distribution of the generated formulas can be found in Appendix B
In the following table, we illustrate the complexity of our training dataset with two examples from the above described set LTLPattem1126, where the subsequent number of the notation of our datasets denotes the maximum size of formula's 's syntax tree. The first line shows the LTL for- mula and the symbolic trace in mathematical notation. The second line shows the input and output representation of the Transformer (in Polish notation):
LTL. formula
satisfying symbolic trace
Da Od) - ///
( - TV CAdA D
[Iaslos!E]!caddlE
(UN---1N111111111111011111000000 -> OI
(<aAcA -A aA
c))
Aws656GGx....77000062222ooo..... fG!
# sedlalclaffj&aalallelt [salale!E)
& elefxU!es!!ee accaaaaddeellllaaaaaaaaa.eeee
4

---

Published as a conference paper at ICLR 2021
3.1.2 RANDOM FORMULAS
To show that the generalization properties of the Transformer are not specific to our data generation, we also generated a dataset of random formulas. Our dataset of random formulas consist of million generated formulas and their solutions, i.e., satisfying symbolic trace. The number of different propositions is fixed to 5. Each dataset is split into training set of 800K formulas. validation set of 100K formulas, and a test set of 100K formulas. All datasets are uniformly distributed in size, apart from the lower-sized end due to the limited number of unique small formulas. The formula and trace distribution of the dataset I.T..Random355, as well as three randomly drawn example instances can be found in Appendix B Note that we filtered out examples with traces larger than 62 (less than 0.05% of the original set).
To generate the formulas, we used the randlti tool of the spot framework, which builds unique formulas in a specified size interval, following a supplied node probability distribution. During the building process, the actual distribution occasionally differs from the given distribution in order to meet the size constraints, e.g., by masking out all binary operators. The distribution between all k-ary nodes always remains the same. To furthermore achieve (quasi) uniform distribution in size, we subsequently filtered the generated formulas. Our node distribution puts equal weight on all operators 7, A, and U. Constants True and False are allowed with 2.5 times less probability than propositions.
3.2 ASSIGNMENT GENERATION FOR PROPOSITIONAL. LOGIC
To show that the generalization of the Transformer to the semantics of logics is not a unique attribute of LTL, we also generated a dataset for propositional logic (SAT). A propositional formula consists of Boolean operators A (and), V (or), - (not), and variables also called literals or propositions. We consider the derived operators (o1 82 -iz Vipz (implication), (1 +> f22 (f21 + (22)
sP)) (equivalence), and @ iP2 = -(9 ++ (P2) (xor). Given a propositional Boolean formula s. the satisfiability problem asks if there exists Boolean assignment II V IB for every literal in yp such that & evaluates to Jrue. For example, consider the following propositional formula, given in conjunctive normal form (CNF): (11 V 12 V -x3) A (-#1 23). A possible satisfying assignment (I3, (. We allow a satisfying assignment to
for this formula would be {(z1, true). be partial, i.e., if the truth value of a propositions can be arbitrary, it will be omitted. For example, {(11, true), (I3, true)} would be a satisfying partial assignment for the formula above. We define a minimal unsatisfiable core of an unsatisfiable formula sp, given in CNF, as an unsatisfiable subset of clauses Poore of sp such that every proper subset of clauses of eerne is still satisfiable.
We, again, generated million random formulas. For the generation of propositional formulas, the specified node distribution puts equal weight on A, V, and operators and half much weight the derived operators ++ and @ individually. In contrast to previous work (Selsam et al. 2019), which is restricted to formulas in CNF, we allow arbitrary formula structure and derived operators.
A satisfying assignment ues, given as 0 and 1. The sequence a0b1c0, for example, represents the partial assignment ((, (b, truc), (c, false), meaning that the truth values of propositions and e can be cho- arbitrarily (note that we allow five propositions). We used pyaiger (Vazquez-Chanl Chanllate 2018), which builds on Glucose 4 (Audemard & Simon] 2018) as its underlying SAT solver. We construct the partial assignments with a standard method in SAT solving: We query the SAT solver for a min- imal unsatisfiable core of the negation of the formula. To give the interested reader an idea of the level of difficulty of the dataset, the following table shows three random examples from our training set Prop Random35. The first line shows the formula and the assignment in mathematical notation. The second line shows the syntactic representation (in Polish notation):
represented as an alternating sequence of propositions and truth val-
propositional formula
satisfying partial assignment
(d -e)- - (+)
(b,0), (c, 1), (d. (e,
v((e@ (bA (<e
hataee/lllaaletttb----bbbooooee Io !oc->!ae
a0b0cldle0
V + -b) lice<>blabb
[]c,1)) cl
([
[Id,1),(e, 11}
v( (((T0A)) -8) Ad)))
!xor!be baa->!ddeel !bsaa lbbbbd
dlel
5

---

Published as a conference paper at ICLR 2021
trained
tested on
LTLRandom35
LTLRRndom35
83.8
14.7
LTLRandom35
LTLRandom50
67.6
24.6
L7LPattem126
69.1
27.6
LTLPuttem120
LTLUnsolved254
83,8
16.1
PropRandom35
PropRandom35
58.1
38.4
PropRandom35
PropRandom50
35.8
50.3
13.9
Overview of our main experimental results: the performance of our best performing mod- els on our different datasets. The percentage of a dark green bar refers to the syntactic accuracy, the percentage of light green bar the semantic accuracy without the syntactic accuracy, and the incorrect predictions are visualized in orange.
Figure 2:
To test the Transformer even more challenging formulas, constructed dataset of CNF formu- las using the generation script of Selsam et al. (2019) from their publicly available implementation. A random CNF formula is built by adding clauses until the addition of further clause would lead to an unsatisfiable formula. We used the parameters Pgeo = 0.9 and Pk2 = 0.75 to generate formulas that contain up 15 variables and have maximum size of 250. We call this dataset PropCNF250.
4 EXPERIMENTAL SETUP
We have implemented the Transformer architecture (Vaswani et al.) 2017). Our implementation processes the input and output sequences token-by-token. We trained on a single GPU (NVIDIA P100 V100). All training has been done with dropout rate of 0.1 and early stopping validation set. Note that the embedding size will automatically be floored to be divisible by the number of attention heads. The training of the best models took up to 50 hours. For the output decoding, we utilized a beam search [Wu et al. 2016), with beam size of 3 and an a of 1.
the
Since the solution of a logical formula is necessarily unique, we use different measures of accuracy to evaluate the generalization to the semantics of the logics: we distinguish between the syntactic accuracy, i.e., the percentage where the Transformers prediction syntactically matches the output of our generator and the semantic accuracy, i.c., the percentage where the Transformer produced a different solution. We also differentiate between incorrect predictions and syntactically invalid outputs which, in fact, happens only in 0.1% of the cases in I.TT U.T..unsolved25..
In general, our best performing models used 8 layers, 8 attention heads, and an FC size of 1024. We used a batch size of 400 and trained for 450K steps (130 epochs) for our specification pattern dataset, and a batch size of 768 and trained for 50K steps (48 epochs) for our random formula dataset. A hyperparameter study can be found in Appendix C
5 EXPERIMENTAL RESULTS
In this section, we describe our experimental results. First, we show that a Transformer can indeed solve the task of providing solution, i.... trace for linear-time temporal logical (LTL) formula. For this, we describe the results from training on the dataset LTLPattern126 of specification pat- terns that are commonly used in the context of verification. Secondly, we show two generalization properties that the Transformer evinces on logic reasoning tasks: 1) the generalization to larger for- mulas (even so large that our data generator timed out) and 2) the generalization the semantics of the logic. We strengthen this observation by considering different dataset of random LTL formulas. Thirdly, we provide results for a model trained on a different logic and with a different data genera- tor. We thereby demonstrate that the generalization behaviors of the Transformer LTL and the LTL solver implemented with spot that we used to generate the data. An overview of training results is displayed in Figure
not specific to

---

Published as a conference paper at ICLR 2021
100
gdrcentage
syraati Mccurwty semantic accuracy
Incorrect Inveld
50
100
150 formula size
200
250
Figure 3: Predictions of our best performing model, trained on LTL Unsoleedd25, on 5704 specifi- cation patterns for which spot timed out (> 60s). Semantic accuracy is displayed in green; incorrect traces in orange; syntactically invalid traces in red.
5.1 SOLVING LINEAR-TIME TEMPORAL LOGICAL FORMULAS
We trained a Transformer on our specification on LTLPPtterm126. Figure I in the introduction displays the performance of our best model this dataset. We observed a syntactic accuracy of 69.1% and a semantic accuracy of 96.8%. With this experiment we can already deduce that it seems easier for the Transformer learn the underlying semantics of LTL than to learn the particularities of the generator. Further we can see that as the formula length grows, the syntactic accuracy begins to drop. However, that drop much smaller in the semantic accuracy- the model still mostly predicts correct traces for long formulas.
As challenging benchmark, we tested best performing model on LTL Unsolued22... It pre- dicted correct solutions in 83% of the cases, taking on average 15s on a single CPU. The syntactic accuracy is 0% as there was no output produced by spot within the timeout. The results of the experiments are visualized in Figure Note that this does not mean that our Transformer models necessariy outperform classical algorithms across the board. However, since verifying solutions to LTL formulas is much easier than finding solutions (AC' (logDCFL) vs PSPACE), this experiment shows that the predictions of deep neural network can a valuable extension to the verification tool box.
5.2 GENERALIZATION PROPERTIES
To prove that the generalization the semanties is independent of the data generation, we also trained a model on a dataset of randomly generated formulas. The unshaded part of Figure the performance of our best model on the LTT.Random35 dataset. The Transformers were solely trained on formulas of size less or equal to 35. We observe that in this range the exact syntactic accuracy decreases when the formulas grow in size. The semantic accuracy, however, stays, again, high. The model achieves syntactic accuracy of 83.8% and semantic accuracy of 98.5% on LTTLRandom335, i.e., 14.7% of the cases, the Transformer deviates from our automaton-based data generator. The evolution of the syntactic and the semantic accuracy during training can be found in Appendix D
To show that the generalization to larger formulas is independent from the data generation method, we also tested how well the Transformer generalizes to randomly generated LTL formulas a size it has never seen before. We used our model trained LTLRandomo5 and observed the performance on LTLRandom50. The model preserves the semantic generalization, displayed in the shaded part of Figure 4 It outputs exact syntactic matches in 67.6% of the and achieves a semantic accuracy of 92.2%. For the generalization to larger formulas we utilized a positional encoding based the representation of the formula (Shiv & Quirk 2019). When using the

---

Published as a conference paper at ICLR 2021
standard positional encoding instead, the accuracy drops, as expected, significantly. A visualization of this experiments can be found in Appendix E
In further experiment, we tested the -ustof-distriuution (OOD) generalization of the Transformer on the trace generation task. We generated a new dataset LTLRanddm126 to match the formula A model trained on LTI.Random 1 126 achieves a
sizes and the vocabulary of mantic accuracy of 24.7% (and a syntactic accuracy of only 1.0%) when tested on LTLPaftern 126. Vice versa, model trained on LTTLPatterm12 126 achieves a semantic accuracy of 38.5% (and semantic accuracy of only 0.5%) when tested on LTL 126. Testing the models OOD in- creases the gap between syntactic and semantic correctness dramatically. This underlines that the models learned the nature of the LTL semantics rather than the generator process. Note that the two distributions are very different.
Following these observations, we also tested the performance of our models on other patterns from the literature. We observe a higher semantic accuracy for our model trained on random formulas and a higher gap between semantic and syntactic accuracy for model trained on pattern formulas:
Patterns
Number of Patterns
Trained
Syn. Acc.
Sem. Acc.
dac (wwer et al. [998]
55
LTnRRndom 126
49.1%
81.8%
ch (Etessami & Holzmann 2000
11
LTLRondom 126
81.8%
90.9%
hirrss (Holecek al. 2004
49
LTLRandom 126
71.4%
83.7%
p (Pelánek 2007
20
LTLRandom 126
65.0%
90.0%
eh (Etessami Holzmann, 2000
L.TLPatter
0.0%
36.4%
fikrss HHllebek et al. 2004
49
LTLPattern126 14.3%
49.0%
Peelane 2007
20
LTLPPatern122
10.0%
60.0%
In last experiment on LTL, we tested the performance of our models on handcrafted formulas. We observed that formulas with multiple until statements that describe overlapping intervals were the most challenging. This is no surprise as these formulas are the source of PSPACE- of LTL.
aubbau & &UaUUa!b
(a A -b) (b) (true)" & lblb; (1)
While the above formula can be solved by most models, when scaling this formula to four over- lapping until intervals, all of our models fail: For example, a model trained on LTLRandom35 predicted the trace (a (a -A o) (bAc) (Irue)", which does not satisfy the LTL formula.
A Pa ee (aAbAc) bA <) (b (true) & &sa lb! !ble &be;]
&&&UasbeUaa lbcUasb! cUa&!ble
5.3 PREDICTING ASSIGNMENTS FOR PROPOSITIONAL LOGIC
To show that the generalization to the semantic is not a specific property of LTL, we trained a Trans- former solve the assignment generation problem for propositional logic, which is substantially different logical problem.
As a bascline for our generalization experiments on propositional logic, we trained and tested Transformer model with the following hyperparameter on PropRandomis
Embedding size cnc: dec:64
Layers
Heads
FC size
Batch Size
Train Steps
Syn. Acc. Sem. Acc. 96.5% %
6
512
1024
50K
58.1%
We observe a striking 38.4% gap between predictions that were syntactical matches of our DPLL- based generator and correct predictions of the Transformer. Only 3.5% of the time, the Transformer outputs an incorrect assignment. Note that we allow the derived operators () and <-> in these experi- ments, which succinctly represent complicated logical constructs.
The formula 6 V (a A d) occurs our dataset Pondom35 and its corresponding assignment is (a, O)}. The Transformer, however, outputs d0, i.e., it goes with the assignment of setting d to false. which is also a correct solution. A visualization of this example can be found in Appendix When the formulas get larger, the solutions where the Transformer differs from the DPLL algorithm accumulate. Consider, for example, the formula -bV (e ++ bVcV-dl V (cA (b@ (a--d)) O @0-c (-c < d) A (a (b (b e)))), which is also in the dataset Propoand The generator suggests
8

---

Published as a conference paper at ICLR 2021
60
aptlacti: 4SCUTAS7
Figure Syntactic and semantic accuracy of our best performing model (only trained on I.T.Random35) on I.T.Rondom50. Dark green is syntactically correct; light green is seman- tically correct, orange incorrect.
the assignment {(a, 1), (c, 1). (d, 0)). The Transformer, however, outputs e0, i.e., the singleton assignment of setting false, which turns be a (very small) solution well.
We achieved stable training in this experiment by setting the decoder emhedding size to either 64 or 32. Keeping the decoder embedding size 128 led very unstable training.
We also tested whether the generalization to the semantics is preserved when the Transformer en- counters propositional formulas of larger size than ever saw during training. We, again, utilized the tree positional encoding. When challenged with formulas of size 35 to 50, our best performing model trained on PropRandom33 achieves syntactic accuracy of 35.8% and semantic accuracy of 8..1%. In comparison, without the tree positional encoding, the Transformer achieves syntactic match of only 29.0% and an overall accuracy of only 75.7%. Note that both positional encodings work equally well when not considering larger formulas.
In a last experiment, we tested how the Transformer performs on more challenging propositional formulas in CNF. We thus trained a model on PropCNF 250, where it achieved semantic accuracy of 65.1% and syntactic accuracy 56.6% 6%. We observe slightly lower gap compared to our LTL experiments. The Transformer, however, still deviates even on such formulas from the generator.
CONCLUSION
We trained a Transformer to predict solutions to linear-time temporal logical (LTL) formulas. We observed that our trained models evince powerful generalization properties, namely, the generaliza- tion to the semantics of the logic, and the generalization to larger formulas than seen during training. We showed that these generalizations do not depend on the underlying logical problem nor on the data generator. Regarding the performance of the trained models, we observed that they can compete with classical algorithms for generating solutions LTL formulas. We built a test set that contained only formulas that were generated out of practical verification patterns, which even our data gen- erator timed out, Our best performing model, although it was trained on much smaller formulas, predicts correct traces 83% of the time.
The results this paper suggest that deep learning can already augment combinatorial approaches in automatic verification and the broader formal methods community. With the results of this paper, can, for example, derive novel algorithms for trace generation or satisfiability checking of LTL that first query Transformer for trace predictions. These predictions be checked efficiently. Classi- cal methods can serve as a fall back or check partial solutions providing guidance to the Transformer. The potential that arises from the advent of deep learning logical reasoning is immense. Deep learning holds the promise to empower researchers in the automated reasoning and formal methods communities to make bigger jumps in the development of new automated verification methods, but also brings new challenges, such as the acquisition of large amounts of data.
ACKNOWLEDGEMENTS
We thank Christian Szegedy, Jesko Hecking-Harne Harbusch, and Niklas Metzger for their valuable feed- back earlier version of this paper.

---

Published as a conference paper at ICLR 2021
REFERENCES
Miltiadis Allamanis, Mare Brockschmidt, and Mahmoud Khademi. Learning to represent programs with graphs. arXiv preprint (exXiv/711.007440 2017.
Gilles Audemard and Laurent Simon. On the glucose SAT solver. Int. J. Artif. Intell. Tools, 27 (D:1840001111184000022) 2018. doi: 10. 1411//00218233318400000 URL httpss://doi.
Mislav Balunovic, Pavol Bielik, and Martin Vechev. Learning solve smt formu- las. In S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett (eds.), Advances Neural Information Processing Systems 31, pp. 10317- 10328. Curran Associates, Inc., 2018. URL http: http://papera nips. cc/paper/ 1193-learning to solve- smt formulas as pdf
Kshitij Bansal, Sarah M Loos, Markus N Rabe, Christian Szegedy, and Stewart Wilcox. HOList: An environment for machine learning of higher-order theorem proving. arXiv preprint
arXiv:1904.0324] 2019.
Bhatia, P. Kohli, and Singh. Neuro-symbolic program corrector for introductory programming assignments. In 2018 IEEE/ACM 40th International Conference on Software Engineering (ICSE), pp. 60-70, May 2018. doi: 10. 145/3 10000155..10211111
Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C Paulson, and Josef Urban. Hammering towards QED. Journal of Formalized Reasoning, 91):1011-44, 2016.
Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhari- wal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Vors Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter, Christopher Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Radford, Ilya Sutskever, and Dario Amodei. Language models are few-shot learners. 2020.
Paul Cairns. Informalising formal mathematics: Searching the mizar library with latent semantics. In International Conference on Mathematical Knowledge Management, pp. 58-72. Springer, 2004.
Tommaso Dreossi, Alexandre Donzé, and Sanjit A Seshia. Compositional falsification of cyber- physical systems with machine learning components. Journal of Automated Reasoning, 63(4): 1031-1053, 2019.
Alexandre Duret-Lutzz Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Re- nault, and Laurent Xu. Spot 2.0-a framework for itl and w-automata manipulation. In Interna- tional Symposium on Automated Technology for Verification and Analysis, pp. 122-129. Springer, 2016.
Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Property specification patterns for finite-state verification. In Mark A. Ardis and Joanne M. Atlee (eds.), 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. 11..4/22289992999999999 URL hattps://dol orq/10. 1145 988998859888 298598
Kousha Etessami and Gerard J. 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 in Computer Science, pp- 153-167. Springer, 2000. doi: 10. 111100773-540444418-44 1007/3-540-44611
URL https: /ttpps://do /oo. orgg/C.
13
Richard Evans, David Saxton, David Amos, Pushmeet Kohli, and Edward Grefenstette. Can neural networks understand logical entailment? arXiv preprint arXiv: 1802.08535, 2018.
Patrick Fernandes, Miltiadis Allamanis, and Mare Brockschmidt. Structured neural summarization. arXiv preprint arXiv: 181 1.0184,, 2018.
10

---

Published as a conference paper at ICLR 2021
Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. Tactictoe: Learning reason with hol4 tactics. arXiv preprint arXiv:1804.00530 2018.
Timon Gehr, Matthew Mirman, Dana Drachsler- Cohen, Petar Tsankov, Swarat Chaudhuri, and Mar- tin Vechev. Ai2: Safety and robustness certification neural networks with abstract interpreta- tion. In 2018 IEEE Symposium on Security and Privacy (SP), pp. 3-18. IEEE, 2018.
Justin Gilmer, Samuel Schoenholz, Patrick F Riley, Oriol Vinyals, and George E Dahl. Neural message passing for quantum chemistry. In Proceedings of the 34th International Conference on Machine Learning- Volume 70, pp. 1263-1272. JMLR. org, 2017.
Rahul Gupta, Soham Pal, Aditya Kanade, and Shirish Shevade. Deepfix: Fixing common C language errors by deep learning. In Thirty-First AAAI Conference on Artificial Intelligence, 2017.
Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun. Delving deep into rectifiers: Surpassing human-level performance on imagenet classification. In 2015 IEEE International Conference on Computer Vision, ICCV 2015, Santiago, Chile, December 7-13, 2015, pp. org.//.rg110..0 09 2015..2211..2.. 123
2015. doi:
10.1109/1CCV22015.222 1233.
Vincent Hellendoorn, Charles Sutton, Rishabh Singh, and Petros Maniatis. Global relational models of source code. In International Conference on Learning Representations, 2020. URL
hittps://geerreveew net httpgppnreerree..neefforrrrrosss ImbbRNE
Jan Holeček, Tomáš Kratochvíla, Vojtëch Rehák, David Šafránek, Pavel Šimeček, et al. Verification results in liberouter project, 2004.
Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. Gamepad: A learning environ- ment for theorem proving. arXiv preprint arXiv: 806.00608, 2018.
Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. Safety verification of deep neural networks. In International Conference Computer Aided Verification, pp. 3-29. Springer, 2017.
IEEE-Commission et al. Icee standard for property specification language (psl). IEEE Std 1850- 2005, 2005.
Cezary Kaliszyk and Josef Urban. Searning-assisted automated reasoning with flyspeck. Journal of Automated Reasoning. 53(2):173-213, 2014.
Cezary Kaliszyk, François Chollet, and Christian Szegedy. HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving. In Proceedings of International Conference on Learn- ing Representations (ICLR), 2017.
Guillaume Lample and François Charton. Deep learning for symbolic mathematics. ICLR, 2020.
Gil Lederman, Markus N. Rabe, Edward A. Lee, and Sanjit A. Seshia. Learning heuristics for quantified boolean formulas through deep reinforcement learning. 2020. URL/tttp:/arxxi
08058
Dennis Lee, Christian Szegedy, Markus N. Rabe, Sarah M. Loos, and Kshitij Bansal. Mathematical reasoning in latent space. 2020.
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, Septem- ber 26-28 2013, pp. 91-98. IEEE Computer Society, 2013. doi: 1.110//TMM..0013.199 URI. ht.t / doi.ooo.../ooooo org.or//g.oo / 10. 1091009170 T9/TTME...... 2013.19
Jianwen Li, Yinbo Yao, Geguang Pu, Lijun Zhang, and Jifeng He. Aalta: Itl satisfiability checker over infinite/finite traces. In Proceedings of the 22nd ACM SIGSOFT international symposium on foundations of software engineering, pp. 731-734, 2014.
Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. Modelling high-level mathematical rea- soning in mechanised declarative proofs. arXiv preprint 0rXiv:2000.09265, 2020.
11

---

Published as a conference paper at ICLR 2021
Yaguang Li, Rose Yu, Cyrus Shahabi, and Yan Liu. Diffusion convolutional recurrent neural net- work: Data-driven traffic forecasting, arXiv preprint arXiv:1707.01926, 2017.
Sarah Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof
search. In LPAR, 2017.
Jia Meng and Lawrence C Paulson. Lightweight relevance filtering for machine-generater resolution problems. Journal of Applied Logic, 7(1):41-57, 2009.
Matej Moraveík, Martin Schmid, Neil Burch, Viliam Lisý, Dustin Morrill, Nolan Bard, Trevor Davis, Kevin Waugh, Michael Johanson, and Michael H. Bowling. Deepstack: Expert-level ar- tificial intelligence in no-limit poker. CoRR. abs/1701.01724, 2017. URL http:://axxi..
erg/abs/1701 01724
Aditya Paliwal, Sarah M. Loos, Markus N. Rabe, Kshitij Bansal, and Christian Szegedy. Graph representations for higher-order logic and theorem proving. AAAI, 2020.
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-267. 0111//9788--4------ 5430--37777775-3 978- 578-3-540-73370-62
Springer, 2007. doi: 10. 1001007977--3-10000
URL https:://cc...... /ttp://///ol..o//1100000000
Chris Piech, Jonathan Huang, Andy Nguyen, Mike Phulsuksombati, Mehran Sahami, and Leonidas Guibas. Learning program embeddings to propagate feedback on student code. In International Conference on Machine Learning, pp. 1093-1102, 2015.
Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October November 1977, pp. 46-57, 1977. doi: 10.1109/SFC..197..33 URL bttts:::: /doi. owt.ooooo//..10000001.0........0 www.::..111/SSSS.. 1977 32
Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving, 2020.
Markus N. Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical reasoning via sule-supe skip-tree training. 2020.
Kristin Y Rozier and Moshe Y Vardi. Ltl satisfiability checking. In International SPIN Workshop on Model Checking of Software, pp. 149-167. Springer, 2007.
David Saxton, Edward Grefenstette, Felix Hill, and Pushmeet Kohli, Analysing mathematical rea- soning abilities of neural models. CoRR, abs/1904.01557,, 2019. [RLp:t:p//arxxiorrr
abs/ abs/1904. 1904.01557
Franco Scarselli, Marco Gori, Ah Chung Tsoi, Markus Hagenbuchner, and Gabriele Monfardini. The graph neural network model. IEEE Transactions Neural Networks, 20(1):61-80, 2008.
Imanol Schlag, Paul Smolensky, Roland Fernandez, Nebojsa Jojic, Jürgen Schmidhuber, and Jian- feng Gao. Enhancing the transformer with explicit relational encoding for math problem solving. arXiv preprint arXiv: /910.0661 2019.
Stephan Schulz. System description: E 1.8. In International Conference on Logic for Sooeeoorrrrrrrr Programming Artificial Intelligence and Reasoning, pp. 735-743. Springer, 2013.
Viktor Schuppan and Luthfi Darmawan. Evaluating Itl satisfiability solvers. In International Sym- posium on Automated Technology for Verification and Analysis, pp. 397-413. Springer, 2011.
Stefan Schwendimann. A new one-pass tableau calculus for pltl. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pp. 277-291. Sprinee,,,,, 1998.
Daniel Selsam and Nikolaj Bjørner. Guiding high high-peeformance SAT solvers with unsat-core predictions. In Theory and Applications of Satisfiability Testing SAT 2019 22nd Inter- national Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings, pp. 336- 353. 2019. doi: 10.10077978--3-000 00-00000022-9999 24. URL hctps: //ttp:://ci.... orq/10.1007/ 978- 178-3-030-22258-93
12

---

Published as a conference paper at ICLR 2021
Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. Learning a SAT solver from single-bit supervision. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019, 2019. URL http://eaaaaaeeeeee.eeooooooooaa
htttps://openreviee..nsst htte://forrmmidddduem 1A5tm
Sanjit A. Seshia and Dorsa Sadigh. Towards verified artificial intelligence. CoRR, abs/ 100./1606.0814,
2016. HRRlAttp://arxtt org/ 0a0..a/111600811144
Sanjit A Seshia, Ankush Desai, Tommaso Dreossi, Daniel J Fremont, Shromona Ghosh, Edward Kim, Sumukh Shivakumar, Marcell Vazquez- and Xiangyu Yue. Formal specification for deep neural networks. In International Symposium Automated Technology for Verification and Analysis, pp. 20-34. Springer, 2018.
Vighnesh Leonardo Shiv and Chris to
Quirk. In
Novel positional
encodings URL
enable tree-based transformers.
NeurIPS 2019,
2019.
David Silver, Julian Schrittwieser, Karen Simonyan, loannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, et al. Mastering the game of go without human knowledge. Nature, 55017676):35-335) 2017.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for cer- tifying neural networks. Proceedings of the ACM on Programming Languages, 3(POPL):1-30, 2019.
Yaniv Taigman, Ming Yang. Marc' Aurelio Ranzato, and Lior Wolf. Deepface: Closing the gap to human-level performance in face verification. 2014 IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2014, Columbus, OH, USA, June 23-28, 2014, pp. 1701-1708, 2014. doi: 10. 20.100992PP..2004.22200
htttshts: http:///oooorg/////////o org/10. 1109 20109/CVVRR CWR./ 2014. 220
Josef Urban. MPTP- mottiimoivv,,,n, implementation, first experiments. Journal of Automated Reason- ing, 33(3-4):319 333, 2004.
Josef Urban. Malarea: a metasystem for automated reasoning in large theories. ESARLT, 257, 2007.
Josef Urban and Jan Jakubův. First neural conjecturing datasets and experiments. In Conference on Intelligent Computer Mathematics, 2020.
Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jifí Vyskočil. Malarea sgl- agl-machine learner for auto- mated reasoning with semantic guidance. In International Joint Conference on Automated Rea- soning, pp. 441-456 Springer, 2008
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Advances in Neural In- formation Processing Systems 30: Annual Conference on Neural Information Processing Sys- tems 2017, 4-9 December 2017, Long Beach, CA, USA, pp. 5998 6008, 2017. URL http: 7/ 7/papers. nips. (atapprr1111-atteeeee
is aas-all- aalalloooo-- need
Marcell Vazquez-Chanlatte. mvcisback/py-aigee August 2018. http1//enddo.1126600
Ke Wang, Rishabh Singh, and Zhendong Su. Dynamic neural program embedding for program repair. In ICLR, 2018
Yonghui Wu, Mike Schuster, Zhifeng Chen, Quoe V. Le, Mohammad Norouzi, Wolfgang Macherey, Maxim Krikun, Yuan Cao, Qin Gao, Klaus Macherey, Jeff Klingner, Apurva Shah, Melvin John- son, Xiaobing Liu, Lukasz Kaiser, Stephan Gouws, Yoshikiyo Kato, Taku Kudo, Hideto Kazawa, Keith Stevens, George Kurian, Nishant Patil, Wei Wang. Cliff Young, Jason Smith, Jason Riesa, Alex Rudnick. Oriol Vinyals, Greg Corrado, Macduff Hughes, and Jeffrey Dean. Google's neural machine translation system: Bridging the gap between human and machine translation. CoRR, abs/16009006 44, 2016. URL http:tt::////// /ttp:///axx org/ abs 609. 081 44
13

---

Published as a conference paper at ICLR 2021
Yuhuai Wu, Albert Jiang, Jimmy Ba, and Roger Grosse. INT: An Inequality Benchmark for Evalu- ating Generalization in Theorem Proving. arXiv preprint arXiv:2007.02924, 2020.
Zonghan Wu, Shirui Pan, Fengwen Chen, Guodong Long, Chengqi Zhang, and Philip S Yu. A
comprehensive survey graph neural networks. arXiv preprint arXiv:1901.00596, 2019.
Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. arXiv 2019.
preprint
14

---

Published as a conference paper at ICLR 2021
APPENDIX
A LINEAR-TIME TEMPORAL LOGIC (LTL)
In this section, we provide the formal syntax and semantics of Linear-time Temporal Logic (LTTL). The formal syntax of LTL is given by the following grammar:
f p up A Of 1 u.
where E AP is an atomic proposition. Let AP be a set of atomic propositions. A (explicit) trace is an infinite sequence over subsets of the atomic propositions. We define the of traces TR (2AP)M. We use the following notation to manipulate traces: Let f E TR be a trace and i E be natural number. With tlj] we denote the set of propositions at i-th position of Therefore, t|0] represents the starting element of the trace. Let j N and j > i. Then f(ū, jl denotes the sequence {[]] {ii + 1]....tj - 1] {[]] and t(i, oc] denotes the infinite suffix starting position i.
Let E AP and f E TR. The semantics of an LTL formula is defined as the smallest relation } that satisfies the following conditions:
iff
p E [(]
up
iff
f | p
t = A 422
iff
t + 91 and - 422
= Opp
iff
f[L,
F 6p
{ + 4 U 922
iff
there exists 2 0 f(i,,, 00) F 92
and for all S i we have t
F
There are several derived operators, such as O true uI yp Uy - m. O p states that op will eventually hold the future and D states that yp holds globally. Operators can be nested: e, for example, states that & has to occur infinitely often.
B SIZE DISTRIBUTION IN THE DATASETS
this section, we provide insight into the size distribution of our datasets. S the size distribution of the formulas in our dataset LTLPatterm126.
Figure 6 shows the size distribution of our generated formulas and their traces in the dataset LTTRandom35. Table I shows three randomly drawn example instances of the dataset L.T R.T.Rond..3.
Lastly, Figure shows the size distribution of formulas in dataset Uns.wwwsw.d22...
700
600
number of Tams
800
300
100
40
129
formula size
Figure 5: Size distributions in the LTLPattern22 test set: on the x-axis is the size of the formulas; on the y-axis the number of formulas.
15

---

Published as a conference paper at ICLR 2021
10a
25000
10
15000
10a
10000
5
10
25
20
25
30
10
20
30
40
50
60
Formula distribution by size.
(b) Trace distribution by size.
Figure 6: Size distributions in the I.T.Random's training set: on the x-axis is the size of the formulas/traces; on the y-axis the number of formulas/traces.
Table 1: Three random examples from L.L.Randoms training set. The first line shows the LTL. formula and the symbolic trace in mathematical notation. The second line shows the syntactic representation (in Polish notation):
LTL formula
satisfying symbolic trace
true (b A -c A nd) (-c
(true)"
6xUUdexxaxab/Uldo
1; d; cd;d;
-O((Oe (ru
true (-b A -e)
(-b)"
IXUG&XeU1bXcc
1;&lblc; (cllcc;(bb))
O O-((=eAd)UOd)
brue (eV d) (-d) (brue)
X! cdxd
1; lcldd [1;
number Itmm
0
Figure 7: Size distributions in the L.T..nnolved225 test set: on the x-axis the size of the formulas; on the y-axis the number of formulas.
C HYPERPARAMETER ANALYSIS
Table[[show the effect of the most significant parameters on the performance of Transformers. The performance largely benefits from an increased number of layers, with yielding the best results. Increasing the number further, even with much more training time, did not result in better even led to worse results. A slightly less important role plays the number of heads and the dimension of the intermediate fully-connected feed-forward networks (FC). While certain FC size is important, increasing alone will not improve results. Changing the number of heads alone has also almost impact performance. Increasing both simultaneously, however, will result in small gain.
16

---

Published as a conference paper at ICLR 2021
Table 2: Syntactic accuracy and semantic accuracy of different Transformers, tested on LoTRonndm33: Layers refer to the size of the encoder and decoder stacks; Heads refer to the number of attention heads; FC size refers the size of the fully-connected neural networks inside the encoder and decoders.
Embedding size
Layers
Heads
FC size
Batch Size
Train Steps
Syn. Acc.
Sem. Acc.
128
4
512
512
45K
78.0%
97.1% %%
128
2
512
512
45K
80.4%
97.4%
128
4
256
512
45K
81.0%
97.4%
128
512
512
45K
82.0%
97.9%
128
1024
512
45K
80.3%
97.3%
128
6
1024
512
45K
81.8%
97.7%
128
512
512
45K
82.0%
97.8%
128
8
1024
512
45K
82.5%
97.9%
128
8
1500
512
45K
82.6%
97.8%
128
1024
512
45K
81.9%
97.5%
128
4
512
512
45K
83.2%
98.3%
128
8
1024
768
50K
83.8%
98.5%
128
10
4
512
512
75K
82.9%
97.6%
256
4
512
512
45K
82.3%
97.9%
This seems reasonable, since more heads can provide more distinct information to the subsequent processing by the fully-connected feed-forward network. Increasing the embeddings size from 128 to 256 very slightly improves the syntactic accuracy. But likewise it also degrades the semantic accuracy, therefore stuck with the former setting.
D ACCURACY DURING TRAINING
In Figure g we show the evolution of both the syntactic accuracy and the semantic accuracy during the training process. Note the significant difference right from the beginning. This demonstrates the importance of suitable performance measure when evaluating machine learning algorithms on logical reasoning tasks.
100
Accuracy percent
80
40
20
10
20
30
40
50
Epoch
Figure 8: Syntactic accuracy (blue) and semantic accuracy (red) of our best performing model, evaluated on subset of 5K samples of I.T.Rondom35 per epoch.
17

---

Published as a conference paper at ICLR 2021
E DIFFERENT POSITIONAL ENCODINGS
patcert-gee
40
40-
Sy Tacticc accuracy
Semanbic Bcouracy
Incomeect
Insulid
50
parcaroge
40-
20-
Incerwet
Somulaa size
Figure 9: Performance of our best model (only trained on LTLRandom35) LTLRandom50 with a standard positional encoding (top) and a tree positional encoding (bottom). The syntactic accuracy displayed in green, the semantic accuracy in light green and the incorrect predictions in orange. The shaded area indicates the formula sizes the model was not trained on.
F HANDCRAFTED EXAMPLES
Layer:
Attention: Sentence Sentence A
Layer: 5 v Attention: Sentence > Sentence A
&
<00%>
Figure 10: Self-attention of the example propositional formula -(a d) in dataset PropRandomas (left). Encoder-decoderaattennioo of the example LTL formula (bll a) A (all -a) in dataset LTTRRandm335 (right).
The LTL formula (bl a) A (all -a) states that à has to hold along the trace until a holds and a has hold until does not hold anymore. The automaton- based generator suggests the trace (-a b) a (true)". i.e., to first satisfy the second until by immediately disallowing a. The satisfaction of the first until then postponed the second position trace, which forces hold on the first position. The Transformer, however, chooses the following more general trace (-a) (frue) by satisfying the until operators in order (see Figure 10).
18


Reviews:
[{"review_id": "fq_woJrexkC", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 7, "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": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The paper presents multiple dataset generation and testing procedures for linear temporal logic and propositional logic satisfiability. They are then used to train Transformers with tree positional encoding. The approach amounts to imitation learning based on existing solvers for satisfiability for the considered logics. In contrast to previous work, the approach supports logical formulas of arbitrary shape. The experiments demonstrate successful generalization for multiple approaches to dataset generation.\nMost importantly, the LTL model generalizes to examples that lead to timeout when using the imitated solver directly.\n\nStrengths:\n- Satisfiability is a prime use case for deep learning in rigorous formal methods, as solutions are hard to find but easy to check.\n- Deep learning for LTL is interesting and I have not seen it done before.\n- The models train and generalize successfully, they beat the existing approaches used for dataset generation on some instances.\n- The authors attempted to exclude a strong dependency of generalization on their specific generation procedure by considering multiple different distributions for dataset generation.\n\nWeaknesses:\n- The training and test datasets (with the apparent exception of LTLUnsolved) are limited to easy instances, skewing the distribution. What happens if you use satisfiable examples where the generator times out after 1s as a test set?\n- The distribution of LTLUnsolved is not discussed in detail. How exactly were those formulas obtained? Is it a similar procedure as the one used for LTLPattern126? If not, how does it differ? How do you make sure that the formulas are satisfiable?\n- The paper does not show generalization between LTLRandom and LTLPattern datasets, even though this would be an obvious experiment to try if the goal is to demonstrate that the model learns LTL semantics in both cases instead of overfitting to the dataset generation procedure and the generator.\n\n\nDetailed comments/questions:\n\nPage 4:\nTermination condition 4 requires solving a satisfiability instance after each new conjunct is added. How do you check this satisfiability and how does it relate to the 1s timeout?\n\nPage 6:\n\"With this experiment we can already deduce that it seems easier for the Transformer to learn the underlying semantics of LTL than to learn the particularities of the generator.\"\n\nActually, I would also expect semantic accuracy to suffer quite a bit less than syntactic accuracy if the Transformer learns an imperfect copy of the generator, so it is not so clear whether the model learns semantics or just predicts imperfect sequences that coincidentally also work. (After all, your loss function instructs the model to imitate the generator.)\nMaybe you could analyze the sensitivity of the generated traces to random noise. It is of course plausible that different aspects of multiple input/output-examples are successfully combined by the model in a way that leads to successful generalization even though it is distinct from what the generator does, but personally, I wouldn't claim that the model discovers a representation of the underlying semantics without some sort of demonstration of knowledge transfer to a vastly different LTL-related task.\n\nPage 7:\nThe caption of Figure 3 claims that your model was trained on LTLUnsolved254 which seems impossible as that data set does not have output examples. In the text, you say that you trained on LTLPattern126, which makes more sense.\n\nPage 8:\n\"Note that we allow the derived operators ⊕ and ↔ in these experiments, which succinctly represent complicated logical constructs.\" Those operators are not any more complicated than ∧ and ∨.\n\n\nMinor:\n\nPage 3:\n- \"significant improvements on a theorem proving\"\n- \"(Selsam et al., 2019) presented\". Use \\citet{...} here.\n- \"(LTL) (Pnueli, 1977)\". Maybe use \\citep[LTL,][]{...}, here.\n\nPage 7:\n- \"this experiments\"\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "LEP5quICJSi", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 5, "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": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper applies transformer models to learning linear-time temporal logic (LTL) and propositional logic. The results show that, when trained on large datasets of random formulas, transformer models can perform quite well on within-distribution held out test tasks, and when equipped with tree-positional encodings, they exhibit generalization to longer formulas.\n\nStrengths:  \n-The paper is very clearly written \n-Novel domain for neural approaches  \n-The results on the provided datasets are strong  \n\nWeaknesses:  \nI think the main weaknesses fall into three categories: novelty of the approach, analysis and comparison to baselines, and use of purely synthetic test data.\n\nNovelty of the approach:  \nThe approach is not novel, using a transformer model and a previously proposed tree-positional encoding scheme.\nNovelty in the approach is not required, as long as the paper also contains experimental analysis which provides insight into either the technique or the problem studied, and the evaluation is thorough. However, I find that there are weaknesses in both these aspects.\n\nAnalysis and baselines:  \nThe main paper reports results of a single model, and does not report results of any baselines, besides the length generalization results. If the paper claims that transformers specifically perform well on these problems, then comparing with alternate baselines (such as sequence or tree RNNs) is necessary. If the claim is instead that high capacity models in general can perform well on important LTL tasks, then I think that the use of only synthetic test data is a weakness (see below). In either case, I think further analysis of the conditions under which the model succeeds vs fails is warranted. \n\nSynthetic data:  \nThis work evaluates models only on randomly generated synthetic test data, which I view as a disadvantage. Although the paper demonstrates that training models on a large synthetic corpus provides good within-distribution test performance (as well as length generalization), it’s unclear how it would perform on natural data. I also don’t have a clear sense of how difficult the training and testing problems are relative to tasks relevant to people. Is it possible to collect a small non-synthetic test corpus of LTL formulas, to verify that the trained models can generalize to tasks relevant to people? The LTLPattern126 dataset is constructed from formulas from 55 LTL specification patterns identified from the literature. Can the models trained on these patterns generalize to other patterns from the literature? Similarly, could models trained on a subset of the 55 patterns generalize to the held-out patterns?\n\nBecause of the lack of baselines and analysis, and the use of purely synthetic test data, it’s difficult to evaluate the results of the paper. For this reason, coupled with the fact that the approach is not novel, I recommend a weak reject. However, I would be willing to raise my score if concerns about baselines, analysis, or synthetic data were addressed. In particular, evaluation on non-synthetic data would be very valuable. \n\nAdditional suggestions:  \nAs stated above, I think more detailed experimental analysis would be very helpful, and could greatly strengthen the paper.  \n-How do transformers compare to other models, such as tree or sequence RNNs?  \n-What qualitatively (or quantitatively) distinguishes those formulas which a transformer can solve from those it can’t? Could insights here lead to proposed changes in architecture or data generation?  \n-What qualitatively (or quantitatively) distinguishes those formulas for which a transformer achieves syntactic accuracy from those for which it achieves semantic accuracy but not syntactic accuracy? Again, could insights here lead to proposed changes in architecture or data generation?  \n-Could a model trained on LTLRandom35 generalize to LTLPattern126 and visa versa?  \n-How do models with the sequence positional encoder perform on the LTLpattern126 and LTLUnsolved254 datasets? \n\nMinor comments:  \n-I’d definitely recommend moving figure 9 to the main text, as it’s the only comparison between the model and a baseline.  \n\n\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "ALGNtpcB02L", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 6, "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": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper presents a dataset of linear-time temporal logic (LTL) formulas, which are generated by conjoining popular LTL specification patterns, and then investigates the learning capability of the Transformer over these LTL formulas.  The experimental evaluation shows that the Transformer predicts solution with high accuracy and sometimes even outperforms the classic solver used for providing training data. \n\n- Quality: Though Transformers are fairly standard models, this paper shows an interesting application, i.e. solving LTL formulas, and the experimental evaluations are convincing and promising. \n- Clarity: The writing is very clear and easy to follow. \n- Originality: There is no technical innovation, but the presented dataset is new. \n- Significance: This work demonstrates the surprising capability of Transformers on predicting solutions of LTL formulas, which suggests a competitive alternative approach for solving LTL formulas, and also motivates other logical reasoning applications of Transformer.\n\nQuestions: \n\nQ1: Any particular reason for choosing \"126\"? Is it a representative size of LTL formulas in real-world verification tasks?\n\nQ2: If the Transformer _truely_ learns the semantics of LTL formulas, the syntactic distribution of LTL formulas should not matter. Have you tried to train Transformer on LTLPattern126 and tested it on LTLRandom35?\n\nQ3: Boolean satisfiability in the DNF form is trivial to solve. The propositional logic formulas seem quite close to DNF. Have you considered SAT solving in the CNF form? SAT competitions (e.g. https://baldur.iti.kit.edu/sat-competition-2017/index.php?cat=results) provide various kinds (e.g. industrial, random) of SAT benchmarks.\n\n\nMinor typos: \npage-2, \"Where we focus \" => \"While we focus\"\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "5lgfqex5uJc", "reviewer": "AnonReviewer4", "summary": "", "questions": "", "limitations": "", "rating": 7, "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": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "\nThe paper explores the application of modern learning techniques (transformers and tree positional encodings) to the task of producing valid traces for a given LTL specification. A series of experiments are conducted to explore the generalization power of the proposed approach, both in terms of formula size and style of constraint. The work follows a recent trend of the application of deep learning techniques to logic-based settings, and the authors present (to the best of my knowledge) the first attempt of applying deep learning techniques to this particular task.\n\nOne weakness of the paper is that the details on the proposed model are extremely sparse -- the authors jump from background to data sets to evaluation, without ever pausing to describe the transformer+tree propositional encoding. We are left to infer from the parameter settings included in the appendix as to what was actually done.\n\nOn the other hand, the work seems to make a significant contribution empirically. In particular, the following claim from 5.1 is extremely exciting: \"Our best model predicted correct solutions in 83% of the cases, taking on average 15s on a single CPU\". The authors fall short of describing how they will turn an arguably unsound process for generating valid traces into one that is verifiably correct, but the initial evidence looks extremely promising.\n\nThroughout the evaluation, there seems to be an over-emphasis on syntactic accuracy. There are countless ways to solve many LTL formulae, and very few for any given formula will be syntactically close. While it is an interesting phenomenon to explore in the context of other claims (such as the choice of structural representation in Fig 9), it is of very little interest to be able to map an LTL to one particular syntactic style of trace.\n\nAnother negative aspect is the claim to generalization. I'm on board with the generalization to larger instances (this seems like a wonderful result!), but the claim that using SAT encodings is indicative of generalization doesn't seem to be well supported. In particular, the very nature of the constraints has changed compared to the spot-generated benchmarks, and so there is little evidence from this evaluation that you haven't just learned to re-produce spot-like constraints. To show that level of generalization, I would expect to see a model trained using random LTL or benchmark LTL problems w/ spot, and testing done in a different (out-of-distribution) setting (like SAT or traces generated in an entirely different way than spot). Ultimately, I think that syntactic similarity is far less interesting than semantic similarity (i.e., correctness), and so I don't view this negative aspect of the paper to be substantial.\n\nI am leaning towards accepting the paper. I would like to see a more complete exposition in terms of the DL model that was actually used, but the strength of the results, particularly in the larger problem sizes, is very promising.\n\n\n1. You report on the \"best model\" results, but how do these compare to the average (mean or median)?\n\n2. How would you embed what it is that you've done to create a sound / complete trace synthesis procedure?\n\n3. How might you invert the process so that the LTL formula is synthesized that best captures a set of traces (or similarly describes the contrastive difference between two sets of traces)? E.g., the setting of \"Bayesian Inference of Linear Temporal Logic Specifications for Contrastive Explanations\" Kim et al.\n\nA final point of recommendation (not affecting my decision on the paper). It's unclear how difficult the produced formulae are for producing a valid trace -- beyond that, it is unclear even how this might be measured. But one thing that is worth considering in the discussion part of the paper (if you have a clear sense of these aspects) is where th benchmark instances lay on the spectrum of easy-to-hard. If it is overly easy to produce a trace that satisfies the formula, then the results of the paper are less interesting (I doubt this is the case, given that standard solvers in the field are failing to find a solution). It would be interesting to know if the performance of the approach is a function of the problem \"difficulty\" (or space of possible solutions).", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: The paper shows that standard transformers can be trained to generate satisfying traces for Linear Temporal Logic (LTL) formulas. To establish this, the authors train a transformer on a set of formulas, each paired with a single satisfying trace generated using a classical automata-theoretic solver. It is shown that the resulting model can generate satisfying traces on held-out formulas and, in some cases, scale to formulas on which the classical solver fails.

The reviewers generally liked the paper. While the transformer model is standard, the use of deep learning to solve LTL satisfiability is novel. Given the centrality of LTL in Formal Methods, the paper is likely to inspire many follow-up efforts. There were a few concerns about the evaluation; however, I believe that the authors' comments address the most important of them. Given this, I am recommending acceptance. Please add the new experimental results (about out-of-distribution generalization) to the final version of the paper. 
Decision: Accept (Poster)