Logic is the main formal language to perform automated reasoning, and it is further a human-interpretable language, at least for small formulae. Learning and optimising logic requirements and rules has always been an important problem in Artificial Intelligence. State of the art Machine Learning (ML) approaches are mostly based on gradient descent optimisation in continuous spaces, while learning logic is framed in the discrete syntactic space of formulae. Using continuous optimisation to learn logic properties is a challenging problem, requiring to embed formulae in a continuous space in a meaningful way, i.e. preserving the semantics. Approaches like [1] are able to construct efective semantic-preserving embeddings via kernel methods (for linear temporal logic), but the map they define is not invertible. In this work we address this problem, learning how to invert such an embedding leveraging deep architectures based on the Graph Variational Autoencoder framework. We propose a novel model specifically designed for this setting, justifying our design choices through an extensive experimental evaluation. Reported results in the context of propositional logic are promising, and several challenges regarding learning invertible embeddings of formulae are highlighted and addressed.
Logic, in its many variants, is arguably one of the most prominent languages used to represent
knowledge, specify requirements and explanations for complex systems, and reason in a
humancomprehensible way [
Our Contribution Moving from the rationale of GVAE models for Direct Acyclic Graphs
(DAG, [
Related Work Learning autoencoder models for DAGs was originally addressed via sequence
models [
As mentioned in Section 1, in this work we restrict the investigation to the setting of propositional logic. Denoting by {}=1 a set of propositional variables, where each is a binary variable that can evaluate either to true (1) or false (0), the set of propositional formulae (hereafter referred to also as propositions or requirements) is defined recursively by the syntax := 1 | | ¬ | 1 ∧ 2 | 1 ∨ 2. Semantics is defined recursively following the usual meaning of Boolean operators (see Appendix A.1 for details).
A convenient way to represent propositions in this context is by means of their abstract
syntax tree (AST), i.e. a tree representation of the syntactic structure of the formula where
internal nodes are the Boolean operators and the leaves are the propositional variables. Since
Boolean operators are at most binary, the AST arising from propositional formulae are binary
trees. This representation opens the doors to the application of Graph Neural Network (GNN,
[
In this work we wish to learn both an encoder and a decoder for mapping inputs x to and from continuous vectors z. The Variational Autorencoder (VAE, [21]) framework is designed to learn simultaneously two parametric functions: a probabilistic generation network (decoder) (x|z) and an approximated posterior distribution (encoder) (z|x), by maximizing the evidence lower bound: ℒ(, ; x) = Ez∼ (z|x)[log (x|z)] − [(z|x)||(z)] (1) where [(· )||(· )] denotes the Kullback-Leibler divergence between (· ) and (· ) and (z) the prior distribution over latent variables z.
The VAE model has been generalized to graph structured data by employing a GNN as encoder
(and possibly decoder) model [
If auxiliary information y (such as category labels or semantic context) about the input x should be incorporated into the learning process, frameworks like the Conditional Variational Autoencoder (CVAE, [24, 25]) allow to control the generative process by imposing a condition on both the encoder (in this context defined as (z|y, x)), the prior ( (z|y), which is parametric) and the decoder ( (x|y, z)). The network is trained by optimizing the following conditional marginal log-likelihood (notation is the same of Equation 1): ℒ(, , ; x, y) = Ez∼ (z|y,x)[log (x|y, z)] − [(z|y, x)|| (z|y)] (2)
While for euclidean input formats the vector y is commonly concatenated to the input x (resp. the latent z) before the computation of the encoding (resp. decoding) functions, in the context of graph generative models several possibilities exist: in cases in which there is additional information for all the nodes of the graph, it is concatenated to the initial node states [26]; when y is a property of the whole graph, it can be either concatenated to the latent vector z before the decoding process [27] or incorporated into the GNN decoding architecture itself [28].
Learning embeddings of logic formulae preserving semantic similarity is addressed in [
∈ (, ) = ( ) · ( ) (3) and compute it using Monte Carlo approximation putting a uniform probability measure over the space of configurations . Experiments confirm that the Boolean kernel of Equation 3 maps propositional formulae in a semantic-preserving continuous space, as reported in Appendix B, where we also show its correlation with Jaccard similarity coeficient among propositional formulae. Moreover, reducing the dimensionality of the embedding space using Principal Component Analysis (PCA) shows that it is sensible to consider an embedding space of dimension much lower than the number of formulae used to construct the kernel of Equation 3. We defer to Appendix B for experimental results on dimensionality reduction.
The main objective of this work is to investigate algorithms for computing invertible embeddings of propositional logic formulae, starting from their syntax and exploring methods for including semantic information, towards the goal of learning a latent space characterising the semantic of the logic. As every formula can be represented by its AST without any loss of information (see Section 2 and Appendix A), architectures based on the GNN framework provide a sensible inductive bias for our setting. Moreover, as we require to learn both an encoder and a decoder for formulae, we find it meaningful to deploy a Graph Variational Autoencoder (GVAE) model. Formally, given a propositional formula sampled according to the algorithm detailed in Appendix C.1, we design the input to our model to be the rooted tree arising from its AST, i.e. inputs are graphs = (, ) with set of vertices corresponding to operators and variables (taken with their multiplicity) appearing in and set of directed edges ⊆ × such that (, ) ∈ if is a main subformula of in . Although normal forms exists for propositional logic, we decided not to adopt any of them for mainly two reasons: firstly, rewriting formulae in normal form usually involves increasing the number of terms (namely every formula in variables written either in conjunctive or disjunctive normal form can have up to 2 terms) and this can yield to scalability issues when the formula is used as input for a GNN; secondly, in this work we are using propositional logic as a proof of concept for models that we wish to deploy for temporal logics, which in general do not admit simple normal forms.
Commonly, GNN models (and in particular those based on the Message Passing paradigm
[29]) organize computations in a synchronous update scheme, i.e. all nodes update their state
and exchange messages simultaneously. However, the nodes of the graphs we consider in this
context have well-defined dependency relationships, hence following the approach adopted
in [
The encoder is the network responsible for mapping the discrete input graph to a continuous
latent representation z, and in this case consists of a GNN with a (possibly bidirectional)
asynchronous update scheme, as described earlier in this Section. In our model, the encoder is
formulated by adapting the Graph Attention Network (GAT, [30]) to the asynchronous message
passing scheme of [
The initial nodes hidden states are the one-hot-encoding of their type (note that increasing the number of variables allowed increases the number of node types). Then, once the message phase terminates, all nodes states are computed, and we take as output of the encoder the state of the node without any successor (referred to as end node; if no such node exists, a virtual one is added to the input graph). In case of bidirectional encoding, a concatenation of the state of the end nodes of both computation directions is taken. As approximate posterior (· ) of Equation 1 and 2 we consider a Gaussian distribution, whose mean and variance are obtained by feeding to two MLPs.
Given a real-valued latent vector z, the goal of the decoder is to convert it to a discrete graph
representing the AST of a formula . The main requirement for the decoder is validity, i.e. it
should produce syntactically correct formulae. Towards this objective we decided (ablations are
discussed in Section D.1) to design a decoder which implements syntactic rules architecturally,
i.e. that does not allow the generation of invalid formulae. This is integrated in a node-wise
generation procedure (derived from that of [
∑︁ ∈ () (h ) ⊙ (h ) (4) where is a Gated Recurrent Unit [31] and ⊙ represents the gated sum between a mapping network and a gating network , implemented as MLPs.
Decoding thus results in the following top-down iterative algorithm: 1. Given the initial latent vector z, the starting graph state h = h0 is produced by feeding it to a MLP with softmax activation. By construction, the type of the first created node 0 is start, i.e. it is a synthetic starting node; 2. Each node , with 1 ≤ ≤ max (where max is an input parameter specifying the maximum number of nodes admitted during generation), is generated as: a) the type of is inferred by first computing a distribution over all possible types using an MLP with softmax activation taking as input the current graph state h, then sampling its type from such distribution; b) the hidden state of is updated using Equation 4; c) the graph state is updated as: h = h ; 3. Nodes are expanded following a depth-first traversal of the tree, taking into account the arity of the operators represented by node types, this prevents the violation of syntactic constraints; 4. The graph generation stops when the tree cannot grow further (i.e. all leaf nodes are variables), or when = max (this latter case is the only possibility of having invalid formulae as output).
In Section 2.1 (and more in detail in Appendix B) we describe an efective methodology to compute finite-dimensional semantic embeddings of propositional formulae. We remark that, in order to construct such representations for a formula , it is not necessary to explicitly know itself, but only its valuations of a set of assignments { }=1 ⊆ . This makes it sensible to formulate a conditional variant of our model, i.e. a CVAE architecture using as semantic context vector the kernel embedding y of the input formula (obtained after performing PCA dimensionality reduction), concatenated to the latent representation z before starting the decoding computations.
Training is performed using teacher forcing, i.e. the decoder is fed with the ground truth graph it has to reconstruct during loss computation. At each iteration of the decoding algorithm of Section 3.2, we accumulate the negative log-likelihood by feeding the network with a vertex having the ground truth node type, so that the network is forced to stay close to true node sequences.
Experiments on a family of variations of our model pursue mainly two goals: measure VAE
reconstruction and generative abilities and qualitatively evaluate the smoothness of the latent
space. Hence, following [
We propose the following versions of our model (hereafter referred to as LogicGVAE): • Syntax-only: given an input formula , it encodes its AST without any additional information, i.e. it has access only to the syntactic information of ; • Semantic-conditioned: given an input formula , we evaluate its semantic-context vector using the kernel of Section 2.1 and perform conditional decoding as described at the end of Section 3.2;
For both variants, we perform experiments on a set of diferent asynchronous encoding GNNs, namely GRU, Graph Convolutional Networks (GCN, [33]) and GAT. Architectural and training details of all models are specified in Appendix D.
(b) Results of CVAE abilities tests. This suite of experiments aims at evaluating: (a) accuracy, i.e. ability to perfectly reconstruct the input AST; (b) validity, i.e. ability to generate syntactically valid formulae; (c) uniqueness, i.e. proportion of distinct graphs out of valid generations; (d) novelty, i.e. proportion of generated graphs which are not in the training set. To evaluate accuracy, we encode each test graph to get mean and variance of the posterior approximation (z|), then we sample 10 latent vectors from such distribution and decode each 10 times. Accuracy is defined as the percentage of these 100 graphs which are identical to the input . Validity is instead computed as the proportion of syntactically valid AST obtained by sampling 1000 latent vectors from the prior (z) and decoding each 10 times. For what concerns the conditional variant of our architecture, (· ) and (· ) are those of Equation 2.
In the conditional setting, we test accuracy as described above, then we test how well the learned latent space preserves semantic-similarity by computing: (a) mean distance from the input context vector, i.e. given a semantic vector y on which we condition the decoding, we sample 100 vectors from the prior z ∼ (z|y) and decode each 10 times, the most commonly decoded formula is kept for each z and its semantic embedding computed and compared with ground truth y using 2 norm; (b) mean kernel similarity among formulae with same semantic vector y, i.e. following the procedure of the previous point, we compute the kernel among the most decoded formulae for each y.
Table 1a reports results of the tests checking VAE abilities for diferent encoders (described in full details in Appendix D). The first aspect to notice is that a convolution-style GNN (either GCN or GAT) outperforms a recursive one (GRU) on all performance indices. This might be due to the fact that convolutions exploit more local substructure patterns and they leverage the hidden state of the node we are updating, instead of only those of its neighbors, diferently from a GRU architecture. The reconstruction accuracy of both GCN and GAT is high and comparable, however when encoding with a GAT we record a higher ability of the latent space to capture structural features of data, as witnessed by a higher percentage of unique and novel decoded formulae. These results can be leveraged in a requirement optimization scenario, by mapping a given formula in its latent representation and optimize its structure in the continuous embedding space.
Table 1b reports results of CVAE abilities tests (using as encoding networks only the most promising ones according to Table 1a). If we take a pool of 5000 random Boolean formulae with 5 variables, which we use to generate the semantic context vectors for each test instance, they have an average distance between semantic embeddings of 18.7325 and an average kernel similarity of 0.1695. Since the semantic distances and the kernel values reported in Table 1b are much lower (resp. higher), we observe that conditioning on a semantic vector our input data actually maps them in a space where semantic similarity is to some extent preserved.
It is worth noting that, although the reconstruction accuracy of the conditional architecture (Table 1b) is lower than that of the unconditional architecture (Table 1a), the former might be leveraged in a requirement-mining scenario, where only valuations of a formula in a set of configurations are observed (thus allowing the construction of the semantic context vector) and an explicit formula optimising a fitness function has to be found (i.e. decoded). Essentially, in this case we need to use the CVAE as a generative model, to sample formulae which (approximately) have the semantics specified by a given semantic context vector, obtained by solving an optimization problem in the semantic embedding space. This task cannot even be defined in a vanilla VAE scenario, where only syntactic information is exploited. Moreover, the reconstruction accuracy increases significantly if we compute it considering only the most frequently decoded formula for each test point, as reported as second row of the accuracy column of Table 1b.
More experimental results and ablation studies are reported in Appendix D, we underline in particular the cruciality of the syntactic constraints in the decoder architecture (Section 3.2).
We use spherical interpolation (slerp, [34]) around a given latent point to qualitatively evaluate the smoothness of the latent space. This briefly consists in interpolating points following a great circle of a hypersphere in a space having the same dimension of the latent space. Starting from a point z encoding a formula , we follow a great sphere starting from z and pick 35 evenly spaced points to decode. From Figure 1 we notice that the model using a GAT encoder produces a smoother latent space, as it changes less nodes at each step of the interpolation.
In this work we propose LogicVAE, a configurable GVAE model built to learn a data-driven representation for propositional logic formulae. By leveraging an asynchronous message passing computational scheme in the encoder and ad-hoc syntactic constraints in the decoder, it is able to learn an expressive latent space. We provide a novel way to incorporate semantic information in the learning process, towards the goal of building an embedding space which is semantic-preserving. The main bottleneck of this approach is scalability to datasets with more than 5 variables, a possible solution is a hierarchical approach, sketched in Appendix D.2.
As already mentioned, results reported in this paper should be taken as a proof of concept towards extending the model to more complex formalisms, such as temporal logic, which come with the additional challenge of learning temporal and/or threshold parameters associated to operator (resp. variable) nodes, but which generally operates on few signals only (typically no more than 5 [35]). Moreover, inspired by AlphaCode [36], which defines a generative model for programs (another context in which the syntactic-semantic interplay has a fundamental role), we plan to both incorporate a self-supervised pre-training stage in our encoder (adapting the masked language modelling loss used in AlphaCode), and to check the viability of using large language transformer-based models [37] to encode and decode logic formulae.
This study was carried out within the PNRR research activities of the consortium iNEST (Interconnected North-Est Innovation Ecosystem) funded by the European Union Next-GenerationEU (Piano Nazionale di Ripresa e Resilienza (PNRR) – Missione 4 Componente 2, Investimento 1.5 – D.D. 1058 23/06/2022, ECS_00000043). This manuscript reflects only the Authors’ views and opinions, neither the European Union nor the European Commission can be considered responsible for them. December 3-8, 2018, Montréal, Canada, 2018, pp. 7806–7815. [18] V. Kondratyev, M. Dryzhakov, T. Gimadiev, D. Slutskiy, Generative model based on junction tree variational autoencoder for HOMO value prediction and molecular optimization, J.
Cheminformatics 15 (2023) 11. [19] M. J. Kusner, B. Paige, J. M. Hernández-Lobato, Grammar variational autoencoder, in: Proceedings of the 34th International Conference on Machine Learning, ICML 2017, Sydney, NSW, Australia, 6-11 August 2017, volume 70 of Proceedings of Machine Learning Research, PMLR, 2017, pp. 1945–1954. [20] T. Ma, J. Chen, C. Xiao, Constrained generation of semantically valid graphs via regularizing variational autoencoders, in: Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada, 2018, pp. 7113–7124. [21] D. P. Kingma, M. Welling, Auto-encoding variational bayes, in: 2nd International Conference on Learning Representations, ICLR 2014, Banf, AB, Canada, April 14-16, 2014, Conference Track Proceedings, 2014. [22] Y. Zhu, Y. Du, Y. Wang, Y. Xu, J. Zhang, Q. Liu, S. Wu, A survey on deep graph generation: Methods and applications, in: Learning on Graphs Conference, LoG 2022, 9-12 December 2022, Virtual Event, volume 198 of Proceedings of Machine Learning Research, PMLR, 2022, p. 47. [23] X. Guo, L. Zhao, A systematic survey on deep generative models for graph generation,
CoRR abs/2007.06686 (2020). URL: https://arxiv.org/abs/2007.06686. arXiv:2007.06686. [24] K. Sohn, H. Lee, X. Yan, Learning structured output representation using deep conditional generative models, in: Advances in Neural Information Processing Systems 28: Annual Conference on Neural Information Processing Systems 2015, December 7-12, 2015, Montreal, Quebec, Canada, 2015, pp. 3483–3491. [25] O. Ivanov, M. Figurnov, D. P. Vetrov, Variational autoencoder with arbitrary conditioning, in: 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019, 2019. [26] C. Yang, P. Zhuang, W. Shi, A. Luu, P. Li, Conditional structure generation through graph variational generative adversarial nets, in: Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada, 2019, pp. 1338–1349. [27] Y. Li, O. Vinyals, C. Dyer, R. Pascanu, P. W. Battaglia, Learning deep generative models of graphs, CoRR abs/1803.03324 (2018). URL: http://arxiv.org/abs/1803.03324. arXiv:1803.03324. [28] Y. Li, L. Zhang, Z. Liu, Multi-objective de novo drug design with conditional graph generative model, Journal of Cheminformatics 10 (2018) 33. [29] J. Gilmer, S. S. Schoenholz, P. F. Riley, O. Vinyals, G. E. Dahl, Neural message passing for quantum chemistry, in: Proceedings of the 34th International Conference on Machine Learning, ICML 2017, Sydney, NSW, Australia, 6-11 August 2017, volume 70 of Proceedings of Machine Learning Research, PMLR, 2017, pp. 1263–1272. [30] P. Velickovic, G. Cucurull, A. Casanova, A. Romero, P. Liò, Y. Bengio, Graph attention networks, in: 6th International Conference on Learning Representations, ICLR 2018, Vancouver, BC, Canada, April 30 - May 3, 2018, Conference Track Proceedings, 2018. [31] K. Cho, B. van Merrienboer, Ç. Gülçehre, D. Bahdanau, F. Bougares, H. Schwenk, Y. Bengio, Learning phrase representations using RNN encoder-decoder for statistical machine translation, in: Proceedings of the 2014 Conference on Empirical Methods in Natural Language Processing, EMNLP 2014, October 25-29, 2014, Doha, Qatar, A meeting of SIGDAT, a Special Interest Group of the ACL, ACL, 2014, pp. 1724–1734. [32] M. J. Kusner, B. Paige, J. M. Hernández-Lobato, Grammar variational autoencoder, in: Proceedings of the 34th International Conference on Machine Learning, ICML 2017, Sydney, NSW, Australia, 6-11 August 2017, volume 70 of Proceedings of Machine Learning Research, 2017, pp. 1945–1954. [33] T. N. Kipf, M. Welling, Semi-supervised classification with graph convolutional networks, in: 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings, 2017. [34] T. White, Sampling generative networks: Notes on a few efective techniques, CoRR abs/1609.04468 (2016). [35] G. Ernst, P. Arcaini, I. Bennani, A. Donze, G. Fainekos, G. Frehse, L. Mathesen, C. Menghi, G. Pedrielli, M. Pouzet, S. Yaghoubi, Y. Yamagata, Z. Zhang, Arch-comp 2020 category report: Falsification, in: ARCH20. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20), volume 74 of EPiC Series in Computing, 2020, pp. 140–152. [36] Y. Li, D. Choi, J. Chung, N. Kushman, J. Schrittwieser, R. Leblond, T. Eccles, J. Keeling, F. Gimeno, A. D. Lago, T. Hubert, P. Choy, C. de Masson d’Autume, I. Babuschkin, X. Chen, P.-S. Huang, J. Welbl, S. Gowal, A. Cherepanov, J. Molloy, D. J. Mankowitz, E. S. Robson, P. Kohli, N. de Freitas, K. Kavukcuoglu, O. Vinyals, Competition-level code generation with alphacode, Science 378 (2022) 1092–1097. [37] A. Vaswani, N. Shazeer, N. Parmar, J. Uszkoreit, L. Jones, A. N. Gomez, L. Kaiser, I. Polosukhin, Attention is all you need, in: Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, 2017, pp. 5998–6008. [38] O. Maler, D. Nickovic, Monitoring temporal properties of continuous signals, in: Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2004, Grenoble, France, September 22-24, 2004, Proceedings, volume 3253 of Lecture Notes in Computer Science, Springer, 2004, pp. 152–166. [39] A. Paszke, S. Gross, S. Chintala, G. Chanan, E. Yang, Z. DeVito, Z. Lin, A. Desmaison, L. Antiga, A. Lerer, Automatic diferentiation in pytorch, in: NIPS 2017 Workshop on Autodif, 2017. [40] I. Higgins, L. Matthey, A. Pal, C. P. Burgess, X. Glorot, M. M. Botvinick, S. Mohamed, A. Lerchner, beta-vae: Learning basic visual concepts with a constrained variational framework, in: 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings, 2017. [41] D. P. Kingma, J. Ba, Adam: A method for stochastic optimization, in: 3rd International Conference on Learning Representations, ICLR 2015, San Diego, CA, USA, May 7-9, 2015, Conference Track Proceedings, 2015. [42] T. Akiba, S. Sano, T. Yanase, T. Ohta, M. Koyama, Optuna: A next-generation hyperparameter optimization framework, in: Proceedings of the 25th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, ACM, 2019, pp. 2623–2631.
Propositional logic is a formal language whose grammar recursively defines well-formed for mulae by combining variables {}=1 and logical operators ¬ (negation), ∧ (conjunction) and ∨ (disjunction) . More precisely, variables are valid formulae (also called atomic sentences), and given valid sentences and it holds that ¬ , ∧ and ∨ are valid sentences as well.
Semantics of propositional logic is defined starting from assignments of truth values to each propositional variable then recursively applying the following rules to each sub-formula (the valuation of on is denoted by ( )): ¬ ( ) = 1 if ( ) = − 1, ( ∧ )( ) = 1 if both ( ) = 1 and ( ) = 1, ( ∨ )( ) = 1 if either ( ) = 1 or ( ) = 1.
As mentioned in Section 2, every propositional formula can be represented by its Abstract Syntax Tree (AST), as showed in Figure 2.
Graph Neural Networks (GNNs, [
Arguably the most common framework for GNN is the so called Message Passing Neural Network framework (MPNN, [29]), which abstracts many commonalities between existing GNN models. As the name suggests, the defining characteristic of MPNNs is that they use a form of neural message passing in which real-valued vector messages are exchanged between nodes (in particular between 1-hop neighboring vertices), for a fixed number of iterations. where (the readout function) needs again to be a diferentiable function, invariant to permutations of the node states.
Hence, the intuition behind MPNNs is that at each iteration every node aggregates information from its immediate graph neighbors, so as iterations progress each node embedding contains information from further reaches of the graph.
A way to instantiate the message and update functions of Equation 5 is the Graph Convolutional Network (GCN, [33]) model, which generalizes the convolution operation to graph structured data by updating the representation h of each node as:
y = ({h( )| ∈ }) h(+1) = ︂(
∑︁ ∈ ()
1
ℎ() (+1)︂) h(+1) = (h(),
(h(), h())) ∑︁ ∈ () where is called message function and is called message update function: both are arbitrary diferentiable functions (typically implemented as neural networks).
After running iterations of this message passing procedure, a readout phase is executed to compute the final embedding y of each node as: (5) (6) (7) (8)
In detail, during each message passing iteration in a MPNN, the hidden representation h() of each node is updated according to the information m() aggregated from its neighborhood () as: being a non-linear activation function, a a vector of learnable parameters and || a node-wise operation like concatenation or sum. Possibly GAT uses a multi-head attention mechanism to increase the model capabilities, by replicating the operations of Equation 8 multiple times independently and aggregating the results.
In its original version, the MPNN model is expected to exchange messages between nodes
synchronously, however when the input graph is directed it is sensible to follow a partial order
among nodes, as observed in [
Another possible computation scheme for the operations of Equation 5 is the Graph Attention Network (GAT , [30]) which uses self-attention to learn relative weights between neighboring 1 1 nodes. It consists in:
∑︁ ∈ ()∪ h(+1) = (
(+1) (+1)h()) (+1) = softmax(LeakyReLU(a [ (+1)h()|| (+1)h()])) its new hidden state h(), i.e. it uses the current layer representation of its direct neighbors {h()}∈ () before updating its state, instead of the one of the previous layer.
A kernel function for Signal Temporal Logic The kernel we start from when defining
a semantic similarity measure for logic formulae is defined in [
The definition of quantitative satisfaction allows to consider STL predicates as functionals
mapping trajectories to their robustness, i.e. (, · ) : → R, hence a formula can be embedded
into a (possibly infinite-dimensional) Hilbert space. In this space we can consider as ‘scalar
product‘ between pairs of formulae , the following:
(,
) =
∫︁
∈
(, ) · (, ) 0
(9)
being 0 a probability measure over trajectories. It can be proved that (· , · ) of Equation 9 is a
proper kernel function, and Probably Approximate Correct (PAC) bounds can be provided to
give probabilistic bounds on the error committed when using the kernel for learning in formulae
space. Experiments carried out in [
A kernel function for propositional logic Building upon the idea of the STL kernel defined above, we define a similarity measure between propositional formulae as detailed in Section 2.1.
The Jaccard index (or similarity coeficient) measures the similarity between two sets and as (, ) = ||∩∪|| ; given two propositions , and the sets of their assignment valuations , resp. over variable configurations , the Jaccard index (, ) = || ∩∪ || denotes the proportion of configurations in which the two formulae agree, hence measuring semantic similarity between its inputs. On the other hand, the value of (, ) represents the normalized diference between the set of configurations ∈ on which and agree and disagree, being 1 in the case of semantically equivalent formulae. This quantity is positively correlated to the Jaccard index as (, ) = 2 (, ) − 1, corroborating the claim that Equation 3 can be used as a measure of semantic similarity between formulae. Putting all together, we get that the kernel is an interpretable measure of similarity between formulae, for example a kernel of 0.8 can be understood as formulae agreeing on 90% of configurations.
Moreover, we can give a deeper insight on the performance of the Boolean kernel in measuring semantic similarity between propositional formulae by showing the results of kernel classification on the satisfaction of assignments to formulae, reported in Figure 3.
As the dimensionality of the embeddings computed by the kernel is equal to the number of training formulae used to evaluate the kernel itself (i.e. it is the vector of kernel evaluations according to Equation 3 of the input formula against all the formulae in the training set), we verify if it can be reduced without significant information loss by performing dimensionality reduction in the embedding space using Kernel Principal Component Analysis (kernel PCA). We answer this question afirmatively by showing that keeping 100 components for formulae having at most 5 variables and 500 components for formulae with 6 to 10 variables retains much of the variance of the original dataset made of 5000 formulae, as shown in Figure 4.
In order to construct synthetic datasets of propositional formulae we adapt the algorithm
defined in [
3 Algorithm 1 Syntax-tree random recursive growing scheme .index ← () ◁ Queue of uncomplete nodes ◁ Root is an operator node ◁ Next node to expand ◁ is a variable node ◁ Variable index is sampled randomly
All the models described in Section 4 have been implemented in Python exploiting the PyTorch [39] library for leveraging GPU acceleration.
Then, the loss function we optimize via mini-batch gradient descent is that of Equation 1 or its variant of Equation 2 in the conditional version of our architecture. We allow the term of such losses to be weighted by a tunable hyperparameter > 0, i.e. using the loss of the so-called -VAE [40] model.
Each architecture has been trained with Stochastic Gradient Descent (SGD) on a set of 4000 diferent propositional formulae (generated as described in Section C.1) divided in minibatches of size 32 with an initial learning rate of 10− 3, using the Adam optimizer [41] and early stopping to regulate the number of training epochs (we put a validation step every 30 epochs and stop the training if validation loss does not significantly improve with a patience of 3 checkpoints; this resulted on having the non-conditional models trained for ∼ 300 epochs and the conditional ones for ∼ 600 epochs).
Datasets for training and testing the models have been generated following algorithm 1, ifxing leaf = 0.4 and varying ∈ {3, 4, 5}. This resulted in sets having an average of [10.2955, 13.6632, 17.7475] nodes and average depth of [5.4687, 8.5132, 9.4419] for increasing . We remark that increasing the number of variable indexes allowed increases the number of node types the network has to learn (hence further increasing the complexity of the datasets).
We tested three diferent encoder architectures, each consisting on a GNN with the following
distinctive features:
• GRU, same as [
All of them implement the asynchronous message passing scheme. For all the encoders, we report results for the bidirectional setting, as justified by ablation studies in Appendix D.1. To compute the mean and covariance of the approximate latent distribution (· ) we use two 1-layer MLPs.
The hidden size of the models is set to 250 and the latent size to 56, these hyperparameters as
well the ones listed above have been tuned with the hyperparameter optimization framework
Optuna [42]. As noted in [
For what concerns the semantic context vector used in the CVAE version of our model, we computed it by kernel PCA as described in Section B. Since our train and test datasets contain formulae having at most 5 variables, we keep 100 components, as justified by Figure 4.
In Tables 2 and 3 we report more VAE and CVAE abilities results on diferent datasets of increasing complexity. We remark that GAT is the best performing encoder, both for the syntactic and the semantic-conditioned task. In particular in the conditional case it is able to better capture the multimodality of each y w.r.t. to formulae and give a better characterization of the semantics in the latent space.
Concerning the latter, Figure 5 gives an insight on the relation between kernel similarity value between a formulae (, ) and distance between their kernel PCA embeddings. Being the kernel evaluated between two formulae an interpretable measure of their semantic similarity (more on this in Section B), this reported inverse correlation justifies the metrics used for evaluating CVAE abilities.
For what concerns the validity of formulae, we recall that the only case in which our decoding algorithm can produce invalid formulae is when it reaches the maximum number of nodes max allowed in the produced graphs, in our experiments set to 30, as described in Section 3.2. 25 e c n ta20 s i D g ind15 d e b Em10 A C P K 5
0 Acc. 5 8
For what concerns the accuracy of reconstructed formulae, we also notice that it increases if we consider, for each of the test formulae, only the most common decoded one (which is a more realistic scenario). Accuracy in this scenario for GAT and GCN encoders is reported as second line of the corresponding model in Tables 2 and 3 for the conditioned and unconditioned case,
Median respectively.
In Figure 6 we show the distributions of kernel values and semantic distances computed as described earlier for LogicVAE with both GAT and GCN encoder, when trained on a dataset of 5 variables. Moreover, in Table 4 we report their first, second and third quantiles.
In Table 5 we report the results of several ablation studies we perform on LogicVAE. They consists in the following: 1. Non-constrained decoding: this represents the most important design choice. We kept the encoding and objective function as described earlier, but we remove from the decoder the constraints imposing to follow logic syntactic rules (i.e. the ones described in Section 3.2). This leads to a dramatic decrease in reconstruction accuracy, highlighting the fundamental importance of this inductive bias. 2. Unidirectional message passing: messages are exchanged only following the original direction of the edges of the input DAG (i.e. without reverting them). For both GCN and DAG encoders, this decreases the reconstruction accuracy, but not dramatically. 3. Number of convolutional/attentional layers: we get the highest accuracy with 2-layer
GCN encoder and 3-layer GAT encoder.
While performing experiments, we noticed that LogicVAE struggled in learning variable indexes,
i.e. its reconstruction accuracy increases (and the architectures converge faster) if we provide
as input a simplified AST for each input formula . This graph is constructed by removing
variable indexes from the input described in Figure 2 and Section 3. The idea is then to build
a hierarchical learning model, which first learns to reconstruct the simplified tree using the
syntactic version of LogicVAE, then recovers variable indexes by a GNN architecture. We
instantiated this latter model using a MPNN architecture, akin to that described in Section
C.2, with node-level readout function on the leaves. We trained the model to minimize a loss
involving both a classification term (namely cross-entropy loss over classes, being the
maximum number of variable indexes allowed) and a semantic term measuring the square loss
between the semantic vector y of the ground-truth formula (as described in Section C.2) and
the one of the reconstructed formula ^, denoted by y^^ at each step of the training algorithm.
Formally we minimize the following (for a formula having leaves over possible indexes):
1 ∑︁(∑︁ log ^) + ||y − y^^ ||2
ℒ(, ^) = −
=1 =1
(10)
where , ^ represent the true (resp. reconstructed) probability of leaf to have index
, and ∈ R≥ 0 is a tunable parameter weighting the semantic term of the loss w.r.t. the
classification one. Interestingly, we found that the loss of Equation 10 reaches a plateau in
correspondence of low values of the semantic term. Indeed, we verified that the true formula
and the reconstructed one ^ evaluated in correspondence of the learning plateau difer on
the [10.34%, 12.29%, 12.48%, 16.85%] of possible configurations with ∈ [