Source-linked AI summary
Backward through Time, Algebraically
Konstantinos Kogkalidis
TL;DR
Differentiable temporal-logic semantics can provide training signals for softly valued systems, but existing implementations require choosing one implicit semantic algebra. The paper develops an algebra-generic, differentiable evaluation engine and audits its algebras, finding distinct backward-pass failure modes and an algebra with duration-invariant verdicts and live credit.
Problem
Differentiable feedback from temporal-logic evaluation can be weak or empty, motivating careful analysis of how semantic algebras distribute gradient credit.
Method
The paper defines an algebra-generic evaluator from abstract carriers and connective operations, reduces temporal operators to tensor-axis iterations, and makes the specification executable.
Results
Audits identify selection, saturation, and decay as backward-pass failure modes, while lifted semantics provide dense gradients that dilute as 1/T rather than vanish exponentially.
Takeaways & Limitations
The audited catalogue includes an algebra delivering duration-invariant verdicts and live credit, while preserving the evaluator’s algebraic generality.
Takeaways & Limitations
The faster evaluator relies on associativity for regrouped folds, so the fold remains the specification and fallback for algebras lacking optimized implementations.
Abstract
from arXiv · showhide
Linear temporal logic is a modal extension of propositional logic that allows one to state how a system should behave over time. Its canonical domain is the booleans, but discretely-valued judgements are of little use in steering softly-valued systems (neural policies, adaptive controllers, sequence models, etc). In such cases, the goal formula's (dis)satisfaction becomes a training signal, and differentiability becomes a prime concern. Candidate differentiable semantics abound, but navigating them is tricky. Implementations, where available, are shallow embeddings, demanding an upfront commitment to a single semantic algebra and its (usually implicit) conduct. The paper casts the reader as a functional programmer asked to come to terms with this predicament, and refusing. Out of that refusal comes an evaluation engine that is algebra-generic and amenable to differentiation, together with an executable specification of the algebras it can accept. Various algebras are implemented and audited for their behavior, both forward and backward. Each algebra turns out to be a choice of which direction to disappoint, and how. Everything described (and more) is part of the PyTorch library telos, to be found at https://github.com/konstantinosKokos/telos.
1 Syntax
This section introduces linear temporal logic syntax through the operators X and U, alongside F and G, and frames evaluation as a judgement over a finite trace. It then exposes why boolean rounding fails when traces are differentiable PyTorch tensors from neural networks.
- Temporal operators: LTL combines familiar propositional connectives with temporal operators whose denotations are evaluated over time.The section presents the syntax as an established logical framework extended with “funny symbols.”
- Temporal operators: Xϕ advances ϕ by one tick, whereas ϕUψ requires ψ eventually and ϕ to remain true until its arrival.The section characterizes X as a step and U as a search carrying two simultaneous promises.
- Trace semantics: A formula is evaluated against a finite trace τ assigning each atom α a value at every tick t across T ticks.Together, the formula and trace form the judgement τ |= ϕ.
- Differentiable evaluation: Rounding neural-network traces above one half to booleans destroys gradient information because the step derivative is zero or infinite.The input is a float32 PyTorch Tensor with requires_grad=True, so downstream loss cannot pass feedback through the verdict.
2 Semantics, Abstract
The paper abstracts differentiable temporal semantics around an algebraic carrier with top and bottom elements and pointwise logical operations. Temporal operators are reduced to tensor-axis iteration, while derived operations serve as an executable specification built from four primitives.
- Algebra abstraction: Each accepted algebra consists of a carrier with distinguished top and bottom elements plus pointwise operations for logical connectives.The abstract interface exposes meet, join, implication, and negation over tensors.
- Temporal operations: Time enters as the last tensor axis, so temporal operators reduce to sweeping operations along that axis.The paper characterizes temporal quantification as first-order iteration and implements it through scans, folds, and spans.
- Derived operations: The algebra recipe derives running, quantified, and span operations from the four abstract primitives.Examples include running_meet, running_join, forall, exists, and span_meet.
- Executable specification: Derived-operation definitions are both reusable implementations and an executable specification of the accepted algebras.They are written once in terms of the abstract primitives and can therefore be run directly.
3 Interface
The interface evaluates temporal formulas by structural recursion, delegating each case to an algebra. Derived temporal operators reduce to reversed-time running reductions, while general Until searches windows for the best witness outcome.
- Structural evaluation: Evaluation recursively traverses the formula structure, with each case deferring its operation to the supplied algebra.The model interface accepts an Algebra and Judgement and returns a value of type T.
- Structural evaluation: Negation, conjunction, and Next invoke algebra negation, meet, and end-padding with the algebra’s bottom value.Next shifts values left and pads the unoccupied final tick with A.bot.
- Temporal operators: Globally and finally are desugared into reversed-time running meet and join reductions, making them compute-friendly suffix searches.The two aliases of Until become primitives differing only in the running reduction used.
- Temporal operators: General Until meets each candidate window of 𝜙 with its witness 𝜓, then existentially selects the best outcome for each starting time.A span meet aggregates 𝜙 across each segment, while the witness is broadcast across windows before the exists reduction.
4 Semantics, Concrete
Concrete instantiations recover Boolean semantics exactly while supporting differentiable fuzzy and signal-temporal algebras. Mechanical audits expose which lattice laws each algebra preserves or sacrifices, with differentiability gained beyond Boolean boundaries.
- Boolean semantics: Boolean semantics are recovered as a special case using tensor-valued truth, falsity, conjunction, disjunction, implication, and negation.Instantiation and evaluation return the promised answers, establishing correctness of the algebra-generic blueprint.
- Fuzzy algebras: The Product algebra interprets conjunction as multiplication, disjunction as probabilistic sum, implication by a clamped ratio, and negation as one minus the input.Its evaluator returns numerical judgements that behave like probabilities.
- Auditing: Product fails idempotence, absorption, distributivity, and complementation away from the domain’s edges, while always depends on formula duration through JG𝜙K = 𝑥^T.For complementation, x ∗ (1 − x) remains above the bottom value.
- Auditing: Audits test algebraic laws mechanically by searching for counterexamples across every law and algebra over batches of initially random tensors.Finite-precision arithmetic motivates lax equality rather than strict equality.
- Algebra landscape: Boolean is the only proper lattice, while descendant algebras trade lawfulness for differentiability; on {0, 1}-valued traces, all algebras agree with Boolean semantics.Robustness and LSE instead use the extended real line with arithmetic negation, and generalized families introduce a parameter p.
5 Semantics, Faster
The evaluator’s time cost comes from serial depth iteration rather than rereading ticks, while algebraic laws expose faster running operations. Idempotence, De Morgan duality, generator coordinates, and associativity replace generic folds with specialized scans, leaving the fold as specification and fallback.
- Bottleneck: Serial depth iteration makes evaluation slow despite reading each of the T ticks exactly once.The evaluator otherwise incurs quadratic memory spans and linear-depth folds and scans.
- Specialized scans: Idempotence lets Goedel replace its running meet and join with torch.cummin and torch.cummax.The override is retained as an auditable law because the displaced fold remains executable for counterexample checking.
- Specialized scans: Product and LSE likewise use cumulative kernels, while De Morgan duality derives Product’s running join from a negated running meet.Product uses cumulative product; LSE uses logcumsumexp for its running join.
- Generator coordinates: Archimedean meets become running sums in generator coordinates, allowing torch.cumsum to derive meets, implications, and universal aggregation.Each meet has the form g^-1(g(x) + g(y)), with pseudo-inverse clamping where the family saturates at 0.
- Window evaluation: Associativity reduces the general ·U· window construction from separately computed cubic work to one triangular running sweep across each row.Windows sharing a start differ only in their end, so each becomes a prefix of the next.
- Fallback: The fold remains only as a specification and fallback for future algebras, rather than as an implementation used by the current catalogue.The passage frames this status as the result of taming evaluation time.
6 Semantics, Backward?
Backward evaluation remains differentiable but produces sparse, erased, or vanishing feedback. These failures combine the weaknesses of standard fuzzy operators with the vanishing gradients of naively unrolled contracting operators.
- Failure modes: Backward feedback exhibits three forms of emptiness: selection, saturation, and decay.Gödel and Robustness select one atom-time entry; Łukasiewicz clamping erases gradients on sufficiently long traces; the passage introduces decay without elaborating it.
- Selection: Gödel and Robustness derivatives are indicator functions, assigning all credit to one tick of one atom and exact zero to every other entry.This concentration is independent of trace length or formula complexity.
- Saturation: Łukasiewicz’s repeated clamping causes outputs to plateau and gradients to disappear on traces of serious length.The saturation problem arises from the operator’s repeated clamping behavior.
- Compounding problems: Two problems compound: standard fuzzy operators are poor neural-network components, while naively unrolled contracting operators yield parameterless recurrent networks with vanishing gradients.The paper attributes both problems to treating time as quantification in disguise.
7 Semantics, Lifted
The section extends temporal semantics beyond binary-fold algebras by prescribing softmax credit and duration-invariant verdicts, then introduces lifted monoidal states to support variadic reductions. A Boltzmann algebra instantiates this design with dense gradients, though its laws remain to be audited.
- Motivation: LSE’s backward pass yields dense credit: softmax weights sum to one and none is zero.LSE remains classified as strict after transport across its algebra isomorphism with Product.
- Motivation: The desired semantics prescribe softmax credit assignment and normalize verdicts like a mean, making them independent of duration.These requirements exceed the existing specification because averaging is irreducibly variadic and an average of averages need not equal the overall average.
- Lifted abstraction: Lifted semantics represent reductions with monoidal states requiring associativity for speed and an identity for padding, while keeping tensor-valued algebras at the interface.States summarize intervals, combine adjacent intervals without revisiting ticks, and support prefix and span computations.
- Boltzmann algebra: The Boltzmann algebra carries a weighted mean through a numerator, denominator, and running maximum, and runs at catalogue speed with dense credit by construction.Its implementation embeds values using a scaled negation, combines states with numerically stabilized exponentials, and reads out the weighted ratio.
- Lifted abstraction: Each running reduction factors as readout ◦ sweep ◦ embed, with meet and join sharing a monoid and differing only through their crossing operations.The abstraction assumes involutive negation to derive join and related operations from meet.
8 Semantics, Backward!
The initial backward semantics is differentiable, dense, smooth, and normalized but violates monotonicity because value-dependent weights can make raising a low judgement lower the verdict. A repaired mean-based construction restores duration invariance and key logical properties, while retaining specified failures such as associativity and lattice laws.
- Failure: The backward feedback is dense, smooth, and normalized, but monotonicity fails: raising a faint tick can lower the verdict.The weights depend on the judged values, so promoting a low-valued straggler also increases its weight and pulls the average downward.
- Repair: The repair keeps the survivor’s aggregation and changes its sum into a mean, moving the softmax from the verdict to the feedback.The demands specify where the softmax must appear, while the survivor already places the shares in the backward pass.
- Repaired behavior: The repaired backward pass yields dense, smooth, normalized, non-negative feedback matching LSE’s softmax, while the mean makes the verdict duration-invariant and idempotent.For a pinned judgement at x, the semantics reads x at any duration T.
- Audit: The audit passes monotonicity, involution, De Morgan duality, and the section law, but fails associativity, the residuum, absorption, distributivity, complementation, and non-material implication.The construction emulates the unit in State-space despite not being unital in the carrier.
9 Semantics, in Hindsight
The section concludes that each semantic concession is a structural trespass exchanged for behavior in the feedback world, while the evaluator remains correct for every formula under every algebra. The result is a qualified collection of algebras that users can choose according to their well-behavedness.
- 9 Semantics, in Hindsight: Each concession is understood as a structural trespass: a property is broken in the verdict world to gain a behavior in the feedback world.The section frames the concessions as deliberate tradeoffs between structural properties and feedback behavior.
- 9 Semantics, in Hindsight: The evaluator keeps its promise throughout, handling every formula under every algebra without perceiving the resulting disruption.The evaluator’s stated guarantee is algebra- and formula-independent.
- 9 Semantics, in Hindsight: The outcome is a collection of algebras users can choose among, with each option properly qualified by its degree of well-behavedness.The section presents algebra selection as a user-facing choice rather than a single imposed semantics.