PaperlayerView exact revision on arXiv

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

arXiv:2608.16443v1cs.AI

TL;DR

Existing temporal neurosymbolic approaches lack a unified analysis of fuzzy LTLf semantics and often rely on poorly scalable automata representations. The paper introduces DiffLTLf for direct fuzzy evaluation and finds comparable or better accuracy with substantially greater efficiency than DFA-based methods.

  • Problem

    Temporal neurosymbolic research lacks unified analysis of fuzzy LTLf semantics and commonly relies on automata-based representations with limited scalability.

  • Method

    The paper systematically studies fuzzy LTLf semantics and integrates them into DiffLTLf, which evaluates temporal specifications directly without intermediate automata.

  • Results

    Direct fuzzy evaluation achieves comparable or better classification accuracy than DFA-based methods while requiring a fraction of their computational cost.

  • Takeaways & Limitations

    Direct fuzzy evaluation provides a practical and scalable alternative to automata-based integration of temporal knowledge.

  • Takeaways & Limitations

    The evaluation uses synthetically built sequences because real-world temporal datasets with ground-truth LTLf satisfaction labels are unavailable at the required scale.

Abstract

from arXiv · show

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 frames temporal NeSy for LTLf as promising but limited by insufficient theoretical analysis of fuzzy semantics and scalability concerns. It presents DiffLTLf, a direct fuzzy framework, alongside systematic semantic analysis and a more challenging evaluation protocol.

  • NeSy AI integrates Deep Learning architectures with symbolic reasoning to combine their strengths while addressing limitations in data efficiency, fairness, trust, and safety.
  • Recent NeSy research has extended beyond propositional and first-order logics toward temporal logics, especially LTL and LTLf for finite traces.
  • Existing temporal NeSy proposals use different differentiable semantics for classical LTL but do not systematically investigate their theoretical relationships or effects.
  • Scalability remains insufficiently studied in temporal NeSy despite weakly supervised symbol grounding providing a clear evaluation task.
  • The work systematically studies fuzzy temporal semantics, introduces DiffLTLf without automata, and reports comparative performance with state-of-the-art methods while significantly increasing scalability.The paper also proposes a novel evaluation setting and links its findings to broader trends contrasting probabilistic predictive performance with fuzzy-logical computational efficiency.

2. Background

The paper addresses weakly supervised symbol grounding from image sequences labeled only by compliance with temporal specifications. It formalizes LTLf over non-empty finite traces and introduces its core and derived temporal operators for the neurosymbolic setting.

  • Weakly Supervised Symbol Grounding: Weakly supervised symbol grounding requires discovering image categories from sequences using only a binary label indicating compliance with a temporal specification.The specification constrains the admissible ordering of symbols over time, while individual image categories remain unobserved.
  • Weakly Supervised Symbol Grounding: Each input is a sequence of images from an unknown finite category set, annotated according to whether its symbolic interpretation satisfies or violates a given temporal rule.The model is never told the category assigned to any individual image.
  • Linear-Time Temporal Logic on Finite Traces: LTLf extends linear-time temporal logic to unbounded but finite traces, which naturally represent dynamics in domains such as planning and process mining.Traditional LTL assumes infinitely long traces, whereas LTLf uses finite traces.
  • Linear-Time Temporal Logic on Finite Traces: An LTLf trace is a non-empty vector of instants, each assigning every propositional symbol a Boolean value, with the final instant indexed as last(λ) = n−1.For a trace of length n, each λ_i maps P to {0, 1}.
  • Declare Patterns: Declare pattern templates provide process-oriented LTLf formulae for declaratively describing business processes and are used to evaluate the proposed approach.The benchmark templates use stream-specific propositions or Boolean combinations of them.

3. State of the Art in Temporal NeSy

Recent temporal NeSy methods address LTLf learning under distant temporal supervision but differ in knowledge integration and differentiable semantics. Existing automata-based methods face scalability limits, while prior semantics and benchmark designs lack systematic comparison and isolate temporal reasoning imperfectly.

  • Scope: Recent temporal NeSy frameworks focus on LTLf and solve weakly supervised symbol grounding under distant temporal supervision in different ways.They differ mainly in how temporal knowledge enters learning and which differentiable semantics interprets it.
  • Knowledge integration: FuzzyA and NeSyA compile LTLf specifications into deterministic finite-state automata whose transitions are evaluated differentiably over neural perception outputs.At each timestep, soft atomic-proposition values evaluate automaton guards, which update automaton-state truth values.
  • Knowledge integration: Automaton construction can be double-exponential in formula size, while recurrent state evaluation is inherently sequential and prevents parallelisation over time.These limitations require the automaton before training and make sequence evaluation depend on the previous timestep.
  • Knowledge integration: T-ILR evaluates LTLf formulas directly through fuzzy semantics without an intermediate automaton, computing satisfaction degrees from neural outputs for gradient-based optimization.The paper follows this automata-free approach in ∂LTLf.
  • Differentiable semantics: Existing frameworks use heterogeneous semantics: FuzzyA adopts Product semantics, T-ILR uses Gödel semantics, and probabilistic semantics provides exact inference at the cost of Weighted Model Counting.Prior work also indicates that fuzzy-semantics choices can significantly affect predictive performance, motivating systematic investigation.
  • Evaluation benchmarks: LTLZinc mixes temporal operators with relational constraints and adds intermediate supervision and supervised perception pre-training, limiting comparisons under purely distant supervision.The proposed evaluation protocol uses only sequence-level labels and separately varies temporal-specification size and input-sequence length for automata-based and automata-free methods.

4. Fuzzy LTLF

Section 4 defines finite-trace fuzzy LTLf through three alternative connective semantics—Gödel, Product, and Łukasiewicz—and formalizes temporal evaluation over traces with truth degrees in [0, 1]. It analyzes derived temporal operators and shows that semantic choice affects operator equivalences and formula values.

  • 4. Fuzzy LTLF: The framework defines three fuzzy LTLf variants by choosing Gödel, Product, or Łukasiewicz semantics for logical connectives.They are denoted fltlG_f, fltlP_f, and fltlŁ_f, respectively.
  • 4.1. Syntax and Semantics: Formulas are evaluated on non-empty finite traces assigning each proposition a real truth degree in [0, 1].The temporal operators X and U use next-state and recursive until semantics, with X returning 0 beyond the final instant.
  • 4.1. Syntax and Semantics: The recursive U semantics explicitly combines deferred support through the selected t-norm and t-conorm, so different semantics can produce different formula values.Under the discussed behavior, repeated local support values need not compound, while the same formula’s value can still vary with how alternative realizations interact.
  • 4.2. Additional Temporal Operators: De Morgan’s laws hold across all three fuzzy LTLf logics, and simplified semantics for F and G enable more efficient implementations.The proposition gives both negation-conjunction and negation-disjunction equivalences for every trace and instant.
  • 4.2. Additional Temporal Operators: Some classical LTLf operator equivalences fail: in Product semantics, a counterexample shows W cannot equal the combination of U and G because distributivity does not hold.The supplied counterexample evaluates the two sides at 0 as 0.764 and 0.74 ⊕ 0.2, respectively.
  • 4.2. Additional Temporal Operators: R is obtained by duality from U and M from W, but W is an abbreviation only under Gödel semantics; M and R otherwise require native definitions.The results distinguish operators derivable by duality from those unavailable through standard LTLf equivalences.

5. The ∂LTLf Framework

The ∂LTLf framework performs weakly supervised sequence classification by mapping observations to fuzzy proposition values and evaluating temporal specifications directly on the resulting fuzzy traces. Its differentiable, automaton-free pipeline supports end-to-end training through binary cross-entropy and tensorized batch evaluation.

  • 5.1 Problem formulation: ∂LTLf learns from raw observation sequences and binary specification-satisfaction labels without access to the intermediate crisp symbolic traces.The perception module fθ maps observations to fuzzy truth values, making the task weakly supervised symbol grounding.
  • 5.2 Proposed approach: Binary cross-entropy compares v(Φ, λθ) with y, and gradients are backpropagated through the temporal logic and perception modules to update θ.This enables end-to-end training directly from the framework’s outputs.
  • 5.2 Proposed approach: The perception module applies fθ independently across streams and time, producing fuzzy truth values for each stream-specific atomic proposition and forming the fuzzy trace λθ.Each output lies in [0, 1]^|C|, and collecting outputs across instants yields proposition sequences across all streams.
  • 5.2 Proposed approach: The temporal logic module evaluates Φ recursively on λθ under any of three fuzzy semantic instances, without constructing an intermediate automaton.The resulting value v(Φ, λθ) represents the formula’s satisfaction degree at the beginning of the trace and is differentiable almost everywhere.
  • 5.3 Implementation: The PyTorch implementation evaluates batches as tensor operations over a common padded length, using a boolean mask to distinguish valid from padded instants.For a batch, T = max_b n_b is the maximum sequence length, while μ ∈ {0, 1}^{B×T} marks valid and padded positions.

6. Evaluation

The evaluation tests ∂LTLf on weakly supervised temporal multi-stream classification, comparing fuzzy semantics and DFA-based baselines across predictive accuracy, symbol grounding, and scalability. It varies formula complexity and sequence length using controlled benchmark settings.

  • Evaluation questions: The evaluation compares ∂LTLf with DFA-based FuzzyA and NeSyA on sequence classification accuracy, symbol grounding quality, and training-time computational cost.The logic-module runtime is measured per training epoch.
  • Benchmark design: The benchmark uses three parallel image streams, removes relational constraints, and provides only sequence-level formula-satisfaction labels for weak supervision.The setup avoids intermediate symbolic traces, automaton states, and constraint labels during training.
  • Benchmark design: Four experimental cases pair two formula sets with MNIST and Fashion-MNIST, distinguishing Response-family templates from Precedence-family templates.Set 1 uses Response, Not Succession, Chain Succession, and Not Chain Succession; Set 2 uses Precedence, Chain Precedence, Responded Existence, and Not Co-existence.
  • Formula complexity: Formula-complexity experiments vary K ∈ {1, 2, 3, 4}, yielding |C| = 2K classes while sampling sequence lengths uniformly from [2, 10].Sequence-length distributions remain fixed across K so performance differences reflect formula complexity.
  • Sequence length: Sequence-length experiments vary fixed lengths from 20 to 200 in steps of 20 using MNIST and specifications with |C| = 4 or |C| = 8 classes.The two specifications use Response or Precedence templates to examine whether length effects depend on temporal complexity.
  • Metrics: Evaluation reports symbol grounding accuracy on images and sequence classification accuracy, predicting formula satisfaction when v(Φ, λθ) ≥ 0.5.Per-image labels are used only for evaluation, not training.

7. Results

The results show that fuzzy-semantics choice strongly affects ∂LTLf accuracy, with Product remaining robust as temporal specifications become more complex. Compared with DFA-based neurosymbolic methods, ∂LTLf achieves comparable or higher accuracy while requiring substantially less computational cost.

  • RQ1: Fuzzy semantics: Product semantics remains robust as formula complexity increases, while Gödel and Łukasiewicz degrade through higher variance and sensitivity to local optima.At |C| = 2, all three semantics achieve grounding accuracy above 99% in almost all settings; degradation becomes more severe for |C| ≥6.
  • RQ1: Fuzzy semantics: Product maintains average grounding accuracy above 92% on MNIST and 85% on Fashion-MNIST even at |C| = 8, with low variance across 10 runs.The low variance indicates that convergence to correct grounding does not depend on initialization.
  • RQ2: Method comparison: Across formula complexity and sequence length, the three neurosymbolic methods generally remain competitive, while ∂LTLf outperforms DFA-based competitors in the most demanding configurations.For sequence length, all methods retain high and stable grounding accuracy, and observed differences never exceed 0.2 percentage points.
  • RQ2: Method comparison: The purely neural baselines fail to learn valid symbol groundings as formula complexity or sequence length increases, with grounding accuracy collapsing toward random-guess performance.They are therefore omitted from the main comparison tables and sequence-length figure, with complete numerical results reported in Appendix C.
  • RQ3: Computational cost: ∂LTLf is the fastest neurosymbolic method in every tested configuration, and its advantage increases with formula complexity and sequence length.Unlike FuzzyA and NeSyA, ∂LTLf avoids constructing a finite-state automaton and evaluates the temporal specification directly, so cost depends on Φ rather than a potentially double-exponentially larger automaton.

8. Threats to Validity

The study’s validity is limited by synthetic evaluation data, restricted temporal-specification complexity, and training-design choices that prioritize controlled, fair comparisons over exhaustive tuning.

  • Synthetic dataset: The evaluation uses synthetically generated input sequences, enabling control over formula complexity and sequence length for scalability stress tests.The authors note that no real-world temporal dataset is known to them.
  • Selection of temporal specifications: Temporal specifications use conjunctions or simple combinations of declare patterns rather than LTLf formulas with deeply nested temporal operators.This follows prior work and reflects declare patterns’ established use in process mining while preserving control over formula complexity.
  • Design choices: No exhaustive hyperparameter search was performed; Adam, a 10^-4 learning rate, and training epochs followed a related benchmark’s configuration.All compared methods used the same configuration for fair comparison, with a standard 80/20 train/test split.

9. Conclusions

The paper introduces ∂LTLf, which directly evaluates LTLf formulas through fuzzy semantics during neural sequence-classifier training without intermediate automata. Its analyses and experiments show that semantics choice affects learning behaviour, while the framework offers comparable or better performance and a scalable alternative to automata-based integration.

  • Contributions: ∂LTLf injects LTLf specifications into neural sequence classifiers by evaluating formulas directly on finite traces through various fuzzy semantics, without intermediate automata.The symbolic specification contributes to the training objective while leaving the perception module’s architecture unchanged.
  • Contributions: The systematic semantic study shows that fuzzy-semantics choices affect temporal-operator interpretation and resulting learning behaviour.Different fuzzy semantics produce different predictive behaviour, making semantics selection an important design decision in temporal NeSy frameworks.
  • Evaluation: ∂LTLf was evaluated across temporal specifications, formula complexities, class counts, and sequence lengths against DFA-based neurosymbolic baselines.The experiments assessed classification tasks under varied temporal and sequence conditions.
  • Implications: Direct fuzzy evaluation of LTLf formulas provides a practical and scalable alternative to automata-based temporal-knowledge integration, supporting future systematic assessment of temporal NeSy systems.The paper also introduces an evaluation protocol and identifies richer temporal logics, larger benchmarks, and more realistic benchmarks as future directions.

Appendix A. Implementation Details of Baselines

Appendix A details the implementations of the FuzzyA and NeSyA baselines, selected to support fair comparison of computational efficiency and theoretical adherence.

  • Implementation Details of Baselines: The appendix describes implementation details for the FuzzyA and NeSyA baseline methods used in the comparative analysis.These implementations were adopted to support a fair comparison in computational efficiency and adherence to each method’s theoretical foundations.

Appendix A.1. FuzzyA

The FuzzyA baseline uses the LTLZinc implementation, with batched sequence evaluation and two modifications to the original implementation: timestep-wise state renormalization and a binary cross-entropy objective.

  • Implementation: FuzzyA uses the LTLZinc implementation with batched sequence evaluation, softmax renormalization of automaton state distributions at each timestep, and a binary cross-entropy objective.The loss compares the sum of fuzzy values assigned to accepting states with the sequence label.

Appendix A.2. NeSyA

The NeSyA baseline uses the architecture from the original work rather than the LTLZinc implementation, compiling only transition guards into d-DNNF circuits. State probabilities are then updated by multiplying the previous state distribution with the transition matrix.

  • Implementation: The NeSyA baseline implements the architecture described in the original NeSyA work instead of using the LTLZinc implementation.The LTLZinc version was avoided because it combines state variables and transition guards into one logical circuit, which can be inefficient for large automata.
  • Implementation: Only transition guards are compiled into d-DNNF circuits to enable exact probabilistic reasoning.
  • State update: The probability over states is updated through matrix multiplication between the previous state distribution and the transition matrix.

Appendix B. Experimental Setup Details

The appendix specifies a shared perception architecture, standardized optimization settings, and procedurally generated sequence datasets for all experiments. Training duration varies by experimental setting, while evaluation uses held-out data and fixed hardware/software.

  • Training configuration: Models are trained with Adam, a learning rate of 10−4, batch size 64, and binary cross-entropy against sequence labels y ∈{0, 1}.Formula-complexity experiments run for 50 epochs, whereas sequence-length experiments run for 30 epochs.
  • Dataset construction: Each experimental configuration generates 1000 sequences by independently sampling class labels across S = 3 streams and retrieving corresponding MNIST or Fashion-MNIST images.Ground-truth labels are computed by evaluating the LTLf specification on the resulting symbolic trace.
  • Dataset construction: Datasets are partitioned into 80% training and 20% held-out test data, with the test set never observed during training.The split is applied to each generated experimental dataset.
  • Hardware and software: Experiments run on a single NVIDIA RTX A6000 GPU with 48 GB memory, using PyTorch 2.3.1 and CUDA 12.1.The hardware and software configuration is fixed across the reported experiments.

Appendix C. Complete Experimental Results

Appendix C reports complete experimental results across all evaluated temporal neurosymbolic methods and neural baselines. It covers formula-complexity and sequence-length experiments, with accuracy and logic-module runtime metrics averaged over repeated runs.

  • Methods: The appendix evaluates three ∂LTLf semantics—Product, Gödel, and Łukasiewicz—alongside T-ILR, two FuzzyA variants, NeSyA, GRU, and Transformer.The FuzzyA variants are the LTLZinc version used throughout the paper and the original implementation.
  • Formula complexity: Tables C.5 and C.6 report full results for varying formula complexity on MNIST and Fashion-MNIST, respectively, averaged over 10 runs.Both tables report image accuracy, sequence accuracy, and logic-module time per epoch.
  • Sequence length: Tables C.7 and C.8 report full results for varying sequence length with |C| = 4 and |C| = 8, respectively, averaged over 10 runs.The reported metrics are image accuracy, sequence accuracy, and logic-module time per epoch.
  • Statistical analysis: Bold values denote results statistically significantly better than all other methods under a Wilcoxon test with p < 0.05.This significance convention is specified for the complete-results tables.
Loading 2608.16443v1…