NeSyA: Neurosymbolic Automata

TL;DR

NeSyA introduces a probabilistic neurosymbolic framework that integrates neural perception with Symbolic Automata (SFA) to tackle temporal sequence classification and tagging. By mapping observations to symbol probabilities via a neural module and performing exact, matrix-based inference over an SFA with probabilistic semantics, NeSyA achieves end-to-end differentiability and scalable inference through knowledge compilation and weighted model counting. The approach outperforms prior NeSy systems in temporal domains, offering stronger generalization and efficiency on synthetic driving patterns and real-world CAVIAR event recognition. This work paves the way for scalable temporally-aware NeSy systems and suggests future extensions to reinforcement learning constraints and high-level NeSy programming interfaces.

Abstract

Neurosymbolic (NeSy) AI has emerged as a promising direction to integrate neural and symbolic reasoning. Unfortunately, little effort has been given to developing NeSy systems tailored to sequential/temporal problems. We identify symbolic automata (which combine the power of automata for temporal reasoning with that of propositional logic for static reasoning) as a suitable formalism for expressing knowledge in temporal domains. Focusing on the task of sequence classification and tagging we show that symbolic automata can be integrated with neural-based perception, under probabilistic semantics towards an end-to-end differentiable model. Our proposed hybrid model, termed NeSyA (Neuro Symbolic Automata) is shown to either scale or perform more accurately than previous NeSy systems in a synthetic benchmark and to provide benefits in terms of generalization compared to purely neural systems in a real-world event recognition task.

Figures (6)

• Figure 1: Symbolic automata (middle) are used to reason over sequences of subsymbolic inputs (top) from which information is extracted with the aid of a neural network, performing multilabel classification. For instance, for the image , the correct symbol grounding is $\{ \mathrm{tired}, \neg \mathrm{blocked}, \neg \mathrm{fast} \}$. The symbolic automaton shown captures the following logic: If the driver is tired or the road is blocked, then in the next timestep they should not be going fast. NeSyA computes the probability of the SFA accepting the input sequence (bottom), which is then used for learning.
• Figure 2: A d-DNNF circuit for the formula $\phi = \neg \mathrm{fast} \land (\mathrm{blocked} \lor \mathrm{tired})$ (left) and an arithmetic circuit produced from the d-DNNF circuit (right). The computation of $\mathrm{WMC}$ is shown for the vector $\mathrm{p} = [0.8, 0.3, 0.6]$ for the symbols $\{\mathrm{tired}, \mathrm{blocked}, \mathrm{fast}\}$ respectively.
• Figure 3: Graphical model for NeSyA. Following the approach used in mccallum2000maximum, it resembles a Hidden Markov Model with the arrows between states and observations reversed. The random variables $q_{t}$ take values from $Q$, the state space of the SFA, and the random variables $o_t$ take values from high-dimensional continuous spaces.
• Figure 4: Scalability results for NeSyA (solid) and DeepStochLog (dashed) for each of the three patterns tested.The y-axis represents the update time for a single batch of 16 sequences in logarithmic scale and the x-axis the sequence length. The systems were benchmarked for three different patterns of varying complexity both in terms of symbols, as well as states of the automaton.
• Figure 5: Sample of the CAVIAR data. Models are given the two bounding boxes per timestep instead of the complete image, in order to make the task simpler for the neural component. Along with the pair of bounding boxes, a $\mathrm{close(p1, p2)}$ feature is provided, which captures whether the two people are close to each other.The CNN for NeSyA must ground one bounding box to the symbols $\mathrm{walking(p1)}$, $\mathrm{running(p1)}$, $\mathrm{active(p1)}$, $\mathrm{inactive(p1)}$ and correspondingly to $\mathrm{p2}$ for the second bounding box. The correct grounding for this image is $\mathrm{active(p1)}$ and $\mathrm{walking(p2)}$. These are the low-level activities performed by each person. The high-level activities performed by the pair are annotated for each image in one of the three classes $\mathrm{no\_event}$, $\mathrm{meeting}$, $\mathrm{moving}$. For the image shown here the annotation is $\mathrm{moving}$.

Theorems & Definitions (2)

• Theorem 1: $\alpha$-semantics
• proof