PaperlayerView exact revision on arXiv

Source-linked AI summary

Teaching Temporal Logics to Neural Networks

Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus N. Rabe, Bernd Finkbeiner

arXiv:2003.04218v3cs.LOcs.AIcs.LGstat.ML

TL;DR

The paper asks whether neural networks can solve challenging logical problems directly and learn logic semantics despite training on one solver-selected solution per formula. It trains Transformers to predict LTL traces and finds high semantic accuracy, including on formulas where the classical solver times out, while exposing limits on highly overlapping temporal constraints.

  • Problem

    Deep learning has been considered insufficient for complex symbolic reasoning, motivating the question of whether Transformers can directly solve challenging verification logics.

    Source: §1 · p. 1

  • Method

    The paper trains a Transformer on classical-solver-generated satisfying traces for LTL formulas and evaluates generalization on other LTL and propositional datasets.

    Source: §1 · p. 2, §3.2 · p. 6

  • Results

    Transformers predict correct solutions for 96.8% of held-out LTL formulas and 83% of formulas on which spot timed out, while often producing semantically correct traces different from the generator’s.

    Source: §1 · p. 2, §5.1 · p. 7

  • Takeaways & Limitations

    The results suggest that direct neural prediction can augment classical algorithms for trace generation and verification-oriented logical reasoning.

    Source: §6 · p. 9

    All models fail on formulas scaled to four overlapping Until intervals, a challenging source of LTL’s PSPACE-hardness.

    Source: §5.2 · p. 8

Abstract

from arXiv · show

We study two fundamental questions in neuro-symbolic computing: can deep learning tackle challenging problems in logics end-to-end, and can neural networks learn the semantics of logics. In this work we focus on linear-time temporal logic (LTL), as it is widely used in verification. We train a Transformer on the problem to directly predict a solution, i.e. a trace, to a given LTL formula. The training data is generated with classical solvers, which, however, only provide one of many possible solutions to each formula. We demonstrate that it is sufficient to train on those particular solutions to formulas, and that Transformers can predict solutions even to formulas from benchmarks from the literature on which the classical solver timed out. Transformers also generalize to the semantics of the logics: while they often deviate from the solutions found by the classical solvers, they still predict correct solutions to most formulas.

1 INTRODUCTION

The paper asks whether Transformers can directly solve challenging logical problems in verification and learn logic semantics from solver-generated solutions. On LTL, the models achieve high semantic accuracy, generalize beyond training formulas, and can complement classical methods.

1 INTRODUCTION

  • The study targets direct end-to-end solution prediction for LTL formulas, a verification logic describing infinite system-behavior sequences.The approach trains on traces generated by classical algorithms, which provide one solution among potentially many.Source: §1 · pp. 1–2
  • Transformers predict correct LTL solutions for 96.8% of held-out formulas and 83% of formulas on which spot timed out.The latter benchmark required predictions where the classical generator produced no output within its timeout.Source: §1 · p. 2
  • The results suggest that direct machine learning may augment classical algorithms in logical reasoning tasks.The paper positions neural predictions as a complement to established verification procedures rather than a universal replacement.Source: §1 · p. 2
  • Tree-positional encodings generalize to much longer formulas, whereas standard positional encodings do not.The models also often produce semantically correct traces different from those selected by the classical generator, especially out of distribution.Source: §1 · p. 2
  • Experiments on random LTL and propositional formulas test whether the observed generalization depends on the benchmark or on spot as the data generator.The propositional experiments generate solutions with SAT solvers rather than spot.Source: §1 · p. 2

2 RELATED WORK

Related work applies learning to theorem proving, symbolic mathematics, and logical reasoning, but this paper targets direct trace prediction for verification formulas. Its sequence-to-sequence approach differs from graph-based SAT systems by predicting solutions rather than only satisfiability.

2 RELATED WORK

  • Prior work uses learned systems for premise or clause ranking, proof-step prediction, theorem proving, symbolic mathematics, and mathematical reasoning.The cited literature spans automated and interactive theorem provers, symbolic mathematics, and natural-language mathematics.Source: §2 · p. 3
  • Neural logical-reasoning architectures include graph neural networks for theorem proving, SAT solving, unsat-core prediction, and solver heuristics.Other work studies logical entailment with tree-RNNs.Source: §2 · p. 3
  • This paper applies a generic sequence-to-sequence Transformer to predict formula solutions, not merely whether a solution exists.That formulation supports a wider set of logics, including logics without conjunctive normal form.Source: §2 · p. 3
  • Transformers have also been used for code summarization, variable naming, misuse detection, and related program-analysis tasks.The paper distinguishes these program applications from its verification-focused logical reasoning problem.Source: §2 · p. 3

3 DATA SETS

The datasets pair logical formulas with satisfying traces or assignments generated by classical tools, covering practical and random LTL as well as propositional formulas. They include larger and harder distributions designed to test semantic and size generalization.

3.1 TRACE GENERATION FOR LINEAR-TIME TEMPORAL LOGIC

  • LTL traces represent infinite sequences as finitely encoded ultimately periodic lassos, allowing symbolic underspecification of irrelevant propositions.The data uses compact syntax with delimiters marking positions and the repeated period.Source: §3.1 · p. 4
  • For each satisfiable LTL formula, spot constructs a Büchi automaton and extracts an arbitrary accepted symbolic trace.The accepted language of the automaton matches the language defined by the formula.Source: §3.1 · p. 4

3.1.1 SPECIFICATION PATTERN

  • The main LTLPattern126 dataset combines 55 literature-based specification patterns, stopping at size 126, more than eight patterns, generator timeout, or unsatisfiability.It contains 1,664,487 formula-trace pairs split into 80% training, 10% validation, and 10% test data.Source: §3.1.1 · p. 4
  • LTLUnsolved254 contains pattern formulas up to twice the training length whose spot trace search timed out after 60 seconds.Its maximum formula length is 254, compared with 126 for the main training distribution.Source: §3.1.1 · p. 4

3.1.2 RANDOM FORMULAS

  • LTLRandom35 contains one million random LTL formulas with satisfying symbolic traces, using five propositions and 800K/100K/100K train-validation-test splits.Examples with traces longer than 62 were filtered out.Source: §3.1.2 · p. 5

3.2 ASSIGNMENT GENERATION FOR PROPOSITIONAL LOGIC

  • The propositional dataset defines satisfiability through Boolean assignments, permits partial assignments, and represents them as proposition-value sequences.The generation includes arbitrary formula structures and derived operators rather than restricting formulas to CNF.Source: §3.2 · p. 5
  • PropCNF250 uses an established random-CNF generator to create formulas with up to 15 variables and maximum size 250.Clauses are added until another clause would make the formula unsatisfiable.Source: §3.2 · p. 6

4 EXPERIMENTAL SETUP

The experiments use a standard token-level Transformer with beam-search decoding and evaluate both agreement with generator outputs and semantic correctness. Training uses early stopping, dropout, and task-specific batch sizes and schedules.

4 EXPERIMENTAL SETUP

  • The Transformer processes input and output sequences token by token and decodes with beam search using beam size 3 and α=1.Training used one NVIDIA P100 or V100 GPU, dropout 0.1, and early stopping on validation performance.Source: §4 · p. 6
  • Syntactic accuracy measures exact agreement with the generator, while semantic accuracy counts different predictions that still solve the formula.Incorrect predictions and syntactically invalid outputs are tracked separately.Source: §4 · p. 6
  • The best models generally use 8 layers, 8 attention heads, and feed-forward size 1024.Specification-pattern training runs for 450K steps, while random-formula training runs for 50K steps.Source: §4 · p. 6

5 EXPERIMENTAL RESULTS

The experiments show that Transformers can generate semantically correct solutions for LTL and propositional formulas, including cases beyond classical-solver training outputs and timeout instances. Tree positional encodings support generalization to larger formulas, while difficult overlapping-until formulas remain a boundary.

5.1 SOLVING LINEAR-TIME TEMPORAL LOGICAL FORMULAS

  • 96.8% semantic accuracy on LTLPattern126 exceeded 69.1% syntactic accuracy, and semantic accuracy declined less with formula length.This gap indicates that the Transformer often found valid traces different from the generator’s particular output.Source: §5.1 · p. 7
  • 83% of LTLUnsolved254 formulas received correct solutions despite spot timing out, although this does not establish superiority over classical algorithms.The model took 15s per formula on average, and syntactic accuracy was 0% because spot produced no output within the timeout.Source: §5.1 · p. 7, Figure 3 · p. 7

5.2 GENERALIZATION PROPERTIES

  • On LTLRandom35, the model achieved 98.5% semantic and 83.8% syntactic accuracy, showing semantic generalization beyond exact generator imitation.The model was trained only on formulas of size at most 35, and semantic accuracy remained high as formulas grew.Source: §5.2 · p. 7
  • Tree positional encoding preserved semantic generalization from LTLRandom35 to unseen LTLRandom50 formulas, reaching 92.2% semantic and 67.6% syntactic accuracy.With standard positional encoding, accuracy dropped significantly on larger formulas.Source: §5.2 · pp. 7–8, Figure 4 · p. 9
  • Models trained on LTLRandom126 and tested on LTLPattern126 achieved 24.7% semantic and 1.0% syntactic accuracy, while the reverse direction achieved 38.5% semantic accuracy and a reported 0.5% semantic accuracy.OOD testing dramatically increased the gap between syntactic and semantic correctness, despite very different distributions, supporting that models learned LTL semantics rather than the generator process.Source: §5.2 · p. 8
  • Formulas with four overlapping until intervals defeated all models, identifying overlapping temporal constraints as a concrete difficulty.A model trained on LTLRandom35 produced a trace that did not satisfy the scaled formula.Source: §5.2 · p. 8

5.3 PREDICTING ASSIGNMENTS FOR PROPOSITIONAL LOGIC

  • In propositional logic, correct assignments differed from DPLL-generated assignments by 38.4%, while only 3.5% of predictions were incorrect.This demonstrates that semantic correctness can substantially exceed exact agreement with a single solver output.Source: §5.3 · p. 8
  • For propositional formulas of sizes 35–50, tree positional encoding achieved 86.1% semantic accuracy versus 75.7% without it.Syntactic accuracy was 35.8% with tree encoding and 29.0% without; the encodings performed equally on non-enlarged formulas.Source: §5.3 · p. 9

6 CONCLUSION

The paper concludes that Transformers can learn LTL semantics and generalize to larger formulas, including cases where classical trace generation timed out. These results suggest neural models may augment classical verification algorithms.

6 CONCLUSION

  • Transformers predict correct traces for 83% of practical-pattern formulas on which the data generator timed out, despite training on much smaller formulas.The paper reports that the models can compete with classical algorithms for generating LTL solutions.Source: §6 · p. 9
  • The trained models generalize both to LTL semantics and to formulas larger than those seen during training.These generalization behaviors did not depend on the underlying logical problem or data generator.Source: §6 · p. 9
  • The conclusion proposes querying Transformers for trace predictions and checking them efficiently, while retaining classical methods as fallbacks or partial-solution checks.This is presented as a possible way to develop new trace-generation or satisfiability-checking algorithms.Source: §6 · p. 9

A LINEAR-TIME TEMPORAL LOGIC (LTL)

  • The formal appendix defines LTL formulas over atomic propositions and infinite traces, with temporal operators interpreted over trace suffixes.Derived operators include eventuality, globally, and infinitely often.Source: A LINEAR-TIME TEMPORAL LOGIC (LTL) · p. 15

B SIZE DISTRIBUTION IN THE DATA SETS

The datasets cover formula and trace sizes across benchmark-pattern, random, and solver-unsolved collections. Their distributions are documented with size histograms and example instances.

B SIZE DISTRIBUTION IN THE DATA SETS

C HYPERPARAMETER ANALYSIS

The hyperparameter analysis finds that model depth is the strongest reported performance factor, while heads and feed-forward width have smaller or conditional effects.

C HYPERPARAMETER ANALYSIS

  • Eight encoder-decoder layers yield the best reported performance, whereas adding more layers does not improve and can worsen results.The analysis identifies layer count as the most beneficial parameter among those tested.Source: C HYPERPARAMETER ANALYSIS · p. 16, Table 2 · p. 17
  • Increasing feed-forward width or changing attention-head count alone provides little benefit, while increasing both together gives a small gain.A suitable feed-forward size remains important even though increasing it alone does not improve results.Source: C HYPERPARAMETER ANALYSIS · p. 16
  • Increasing embedding size from 128 to 256 slightly improves syntactic accuracy but degrades semantic accuracy, so the smaller setting is retained.The trade-off motivates keeping the 128-dimensional embedding setting.Source: C HYPERPARAMETER ANALYSIS · p. 17

D ACCURACY DURING TRAINING

Training curves show a persistent gap between syntactic and semantic accuracy from early training onward. The figure tracks both measures on LTLRandom35 samples per epoch.

D ACCURACY DURING TRAINING

  • Syntactic and semantic accuracy differ significantly from the beginning of training, underscoring the need for suitable evaluation measures.Figure 8 evaluates the best model on a 5K-sample LTLRandom35 subset per epoch.Source: D ACCURACY DURING TRAINING · p. 17, Figure 8 · p. 17

E DIFFERENT POSITIONAL ENCODINGS

The best model trained on LTLRandom35 is evaluated on larger LTLRandom50 formulas using standard and tree positional encodings.

E DIFFERENT POSITIONAL ENCODINGS

  • Performance on LTLRandom50 is shown for standard and tree positional encodings, with syntactic accuracy, semantic accuracy, and incorrect predictions distinguished by color.The shaded area marks formula sizes absent from training.Source: Figure 9 · p. 18

F HANDCRAFTED EXAMPLES

The handcrafted example compares attention patterns for propositional and LTL formulas and illustrates that the Transformer can produce a different, more general satisfying trace than the automaton-based generator.

F HANDCRAFTED EXAMPLES

  • Figure 10 visualizes self-attention for a propositional formula and encoder-decoder attention for an LTL formula.Source: Figure 10 · p. 18
  • The Transformer predicts a (¬a) (true)ω trace for (b U a) ∧(a U ¬a), satisfying the until operators in order, whereas the generator proposes (¬a ∧ b) a (true)ω.Both traces satisfy the formula, but the Transformer’s trace is described as more general.Source: F HANDCRAFTED EXAMPLES · p. 18
Loading 2003.04218v3…