Source-linked AI summary
Time to Reason: Scalable Neurosymbolic Learning for LTLf via Fuzzy Semantics
Riccardo Andreoni, Andrei Buliga, Alessandro Daniele, Paolo Felli, Chiara Ghidini, Marco Montali, Massimiliano Ronzani
TL;DR
Temporal NeSy lacks systematic analysis of how fuzzy semantics affect LTLf interpretation and learning, while automata-based methods face scalability challenges. This paper studies fuzzy semantics and introduces direct fuzzy evaluation in ∂LTLf, which achieves comparable or better classification performance with greater computational efficiency than DFA-based methods.
Problem
Temporal NeSy lacks systematic analysis of how fuzzy semantics affect LTLf interpretation and learning, and automata-based approaches face scalability concerns.
Source: §1 · p. 3, §9 · p. 46Method
The paper systematically studies fuzzy temporal semantics and integrates them into ∂LTLf, which evaluates LTLf specifications directly without intermediate automata.
Source: §9 · pp. 45–46Results
∂LTLf achieves comparable or better classification performance while being substantially more efficient than DFA-based techniques, especially as specifications become more complex.
Source: §7.3.2 · p. 44, §9 · p. 46Takeaways & Limitations
Direct fuzzy evaluation of LTLf formulas is a practical and scalable alternative to automata-based integration of temporal knowledge.
Source: §9 · p. 46The evaluation uses synthetic sequences and temporal specifications formed from conjunctions or simple combinations rather than deeply nested temporal formulas.
Source: §8 · p. 45
Abstract
from arXiv · showhide
Neurosymbolic (NeSy) Artificial Intelligence aims to integrate Deep Learning (DL) architectures with symbolic reasoning. While initial NeSy approaches have targeted mainly symbolic reasoning in propositional and first-order logics, recent works have started to address the construction of neurosymbolic frameworks for Temporal Logics, and in particular for LTLf. These approaches have established temporal NeSy as a promising research direction, laying the foundations for learning under temporal constraints. Nonetheless, they leave many questions unanswered. From a theoretical perspective, several differentiable semantics for interpreting LTLf have been proposed but have not yet been formally and systematically defined within a unified framework. Moreover, existing approaches commonly rely on automata to represent temporal knowledge, resulting in limited scalability. Motivated by this research gap, this paper provides the following contributions: (i) formally defining different fuzzy semantics for LTLf, and systematically analysing theoretical properties regarding equivalences and dualities of temporal operators; (ii) showing how these semantics can be directly integrated within a novel NeSy framework, called DiffLTLf, enabling flexible and scalable learning without relying on the usage of automata; and (iii) introducing a novel evaluation protocol of increased complexity of learning tasks w.r.t. existing benchmarks. Our results show that the choice of fuzzy semantics has a significant impact on predictive performance. Moreover, DiffLTLf achieves performance on par with, and sometimes superior to, state-of-the-art probabilistic approaches while substantially improving scalability. Taken together, these results establish direct fuzzy interpretations as a competitive and scalable alternative to existing temporal NeSy frameworks.
1. Introduction
The introduction positions DiffLTLf as a direct fuzzy-semantics approach to temporal NeSy learning, addressing gaps in theoretical analysis and scalability. It reports that semantics affect predictive performance and that the approach scales better while achieving comparative performance with a state-of-the-art method.
Introduction
- NeSy combines deep learning and symbolic reasoning; temporal approaches include automata-based methods and direct Gödel-semantics interpretation of LTLf.The introduction describes LTL and LTLf as useful across domains including formal methods, planning, process mining, and reinforcement learning.Source: §1 · p. 2
- Prior temporal NeSy work left the impact of fuzzy-semantic choices and scalability underexplored, while the benchmark of Lorello et al. covered only automata-compiling methods.The introduction notes that existing proposals used different differentiable semantics without systematically studying their relation to classical semantics or their performance effects.Source: §1 · p. 3
- DiffLTLf’s direct fuzzy interpretations achieve performance comparative with the state-of-the-art method while significantly increasing scalability, and fuzzy semantics affect predictive performance.The authors also note a trend in which probabilistic approaches tend to improve predictive performance while fuzzy logics tend to increase computational efficiency.Source: §1 · pp. 3–4
- Classical LTLf equivalences between temporal operators are fully preserved only under Gödel semantics; Product and Łukasiewicz semantics require native definitions for some operators.The paper presents this as part of a systematic study of fuzzy semantics in temporal NeSy learning.Source: §1 · p. 3
- DiffLTLf directly integrates different fuzzy semantics for flexible learning without automata, avoiding reliance on automata-based temporal knowledge representations.The introduction describes this as a novel NeSy framework.Source: §1 · p. 3
- The paper introduces an evaluation protocol for both automata-based and automata-free frameworks, increasing learning-scenario complexity relative to Lorello et al..The authors position the theoretical investigation and evaluation setting as contributions to future temporal NeSy framework development.Source: §1 · pp. 3–4
2. Background
The background frames the target as weakly supervised symbol grounding under temporal constraints and introduces finite-trace temporal logic; fuzzy-logic notions are deferred to Section 4.
2.1. Weakly Supervised Symbol Grounding under Distant Temporal Supervision
- The task is to infer symbolic categories for images using only each sequence’s binary temporal-compliance label, with no image-level category supervision.The sequence-level label indicates whether the symbolic sequence satisfies or violates the temporal specification.Source: §2.1 · p. 5
2.2. Linear Temporal Logic on Finite Traces
- LTLf evaluates formulas over non-empty finite traces assigning Boolean values to propositions; strong next requires a successor, while until requires its right operand to hold eventually and its left operand beforehand.A trace satisfies a formula when the formula holds at its first instant.Source: §2.2 · pp. 6–8
- Weak next, release, globally, eventually, strong release, and weak until are defined using strong next and until.These operators capture variants of next, persistence, eventual occurrence, and until conditions.Source: §2.2 · pp. 8–9
- Declare patterns provide LTLf descriptions of declarative business-process constraints and are used to evaluate the approach.The paper points to Table 1 for pattern templates and their formalizations.Source: §2.2 · p. 9, Table 1 · p. 9
3. State of the Art in Temporal NeSy
Recent temporal NeSy work focuses on LTLf and weakly supervised symbol grounding under distant temporal supervision, but differs in how it integrates temporal knowledge and interprets formulas. Its architectural, semantic, and benchmark limitations motivate an automata-free fuzzy framework and a more challenging evaluation protocol.
3.1. NeSy Frameworks for Temporal Logic
- FuzzyA and NeSyA compile LTLf into automata and recurrently propagate neural outputs, facing worst-case double-exponential automaton size and inherently sequential evaluation.At each timestep, soft truth values for atomic propositions evaluate transition guards, which update automaton-state truth values from the start to the end of the sequence.Source: §3.1 · p. 11
- T-ILR evaluates LTLf formulas directly through differentiable fuzzy semantics, and this work adopts the same automata-free approach for ∂LTLf.Direct evaluation computes a satisfaction degree from neural outputs and supports gradient-based optimization.Source: §3.1 · p. 11
- FuzzyA [29] uses Product semantics, T-ILR [1] uses Gödel semantics, and NeSyA [22] uses probabilistic reasoning whose exact inference requires weighted model counting.The paper identifies a lack of systematic investigation into semantic choices and their impact, including the predictive-performance and computational-cost trade-off between probabilistic and fuzzy approaches.Source: §3.1 · pp. 11–12
- To prioritize scalability, ∂LTLf is proposed as a semantics-agnostic fuzzy framework, with theoretical analysis of t-norm-based semantics and systematic evaluation of predictive performance and computational cost.The evaluation is intended to compare different fuzzy and probabilistic semantics and reveal their effects on the task.Source: §3.1 · p. 12
3.2. Temporal NeSy benchmarks
- LTLZinc interleaves temporal and relational constraints, adds intermediate supervision and supervised perception pretraining, and requires next-state supervision, limiting distant-only evaluation and excluding automata-free methods.The proposed protocol instead uses only sequence-level labels, applies to automata-based and automata-free methods, and varies specification size separately from input-sequence length.Source: §3.2 · pp. 12–13
4. Fuzzy LTLF
This section defines three fuzzy finite-trace LTL variants and examines how their connective choices shape temporal evaluation. It establishes operator definability and analyzes equivalences, dualities, and the Boolean-trace case across the variants.
4. Fuzzy LTLF
- Three fuzzy LTLf variants use Gödel, Product, or Łukasiewicz connective semantics to evaluate formulas over finite traces with real-valued proposition truth degrees.Their shared syntax uses fuzzy connectives and the temporal operators next (X) and until (U); formula values are computed recursively using the selected t-norm, t-conorm, negation, and implication.Source: §4 · pp. 13–15
- Until values depend on the connective semantics: Gödel selects the best individual realization, while Product and Łukasiewicz allow multiple realizations to contribute.Gödel’s min/max operations do not compound repeated local support; Product accumulates realizations probabilistically, whereas Łukasiewicz combines support additively up to saturation.Source: §4 · p. 18
4.2. Additional Temporal Operators
- F, G, weak next, and release are definable from the base logic, but weak until and strong release generally require native definitions, except under Gödel semantics.Weak until permits positive support even if its right-hand formula never becomes positive; strong release requires its left-hand formula eventually to become positive, while release does not.Source: §4.2 · pp. 18–19
- De Morgan’s laws hold in all three logics, but distributivity holds for Gödel and not Product semantics; F and G also simplify to combining values across the remaining trace.F combines those values with the t-conorm and G with the t-norm.Source: §4.2 · pp. 19–20
- Weak until is equivalent to until-or-always under Gödel semantics, but this equivalence fails under Product and Łukasiewicz semantics.The supplied counterexamples show unequal values for the two sides in both non-Gödel cases.Source: §4.2 · p. 21
- Strong release and release are dual to weak until and until, respectively.The section establishes these dualities using negation and De Morgan’s laws.Source: §4.2 · p. 22
- For product and Łukasiewicz semantics, the identity M ≡ φ2 U (φ1 ∧ φ2) fails: the examples give 0.384 versus 0.4176 and 0.2 versus 0.1, respectively.The paper attributes the failure to the lack of distributivity for product semantics; the Łukasiewicz example also gives unequal values.Source: §4.2 · pp. 22–23
- The identity R ≡ φ2 W (φ1 ∧ φ2) likewise fails in the examples: product semantics gives 0.51 versus 0.62928, and Łukasiewicz semantics gives 0.6 versus 0.5.The cited calculations evaluate each side on the same trace.Source: §4.2 · pp. 22–23
- R can be obtained by duality from U, and M from W; W is an abbreviation only in Gödel semantics, whose temporal basis can therefore be {X, U}.For the other considered semantics, W is treated as primitive.Source: §4.2 · pp. 23–24
- Regardless of the chosen fuzzy semantics, traces containing only 0/1 values make these logics collapse to standard LTLf.On Boolean values, the t-norm and t-conorm coincide with Boolean conjunction and disjunction.Source: §4.2 · p. 24
5. The ∂LTLf Framework
The ∂LTLf framework learns from sequence-level labels by grounding observations into fuzzy propositions and evaluating temporal specifications directly on fuzzy traces. Its tensor-based implementation supports batched variable-length sequences while preventing padding from changing valid satisfaction values.
5.1. Problem Formulation
- Without per-concept labels, the framework learns shared perception parameters from raw multi-stream sequences and binary labels indicating whether their symbolic traces satisfy a temporal specification.This is weakly supervised symbol grounding: the crisp symbolic trace is unavailable during training, and the specification provides background knowledge.Source: §5.1 · p. 25
5.2. Framework
- Unlike automata-based temporal NeSy approaches, ∂LTLf recursively evaluates fuzzy semantics on the perception module’s trace and trains end-to-end from satisfaction values using binary cross-entropy.The temporal logic module evaluates the specification’s syntactic tree directly, without intermediate automaton construction, and is differentiable almost everywhere.Source: §5.2 · pp. 25–27
5.3. Implementation
- The PyTorch evaluator processes batches as tensors, padding shorter sequences and using a validity mask to substitute operator-specific boundary values so padded positions cannot affect valid satisfaction.In a Gödel-semantics example, a length-3 trace padded to length 5 yields satisfaction 0.7, matching evaluation on the unpadded trace.Source: §5.3 · pp. 28–30
6. Evaluation
The evaluation tests ∂LTLf on temporal multi-stream sequence classification, comparing it with DFA-based FuzzyA and NeSyA on accuracy, symbol grounding, and computational scalability.
6. Evaluation
- The evaluation compares ∂LTLf with DFA-based FuzzyA and NeSyA on sequence classification, symbol grounding, and scalability as formulas and sequences grow.For scalability, it measures logic-module runtime per training epoch.Source: §6 · pp. 30, 32
6.1. Temporal Multi-Stream Benchmark
- The benchmark removes relational constraints, increases temporal-formula complexity, and trains from only sequence-level satisfaction labels, requiring symbol grounding without intermediate annotations.This weak supervision reflects settings where symbolic traces and automaton states are unavailable; automaton-state supervision would also restrict fair comparison to DFA-based methods.Source: §6.1 · pp. 32–33
- The benchmark separates eight templates into response-type and precedence-type sets, pairing each set with MNIST and Fashion-MNIST for four cases.It uses three parallel image streams; Set 1 contains Response, Not Succession, Chain Succession, and Not Chain Succession, while Set 2 contains Precedence, Chain Precedence, Responded Existence, and Not Co-existence.Source: §6.1 · p. 33
6.1.1. Varying Formula Complexity
- Formula complexity varies K from 1 to 4 conjoined sub-formulas, increasing the class count as |C| = 2K while sequence lengths remain uniformly sampled from 2 to 10.Keeping sequence length fixed in distribution isolates the effect of formula complexity.Source: §6.1.1 · pp. 33–34
6.1.2. Varying Sequence Length
- Sequence length varies from 20 to 200 in steps of 20, with fixed-length sequences per configuration and two MNIST specifications containing 4 or 8 classes.The specifications use Response or Precedence patterns to assess whether sequence-length effects depend on formula complexity.Source: §6.1.2 · p. 34
6.2. Evaluation Metrics
- Evaluation reports held-out symbol-grounding and sequence-classification accuracy, and measures computational cost as logic-module time per training epoch.A sequence is predicted to satisfy Φ when v(Φ, λθ) ≥ 0.5; image labels are used only for evaluating grounding, not for training. Response and Precedence combinations are chosen to keep datasets as balanced as possible.Source: §6.2 · p. 34
7. Results
Results assess how fuzzy semantics affect accuracy, how Product-based ∂LTLf compares with temporal neurosymbolic methods, and how the methods scale. Results average 10 runs, with paired one-sided Wilcoxon tests used to assess significance.
7.1.1. Answer to RQ1
- Product is the only semantics robust to growing specification complexity, maintaining grounding accuracy above 92% on MNIST and 85% on Fashion-MNIST at |C| = 8.Its accuracy has low variance across values of |C| and experimental settings.Source: §7.1.1 · pp. 35–36, Figure 6 · p. 36
- Gödel and Łukasiewicz are competitive with Product at |C| = 2, but their variance and performance degradation increase with complexity; sequence-classification accuracy follows the same ranking with smaller differences.At |C| = 4, they sometimes approach optimal performance, but many runs converge lower; degradation is more severe for |C| ≥ 6, suggesting sensitivity to local optima.Source: §7.1.1 · pp. 36–37, Table 2 · p. 37
7.1.2. Discussion on RQ1
- Gradient behavior helps explain the semantic differences: Product sends non-zero gradients to every timestep, whereas Gödel’s single-passing computation sends a learning signal to exactly one observation.For Łukasiewicz, the n-ary t-norm gradient is non-vanishing only when mean truth exceeds (n − 1)/n, a condition met by 1/n! of the input space.Source: §7.1.2 · pp. 37–38
7.2.1. Answer to RQ2
- Across formula complexities, the three neurosymbolic methods are generally competitive; NeSyA’s isolated significant advantages are under half a percentage point, while neural baselines fail to learn valid grounding.At |C| = 2, all three achieve near-perfect grounding; accuracy declines for all as complexity grows.Source: §7.2.1 · pp. 39–40, Table 3 · p. 39, §7.2 · p. 39
- With |C| = 4, all three methods maintain high, stable grounding accuracy as sequence length grows; with |C| = 8, FuzzyA and NeSyA degrade and fall behind ∂LTLf from length 60 onward.NeSyA’s significant gains over its competitors at some |C| = 4 lengths never exceed 0.2 percentage points; the neural baselines remain near random-guess accuracy.Source: §7.2.1 · pp. 40–41, Table 4 · p. 41, Figure 8 · p. 42
7.2.2. Discussion on RQ2
- The cause of the methods’ configuration-dependent accuracy differences remains open; the paper proposes comparing gradients from each logic module on identical perception outputs as a possible avenue for investigation.Final accuracy alone does not identify the mechanism, and whether gradient comparisons suffice is also unresolved.Source: §7.2.2 · pp. 42–43
7.3.1. Answer to RQ3
- ∂LTLf’s temporal-module time changes negligibly from |C| = 2 to 8 (0.04 s to 0.07 s per epoch), while DFA-based methods grow super-linearly; at the longest sequences, ∂LTLf is faster by between one and nearly three orders of magnitude.FuzzyA and NeSyA require automaton construction, whose cost is excluded from reported training times; ∂LTLf avoids the automaton and evaluates the specification directly, with cost governed by formula size.Source: Figure 7 · p. 40, Figure 8 · p. 42, §7.3.1 · p. 43
7.3.2. Discussion on RQ3
- ∂LTLf matches DFA-based methods in classification accuracy and outperforms them in the most demanding configurations, while requiring a fraction of their computational cost.The demanding configurations combine high formula complexity and sequence length; the accuracy advantage appears at both symbol-grounding and sequence-classification levels.Source: Figure 7 · p. 40, §7.2.1 · p. 41, Figure 8 · p. 42
8. Threats to Validity
The evaluation uses synthetic sequences and relatively simple temporal specifications to control task complexity and test scalability. Its design also follows shared training settings rather than an exhaustive hyperparameter search.
Threats to Validity
- Synthetic sequences enable control of formula complexity and sequence length; no real-world temporal datasets with ground-truth LTLf satisfaction labels exist at the required scale, while MNIST and Fashion-MNIST are standard benchmarks.Synthetic generation was used to stress-test the temporal reasoning component under increasingly demanding conditions.Source: §8 · p. 45
- Specifications use conjunctions or simple combinations of Declare patterns rather than deeply nested LTLf operators, enabling formula complexity to be controlled by the number of sub-formulas K [29, 10].Declare patterns are established temporal constraints in process mining; this choice follows previous work.Source: §8 · p. 45
- No exhaustive hyperparameter search was performed; training configurations followed a related benchmark, were shared across methods, and used a standard 80/20 train/test split.The configuration used Adam, a learning rate of 10^-4, and a specified number of training epochs.Source: §8 · p. 45
9. Conclusions
The paper presents ∂LTLf as a direct, automata-free way to integrate fuzzy LTLf specifications into neural sequence classifiers, and finds that fuzzy semantics choices affect learning behavior. Its evaluation and theoretical analysis support direct fuzzy evaluation as a scalable alternative and a basis for future temporal neurosymbolic work.
9. Conclusions
- ∂LTLf injects LTLf specifications into neural sequence classifiers by evaluating formulas directly on finite traces, avoiding intermediate automata and leaving the perception architecture unchanged.The symbolic specification contributes to the training objective.Source: §9 · pp. 45–46
- The systematic study shows that fuzzy semantics choices affect temporal-operator interpretation and learning behavior, making semantics an important design decision in temporal NeSy frameworks.Different fuzzy semantics lead to different predictive behavior across the evaluated classification tasks.Source: §9 · p. 46
- ∂LTLf achieves comparable or better classification performance while being substantially more efficient than state-of-the-art techniques, especially as specifications become more complex.Direct formula evaluation avoids the automaton-size blow-up that can affect DFA-based methods.Source: §9 · p. 46
- The theoretical analysis and evaluation protocol provide a foundation for future temporal NeSy assessment; planned work includes richer logics, more realistic benchmarks, and learning or refining specifications from data.The evaluation varied temporal specifications, formula complexities, numbers of classes, and sequence lengths.Source: §9 · p. 46
Appendix A. Implementation Details of Baselines
The appendix describes the implementations of FuzzyA and NeSyA used as comparative baselines, chosen to support fair comparison.
Appendix A. Implementation Details of Baselines
- FuzzyA and NeSyA baseline implementations were selected to ensure fair comparison in computational efficiency and adherence to each method’s theoretical foundations.The appendix provides implementation details for both baselines.Source: Appendix A · pp. 51–52
Appendix A.1. FuzzyA
The FuzzyA baseline uses the LTLZinc implementation, which differs from the original in state renormalization and training loss while retaining its automaton-based formula evaluation mechanism.
Appendix A.1. FuzzyA
- Under identical perception and training settings, the LTLZinc variant achieves substantially higher symbol-grounding and sequence-classification accuracy than the original, with the loss change accounting for most of the gap.Source: Appendix A.1 · p. 52
- The LTLZinc implementation renormalizes automaton state distributions with softmax at each timestep and trains with binary cross-entropy on summed accepting-state fuzzy values, unlike the original loss.Source: Appendix A.1 · p. 52
- FuzzyA builds a propositional formula for each potential next automaton state by disjoining valid incoming transitions, each formed from the previous state and transition guard.Previous states are logical variables; conjunctions map to multiplication and disjunctions to algebraic summation.Source: Appendix A.1 · p. 52
Appendix A.2. NeSyA
The NeSyA baseline follows the original architecture, compiling transition guards into d-DNNF circuits for exact probabilistic reasoning over input symbols.
Appendix A.2. NeSyA
- At each timestep, compiled guard circuits populate a transition matrix, and matrix multiplication updates the state distribution.The implementation avoids the LTLZinc version, which combines state variables and transition guards into one circuit and can be inefficient for large automata.Source: Appendix A.2 · pp. 52–53
Appendix B. Experimental Setup Details
Appendix B specifies the shared perception architecture, training configuration, dataset construction, and compute environment used across the experiments. It also describes the epoch limits and data split used for comparisons.
Perception module
- All methods share the same CNN perception module so performance differences are attributed to temporal reasoning rather than perception.It uses two 5 × 5 convolutional layers with 32 and 64 filters, followed by fully connected layers of size 1024 and |C|; 32 × 32 inputs produce softmax-normalized class truth values.Source: Appendix B · p. 53
Training configuration
- All models use Adam with learning rate 10^-4, batch size 64, binary cross-entropy, and 10 runs; training lasts 50 epochs for formula-complexity experiments and 30 for sequence-length experiments.The 30-epoch limit reflects the higher per-epoch cost of DFA-based methods on long sequences; the same epoch count was used across methods for fair comparison.Source: Appendix B · p. 53
Dataset construction
- Each configuration uses 1,000 sequences across three streams, with random class labels and MNIST or Fashion-MNIST images; crisp-trace LTLf labels are split 80% for training and 20% for held-out testing.At each timestep, each stream’s class is sampled uniformly from the available classes; the ground-truth label is computed by evaluating the specification on the symbolic trace.Source: Appendix B · pp. 53–54
Hardware and software
- Experiments ran on a single NVIDIA RTX A6000 GPU with 48 GB memory, using PyTorch 2.3.1 and CUDA 12.1.Source: Appendix B · p. 54
Appendix C. Complete Experimental Results
Appendix C expands the main text’s representative-method reporting into full results across all evaluated methods and both experimental axes.
Appendix C. Complete Experimental Results
- Coverage includes ∂LTLf’s Product, Gödel, and Łukasiewicz semantics, T-ILR, both FuzzyA implementations, NeSyA, GRU, and Transformer.FuzzyA includes the LTLZinc variant used throughout the paper and the original implementation.Source: Appendix C · p. 54
- Formula-complexity experiments report full results for MNIST and Fashion-MNIST in Tables C.5–C.6.Both tables average results over 10 runs and report image accuracy, sequence accuracy, and logic-module time per epoch.Source: Appendix C · p. 54, Table C.5 · p. 55, Table C.6 · p. 56
- Sequence-length experiments report full results for |C| = 4 and |C| = 8 in Tables C.7–C.8.Values are averaged over 10 runs using the main-text protocol; bold marks statistical significance over all other methods (Wilcoxon signed-rank, p < 0.05).Source: Appendix C · p. 54, Table C.7 · p. 57, Table C.8 · p. 58