NeSyA: Neurosymbolic Automata

1 Introduction

Sequence classification/tagging is a ubiquitous task in AI. Purely neural models, including LSTMs [Hochreiter, 1997] and Transformers [Vaswani, 2017], have shown exemplary performance in processing sequences with complex highdimensional inputs. Nonetheless, various shortcomings still exist in terms of generalization, data-efficiency, explainability and compliance to domain or commonsense knowledge. NeSy AI [Garcez and Lamb, 2023] aims to integrate neural learning and symbolic reasoning, possibly aiding in the afformentioned limitations of purely neural systems. Recently, various NeSy systems have been developed for sequential/temporal problems [Winters et al., 2022; De Smet et al., 2024; Umili et al., 2023b], with large differences among them, in terms of semantics, inference procedures, and scalability of the proposed hybrid models.

In this work, we identify symbolic automata as an attractive low-level representation of complex temporal properties. These differ from classical automata as they support symbolic transitions between states (defined in propositional logic), thus combining temporal reasoning (through the automaton) and atemporal reasoning (through the logical transitions). We show that symbolic automata can be efficiently integrated with neural-based perception and thereby extended to subsymbolic domains. Figure 1 illustrates the core NESYA architecture in a running example, which is used throughout the paper.

The key characteristics of NESYA that can be used for comparison to existing NeSy systems, are: [C1] its focus on temporal domains, [C2] its probabilistic semantics, [C3] its capacity to integrate static logical reasoning into temporal patterns, [C4] its efficient and exact inference scheme based on matrices and knowledge compilation [Darwiche and Marquis, 2002].

The closest system to our work is FUZZYA [Umili et al., 2023b], which attempts to address the NeSy integration of LTLf with neural networks. That system differs from NESYA primarily in terms of [C2], as it is based on fuzzy logic and specifically on Logic Tensor Networks [Badreddine et al., 2022]. As we shall show in this paper, probabilistic semantics can provide significant benefits, in terms of predictive accuracy, over fuzzy logic, as used in FUZZYA.

On the other hand, NESYA differs from approaches like the Semantics Loss (SL) [Xu et al., 2018] and DEEPPROBLOG [Manhaeve et al., 2018], in terms of [C1], as they are not tailored to temporal reasoning. In this paper, we shall show that this makes them scale considerably worse than NESYA when faced with problems with a temporal component.

The more recent DEEPSTOCHLOG system [Winters et al., 2022] is based on unification grammars and therefore differs from NESYA in terms of both [C1] but mostly [C4]. Our experiments show that this difference makes DEEPSTOCHLOG orders of magnitude slower than NESYA.

Further, systems based on neural networks and classical automata, such as [Umili et al., 2023a; Umili and Capobianco, 2024] differ from NESYA in terms of [C3], since classical automata lack symbolic transitions and support for atemporal reasoning.

Lastly, [De Smet et al., 2024] is based on very expressive models in mixed discrete and continuous domains. It is based on approximate inference, thus differing from NESYA in terms of [C4].

Our contributions are as follows:

• We introduce NESYA a probabilistic NeSy system for sequence classification and tagging, which combines automata, logic and neural networks.
• We introduce an efficient algorithm for inference in NESYA, utilizing matrix-based automata inference and knowledge compilation based approaches for logical inference [Darwiche and Marquis, 2002].
• On a synthetic sequence classification domain, we show that NESYA leads to large performance benefits over FUZZYA [Umili et al., 2023b] and scales orders of magnitude better than DEEPSTOCHLOG [Winters et al., 2022], which is also based on a probabilistic semantics.
• On a real-world event recognition domain we show that NESYA can lead to a more accurate event recognition system, compared to purely neural approaches.

2 Background

2.1 Propositional Logic and Traces

We shall use lowercase to denote propositional variables, e.g. blocked. A propositional formula ϕ over a set of variables V

These connectives are sufficient to then define →, etc. An interpretation ω ⊆ V assigns a truth value to each variable. We use subsets to denote interpretations. For instance for V = {tired, blocked, fast} the interpretation ω = {tired, blocked} is shorthand for {tired, blocked, ¬fast}. If an interpretation ω satisfies a formula ϕ we write ω |= ϕ and ω is called a model of ϕ.

The semantics of propositional logic are given in terms of interpretations. Traces generalize interpretations for temporal domains. A trace over variables V , π = (ω1, ω2, . . . , ωn) is a sequence of interpretations, with ωi ⊆ V . We use πt to denote the interpretation ωt at timestep t.

2.2 SFA: Symbolic Automata

A symbolic automaton (SFA) is defined as:

where V is a set of variables, Q a set of states, q0 ∈ Q the initial state, δ : Q × Q → B(V ) is the transition function and F ⊂ Q is the set of accepting states. B(V ) is used to denote the set of all valid formulae in propositional logic over variables V . The difference between an SFA and a classical automaton is that δ is given in a factored form, e.g. δ(q0, q1) = tired ∨ blocked in Figure 1. One can always convert the SFA to a classical automaton by replacing each transition δ(q, q′ ) with multiple ones representing all models ω |= δ(q, q′ ). This approach does not scale to complex formulae and large sets of variables, as the number of resulting transitions can be exponential in V . This factored transition function is also common in the Markov Decision Process literature [Guestrin et al., 2003] with the goal being to exploit the symbolic nature of the transitions without "propositionalizing".

A symbolic automaton reads traces, i.e. sequences of interpretations (ω1, . . . , ωn) (ωi ⊆ V ) over the variables V . We shall consider deterministic SFAs, in which:

That is, for any state q ∈ Q and any interpretation ω ∈ 2V exactly one transition outgoing from state q will be satisfied by ω. For the SFA in Figure 1 consider the transitions outgoing from state q0. For any intepretation, either (¬tired∧¬blocked) or (tired∨blocked) will be true. If the SFA ends up in an accepting state after reading the trace π we write π |= A.

2.3 Probabilistic Logical Inference

Probabilistic logical inference is the task of computing the probability of a logical formula under uncertain input. For a propositional formula ϕ over variables V , let p denote a probability vector over the same variables. Each element p[i] therefore denotes the probability of the ith symbol in V being true. The probability of the formula given p is then defined as:

This task is reducible to weighted model counting (WMC), one of the most widely-used approaches to probabilistic logical inference [Chavira and Darwiche, 2008]. As computing WMC involves summing over all models of a propositional formula, it lies in the #P complexity class of counting problems [Valiant, 1979]. Knowledge Compilation (KC) [Darwiche and Marquis, 2002] is a common approach to solve WMC problems. It involves transforming a logical formula to a tractable representation, on which WMC queries can be cast in linear time. Importantly, once a formula has been compiled to a tractable representation, WMC cannot only be computed in linear time but also differentiably. The computational complexity of the problem is effectively shifted to an initial compilation phase but can be amortized, since multiple queries can be cast on the compiled representation. Consider for example the formula ϕ = ¬fast ∧ (tired ∨ blocked), i.e. the transition q1 → q1 in Figure 1. Its compiled form as a d-DNNF circuit [Darwiche, 2001], one of the tractable KC representations, and the computation of WMC can be seen in Figure 2. The logical circuit in Figure 2 (left) is converted to an arithmetic circuit Figure 2 (right) by replacing AND gates with multiplication and OR gates with addition. The weighted model count for the probability vector in Figure 2 can be verified to be correct by:

• = 0.344.

Recall that interpretations are given in shorthand, e.g. {tired} is shorthand for {tired, ¬blocked, ¬fast}.

3 Method

3.1 Formulation and Inference

We introduce NESYA as a NeSy extension of the SFAs introduced earlier. Rather than assuming a trace of propositional interpretations π = (ω1, ω2, . . . , ωn) we assume a sequence of subsymbolic observations o = (o1, o2, . . . , on) with oi ∈ Rm. NESYA is defined as a tuple (A, fθ), with A an SFA over variables V and fθ : Rm → [0, 1]|V | a neural network, which computes a probability vector fθ(ot) over the variables V from the observation ot. Therefore fθ(ot)[i] denotes the probability of the ith variable in V being true given the observation ot. The neural network is used to bridge between the discrete representation of the SFA and the continuous representation of the observations.

The resulting model is depicted in graphical model notation in Figure 3, where qt denotes a discrete random variable over the states of the SFA and ot the input observation at time t. Following [McCallum et al., 2000], we define

as the probability of being in state q at timestep t after seeing the observations (o1, ..., ot). αt can be computed recursively (using dynamic programming) as follows:

Thus, to update the probability of being in each state, one must first compute the probabilities of the logical formulae in the SFA's transitions given the outputs of the neural network for the current observation. Instead of naively summing over all models of each formula, we use KC to make the computation efficient. The state update, which is similar to the one in Hidden Markov Models, can be captured via matrix operations and is therefore amenable to parallelization and execution on GPUs. It is well-known that αt can be represented with a vector of size |Q|, whose elements are the probabilities of being in each state at timestep t. In what follows we adopt this notation.

Running example computation:

Consider the SFA in Figure 1. Let the first observation be o1 = and let fθ(o1) = [0.8, 0.3, 0.6] the output of the neural network. We define the transition matrix T(oi) where T(oi)[q′ , q] = P(δ(q′ , q) | fθ(oi)). We thus have:

The calculation of the entry T( )[q1, q1] was shown in Section 2.3. Similarly, the computation of other entries is performed by propagating an arithmetic circuit for each transition, given the neural network predictions for the current observation. Observe that the sum of each row in the transition matrix, i.e. the total mass out of each state is 1. This is a direct consequence of the deterministic propertry of the SFA, where exactly one outgoing transition from each state will be true for any possible intepretation. It also ensures that ∑q∈Q αt[q] = 1 for all t.

We start with α0, where α0[q0] = 1 and α0[q] = 0 for all q ∈ Q, q ̸= q0, We then recursively compute αt for each subsequent timestep. Let o = (o1 = , o2 = ). Consider the neural network predictions for o1 as above and let fθ(o2) = [0.7, 0.9, 0.3]. We is is

Depending on the task, the α-recursion can be used in various ways. For sequence classification, one only cares about the state probabilities in the final timestep and would aggregate over accepting states to get the probability of accepting the sequence. Concretely:

where n is the length of the sequence. In this case Paccept(o) = 0.023 + 0.7179 = 0.742. In other applications, such as sequence tagging, one is interested about the α values in every timestep.

3.2 Learning

For ease of exposition we shall consider the sequence classification task, in which NESYA is given a subsymbolic sequence o and computes Paccept(o). The computation of Paccept(o) is differentiable with respect to the neural network outputs as the only operations necessary to compute the acceptance probability are: (a) the computation of WMC which, as shown in Section 2.3, reduces to propagating an arithmetic circuit comprised of addition, multiplication and subtraction, (b) the α-recursion which is implemented via standard matrix operations, and (c) a summation over the final α values.

Therefore, given a dataset of pairs (o, L), where L ∈ {0, 1} is a binary label for the sequence o, one can train the neural component of NESYA by minimizing a standard supervised learning loss, e.g.

where BCE stands for the standard binary cross entropy. This amounts to training the neural network via weak supervision, where no direct labels are given for the symbol grounding of each observation, but rather for the sequence as a whole. This weak-supervision learning setup is common and can be found in [Manhaeve et al., 2018; Yang et al., 2020; Winters et al., 2022; Umili et al., 2023b]. More concretely, observe that we don't require examples of the form ( , {tired, ¬blocked, ¬fast}), as we would in a fully supervised multilabel problem, but rather of the form (( , , ), 0). Such high-level labels are in general much fewer in number and more easily attained. Given the differentiability of the model, explained at the start of this subsection, the neural component fθ is trained via standard gradient descent on the distant labels.

3.3 Semantics and Discussion

Consider a sequence of probability vectors (p1, p2, . . . , pn) with each vector pt assigning a probability to each proposition v ∈ V at timestep t. In NESYA pt = fθ(ot), i.e. these probability vectors are computed via a neural network conditioned on the observation at each timestep, but we ignore the neural component at this stage of the analysis. Given (p1, . . . , pn), the probability of trace π, a sequence of interpretations, is then:

To elaborate, the probability of a sequence of interpretations is the product of the probability of each interpretation πt given pt.

Theorem 1 (α-semantics). It holds that:

where traces(q, t) is the set of all traces which cause the SFA to end up in state q starting from q0 in t timesteps. The probability of being in state q at timestep t is then the sum of all such traces (sequences of interpretations) weighted by the probability of each trace given (p1, . . . , pt).

This directly follows from the graphical model but refer to Appendix A for a proof from first principles. A direct consequence is that for an SFA A and the sequence (p1, . . . , pn) of symbol probabilities:

Once the logical transitions of the SFA have been compiled to a tractable form, see Section 2.3, this computation is polynomial in the number of nodes of the compiled circuits and the number of states of the SFA. This makes the compiled SFA, a tractable device for performing computations over uncertain symbolic sequences.

This result is important for extending NeSy systems to the temporal domain. Consider the symbolic component of a NeSy system, e.g. DEEPPROBLOG. It eventually reduces to a propositional formula ϕ and relies on the computation of ∑ω|=ϕ P(ω | p), where p is usually the output of a neural network conditioned on an observation. For temporal NeSy systems if the symbolic component can be captured by an SFA A, then ∑π|=A P(π|p1, p2, . . . , pt) is computable as shown

.

in Equation 3. To further motivate the potential efficacy of SFAs as promising low-level representations in the context of NeSy, we note that they are known to capture STRIPS domains as well as temporal logics [De Giacomo et al., 2013] and are thus quite expressive. Hence, it is possible, that SFAs can serve as an efficient compilation target for temporal NeSy systems, much like d-DNNF and similar representations have done for atemporal NeSy systems.

4 Results

In this section we provide empirical results for the performance of NESYA and its comparison to other NeSy systems, as well as to purely neural ones. We aim to answer the following questions:

[Q1] Scalability: How does NESYA compare to DEEPSTOCHLOG and FUZZYA in terms of runtime on the same NeSy learning task?

[Q2] Accuracy: How does NESYA compare to FUZZYA in terms of accuracy on the same NeSy learning task? 1

[Q3] Generalization: How does NESYA compare to purely neural solutions in terms of generalization?

All experiments were run on a machine with an AMD Ryzen Threadripper PRO 3955WX 16-Core processor, 128GB of RAM, and 2 NVIDIA RTX A6000 with 50GB of VRAM of which only one was utilized.

4.1 Synthetic Driving

We first benchmarked NeSy systems on a synthetic task, which allowed us to control the complexity. In particular, we used the domain introduced as a running example, in which a sequence of images must be classified according to a temporal pattern. Each image represents a set of binary symbols. In the example from Figure 1 the symbols were {tired, blocked, fast}, however we test for sets of up to five symbols. Their truth value is represented via two emojis, one corresponding to the value true and one false. Random Gaussian noise is added to each image to make the mapping between an image and its symbolic interpretation less trivial. We generate three patterns (different SFAs) with 3, 4 and 6 SFA states and 3, 4 and 5 symbols respectively. For each pattern, we generated 100 random trajectories which satisfy the pattern (positive) and 100 negative ones. We use the same setup for generating a training and a testing set.

The neural component of all systems is a CNN. The learning task is as described in Section 3.2, where the neural component must perform symbol grounding without direct supervision. Instead supervision is provided at the sequence level and the neural component is trained weakly. We benchmarked against DEEPSTOCHLOG [Winters et al., 2022] and DEEPPROBLOG [Manhaeve et al., 2018] in terms of scalability and with FUZZYA [Umili et al., 2023b] both in terms of scalability and accuracy. Figure 4 shows the comparison of NeSyA against the DEEPSTOCHLOG system on temporal patterns of ranging complexity in the synthetic driving benchmark. The DEEPPROBLOG system lagged behind the other two considerably and therefore is omitted from the results for brevity. Accuracy results are also omitted here, since all three systems are equivalent in their computation and learning setup and therefore perform identically in terms of accuracy. In terms of computational performance, NESYA does significantly better than DEEPSTOCHLOG, being on average two orders of magnitude faster. As an indication, for the most complex task and a sequence length of 30, NESYA takes 0.08 seconds for a single batch update and DEEPSTOCHLOG takes about 30 seconds, rendering the latter system of limited practical use. As an indication of the difference against DEEPPROBLOG, for the simplest pattern and a single sequence of length 15, the update time for DEEPPROBLOG is 140 seconds compared to 0.02 seconds for NESYA.

1 The accuracy of DEEPSTOCHLOG is not compared against that of NESYA, as they generate the same results on the same input.

Next, in Table 1 we show accuracy and scalability results of NESYA against the FUZZYA system. NESYA, which interfaces between the SFA and the neural representations using probability, seems to offer a much more robust NeSy solution. FUZZYA delivers significantly lower accuracy compared to NESYA, especially as sequence length grows. Further FUZZYA lags significantly in terms of scalability.

The results on our synthetic benchmark allow us to affirmatively answer [Q1] and [Q2]. NESYA seems to scale better than both DEEPSTOCHLOG and FUZZYA for even the simplest patterns considered here, often by very large margins. Further, our system is more accurate than FUZZYA, with the difference in performance becoming very large for large sequence lengths and complex patterns.

4.2 Event Recognition

In our second experiment we compared NESYA against pure neural solutions on an event recognition task from the CAVIAR benchmark dataset 2 . The task was to recognize events performed by pairs of people in raw video data. We focused on two of the events present in CAVIAR, namely moving and meeting, which appear more frequently in the data, and a third no event class. We present three methods; NESYA a CNN-LSTM and a CNN-Transformer. The data consists of 8 training and 3 testing sequences. The label distribution for the training data is 1183 frames of no event, 851 frames of moving and 641 frames of meeting. For the test set, these are 692, 256 and 894 respectively. The mean sequence length is 411 with a minimum length of 82 and a maximum length of 1054. We use the macro F1 score for evaluation of all models.

The CAVIAR data is annotated at a frame level with bounding boxes of the people in the scene, as well as with low-level activities they perform, such as walking and running. From the raw data, we extract sequences of two bounding boxes per timestep, as well as a boolean feature of whether the distance between the bounding boxes is smaller than some threshold. Refer to Figure 5 for an overview. The symbolic component of NESYA in this case is a three-state automaton, capturing a variant of the Event Calculus [Kowalski and Sergot, 1986] programs for CAVIAR found in [Artikis et al., 2014] and can be seen in Figure 6. We use the SFA to label the sequence with the current high-level event in each frame given the ground truth labels for the low level activities. The true high-level events are also given in the CAVIAR data, but the labels are noisy, i.e. there is some disagreement between the start and end points of the high-level events generated by the logic and those provided by human annotators. Using the labels generated by the SFA, we assume perfect knowledge, i.e. that the symbolic component of NESYA can perfectly retrieve the high-level events, given the low-level activities. Learning with a label noise is beyond the scope of this work.

The task in CAVIAR is therefore to tag a sequence of pairs of bounding boxes, along with a boolean distance feature, with the high-level event being performed in each timestep.

2 https://homepages.inf.ed.ac.uk/rbf/CAVIARDATA1/

For NESYA each bounding box is processed by a CNN which gives a probability for each of the low-level activities (walking, running, active and inactive). Combining this with the feature close(p1, p2), these are then passed through the SFA which outputs the probability of each high-level event per timestep. As a baseline, we drop the final linear projection of the CNN used for NESYA. The resulting CNN computes a 64-dimensional embedding for each bounding box. We concatenate the embeddings of the bounding boxes along with the distance feature finally producing a 129-dimensional embedding per frame. This embedding is then given to either an LSTM or a Transformer, whose hidden state is projected to the three high-level event classes. All systems are trained by computing a cross entropy loss on the high-level event predictions in every timestep of each sequence. The supervision is therefore in the frame level contrary to the experiment in Section 4.1 where supervision was on the sequence level. For NESYA the loss in the CAVIAR dataset is:

where n denotes the sequence length, αt the probabilities of being in each state of SFA at timestep t (and therefore of emitting each label) and Lt denotes the true high-level event label for that timestep, e.g. meeting. For the pure neural solutions αt is replaced with the output of a linear projection on the LSTM/Transformer hidden state at timestep t. The performance of the three systems can be seen in Table 2.

The results in Table 2 allow us to also answer [Q3] affirmatively. The inclusion of knowledge about the structure of the high-level events based on the low-level activities aids in generalization and the discrepancy between train and test performance is generally small for NESYA and larger for purely neural solutions in this low data regime. The Transformer baseline is able to compete with NESYA, albeit with an order of magnitude more parameters. It is interesting that 2.5 million parameters (the difference between NESYA and the CNN-Transformer) are necessary to find a solution that delivers comparable performance with the three state SFA and simple transition logic used by NESYA as background knowledge. The results in CAVIAR are to be taken with a grain of salt as standard deviations are high due to the small size of the data which causes outlier runs for all methods.

5 FutureWork

Recently, [Yang et al., 2023] used the DEEPPROBLOG system to integrate logical constraints in the training of Reinforcement Learning (RL) agents in subsymbolic environments. We believe NESYA can aid in this direction, by allowing for the specification of more complicated temporal constraints, which require memory, i.e. some notion of state to be remembered from the execution of the environment so far, while being more scalable. A large class of systems is based on constraints for RL agents [Alshiekh et al., 2018; Jansen et al., 2020] often using LTL. This seems a promising avenue for NeSyA which can extend such methods to subsymbolic RL domains. Further, NESYA can be used to extend systems where automata are used to specify tasks and reward structures for RL agents [Icarte et al., 2018] and their NeSy extension [Umili et al., 2023a] to incorporate logical transitions.

Of significant interest is also the work of [Ahmed et al., 2024], who define a pseudo-semantic loss for autoregressive models with constraints and [Zhang et al., 2023], who similarly address the problem of incorporating constraints is LLMs. Both approaches assume a flat vocabulary. We believe NESYA can be beneficial for constrained autoregressive models when the output structure includes many features, i.e. the model generates structured traces, instead of natural language.

Perhaps the most natural avenue for future work is the definition of a high-level NeSy language for the specification of temporal programs which utilizes NESYA as a compilation target. Automata are generally low-level devices, cumbersome to define by hand, motivating the creation of a humancentric interface.

6 Conclusion

We presented the NESYA system for integrating neural networks with symbolic automata, under clean probabilistic semantics. We showed that current systems, such as DEEPSTOCHLOG, DEEPPROBLOG, and FUZZYA struggle to achieve scalable and accurate solutions in temporal domains. The NESYA system was instead shown to scale considerably better and achieve higher accuracy.

A Proof of Theorem 1

We focus on the meaning of αt(q), from which we can also draw further conclusions. Consider an SFA over propositions V . Let traces(q, t) denote all traces over V which starting from state q0 cause the SFA to end up in state q after t timesteps. Further, consider a sequence of probability vectors (p1, p2, . . . , pn) with each vector pi assigning a probability to each proposition v ∈ V at timestep i. Refer to Section 2.3 for an example of pi. The probability of a trace π is then:

Theorem 1 states that

Proof. We shall prove Theorem 1 by induction. For t = 1 we have:

recalling that α0(q) = 1 if q = q0 and 0 otherwise and from Equation 1 and 2. Assuming the hypothesis holds for t, we can prove it for t + 1, as follows:

The last step follows from:

with . the concatentation of an interpretation ω with a trace π, i.e π.ω = (π1, . . . , πt, ω). To elaborate, the set of traces which end in state q in t + 1 timesteps is the union over all traces which ended in state q′ in t timesteps concatenated with each interpretation ω causing the SFA to transition from q′ to q.

An immediate consequence of Theorem 1 is that:

for an SFA A.

B Implementation Details

All experiments were implemented in Pytorch and Python 3.11. For the experiment in Section 4.1 we use the implementation of FUZZYA provided by the authors 3 with minimal changes. Both NESYA and FUZZYA were trained for a fixed ammount of 100 epochs. For the second experiment (Section 4.2) we use an LSTM with a single layer and a 128 dimensional hidden state. The Transformer architechture has 3 attention heads per layer, 4 layers and an hidden state dimensionality of 129 (same with the input dimensions). Both architectures utilize the same CNN to extract visual embeddings of the bounding boxes.

3 https://github.com/whitemech/grounding LTLf in image sequences

Acknowledgments

NM and GP are supported by the project EVENFLOW, Robust Learning and Reasoning for Complex Event Forecasting, which has received funding from the European Union's Horizon research and innovation programme under grant agreement No 101070430. LDR is supported by the KU Leuven Research Funds (iBOF/21/075, C14/24/092), by the Flemish Government under the "Onderzoeks programma Artifici¨ele Intelligentie (AI) Vlaanderen" programme, the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation, and the European Research Council (ERC) under the European Union's Horizon Europe research and innovation programme (grant agreement n°101142702).

Contribution Statement

LDR and GP share last authorship.