Generating Symbolic Reasoning Problems with Transformer GANs
Authors: Jens U. Kreber
Christopher Hahn
Venue: ICLR 2022 Submitted (2022)
Keywords: Transformer
GAN
symbolic reasoning
temporal logic

Abstract: Constructing training data for symbolic reasoning domains is challenging: Existing instances are typically hand-crafted and too few to be trained on directly and synthetically generated instances are often hard to evaluate in terms of their meaningfulness. We study the capabilities of GANs and Wasserstein GANs equipped with Transformer encoders to generate sensible and challenging training data for symbolic reasoning domains. We conduct experiments on two problem domains where Transformers have been successfully applied recently: symbolic mathematics and temporal specifications in verification. Even without autoregression, our GAN models produce syntactically correct instances and we show that these can be used as meaningful substitutes for real training data when training a classifier. Using a GAN setting also allows us to alter the target distribution: We show that by adding a classifier uncertainty part to the generator objective, we obtain a dataset that is even harder to solve for a classifier than our original dataset.

Under review as a conference paper at ICLR 2022
GENERATING SYMBOLIC REASONING PROBLEMS WITH TRANSFORMER GANS
Anonymous authors Paper under double-blind review
ABSTRACT
Constructing training data for symbolic reasoning domains is challenging: Exist- ing instances are typically hand-crafted and too few to be trained on directly and synthetically generated instances are often hard evaluate in terms of their mean- ingfulness. We study the capabilities of GANs and Wasserstein GANs equipped with Transformer encoders to generate sensible and challenging training data for symbolic reasoning domains. We conduct experiments on two problem domains where Transformers have been successfully applied recently: symbolic mathemat- ics and temporal specifications in verification. Even without autoregression, our GAN models produce syntactically correct instances. We show that the generated data can be used substitute for real training data when training a classifier, and, especially, that training data can be generated from a real dataset that is too small to be trained directly. Using GAN setting also allows us to alter the target distribution: erator objective, obtain a dataset that is even harder to solve for classifier than our original dataset.
We show that by adding a classifier uncertainty part to the gen-
INTRODUCTION
Deep learning increasingly applied more untraditional domains that involve complex symbolic reasoning. Examples include the application of deep neural network architectures to SAT (Selsam
al. 2019. Selsam & Björner [019 Ozolins al.) 202T). SMT (Balunovic et al.) 2018), temporal
specifications in verification (Hahn et al. 202 Schmitt et al. 202 symbolic mathematics [Lmple
Charton 2020), or theorem proving (Loos et al. 2017 Bansal et al.) 2019 Huang et al. 2019
Urban & Jakubuv 2020).
The acquisition of training data for symbolic reasoning domains, however, is a challenge. Exist- ing instances, such as benchmarks in competitions (Biere & Claessen 2010 Froleyks et al. 1021
Jacobs et al. 2017) are typically hand-crafted, for example, in a "bring your own benchmarks set- ting (Balyo al. 2017). Since the instances typically generated synthetically. For example by random sampling (Selsam et al.] 2019 Lample & [harton 2020), or by randomly re-combining parts of existing instances (Schmitt et al. 2021). Al- though these data generation methods already lead to good results, training on randomly generated data carries the risk of training on meaningless data or the risk of introducing unwanted biases.
too few to be trained on, training data is, thus,
In this paper, we study the generation of symbolic reasoning problems with Generative Adversar- ial Networks (GANs) (Goodrellow et al. 2014) and show that they can be used to construct large amounts of meaningful training data from significantly smaller data source. GANs, however, can not immediately be applied: Symbolic reasoning problems reside typically main and, additionally, training data is typically sequential and of variable length. We show that training directly in the one-hot encoding space is possible when adding Gaussian noise to each posi- tion. We, furthermore, use Transformer (Vaswani et al.) (017)) encoder to cope with the sequential form of the data and the variable length of the problem instances.
discontinuous do-
We provide experiments to show the usefulness of GAN approach for the generation of reasoning problems. The experiments are based around two symbolic reasoning domains where recent studies on the applicability of deep learning relied on large amounts of artificially generated data: symbolic mathematics and linear- time temporal logic (LTL) specifications in verification. We report our ex- perimnntal results in three sections. We first provide details on how to achieve stable training of

---

Under review as a conference paper at ICLR 2022
standard GAN and Wasserstein GAN (Arjovsky al. 2017) both equipped with Transformer encoders. We analyze the particularities of their training behavior, such as the effects of adding different amounts of noise to the one hot embeddings. Secondly, classifier that the generated data can be used as substitute for real training data, and, especially, that training data can be generated from real dataset that is too small to be trained directly. In par- ticular, we show that out of 10K real training instances, a dataset consisting of 400K instances can be generated, on which a classifier can successfully be trained on. Lastly, we show that generating symbolic reasoning problems in GAN setting has specialty: We can alter the target distribution by adding a classifier uncertainty part the generator objective. By doing this, we show that we can obtain a dataset that is even harder to solve than the original dataset which has been used to generate the data from.
show for an LTL satisfiabilityy
The remainder of this paper is structured as follows. In Section we give a short introduction to the problem domains considered this paper and describe how the origin training data has been 3 we present our Transformer GAN architecture(s), before providing exper- We give an overview over related work in Section 5 before concluding
constructed. In Section
imental results Section
in Section
PROBLEM DOMAIN AND BASE DATASETS
In this section, we introduce the two problem domains on which we base our experiments on: sat- isfiability of temporal specifications for formal verification and function integration and ordinary differential equations (ODEs) for symbolic mathematics. We furthermore give an overview over the data generation processes of these base datasets.
2.1 HARDWARE SPECIFICATIONS IN LINEAR-TIME TEMPORAL LOGIC (LTL)
Linear-ting Temporal Logic (LTL) (Pnulli 1977) is the basis for industrial hardware specifica- tion languages like the IEEE standard PSL (EEEE Commission et al. 2005). It is an extension of propositional logic with temporal modalities, such as the Next-operator (O) and the Until-operator (l). There also exist derived operators, such "eventually" Oyp (= true U yp) and "globally" - For example, mutual exclusion can be expressed as the following specification: (accesss accessp1). ). stating that processes pO and pl should have no access to a shared re- source at the same time. The base problem of any logic is its satisfiability problem. It is the problem decide whether there exists solution to a given formula. The satisfiability problem of LTL is a hard problem, in fact, it is PSPACE-hard [Sistla & Clarke (1982). The full syntax, semantics and additional information on the satisfiability problem can be found Appendix
So far, the construction of datasets for LTL. formulas has been done in two ways (Hahn et al.) 2:2T:: Fither by obtaining LTT. formulas from a fully random generation process, which likely results in unrealistic formulas, or by sampling conjunctions of L.T specification patterns (Dwyer cet al. 1999). To obtain a healthy amount of unsatisfiable and satisfiable instances in this artificial generation process, we slightly refined the pattern-based generation method with two operations. Details can be found in Appendix B Since the formula length correlates to unsatisfiability, we filter for equal proportions of classes per formula length. We restrict the tree size of the formulas to 50. We call this dataset LTLbase.
2.2 SYMBOLIC MATHEMATICS
Lample & Charton (2000) showed that Transformer models perform surprisingly well on symbolic mathematics. More precisely, they applied the models to function integration and ordinary differen- tial equations (ODEs).
We consider the function integration problem and use the forward generated dataset (ttpp:: //github. com up to n operators are generated and their integrals are calculated with computer algebra systems. Functions that the system cannot integrate are discarded. Mathematical expressions are generated randomly. The dataset is cleaned, with equation simplification. coefficients simplification. and fil- tering out invalid expressions (Lample & Charton 2020 We restrict the tree size 50.
Symbol icMat c hematics Random functions with
2

---

Under review as a conference paper at ICLR 2022
prediction
project + avg
attn + FF
discriminator /
critic
attn + FF
noise
attn FF
generated samples
project
attn + FF
real samples
generator
attn FF
attn FF
dataset
2 (random)
Figure 1: TGAN-SR: Transformer GAN for generating symbolic reasoning problems with visual- izations of the per-position one-hot space.
3 ARCHITECTURE
The Transformer GAN architecture for generating symbolic reasoning problems (TGAN-SR) de- picted in Figure 1 It consists of two Transformer encoders as discriminator/critie and generator, respectively. The inner layers of the encoders are largely identical to standard transformers (Vaswani et al. 2017), but their input and output processing is adjusted to the GAN setting. We use an em- bedding dimension of demb 128, n,, attention heads, and feed-forward network dimension of FF 1024 for both encoders as default.
The generator's input is real sealar random value with uniform distribution [0, 1] for each position in the sequence. It is mapped to demb by affine transformation before being processed by the first layer. The position-wise padding mask is copied from the real data during training, so the lengths of real and generated formulas at the same position in batch are always identical. During inference, the lengths can either be sampled randomly or copied from an existing dataset similar to training. Either way, the generator encoder's padding mask is predetermined the unmasked positions. With V being the vocabulary, and [V] being the size of the vocabulary, an affine transformation dimensionality [V] and softmax is applied after the last layer. The generator's 's output lies, thus, in the same space as one-hot encoded tokens. We use niG = 6 layers for our default model's generator.
has adequately populate
A GAN discriminator and WGAN critic are virtually identical in terms of their architecture. The only difference that critic outputs real scalar value where discriminator is limited the range [o. 1], which we achieve by applying an additional logistic sigmoid in the end. To honor their differ- ences regarding the training scheme, we use both terms when referring to exchangeable properties and make no further distinctions between them. For input processing, their |V]ddimensional (per position) input mapped demb by an affine transformation. After the last layer, the final embed- dings aggregated over the sequence by averaging and a linear projection scalar value (the prediction logit) is applied. Our default model uses nu layers. We achieved best results with slightly more generator than discriminator/critic layers. A full hyperparameter study be found in AppendixC C.2
Working in the Vl-sized one-hot domain poses harsh constraints the generator's 's output. Contrary to continuous domains were GANs are usually employed, each component of real one-hot vector is, by definition, either 0 or 1. If the generator were identify this distribution and use it criterion
3

---

Under review as a conference paper at ICLR 2022
0.3
2
0.2
WGAN GAN
WGAN
GAN
0
0
2
3 -102
training steps
-104
training steps
(a) fully correct fraction
(b) sequence entropy
Figure 2: Quality measures for the GAN and WGAN variant when generating temporal specifica- tions.
tell real and generated instances apart, this would pose a serious difficulty for training. We therefore sample |Vi-sized vector of Gaussian noise ((, ozea)) for each position (see Figure 1}. We add to the real samples' one-hot encoding and re-normalize it to sum before handing them to the discriminator/critii.. By default, use value of real 0.1 for all models to get comparable results. We study the effect of different amounts of noise more closely in Section 4.1.2
4 EXPERIMENTS
In this section, report our experimental findings. We structure results in three sections. We first report on the performance of the TGAN-SR architecture in constructing syntactically correct instances of temporal specifications and mathematical expressions. Secondly, for LTL formulas, that the newly generated dataset can be used as a substitute for the origin dataset. Lastly, we show, by altering the target distribution, that the network can generate dataset that is harder to solve for classifier. We trained the models on an NVIDIA DGX A A100 system for around hours. We begin each subsection with a short preamble on the training setting.
show, exemplary
4.1 PRODUCING SYNTACTICALLY CORRECT SYMBOLIC REASONING PROBLEMS
The goal of the experiments in this section is to asses the generator's capability in creating valid symbolic reasoming problems objectively as possible. If not stated otherwise, in plots and ta- bles, we report results from our default model averaged across three runs and with an exponential smoothing (a 0.95) applied. For temporal specifications, we use I.TLbase as training set and for symbolic math the dataset described in section 2.2
4.1.1 TRAINING SETTING
For the GAN variant, we employ the standard GAN training algorithm (Goodfellow et al.) 2014) For our default model, we use n. 2 discriminator training steps per generator training step and a batch size of bs = 1024. Notably, we use the alternative generator loss - -Espp [log (=G instead of the theoretically more sound Es-ps [log (1 D(G()))) The WGAN variant uses the WGAN-GP training with gradient penalty proposed by Guirajani et al. (2017) with Agr = 10. Standard WGAN losses are used and the training loop parameters n. and bs are identical to the GAN variant. To calculate the gradient penalty of intermediate data points according to Guirajani et al. (017). we make use of the fact that for each batch element, real and generated samples share the padding mask. After the gradient with respect an intermediate point is calculated, the gradient's squared components are masked out at padded positions before being summed up over the sequence length. For both variants, both discriminator and generator trained with the Adam (Kingma & Bal (015) optimizer (31 = 0, 32 = 0.9) and constant learning rate = le 4, similar to Gulrajani al. (2017).

---

Under review as a conference paper at ICLR 2022
WGAN dist.
0.5
GAN real
GAN gen
0
2
3
training steps
-101
Figure 3: GAN real/generated predictions and WGAN Wasserstein distance estimate when generat- ing temporal specifications.
4.1.2 RESULTS
Generating valid symbolic reasoning problems. During training periodically sample several generated instances and convert them to their text representation, which involves taking the argmar every position. We then try parse prefix-encoded tree from the resulting tokens. If the parsing of a problem is successful and no tokens remain in the sequence, we note this problem as fully correct. The fraction over the course of training to generate temporal specifications is depicted in Figure [a] Both GAN and WGAN variants increase the measure relatively continuously, but eventually reach their limit around 30K training steps. Still, both generators are able produce large fraction of fully correct temporal specifications, despite the length of the instances (up to 50 tokens) and the non non-autoregressive, fixed-step architecture. We list some examples below:
-hh - -
(a
A- - A -O
A -
+ c) +
+ +c) - - [d) Am -
The network also produces correct symbolic mathematical expressions when training on the forward generated mathematical dataset of Lample & Charton 2020). After 30K steps, average 30% fully correct. We list some examples below:
23 ((-1) (In .x)3 + (acosh (5) + (-1) x (2+x)* 1))
1 81264 5 1n +
(3 (x)) +2 (2+ . x 201 acos(44))
Differences in homogeneity, Comparing the valid generated formulas from the WGAN and GAN variants, we find that often, the latter would produces formulas in the likes of
OOOCOOOOOOO A -0000000000000000000000---0000 (gAgAi) or
lanh 1923356666679995766666
which contains repetitions (of the O-operator) or easily stringed together sequences (for example of numbers). fact, some GAN runs achieved fully correct fractions above 30% (higher than WGAN), but these exclusively produced formulas with such low internal variety. To quantify this, we calcu- lated a sequence entropy which treats the number occurrences of the same token in the sequence relative to the sequences length as probability. Figure 26 shows that indeed this metric decreases for the GAN variant during training but remains stable for WGANs. We therefore speculate that the discriminator/ccrttcc indeed learns to check syntactic validity some extend and some generators "exploit" this fact by producing correct, but repetitive formulas. For further experiments that use generated instances, we therefore exclusively stick the WGAN variant.
Discriminator critic predictions. We observe quick identification of real and generated in- stances by the GAN discriminator depicted in Figure 3 Predictions reach values above 0.99 and
5

---

Under review as a conference paper at ICLR 2022
1
real
1
real
0.2
0.2
0.1
0.1
0.05
0.05
0.5
0.5
0
0
0
0
0
0.5
1.5
0.5
1.5
training steps
-104
training steps
-104
(a) generated, original
(b) generated, arg-maxed
Figure 4: GAN discriminator predictions for generated samples with different noise level real real samples when generating temporal specifications.
below 0.01, respectively, and change directions. Similarly, the WGAN critic's Wasserstein distance estimate soon reaches value of around 0.4 at which it remains for the rest of training. For this behavior, one would expect the generator not improve significantly, which contrary the observed improvements in quality.
Effeets additive noise on one-hot representation. We also studied the effect adding dif- ferent amounts of noise to the one-hot representation of real temporal specification instances (see T.. It strongly affects the performance of the GAN scheme, which is unable to work without added noise. Stronger noise however improves this variants performance. WGAN models the other hand were not significantly influenced by added noise and are able to be trained without it.
Additionally, compare how the GAN discriminator rates unmodified generated instances and argmazed versions thereof (see Figure 4. For this, we also evaluate argmared instances during each step of training without changing the training regime. While the score for unmodified instances immediately decreases at the start of the training, it initially rises for the arymazed ones. After while of training. though, the scores of the argmazed samples quickly deteriorate and, least for lower values of Greal, approach their soft-valued counterparts. A possible interpretation is that the discriminator first identifies generated samples by their different distributions in the one-hot domain, which, naturally, is eased with low noise the real samples, before shifting its focus from this low- level criterion to more global features.
4.2 SUBSTITUTING TRAINING DATA WITH GENERATED INSTANCES
In this subsection, we show that the origin training data can be substituted with generated training data when training a classifier on the LTL satisfiability problem.
Table 1: Comparison on fully correct formulas (fe) and sequence entropy (se) of GAN and WGAN with different Treat when generating temporal specifications. 3-run average, smoothed (a 0.95), standard deviations in Table 5
architecture
Oreal
fc
architecture
Treal
fc
(%%
26%
2.2
0.05
15%
1.7
0.05
25%
2.2
GAN
0.1
17%
1.8
WGAN
0.1
31%
2.2
0.2
41%
0.2
25%
2.2
0.4
11%
2.2
0.4
3%
2.4

---

Under review as a conference paper at ICLR 2022
4.2.1 TRAINING SETTING
Binary classifier. We use classifier that is similar to the GAN discriminator, consisting of Transformer encoder followed by an averaging aggregation and linear transformation to a scalar output value. Finally, a logistic sigmoid is applied to obtain prediction for the formula's satisfiabil- ity. The classification loss is standard cross-entropy between real labels and predictions. Similar to the GAN discriminator, we use ni 4 layers and a batch size of bs 1024. Contrary to GAN training scheme, use the default Transformer scheme Vaswani et al. (2017) with varying learning rate and 4000 warmup steps as well as the Adam optimizer Kingma & Ba (2013) with pa- rameters 31 0.9, 82 0.98. This training scheme resulted in faster improvement and higher final accuracy than adopting the settings from GAN training. We trained the classifier for 30K steps.
Generated dataset. To obtain a dataset of generated instances, we first train a WGAN with de- fault parameters but smaller batch size of 512 set of 10K instances from the LTLbase dataset. After training for 15K steps, we collect 800K generated formulas from it and call this dataset Generated-ran This set is processed similar to the original base dataset: Duplicates are moved and satisfiable and unsatisfiable instances are balanced to equal amounts per formula size. We randomly keep 400K instances and call the resulting dataset Generated.
4.2.2 RESULTS
We compare the performance of similar classifiers on different training sets in Table 2 The training curves can be found in Appendix C.3 The validation accuracy is computed on the LTLbase dataset. Training on differently-sized subsets LTLbase shows that a reduced number of training samples strongly decreases performance. 10K instances lead to immense overfitting and poor accuracy. We were not able to train a classifier on this few formulas with significantly higher accuracy.
A classifier trained the Generated set however achieves almost the identical validation accu- racy on the base set as the classifier that was actually trained on it. Note that the GAN that created this set trained only 10K instances. We therefore find that the data produced by the TGAN- SR is highly valuable as it can serve as full substitute for the complete original training data even when provided with much fewer examples.
Two instances of LTLbase (a) A (00a) and (CO)) A (0-))), i.e. only 0.02%, reappear in the 800K large data set Generated-zan Additionally, in Generated only 2.3K of the 800K (0.28%) generated formulas were duplicates, which displays an enormous degree of variety.
4.3 UNCERTAINTY ORIECTIVE FOR GENERATING MARDEER-TO-CLASSEE INSTANCES
In this experiment, we show that, by adding an uncertainty measure to a simultaneously trained classifier, the model generates instances temporal specifications in LTL. that are harder to classify. We train a model on the I. TLbass dataset to jointly learn to imitate its formulas and classify them as satisfiable or unsatisfiable.
4.3.1 TRAINING SETTING
GAN with included classifier. For this experiment, we combine both critic and LTL satisfiability classifier into one Transformer encoder with two outputs and train them simultaneously. Both parts
Table 2: Accuracies of Transformer classifiers trained different datasets (5-rum average with standard deviations in parentheses); all are validated on the LTLbase dataset.
trained on
bs
train acc 30K
val ace 30K
train ace @ 50K
val acc @ 50K
1024
96.6% (0.5)
95.5% (0.4)
98.1% (0.3)
96.1% (0.3)
LTLbase
512
92.4% (0.7)
93.0% (0.8)
95.4% (0.5)
95.0% (0.8)
LTLbase 100K
512
95.3% (0.7)
88.3% (0.9)
98.1% 1% (0.3)
87.8% (1.0)
LTLbase 10K
512
100% (0.1)
76.4% (1.7)
100% (0.0)
75.5% (1.5)
Generated
1024
95.4% (0.2)
93.6% (1.0)
97.1 % (0.1)
93.9% (0.3)

---

Under review as a conference paper at ICLR 2022
share the three lower layers of the encoder but have separate fourth layers. We found this to improve both classification accuracy and GAN performance slightly compared to sharing all layers (the linear projection layer is never shared). A comparision can be found in Section C.I in the appendix. We stick to the WGAN training scheme from Section 4.1.1 including the optimizer settings, but add an additional classification loss term similar to Section 4.2.T The classification loss is added to the GAN critic loss and scaled by coefficient Gllasss which we set to 10 when training a WGAN. The resulting model achieves similar generative performance the pure WGAN but is limited to classification accuracy of around 92%.
Classifier uncertainty. We calculate the entropy of a class prediction s of the classifier as Hs) -s log(s) -) -log(1 s), as a measure uncertainty on a particular instance. We add a term (u (s) to the generator's loss function, which leads to the uncertainty measure being propagated back through the critic just like the standard GAN objective. H(s) is maximized at 0.5 (with value log 2), so the generator is encouraged to produce instances which "confuse" the classifier included in the critic. Naturally, this conflicts with the original GAN objective, so they must be carefully balanced. As default, we chose Occonf 2. Since GAN training is hindered by adding the uncertainty objective, we only apply it after pre-training for 30K steps with default WGAN and classification objectives. We then train for additional 15K steps with the uncertainty objective included. This decreases the fraction of fully correct formulas to around 10%; sequence entropy as classification accuracy remain unaffected. From the fully trained model, we obtain a dataset similar to Section 4.2. and land call it Uncert-e. Additionally, we construct dataset of 200K formulas from this set and 200K from LTLbase and call it Má xed-e.
Alternative uncertainty objective. The entropy becomes unhandy to compute for values close to O and 1. We therefore explore a pragmatic alternative measure for (un (un)eertainty: the absolute value of the classification logit. Values close to zero lead to predictions around 0.5. We therefore add a generator loss of the form Oumail| for this variant (with / the classification logit; (l)) and use a value of Oreonf = 0.5 in this case. The model is trained similar to the entropy variant and behaves very similarly. We call the dataset obtained from this model Uncert and also construct a mixed set Mixed-a, a.
4.3.2 RESULTS
We compare the accuracy of classifiers trained similar to Section (pure classifiers with optimized training schedule, not included GAN classifiers) on different (generated) datasets in Table 3 The classifier trained on LTLbase serves as reference again with 94.5% accuracy. Training on the Uncert sets however allows the classifier to achieve only 91% and 90.5% accuracy (for entropy and absolute variants, respectively). Also when trained longer than 30K steps, there is no significant improvement.
The datasets produced by WGANs with added uncertainty objective are indeed harder to classify than the original dataset LTLbase. To validate this, we also trained classifiers on Mixed sets and find that they also achieve 4.5 percent points higher accuracy when tested on the base set compared to the generated sets. Additionally, the performance the original dataset is never deteriorated and even slightly higher when training on the mixed set. This approach is especially useful in the domain of symbolic reasoning, because data can, in contrast archetypal deep learning domains, often be labeled automatically (e.g. with classical tools and algorithms). This underpins the usefulness of GAN setting when generating new training instances for symbolic reasoning problems.
Table 3: Performance of classifiers trained and tested on datasets generated with uncertainty objec- tives; 30K steps, 5-run average with standard deviations, not smoothed.
trained on LTLbase Uncert-e
tested on LTLbase
accuracy
trained on
tested on
accuracy
94.8% (0.3)
Uncert-e
91.0% (0.5)
Uncert-a
Uncert-a Uncert-a
90.5% (0.5)
Mixed-e
Uncert-e
90.2% (0.9)
Mixed-a
89.6% (0.4)
Mixed-e
LTLbase
95.3% (0.4)
Mixed-a
ITLbase
94.1% (0.4)
8

---

Under review as a conference paper at ICLR 2022
5 RELATED WORK
GANs.
Generative Adversarial Networks have been applied to discrete domains especially for text
generation in a reinforcement learning setting (Chen et al. 2018: Yu al. 2017 Che et al. 2017
Lin et al. 2017, Fedus et al. 2018 Guo et [ or by using a Gumbel softmax (Kusner & Hernandez-Lobato [0166] Zhang et al.). Kumar& & Tsvetkov 2020) use continuous, pre-trained embedding. Gulraaani et al. (2017) showed that it is possible to directly use a soft one-hot repre- sentation without any sampling. Close related work is |uuan et al. (2020) and Zeng al. (2020) for adversarial text generation. They also combine Transformers and in an adversarial learning setting, where the former rely on Gumbel softmax tricks and the latter extract a style code from reference examples. Transformers and GANs have also been combined in the domain of computer vision (Vondrick & Torralba 2017; Jiang et al., 2021] Hudson Zitnick 2021). GANs have been used for data augmentation, especially for images, e.g.. (Antoniou et al. 2018 Bowles et al. 2018
Temporal logics. Temporal logies have been studied in computer science since their introduc- tion by Pnueli (1977). Since then, many extensions have been developed: e.g.. computation tree logic CTL and CTL (Clarke & Emerson 1981 Emerson & Halpem 1986). signal temporal logic
STL MMaler & Nickovic, 2004), or temporal logics for hyperproperties, e-g., HyperL.TI. CClarkson
jet al.
2014). Verification methods for temporal logics have been studied extensively over the years,
e.g.,
LTL satisfiability (Li et al. [013)] Rozier & Vardi, 2007 SSchuppan & Darmawan 2011
ct al.
2013
2014) Schweediann 1998). LTL synthesis (Finkbeiner & Schewel 2005| 2013 Bohy
al.
2012
Faymonville et al.)
2017 Meyer al. 2018), model checking (Clarke al. (9866) or
monitoring (Clarke et al. 2001: Bauer et al. 2011 Finkbeiner & Sipma 2004 Donzé et al. 2013
Mathematical reasoning in machine learning.
Other works have studied datasets derived from 2017: Gauthier et al., 2021). inter-
automated theorem provers (Blanchette et al. 2016: Loos et al.
active theorem provers (Irving et 2016 Kaliszyk et 2217
[Bansal et al.] Huang et al.,
2019
Yang & Deng, 2019; Polu & Sutskever, 2020
Wu et al.]
b02 Li et al. 2020 Lee et al.,
2020
Urban & Jakubuv| 2020] Rabe et al.
2021:
Paliwal et al. 2020 Rabe & Szegedy 202
symbolic mathematics (Lample & Charton 2020 Zaremba et al. 2014|] Allammniis
al. 2017
Arabshahi et al.] 2018). and mathematical problems in natural language (Saxton et al. [019 Schlag
et (0199) Learning has been applied to mathematics long before the rise of deep learning. Harlier
works focused on ranking premises or clauses (Cairns) 2004 Urban 2004 2007
Urban et al.
2008
Meng & Paulson
2009 Schulz 2013
Kaliszyk & Urban 2014).
Neural architectures for logical reasoning. Wu et al. (2021a) present a reinforcement learning approach for interactive theorem proving. NeuroSAT (Selsam et al., 2019) is a graph neural net- work (Scarselli et al. 2009; Li et al. 2018 Gilmer et al., 2017 Wu et al., 2021c) for solving the propositional satishability problem. simplitied NeuroSAT architecture was trained for unsat-core predictions (Selsam & Bjomer 2019). Neural networks have been applied to 2QBF (Lederman
al.] 2020), logical entailment (Evans et al. 2018). SMT (Balunovic et al. 2018), and temporal logics (Hahn et al., 2021; Schmilt et al. 2021
6 CONCLUSION
We studied the capabilities of (Wasserstein) GANs equipped with two Transformer encoders to gen- erate sensible training data for symbolic reasoning problems. We showed that both can be trained directly on the one-hot encoding space when adding Gaussian noise. We exemplary conducted ex- periments in the domain of symbolic mathematics and hardware specifications in temporal logics. We showed that training data can indeed be generated and that the data can be used as a meaningful substitute when training classifier. Furthermore, we showed that GAN setting has a speciality: by adding an uncertainty measure to the generator's output, the models generated instances on which a classifier was harder to train on. In general, logical and mathematical reasoning with neural net- works requires large amounts of sensible training data. Better datasets will lead to powerful neural heuristics and end-to-end approaches for many symbolic application domains, such as mathemat- ics, search, verification, synthesis and computer-aided design. This novel, neural perspective on the generation of symbolic reasoning instances is also of interest to generate data for tool competitions, such SAT, SMT, or model checking competitions.
9

---

Under review as a conference paper at ICLR 2022
REFERENCES
Miltiadis Allamanis, Pankajan Chanthirasegaran, Pushmeet Kohli, and Charles Sutton. Learning continuous semantic representations of symbolic expressions. In Doina Precup and Yee Whye Teh (eds.), Proceedings of the 34th International Conference
Machine Learning, ICML 2017. Sydney, NSW, Australia, 6-11 August 2017, volume 70 of Proceedings of Machine Learn- ing Research, pp. 80-83 88. PMLR, 2017. URL http: http:::/procceiingg.. mwt.presssvv0/ al allamanisi7a.he html
Antreas Antoniou, Amos Storkey, and Harrison Edwards. Augmenting image classifiers using data augmentation generative adversarial networks. In Vera Kurková, Yannis Manolopoulos, Bar- bara Hammer, Lazaros Iliadis, and Ilias Maglogiannis (eds.), Artificial Neural Networks and Machine Learning- ICANN 2018 27th International Conference on Artificial Neural Networks, Rhodes, Greece, October 4-7, 2018, Proceedings, Purt III, volume 11141 of Lecture Notes in URL
Computer Science, pp. 594-603. Springer, 2018. doi: 10. 10.1007/978.3--00-004222 https::/ddon /tg///i..ggg...../ 1007 978 030 01424-7 5_
Forough Arabshahi, Sameer Singh, and Animashree Anandkumar. Towards solving differential equations through neural programming. In ICML Workshop on Neural Abstract Machines and Program Induction (NAMPI), 2018.
Martín Arjovsky, Soumith Chintala, and Léon Bottou. Wasserstein GAN. CoRR, abs/ 101107877, 2017. URL htRp://p://aatt
orq/ abs /wtp///1.....00
Mislav Balunovic, Pavol Bielik, and Martin T. Vechev. Learning to solve SMT formulas. In Advances Neural Information Processing Systems 31: Annual Conference on Neural In- formation Processing Systems 2018, NeurlPS 2018, December 3-8, 2018, Montréal, Canada, pp. 10338-10880 10349, 2018. URL https: http:::///ccceeeeeeeeeee wwwpeeeeeedinnn...eiees.ee newrips. wct.eecc/pcc cc/paper/2018/ http://63311000725511555555 2tt.://5555166111eeee6e2233233-3
htmll
Tomášs Balyo, Marijn J.H. Heule, and Matti Järvisalo. Proceedings SAT Competition 2017: Solver and Benchmark Descriptions, volume B-2017-1 of Series of Publications B. Department of Com- puter Science, University of Helsinki, Finland, 2017.
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. Holist: An environment for machine learning of higher order logic theorem proving. In Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Research, pp. 454 463. PMLR, 2019.
mlr www.spresss...mm wwtpsss/vv//bbe http//////aaaaaalaaaa// html
Andreas Bauer, Martin Leucker, and Christian Schallhart. Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4): 2011. doi: 10. 10.1145/2000799
URL https:://ol..og///333/ 0ttp:///01111111000990. 200000000000990000
Armin Biere and K Claessen. Hardware model checking competition. In Hardware Verification Workshop, 2010.
Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. Hammering towards QED. J. Formaliz. Reason., 11):101-148, 2016. doi: 10.6092/issn. 1972-57874453.. URL https: wwrddi..org/// wttg//...... 6092 issn 191....77999777775933333
Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Naiyong Jin, and Jean-François Raskin. Aca- cia+, tool for LTL synthesis. In Computer Aided Verification 24th International Conference,
CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, volume 7358 of Lecture Notes in Computer Science, pp. 652 657. Springer, 2012. doi: 10. 10.1007/978 3-222---4222--- 45. URL https://do1 org. 00.11.0000000 1007 978
642 31 424 4_
Christopher Bowles, Liang Chen, Ricardo Guerrero, Paul Bentley, Roger N. Gunn, Alexander Ham- mers, David Alexander Dickie, Maria del C. Valdés Hernández, Joanna M. Wardlaw, and Daniel Rueckert. GAN augmentation: Augmenting training data using generative adversarial networks. CoRR, abs/1810 810. 10863, 2018. hRLpttp: //tp::////iiiii wwwp:ivwooggg/bb/oeee www.r//ab///111/ 10863
10

---

Under review as a conference paper at ICLR 2022
Paul A. Cairns. Informalising formal mathematies: Searching the mizar library with latent seman- tics. In Mathematical Knowledge Management, Third Interaational Conference, MKM 2004, Bialowieza, Poland, September 19-21, 2004, Proceedings, volume 3119 of Lecture Notes in 5. URL
Computer Science, pp. 58-72. Springer. 2004. doi: /t0 /0. 1007/ 978- 3--50-278188-0
https://dof .r..orgg//
Tong Che, Yanran Li, Ruixiang Zhang. R. Devon Hjelm, Wenjie Li, Yangqiu Song, and Yoshua Bengio. Maximmum-lkkeliooo augmented discrete generative adversarial networks. CoRR, abs/1702.07983, 2017. URL /ttp:////aavvvve/. org/ abs 07983
Liqun Chen, Shuyang Dai, Chenyang Tao, Haichao Zhang, Zhe Gan, Dinghan Shen, Yizhe Zhang, Guoyin Wang. Ruiyi Zhang, and Lawrence Carin. Adversarial text generation via feature- mover's distance. In S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett (eds.), Advances in Neural Information Processing Systems, volume 31. Curran As- sociates, Inc., 2018. URL https: htt.tttss: pttttps://prrcceednng.. neurr....eerie ips htcp/papprr2211//5550 074177d3eb63 e 32c1 1e545a3bbf0000 Paper, Paaebb-apppp.... pdff
Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-tie time temporal logic. In Logies of Programs, Workshop, Yorktown Heights, New York, USA, May 1981, volume 131 of Lecture Notes in Computer Science, pp. 52-71. Springer, 1981. URLhtttaa //toi www.orgg.0... 1000 1010000/////0777
doi: 10. 10.1007/BF00025774,
Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst., (2):244 1986. doi: 10.1145/5397.5399 URL 5399
Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model checking. MIT Press, 2001, ISBN 478-0-262-03270-4 URL http::/books. http//ooook.ooolllee... www.looooo...ooo.ooooooo.o de/books w
Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. Temporal logics for hyperproperties. In Martín Abadi and Steve Kremer (eds.), Principles of Security and Trust- Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8414 of Lecture Notes in Computer Science, pp- 265 284. Springer, 2014. doi: 10. 000000/9--3-642-447999999
15. URL httlhttps://// /do. org/
10. 10.1007/978 3 642 2 54792 15
Alexandre Donzé, Thomas Ferrére, and Oded Maler. Efficient robust monitoring for STL. In Natasha Sharygina and Helmut Veith (eds.), Computer Aided Verification 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pp. 264-279. Springer, 2013. doi: 10. 10111110----722--9999970 39799-887 org 1007
URL https:
642 39799-389 8_19
Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Patterns in property specifications for finite-state verification. In Proceedings of the 2/st International Conference on Software Engineering, ICSE '99, pp. 41 1420, New York, NY, USA, 1999. Association for Computing Machinery, ISBN 1581 130740. doi: 10. 10.1145/302405.302677 ICSE '99.
1145/302405 302672
E. Allen Emerson and Joseph Y. Halper. "sometimes" and "not never" revisited: branching versus linear time temporal logic. J. ACM, 33(1):151-77,, 1986. doi: 10.1 10.1145/4904.4999 URL.
hittps://do. leedoi..rgg/i. wrw/r0rg..0.. 11451115/444 904. 4999
Richard Evans, David Saxton. David Amos, Pushmeet Kohli, and Edward Grefenstette. Can neural networks understand logical entailment? In 6th International Conference on Learning Represen- fations, ICLR 2018, Vancouver, BC, Canada, April 30 May 3, 2018, Conference Track Proceed- ew. wwt.:/iwwweeeeeeeeee.e..em.eee forum? 2 0%
ings. OpenReview.net, 2018. uRIlhtttp:://ppeeeee
Peter Faymonville, Bernd Finkbeiner, and Leander Tentrup. BoSy: An experimentation framework for bounded synthesis. In Computer Aided Verification 29th International Conference, CAV 2017, Heidelberg. Germany, July 24-28, 2017, Proceedings, Part II, volume 10427 of Lecture Notes in Computer Science, pp. 325-332. Springer, 2017. doi: 10. 00.1007/978-3331--3339
17.

---

Under review as a conference paper at ICLR 2022
William Fedus, Ian J. Goodfellow, and Andrew M. Dai. Maskgan: Better text generation via filling in the In 6th International Conference on Learning Representations, ICLR 2018, Vancouver, BC, Canada, April 30- May 3. 2018, Conference Track Proceedings. OpenReview.net, 2018.
URL
Bernd Finkbeiner and Sven Schewe. Uniform distributed synthesis. In 20th IEEE Symposium on Logic in Computer Science (LJCS 2005), 26-29 June 2005, Chicago, II, USA, Proceedings, pp. 321-330 133-030. IEEE Computer Society, 2005. doi: 10.1 101119991...0005..0
URL https:://doi
org brg/10.1109/IITC 2005.53
Bernd Finkbeiner and Sven Schewe. Bounded synthesis. Int. J. Softw. Tools Technol. Transf., 15(5- 6):519-539, 2013. doi: 00.1007/11009-012-2222 URL https: /////////i./o/// www.eiiorrrr...0 1007/
s 1000999012-022-22
Bernd Finkbeiner and Henny Sipma. Checking finite traces using alternating automata. Formal Methwds Syst. Des., 24(2):101-127, 2004. doi: 10. B00.::..FRR..00000711110 https::/dde org. 1ttp://1.111111.1 1021/022BBBBBB 0000C1170007771100 28096. 48
URL
Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda. Sat competition 2020.
Artificial Intelligence, 301:10 2021.
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. Tactic- toe: Learning to prove with tactics. Autom. Reason, 65(2):257-286, 2021. doi: 10.1007/ -10817-020-09580-x URL/tttps:/ /ttp::///doi //wo//dooiio .rll.org//// 10. 1007 02001020-11000000000 11111111110101111111111111111111 09580-x
Justin Gilmer, Samuel S. Schoenholz, Patrick F. Riley, Oriol Vinyals, and George E. Dahl. Neu- ral message passing for quantum chemistry. In Proceedings of the 34th International Con- ference on Machine Learning, ICML 2017, Sydney, NSW, Australia, 6-11 August 2017, vol- ume 70 of Proceedings of Machine Learning Research, pp. 1263-1267771 1272. PMLR, 2017. URL http://proceedings www.innggsm.....m.mmmm mlr. wttppppppsss.p/s/pppppte htte7////mmmmm.........
lan Goodfellow, Jean Abaget-Abadie, Mehdi Mirza, Bing Xu, David Warde-Farley, Sher- jil Ozair, Aaron Courville, and Yoshua Bengio. Generative adversarial nets. In Z. Ghahramani, M. Welling, C. Cortes, N. Lawrence, and K. Q. Weinberger (eds.), Advances in Neural Information Processing Systems, volume 27. Curran Associates, Inc., 2014. URL
neuris... cc/ cc/ppaper/2114/112 Paper..ppppp.... pdf
Ishaan Gulrajani, Faruk Ahmed, Martin Arjovsky, Vincent Dumoulin, and Aaron Courville. Im- proved training of wasserstein gans. In I. Guyon, U. V. Luxburg, S. Bengio, H. Wallach, R. Fer- gus, S. Vishwanathan, and R. Garnett (eds.), Advances in Neural Information Processing Systems, volume 30. Curran Associates, Inc., 2017. URL
neurips. cc/ pdf NIPS
'17
Jiaxian Guo, Sidi Lu, Han Cai, Weinan Zhang, Yong Yu, and Jun Wang. Long text generation via adversarial training with leaked information. In Sheila A. Mcllraith and Kilian Q. Weinberger (eds.). Proceedings of the Thirty- Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA,
February 2-7, 2018, pp. 5141-5148, AAAI Press, 2018 URL https: /www www.aara.a............... org/ ocs/ php/ AAT.AAAAAAAAAAAAAAA
vttp///60www 16360
Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus Norman Rabe, and Bernd Finkbeiner. Teaching temporal logics neural networks. In 9th International Conference on Learning Rep- resentations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net, 2021. URL net/ wtt.://www.ee///omrrd-------- Forum?iddd0c0oe E4byz]
Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. Gamepad: A learning envi- ronment for theorem proving. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. URL https:
//openreview. net/ffrum? d=r x
12

---

Under review as a conference paper at ICLR 2022
Fei Huang, Jian Guan, Pei Ke, Qihan Guo, Xiaoyan Zhu, and Minlie Huang. A text gan for language generation with non-autoregrressive generator. 2020.
Drew A Hudson and Lawrence Zitnick. Generative adversarial transformers. arXiv preprint arXiv:2103.01209, 2021.
CEEE-Commission et al. Ieee standard for property specification language (psl). IEEE Std 1850- 2005, 2005.
Geoffrey Irving, Christian Szegedy, Alexander A. Alemi, Niklas Eén, François Chollet, and Josef Urban. Deepmath deep sequence models for premise selection. In Advances Neural Information Processing Systems 29: Annual Conference on Neu- ral Information Processing Systems 2016, December 5-10, 2016, Barcelona, Spain, pp- 2235 2243, 2016. URL https/tttss//prroeeedda neurips wttpaaappppp.ppppppeeeea/a/ /ct/paper/2216/hast/ E19700
Absttsattbtttttat.. html
Swen Jacobs, Roderick Bloem, Romain Brenguier, Rüdiger Ehlers, Timotheus Hell, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, and Adam Walker. The first reactive synthesis competition (SYNT- COMP 2014). Int. J. Softw. Tools Technol. Transf., 19(3):36-3390, 2017. doi: 10.1007/ http::
310009-016-0416-3
org http:/10.1007/110000000
0416-3
Yifan Jiang, Shiyu Chang, and Zhangyang Wang. Transgan: Two transformers can make one strong gan. arXiv preprint arXiv: 202.: 07004, 2021.
Cezary Kaliszyk and Josef Urban. Learning-assisted automated reasoning with flyspeck. J. Autom.
Reason., 53(2) 2014. doi: 10. 10.1007/110817-014-99000 9303-33. URL https: //doi. http//oo.../ org/
10.11077810011-0144-3300
Cezary Kaliszyk, François Chollet, and Christian Szegedy. Holstep: machine learning dataset for higher-order logic theorem proving. In 5th International Conference on Learning Represen- tations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings. OpenRe- view.net, 2017. htthstt:::
wwwp///epeeeeeeeeeeee/eee. htttps://pperreiieee net. weet//orum?ld-yyuuee Ymvel
Diederik P. Kingma and Jimmy Ba. Adam: A method for stochastic optimization. CoRR, Abs/1412.6980, 2015.
Sachin Kumar and Yulia Tsvetkov. End-to-end differentiable GANs for text generation. In Pro- ceedings on "I Can't Believe It's Not Better!" at NeurlPS Workshops, volume 137 of Pro- ceedings of Machine Learming Research, pp. 118-128. PMLR, 12 Dec 2020. URL http: 7/proceedings. mlr. www.:m.w..p...meemmm
html
Matt J. Kusner and José Miguel Hernández-Lobato. Gans for sequences of discrete elements with the gumbel-softmax distribution. ArXiv, abs/161 1.04001,, 2016.
Guillaume Lample and François Charton. Deep learning for symbolic mathematics. In 8th
International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net, 2020. URLhttps: httts:://openreeeee S1eZYeHFDS
net/ forum?id-
Gil Lederman, Markus N. Rabe. Sanjit Seshia, and Edward A. Lec. Learning heuristics for quantified boolean formulas through reinforcement learning. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net, 2020.
(tRLtttss:://// httttps::/ppeereeee new..w.w.e.... net./ forum? uXREKDD
Dennis Lee, Christian Szegedy, Markus N. Rabe, Sarah M. Loos, and Kshitij Bansal. Mathe- matical reasoning in latent space. In 8th International Conference on Learning Representa- fions, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net, 2020. URL htttps://ppenrev/ net hww.:/nrt.oorm 1immmmddkskkkkeeeeemmmmm
Jianwen Li, Lijun Zhang, Geguang Pu, Moshe Y. Vardi, and Jifeng He. LTL satisfiability checking revisited. In 2013 20th International Symposium Temporal Representation and Reasoning, Pensacola, FL, USA, September 26-28, 2013, pp. 91-98. IEEE Computer Society, 2013. doi: 10.1109/TIME.2013..0 URL http:: .rr.a..rrrggoooo 1011110900MM/ 2013.19
13

---

Under review as a conference paper at ICLR 2022
Jianwen Li, Yinbo Yao, Geguang Pu, Lijun Zhang. and Jifeng He. Aalta: LTL satisfia- bility checker over infinite/fnitte traces. In Proceedings of the 22nd ACM SIGSOFT Inter- national Symposium November 16 - 22, 2014, pp. 731-734. ACM, 2014.
Foundations of Software Engineering. (FSE-22), Hong Kong. China, doi: 10. 10.1145/26338882266616
URL.
bitps:///of: .rgg 11w.1...1111118881111 201.55666866666688
Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. Modelling high-level mathematical reasoning in mechanised declarative proofs. CoRR, abs/2006.09265, 2020. URL https:
//axxiv.org/ aba///ba/20000 httpb./22000000 09265
Yaguang Li, Rose Yu, Cyrus Shahabi, and Yan Liu. Diffusson convolutional recurrent neural net- work: Data-driven traffic forecasting. In 6th International Conference on Learning Representa- tions, ICLR 2018, Vancouver, BC, Canada, April 30 May 3, 2018, Conference Track Proceed- net forum?id=sJiHXGHE
ings. OpenReview.net, 2018. Utthttts::///// http:////pppreviieeeeeee opennvvvv///.
Kevin Lin, Dianqi Li, Xiaodong He, Ming-Ting Sun, and Zhengyou Zhang. Adversarial ranking for language generation. In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett (eds.), Ad- vances in Neural Information Processing Systems 30: Annual Conference on Neural In- formation Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, pp. 3155 3165, 2017. URL
Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. In LPAR-21, 21st International Conference on Logic for Programming. Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, volume 46 of EPIC Series in Com- puting, pp. 85-105. EasyChair, 2017. URL http:////aaacccc....ooo///llleoa Saper/ND13
Oded Maler and Dejan Nickovic. Monitoring temporal properties of continuous signals. In Formal Techniques, Modelling and Analysis of Timed and
Systems, Joint Inter- national Conferences Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real-Time and Fault- Tolerat Systems, FTRTFT 2004, Grenoble, France, September 22-24, 2004, Proceedings, volume 3253 of Lecture Notes in Computer Sci- ence, pp. 152-166. Springer. 2004. doi: 10. 00000/9788-354-30220----- //doi.org/1l 10. 1007 3- 540 30206-3
URL https:
Jia Meng and Lawrence C. Paulson. Lightweight relevance filtering for machine-generated res- olution problems. J. Appl. Log., 7(1):41-57, 2009, doi: 10.10166fjal..000.077000 URL
https::/doi..or
1016 jal 2007.07..04
Philipp J. Meyer, Salomon Sickert, and Michael Luttenberger. Strix: Explicit reactive synthesis strikes back! 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 Computer Science, pp. 3578-586 Springer, 2018. doi:
1110079778-3-319-9665----
Emils Ozolins, Karlis Freivalds, Andis Draguns, Eliza Gaile, Ronalds Zakovskis, and Sergejs Kozlovics. Goal-aware neural SAT solver. CoRR, abs/2106.07162, 2021. URL https:
7/arxiv. attpaab...........11..
Aditya Paliwal, Sarah M. Loos, Markus N. Rabe, Kshitij Bansal, and Christian Szegedy. Graph representations for oideer-order logie and theorem proving. In The Thirty-Fourth AAAI Confer- ence on Artificial Intelligence, AAAI 2020, The Thirry-Second Innovative Applications of Ar- tificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Ad- vances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020, pp-
http::///aaa..ooo/////deeeee 2967-2974. AAAI Press, 2020. URL https: hatps://aaaa...om wtt.:oor/oooosoooooooo arti axticle/view/5et
Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October I November 1977, pp. 46-57. IEEE Computer Society, 1977. doi: 10.1109//FC 1977.32. URL htttps://dol orq/10.
1109/ 1977.331977
14

---

Under review as a conference paper at ICLR 2022
Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. CoRR, abs/2009.03 003993, 2020. URL pittps://arxiv> http:///axxxvv.o.aaabaae atggabb//009. 03393
Markus N. Rabe and Christian Szegedy. Towards the automatic mathematician. In Automated Deduction CADE 28 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes Computer Science, pp. 25-37. Springer, 2021. doi: 10. (0007/978883-030-7877-----3 978-3-030-79876-1
URL httppp:///a..oog/111.0.0..0
Markus Norman Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical reason- ing via self-supervised skip-tree training. In 9th International Conference on Learning Repre- sentations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net, 2021. URL
htttps://openreiiie
net Penxummid--mren Y YOQAnY
Kristin Y. Rozier and Moshe Y. Vardi. LTL satisfiability checking. Model Checking Soft- ware, 14th International SPIN Workshop, Berlin, Germany, July 1-3, 2007, Proceedings, vol- ume 4595 of Lecture Notes in Computer Science, pp. 149-167. Springer, 2007. doi: 10.1007/ 978-3-540-73370--6.1111 URL /ttttpp:///o...c///1100. 1007/10...099911 3-00-------00-337-----
/tt:
David Saxton, Edward Grefenstette, Felix Hill, and Pushmeet Kohli. Analysing mathematical reasoning abilities of neural models. In 7th International Conference on Learning Represen-
tations, ICLR 2019, New Orleans, LA. USA, May 6-9, 2019. OpenReview.net, 2019. URL
kttps://openrevalt
net forum cnsuum?icn www.oooomnnniisSS--- H1-H1g1E
Franco Scarselli, Marco Gori, Ah Chung Tsoi, Markus Hagenbuchner, and Gabriele Monfardini. The graph neural network model. IEEE Trans. Neural Networks, 20(1):61-8,, 2009. doi: 10.
2109/TNNN2008.20556005
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. CoRR, abs/1910.06611 2019. httt:tt::/ http:///axvvvvvv wwt. abs 9110 .06611
Frederik Schmitt, Christopher Hahn, Markus N Rabe, and Bernd Finkbeiner. Neural circuit synthesis from specification patterns. arXiv preprint 1xXiv:210..11844 2021.
Stephan Schulz. System description: E 1.8. In Logic for Programming, Artificial Intelligence, and Reasoning- 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings, volume 8312 of Lecture Notes in Computer Science, pp. 735-743, Springer, 2013. doi: 10. 1001977777 300--33--422----- 642-45221-55 376-3-642-45221--2
URL https://dci http://2.c....111.110..0000
Viktor Schuppan and Luthfi Darmawan. Evaluating LTL satisfiability solvers. In Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings, volume 6996 of Lecture Notes in Computer Sci- ence, pp. 397 413. Springer, 2011. doi: 10. 7/doi. 1007/
URL https:
642 24372
Stefan Schwendimann. A new one-pass tableau calculus for PLTL. In Automated Reason- ing with Analytic Tableaux and Related Methods, International Conference, TABLEAUX '98, Oisterwijk, The Netherlands, May 5-8, 1998, Proceedings, volume 1397 of Lecture Notes in Computer Science, pp. 277-292. Springer, 1998. doi: 10.100773-540-69778444 28. URL
https://doi... org/10 1007/3 540 69778 0 28
Daniel Selsam and Nikolaj Bjørner. Guiding high- reshoperffrmmnce 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 11228 of Lecture Notes in Computer Science pp. 336 353. Springer, 2019. doi: 100.1000777000-0000 0-00778--300-225--- 24258-992 24. URL htt.hhttt//oooo.o.. org 3
Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang. Leonardo de Moura, and David L. Dill. Learning SAT solver from single-bit supervision. In 7th International Conference Learning Representations, ICLR 2019, New Orleans, LA. USA. May 6-9, 2019. OpenReview.net, 2019. https:htt:///oeennn
net. west:forrmmiddeem GHJMC 1
15

---

Under review as a conference paper at ICLR 2022
A. Prasad Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logics.
In Harry R. Lewis, Barbara B. Simons, Walter A. Burkhard, and Lawrence H. Landweber (eds.),
Proceedings of the 14th Annual ACM Symposium Theory of Computing, May 5-7, 1982, San Francisco, California, USA, pp. 159-168. ACM, 1982. doi: 10.1 10.1145/800070.88221
URL.
https: //do: www.org............... 114 /ttp///0111110000000011 00014455000..0000
Josef Urban. MPTP- motivation, implementation, first experiments. Autom. Reason., 33(3-4): URL https: org/ otg./0..1/1/7
319-339, 2004. doi: 10. 10.1007/s1081770044-666
610817-004-88 6245---24--
Josef Urban. Malarea: a metasystem for automated reasoning in large theories. In Proceedings of the CADE-2/ Workshop Empirically Successful Automated Reasoning in Large Theories, Bremen, Germany, 17th July 2007, volume 257 of CEUR Workshop Proceedings. CEUR-WS.org, 2007. httthttp
ws. org wwwpoogg/////oooee 2ot.//ooo22223..... Brraa__rraaa__e pdf
Josef Urban and Jan Jakubuv. First neural conjecturing datasets and experiments. In Intelligent Computer Mathematics 13th International Conference, CICM 2020, Bertinoro, Italy. July 26- 31, 2020, Proceedings, volume 12236 of Lecture Notes in Computer Science, pp. 315-323. Springer, 2020. doi: 10. 978 330-
24. URL https:///ot wwweiiorg/11... 1007/
24
Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jirí Vyskocil. Malarea SG1- machine learner for auto- mated reasoning with semantic guidance. In Automated Reasoning, 4th International Joint Con- ference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, volume 5195 of Lec- ture Notes in Computer Science, pp. 441 456. Springer. 2008. doi: 10.10077978-3-10 3-540-710700 .37. URL http::tt///scttc org 10. 1001 9778 0-07778-------7770----0000
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention all you need. 2017.
Carl Vondrick and Antonio Torralba. Generating the future with adversarial transformers. In Pro- ceedings of the IEEE Conference on Computer Vision and Pattern Recognition, pp. 1020-1028, 2017.
Minchao Wu, Michael Norrish, Christian Walder, and Amir Dezfouli. Tacticzero: Learning to prove theorems from scratch with deep reinforcement learning. CoRR, abs/2102.09756, 2021a. URL.
https://arxte wrg. wwtpaa////...... 2112.0955622
Yuhuai Wu, Albert Jiang, Jimmy Ba, and Roger Baker Grosse. INT: an inequality benchmark for evaluating generalization in theorem proving. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021, OpenReview.net, 2021b. URL https::///penreeeeeee wwwpanrweiee...eefoeeeeeee wwwp/eeeoouttee www.mmidd=--Pdddoom domet//Eoommdd=0LPPPP udooNNm
Zonghan Wu, Shirui Pan, Fengwen Chen, Guodong Long, Chengqi Zhang, and Philip S. Yu. A comprehensive survey on graph neural networks. IEEE Trans. Neural Networks Learn, Syst. 32 (1):4-24, 2021c. doi: 10.
URLlttts: :ttp::////o.......111101.1 1109/
TNNLS.
Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In Pro- ceedings of the 36th International Conference on Machine Learning, 2C11,2019, 9-15 June 2019, Long Beach, California, USA. volume 97 of Proceedings of Machine Learning Research, pp. 6984-6994. PMLR, 2019. URL html
.ml wwwppppwssssseeeeeeee. httpa///ss....ppree////////aaaa
Lantao Yu, Weinan Zhang, Jun Wang, and Yong Yu. Seqgan: Sequence generative adversarial nets with policy gradient. In Satinder P. Singh and Shaul Markovitch (eds.), Proceedings of the Thirty-First AAAI Conference Artificial Intelligence. February 4-9, 2017. San Francisco, Cal- iformia, USA, pp. 2852-2858. AAAI Press, 2017. URL http: aaai. wtt///s/////ooooooooooooo.oe org/ocs/Index. index. php/ AAA http:/appprr//// weweviewww 1//1//34//w//4/44 14344
16

---

Under review as a conference paper at ICLR 2022
Wojeiech Zaremba, Karol Kurach, and Rob Fergus. Learning to discover efficient mathematical identities. In Zoubin Ghahramani, Max Welling, Corinna Cortes, Neil D. Lawrence, and Kil- ian Q. Weinberger (eds.), Advances in Neural Information Processing Systems 27: Annual Con- ference on Neural Information Processing Systems 2014, December 8-13 2014, Montreal, Que- bec, Canada, pp. 1278 1286, 2014. URL
neur ps cc/paper/ 3211://a.00011117777722323377272 Abs html
Kuo-Hao Zeng, Mobammad Shoeybi, and Ming- Yu Liu. Style example-guide text generation using generative adversarial transformers. arXiv preprint 4rXiv:2003.00674, 2020.
Yizhe Zhang, Zhe Gan, Kai Fan, Zhi Chen, Ricardo Henao, Dinghan Shen, and Lawrence Carin. Adversarial feature matching for text generation.
17

---

Under review as a conference paper at ICLR 2022
A SYNTAX AND SEMANTICS OF LINEAR-TING TEMPORAL LOGIC (LTL)
In this section, we provide the formal syntax and semantics of Linear-time Temporal Logic (LTL).
The formal syntax of LTL is given by the following grammar:
upp yp A O+p 1 u.
where p E AP an atomic proposition. Let AP be a set of atomic propositions. (explicit) trace is an infinite sequence over subsets of the atomic propositions. We define the of traces TR = (2A1)². We use the following notation to manipulate traces: Let t E TR be a trace and i E N be natural number. With t|i] 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 2 i. Then t denotes the sequence t|{ tli + 1l....ffj 1] t[j] and tli, oc] denotes the infinite suffix of starting at position i.
Let p E AP and & E TR. The semantics of an LTL. formula is defined as the smallest relation }= that satisfies the following conditions:
t =
iff
p E t[0]
F
up
iff
t ト y
t + A 122
iff
t } 91 and | 422
+ Op
iff
E[L, F 4p
t F p1 1 422
iff
there exists 2 0 t(i, 00] F 922
and for all S j i we have tlj. ool
There several derived operators, such as Q true L tp D ~4 O states that o will eventually hold the future and D states that yp holds globally. Operators can be nested: I p, for example, states that y has to occur infinitely often.
In contrast to propositional logic (SAT), where a solution a variable assignment, the solution to the satisfiability problem of an LTL formula is computation trace. Traces are finitely represented in the form of a "lasso" un where u, called prefix, and v, called period, are finite sequences of propositional formulas. For example the mutual exclusion formula above is satisfied by a trace {o {accessp1) } that alternates indefinitely between granting process 0 (p0) and process 1 (pl) access. There are, however, infinite solutions an LTL formula. The empty trace 0 where no access is granted at all, is also a solution. In our data representation, both, the LTL formula and the solution trace are represented as a finite sequence.
B DATA GENERATION DETAILS
B. RICH LTL PATTERN CONCATENATION
Previously, LTL formula generation based on patterns worked by concatenating random instanti- ations of fixed set of typical specification patterns (Hahn al. (021). The instantiations were single variables, i.c. the response pattern S + T could be used like d + aa We keep the concept of concatenating such patterns, but extend the process by mainly two concepts: rich pattern instantiations and groundings.
Dwyer al. (999)) analyzed typical specifications constructed a system of frequently occurring patterns. They are grouped into different types such as absence (-S, something does not occur) or response (S + if S occurred, T' must eventually respond). These patterns can again appear in different scopes such as globally, before or between some events. The global absence pattern then U-S; the absence before Q pattern reads Q S. When generating new pattern for concatenation, for more common and exotic combinations. Additionally, we instantiate patterns not with single variables, but full subformulas, which results in much more reasonable and interesting patterns such as (a A b) or ((-d B) - (cc A f)) e. These subformulas may still contain temporal operators, but are strongly biased towards pure boolean operators.
sample both a type and scope and assign different probabilities to account
During concatenating the different parts a formula, we also distinguish between adding instanti- ated patterns and groundings. The problem with complex patterns and especially complex scopes
18

---

Under review as a conference paper at ICLR 2022
is that they must be "activated" have effect: If some constraint must only hold between Q and R but these events never happen, the whole pattern effectively useless. grounding is a term that is likely to activate scopes, such as OO A -b c The variables used here also biased to coincide with the ones already used in previous patterns to further increase the change for dependencies. Groundings added with 45% probability instead of specification pattern.
We observe that these changes indeed lead to a much higher chance unsatisfiability. Consider the code data.ge aeweangeeaaaeeeeeaee coneration iontiiio/see sapee-ppateerns Pyy for exact reference of the individual steps in the generation process.
B.2 TEMPORAL RELAXATION FOR FORMULA INSPECTION
inspect the unsatisfiable formulas obtained by our generation process more closely. Concretely, we want to make sure that unsatisfiabilitie do not stem from simple boolean contradictions, but actually require temporal reasoning to some extend. For example, the formula (a b) A ^- A 7-a can be found to be unsatisfiable without considering multiple time steps. In contrast, this would be required for a formula like -all AD-bAA
We therefore introduce a temporal relaxation that transforms LTL formula into purely boolean formula. This allows us to check whether the relaxed version is already unsatisfiable (so, no temporal reasoning is required) if it is only temporally unsatisfiable, which is the desired outcome. The relaxation is defined as follows:
Rel(yp wb Rel(ip) * Rel(v) for E {A, V, +,
Rellyp v) Rel(i)) v Rel(v) for E (U, W}
Rellyp R e) Rel(w)
Rel(O yp) T
(1)
Rel(O yp
Rel(O pp) T
Rel(a) for a [P
Rel(-a) aa for APU(T,
Notably, negation is only allowed at the level of atoms. Each LTL formula be rewritten in a negation normal form (NNF), where only operators A, V,M, R, O occur anywhere and negations only before atoms. Consequently, the relaxation be applied each LTL. formula by first bringing to NNE
B.3 BASE DATASET
We generated raw dataset of 1.6M instances (see reproducibility section for details) up to size 50. To determine satisfiability, we use the tool aalta ([.i et al.) 2014). Its length distribution and satisfiability distribution shown in Figures and
40000
25000
number
15000
5000
10
20
30
40
50
length
Figure 5: Raw dataset size distribution
19

---

Under review as a conference paper at ICLR 2022
unsat
sat
0.8
peroentag
0.6
0.4
0.2
10
20
30
40
50
formula length
Figure 6: Raw dataset satisfiability proportions
We filter out duplicates and balance satisfiable and unsatisfiable instances per size (Figure 7 Ad- ditionally, we apply the temporal relaxation and determine the satisfiability of relaxed unsatisfiable instances. This distinction is included in Figure g Finally, the dataset is split into a training set (80%) and validation set (10%). The resulting training set contains around 380K instances.
17500
12500
10000
5000
2500
50
formula lengtth
Figure 7: Final dataset size distribution (average size 34.6)
1.0
0.8
0ercentage
0.6
0.4
0.2
unsat temp. only
50
Figure 8: Final dataset satisfiability proportions
20

---

Under review as a conference paper at ICLR 2022
B.4 WGAN-GENERATED DATASETS
14000
10000
number
6000
4000
40
50
formulaa longth
Figure 9: Generated dataset size distribution (average size 33.6)
20000
15000
12500
10000
7500
2500
10
20
30
40
50
formulla length
Figure 10: Uncert-e dataset size distribution (average size 38.0)
C ADDITIONAL EXPERIMENTS AND INFORMATION
C.I SHARED LAYERS FOR CLASSIFIER INCLUDED IN CRITIC
Table 4: Different number of shared layers for WGAN with included classifier, runs each, 30K
steps
shared layers
fc
val acc
0/4
2.2
31.8% (0.2)
89.9% (2.3)
2 4
2.2
26.6% (1.7)
92.5% (0.1)
3/4
2.2
24.9% (0.3)
92.1% (0.6)
4/4
2.2
24.0% (1.2)
90.5% (0.5)
Table shows classification benefits for sharing only some layers between classifier and critic. Also note that not sharing any layers, while yielding the highest fraction of fully correct formulas in the joint GAN and classification objective, degrades performance in the uncertainty setting, where a loss is backpropagated through the classifier part.
C.2
COMPARISON
A harer-parameter comparison with 2-run average at 15K training steps.
21

---

Under review as a conference paper at ICLR 2022
G
RTD
bs
variant GAN
fully correct
2
1024
6%
2
1024
WGAN
4%
2
2
2
512
GAN
6%
512
WGAN
4%
2
2
2
1024
GAN
7%
1024
WGAN
5%
2
2
2
2048
GAN
5%
2
2048
WGAN
6%
2
1024
WGAN
5%
4
2
1024
GAN
8%
4
1024
WGAN
9%
3
2
1024
GAN
8%
1024
WGAN
13%
2
2
1024
GAN
7%
1024
WGAN
14%
4
2
1024
GAN
10%
1024
WGAN
16%
4
2
1024
GAN
17%
1024
WGAN
20%
2
1024
WGAN
15%
2
1024
WGAN
18%
C.3
TRAINING CURVES DATA SUBSTITUTION EXPERIMENTS
Generated LTLbase 100K
0.8
LTLbase 10K
0.6
2
4
5
training steps
-00
Figure 11:
Validation accuracy during training of Transformer classifiers on different datasets. 5-rum
average, smoothed (a 0.9). Complements Table 2
We provide the training curves for the data substition experiment (see Figure 11
C.4 STANDARD DEVIATIONS FOR TABLE
Table Standard deviations for Table
3-run average, smoothed (a 0.95)
architecture
real
fc sd sd
architecture
Treal
fc sd
se sd
0.00
0.00
0
1.51
0.00
0.05
4.10
0.04
0.05
2.52
0.00
GAN
0.1
6.50
0.03
WGAN
0.1
1.08
0.01
0.2
3.92
0.04
0.2
0.47
0.00
0.4
0.14
0.02
0.4
0.14
0.03
We provide the standard deviations for Table across 3 runs (see Table
22

---

Under review as a conference paper at ICLR 2022
C.5 GAN WITH UNIFORM NOISE
Table 6: GAN variant with uniform instead of Gaussian noise. 2-run average with standard devia- tions, smoothed (a 0.99)
min
max
fc
se
0
0.1
19.2% (2.94)
1.6 (0.19)
0
0.2
33.3% (1.04)
1.8 (0.01)
0.4
11.2% (3.32)
2.0 (0.07)
As evident from Table comparison with Table noise.
uniform noise has no benefit over Gaussian
C.6 OUT-OF-DISTRIBUTION CLASSIFICATION EXPERIMENTS
Table 7: Classifiers trained on different datasets tested out-of-distribution.. smoothed
5-run average, not
trained on
training steps
tested on
accuracy
LTLbase
30K
Benchmarks Benchmarks
85.2% (2.2)
Uncert-e
30K
85.9% (2.9)
Uncert-e
30K
LTLbase
87.5% (0.9)
Mixed-e
30K
Mixed-e
92.7% (0.6)
LTLbase
50K
Benchmarks
86.0% (5.0)
Generated
50K
Benchmarks
94.1% (1.2)
synthetic dataset that is designed bring classical solvers their limits is portfolio dataset (Schuppan & Darmawan 2011), of which around 750 formulas fit into our encoder token and size restrictions. We conducted an -ut-o--distribution test on these scalable benchmarks (Table 77). Note that almost all of the instances are satisfiable.
23


Reviews:
[{"review_id": "F90-vecqQc", "reviewer": "Reviewer_qNn9", "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": "### Strengths\n\n* Simple idea: using GANs for data augmentation.\n\n* Empirically proving that GANs can generate parsable instances and that GANs\n  can generate interesting problems that are hard to solve and contribute to\n  improve the performance of classifiers.\n\n### Weaknesses\n\nI have several concerns and questions as follows.\n\n* I'm not entirely sure of how the generated data are labeled.  Is it done by\n  the GAN discriminator or by another algorithm as labeling LTL formulas in the\n  real dataset with the tool aalta (Appendix B.3)?\n\n  If the latter is employed, it indicates the existence of an algorithm to\n  address the task of interest, so I'm wondering why machine learning is applied\n  to it.  Perhaps ML models might be expected to answer the problems faster\n  than the algorithm, but labeling with the algorithm would be successful only\n  on problems that the algorithm can answer in a given time; thus, it seems hard\n  to label problems that the algorithm cannot solve in a reasonable time,\n  although the ML models should approach such problems.\n\n  For the former, the generated data could be mislabeled.  Then, it is not clear\n  for me why training on such data can produce a model with the performance very\n  close to the model trained on data with correct labels (Table 2).\n\n* I don't think this is the first work to use GANs for data augmentation.  For\n  example, [1] and [2] used GANs for augmenting image data.  Unlike\n  these previous works, the paper addresses sequential data that are textual\n  representations of mathematical expressions, but lacking the discussion and\n  (qualitative) comparison with them makes a challenge and novelty of the paper\n  unclear.\n\n  [1] Antreas Antoniou, Amos J. Storkey, Harrison Edwards.\n  Data Augmentation Generative Adversarial Networks.\n\n  [2] Christopher Bowles, Liang Chen, Ricardo Guerrero, Paul Bentley, Roger N. Gunn, Alexander Hammers, David Alexander Dickie, Maria del C. Valdés Hernández, Joanna M. Wardlaw, Daniel Rueckert:\n  GAN Augmentation: Augmenting Training Data using Generative Adversarial Networks.\n\n\n* The abstract and introduction seem oversold somewhat in that they don't\n  mention that the experiment conducted for symbolic mathematics only\n  confirms the GAN model can produce syntactically correct problems; thus, the\n  full usefulness of the GAN-based data augmentation is still open in the\n  symbolic mathematics domain.  I think it would be nicer to conduct more\n  experiments on symbolic mathematics, which would demonstrate the proposed\n  approach is useful in broader domains.\n\n* The experiments on satisfiability of LTL formulas look interesting, but I'm\n  concerned that it is adequate to be tacked with machine learning.  As written\n  in Appendix B.3, there exists a tool for checking satisfiability of LTL\n  formulas, and it is used to label the (real) dataset. Then, why do we need the\n  trained model for checking satisfiability?  A critical problem with the\n  trained model is that its prediction might be wrong.  How can we use a\n  satisfiability checker that may produce wrong answers?\n\n  For a similar reason, I'm not sure why machine learning is useful for the\n  domain where \"data can ... often be labeled automatically\" (page 8).\n\n* The paper uses GAN and WGAN, but it does not investigate why they make a\n  difference in the experiments (e.g., Table 1).\n\n\n### Minor comments / questions\n\nP2 \"\\neg \\box (access_p0 \\wedge access_p1)\"  I think \\box (globally) should be\nreplaced with \\diamond (eventually) for correction.\n\nP2 \"Mathematical expressions\"  What are these?  Are they different from random functions?\n\nP3 \"continuous domains were\"  where\n\nP4 \"we use the alternative generator loss\"  Why?\n\nP6 \"the origin training data\"  original\n\nP6, Table 1:\n  For GAN, does the use of \\sigmoid_real larger than 0.2 make the fraction of fc larger?\n\nP7 \"we combine both critic and classifier into one Transformer encoder\"  Why are not they separated?\n\nP8: The result in Table 3 seems peculiar to me.  Why does the model trained on\nMixed-e outperform the model trained on LTLbase even when tested on LTLbase?\n\n### Post-Rebuttal\n\nI would like to thank the authors for the additional comments to answer my questions.\nHowever, I still have two major concerns that make me hesitate to accept the paper.\nThe first s that I don't still find the task of generating symbolic expressions interesting.\nThe second is about an application of the approach.  The response from the authors says that neural models may compute solutions faster than classical tools.  I don't disagree with this claim, but the paper doesn't show that the proposed approach is indeed helpful for that task.  I would like to see more discussions and evidence for the story to hold true (e.g., how the augmented data are labeled, whether they can improve the performance of neural models that compute solutions, etc.)", "summary_of_the_paper": "This paper makes the use of GANs equipped with Transformers to generate new\ninstances of the problems in the symbolic reasoning domains, and demonstrated\nthe usefulness of the idea on two domains: satisfiability prediction of LTL\nformulas and mathematical reasoning on integration and ordinary differential\nequations.  The experiments show that the trained GAN models can produce\nparsable instances on both of the domains and that training on the generated\ndata can improve the accuracy performance of a classification model for LTL\nsatisfiability prediction.", "summary_of_the_review": "The paper addresses a critical problem in symbolic reasoning domains, and the\nexperimental results are promising. However, I think it's not ready for\npublication because of lacking a discussion for practical settings to use the\nproposed GAN-based data augmentation, an evidence to show its generality, and a\ncomparison with the previous work.\n", "strength_and_weaknesses": "", "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": "DRwTWMiDmu4", "reviewer": "Reviewer_3zMF", "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": "The problem is interesting and the paper is well motivated.\n\nAbstract: What do they authors mean by “synthetically generated instances are often hard to evaluate in terms of their meaningfulness”?\n\nWhat do the authors mean by “training on randomly generated data carries the risk of training on meaningless data or the risk of introducing unwanted biases”? Provided that the conclusion follow logically, can the authors elaborate on what they mean here? \n\n“We show that training directly in the one-hot encoding space is possible when adding Gaussian noise to each position”. Why use Gaussian noise? The authors should be more clear about why they add noise to the real samples? Presumably this is to make distinguishing the real samples from the fake ones non-trivial? This is only explained later on and is a bit confusing.\n\n“on which a classifier can successfully be trained on”. Do you test on an established dataset?\n\n“The generator’s input is a real scalar random value with uniform distribution [0, 1] for each position.” It is not clear here what is mean by “each position”. I assume this is each symbol in the input? But this is not clearly explained.\n\n“The position-wise padding mask is copied from the real data during training, so the lengths of real and generated formulas at the same position in a batch are always identical.” The first time you refer to **the** padding mask it is not clear what this is or where it comes from?\n\n“Still, both generators are able to produce a large fraction of fully correct temporal specifications, which we find surprising” Could there be overfitting? Are the results the same across many runs? Is 0.3 a large fraction? How does this compare to generating examples randomly? This would make a good baseline (even if your models perform worse).\n\nFigure 4: Interesting results.\n\nThe satisfiability classifier results are interesting. What would be better tho, is to show that training on the generated data improved results on an established dataset. \n\nIt is interesting that you can learn on data generated using the LTLbase 10k dataset and perform better on the validation set than training directly on the LRLbase (and perform similarly well when training on the whole LTLbase dataset). However, it’s clear that the model has overfit to the LTLbase 10k. How did you decide to stop training? Does this happen for all runs? It would be helpful to see the training and test curves while the model is training. Additionally, it would be good to see a graph with multiple runs.\n\nFor all results in the paper, it would be best to perform multiple runs and report the standard deviations. \n\nIn the section titled “GAN with included classifier”: What are you classifying? Are you predicting satisfiability? This is not clear. How do you know the satisfiability of the generated samples? Is there a 50/50 split of satisfiable and unsatisfiable examples?\n\nAre there the same number of training examples in the LTLbase, Uncert-e and mixte-e datasets?\n\nTable 3: Are you training and testing on different splits of the dataset? It would help to add the std? The results somewhat suggest that training to increase uncertainty does produce slightly more challenging problems, but it’s hard to tell because it’s not clear how much results vary between runs and it’s not clear if the differences are statistically significant. \n\nTable 3: It’s very important to know how train and test samples were split for Uncert-e. Uncert-e being more difficult to classify could also be explained by lack of variation and the samples you tested happening to be in a different mode to those in the training set. What is the average length of problems in each data set?\n\nIs there a qualitative difference between samples generated with and without the uncertainty loss? What makes the problems harder?\n\nDoes training on Uncert-e improve performance on LTLbase (more so than training on generated?) Is there a standard dataset that you can show improvement on?\n\nWhy are there not more quantitative results on the integration examples? It’s clear that a classifier can already perform very well on the LTL tasks, perhaps it would be easier to see improvements on the function integration task? It does not appear that there are any results for this in the main text? \n\nGeneral: The paper does not clearly separate LTL results and symbolic math results. This makes some results harder to parse.\n\nGeneral: This model does not generate a supervised training dataset since you still need to use existing algorithms/ programs to compute the labels/targets. This could be a problem for datasets where the solution is intractable and would also suggest that you already have a model capable of solving the problem for which you are generating the data. What is the long term motivation of this work if you either (a) cannot generate labels/targets or (b) can already use existing algorithm to solve these problems.\n", "summary_of_the_paper": "Generating symbolic reasoning training data using transformer GANs. Use classifier uncertainty in the generator objective to generate samples that are harder for the classifier to solve than the original data. The problem is very interesting, but the empirical results could be improved.", "summary_of_the_review": "The problem is really interesting. \n\n\nCorrectness: \nThere are problems with the experimental results. If the authors can add the suggested results and show that their results are statistically significant, I would be very happy to increase my score. \n\nNovelty: The approach also lacks novelty, only proposing an additional loss which is not clearly described. However, their application is very interesting.", "strength_and_weaknesses": "", "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": "Not applicable"}, "extra_text": {}}, {"review_id": "9EL3oHJxTAa", "reviewer": "Reviewer_JuGn", "summary": "", "questions": "", "limitations": "", "rating": 8, "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": "This is a strong paper overall: innovative, well-written, and potentially important.\n\n- I found it awkward that the prose stressed that two domains would be considered, in some cases even listing symbolic mathematics (i.e. function integration) first, even though the integration domain received much shorter shrift and most of the experiments seem to be LTL only. I think the paper would be stronger with two domains throughout rather than one. \n\n- How many examples were in LTLBase? It might be nice to see an estimate of the effective size of the \"Generated\" dataset with respect to the original distribution.\n\n- I see that in S4.2 you are starting with only 10k samples from LTLBase, but what are you training on exactly for S4.1? If a larger dataset than in S4.2, did you do a similar check for duplicates between the generated examples and the training dataset? How many (if any) of the 30% that are syntactically valid were seen during training?\n\n- It is not clear to me whether the last paragraph of S4.1 is describing a different training regime than the paragraph preceeding it.\n\n- The first sentence seems more suitable for a blog post than a conference paper; in particular, the claim that deep learning is \"on the verge\" of something sounds unscientific. Also, the word \"transitioning\" may not be appropriate, since presumably deep learning will continue to be applied to e.g. image recognition.\n\n- I particularly liked the approach in S4.3 in which an additional objective is introduced that shifts the generated distribution away from the original one. In general, the true objective of data augmentation may be broader than simply modeling the specific distribution of training examples one has at hand. Have the authors considered other \"knobs\" to add that would allow generating more diverse examples, that may provide useful augmentation either for the original distribution or for out-of-distribution evaluations?\n\n- Minor comment: I did not find that it added much to the paper to consider both GANs and WGANs. I would suggest only discussing WGANs.\n", "summary_of_the_paper": "The authors apply (W)GANs with transformer encoders for data-augmentation in two symbolic domains: LTL and function integration. There are many interesting findings, three of which stand out. First, in both domains, the network learns to generate syntactically-correct examples roughly 30% of the time. Second, for LTL, a GAN trained on a dataset of size 10k can produce a much larger dataset, such that training on the new dataset is almost as good as training on the original distribution (when evaluating on the original distribution). Third, by also rewarding the generator for confusing a classifier, they can generate new problems that are harder to classify than those in the original distribution.", "summary_of_the_review": "This is a strong paper overall: innovative, well-written, and potentially important. I think it will be of interest to anyone applying machine learning in data-sparse symbolic domains.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "3tuLK8vcPLw", "reviewer": "Reviewer_vhbE", "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": "** Update after author responses ** After the author clarified with the format of the data and results, my problems have resolved in part and thus I updated the score. My concern in the motivation of the paper still remains. The paper claims that synthetic dataset generated from rules is limited in the coverage so that it is valuable to construct synthetic dataset from neural models --- however, it is still not clear to me if experiments demonstrate that the resulting data from neural models are shown to have better coverage and higher quality than data from rules.\n\nThe model introduced in the paper is well-executed, and based on the generated data attached in the submission, the data quality appears to be good enough. There are still a few concerns I have in the motivation of the problem and experiments.\n\nFirst, the problem setup is not convincing to me and is not well-motivated in the paper. If data for the symbolic reasoning --- which is not precisely defined in the paper --- can easily be generated at scale using rules, as done for the base data in the paper, what is the reason for training a neural model to generate more data? How is it inherently different from generating more using rules, as data, either generated automatically from rules or generated by neutral models, is equally artificial?\n\n~~Second, although the paper claims that the generated data is high quality, it seems to have quite bad quality to me. I checked Supplementary materials and most formulas contain many repetitions like “&&&&&&&GXaG>!” and are very hard to interpret. It is very difficult to find good examples as listed in Section 4.2.1, so there is a high likelihood that these good examples are cherry-picked.~~\n\nThird, the experiments in Section 4 do not demonstrate that the generated data has high quality and effectively replaces the base data. For example, Table 2 shows that training on generated data achieves performance that is comparable to the model trained on the original data, but not better. This is related to my first point in the motivation of the problem - if the original data can be obtained automatically at scale and generated data from the proposed model is not significantly better than the original data, is there a justification for not using the original data?\n\n", "summary_of_the_paper": "This paper aims to generate training data for symbolic reasoning by training GANs based on Transformers. Specifically, the paper explores two methods --- standard GAN and Wasserstein GAN --- which has a Transformer as an encoder and a decoder, respectively. Training these models on symbolic reasoning data that is randomly generated --- LTL and Symbolic mathematics --- is found to generate high quality formulas.", "summary_of_the_review": "The model introduced in the paper is well-executed, and based on the generated data attached in the submission, the data quality appears to be good enough. However, in my opinion, there are more fundamental issues in the motivation of the problem and whether experiments successfully justified the usefulness of the generated data from the proposed model.", "strength_and_weaknesses": "", "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": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}]

Author rebuttal:

Meta-review: The paper aims to improve complex reasoning. In this regard, authors identify that acquisition of data for symbolic reasoning domains is a challenge and propose generating the data by GANs. A transformer-based architecture is proposed and trained for LTL and Symbolic mathematics. Experiments show samples generated are of good quality (e.g., correct syntax). We thank the reviewers and authors for engaging in an active discussion. However, the reviewers did not find the task of such data on its own not to be particularly interesting. Also, neither the architecture nor the training algorithm is very novel. If authors could provide a complete story i.e., show the augmented data can improve the performance of neural models that compute solutions, etc., it would make the paper much stronger. Thus, unfortunately I cannot recommend an acceptance of the paper in its current form.
Decision: Reject