# Teaching Temporal Logics to Neural Networks

arXiv: https://arxiv.org/abs/2003.04218 · HTML: https://mlsanity.com/paper/2003.04218/

## Key facts

- Cited by 51 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 6 Mar 2020.

## Built on by (most cited first, 30 of 51)

- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [FOLIO: Natural Language Reasoning with First-Order Logic](https://mlsanity.com/paper/2209.00840/) (2022)
- [Memorizing Transformers](https://mlsanity.com/paper/2203.08913/) (2022)
- [End-to-end symbolic regression with transformers](https://mlsanity.com/paper/2204.10532/) (2022)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [On the Paradox of Learning to Reason from Data](https://mlsanity.com/paper/2205.11502/) (2022)
- [From Statistical Relational to Neurosymbolic Artificial Intelligence: a Survey](https://mlsanity.com/paper/2108.11451/) (2021)
- [A Comprehensive Survey on Applications of Transformers for Deep Learning Tasks](https://mlsanity.com/paper/2306.07303/) (2023)
- [LogicBench: Towards Systematic Evaluation of Logical Reasoning Ability of Large Language Models](https://mlsanity.com/paper/2404.15522/) (2024)
- [Length Generalization in Arithmetic Transformers](https://mlsanity.com/paper/2306.15400/) (2023)
- [Linear algebra with transformers](https://mlsanity.com/paper/2112.01898/) (2021)
- [ODEFormer: Symbolic Regression of Dynamical Systems with Transformers](https://mlsanity.com/paper/2310.05573/) (2023)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [Towards LogiGLUE: A Brief Survey and A Benchmark for Analyzing Logical Reasoning Capabilities of Language Models](https://mlsanity.com/paper/2310.00836/) (2023)
- [Formal Specifications from Natural Language](https://mlsanity.com/paper/2206.01962/) (2022)
- [DecoderLens: Layerwise Interpretation of Encoder-Decoder Transformers](https://mlsanity.com/paper/2310.03686/) (2023)
- [Neural Circuit Synthesis from Specification Patterns](https://mlsanity.com/paper/2107.11864/) (2021)
- [Teaching Autoregressive Language Models Complex Tasks By Demonstration](https://mlsanity.com/paper/2109.02102/) (2021)
- [Iterative Circuit Repair Against Formal Specifications](https://mlsanity.com/paper/2303.01158/) (2023)
- [Generating Symbolic Reasoning Problems with Transformer GANs](https://mlsanity.com/paper/2110.10054/) (2021)
- [Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis](https://mlsanity.com/paper/2205.14229/) (2022)
- [Al-Khwarizmi: Discovering Physical Laws with Foundation Models](https://mlsanity.com/paper/2502.01702/) (2025)
- [Guiding Multi-agent Multi-task Reinforcement Learning by a Hierarchical Framework with Logical Reward Shaping](https://mlsanity.com/paper/2411.01184/) (2024)
- [Lean-ing on Quality: How High-Quality Data Beats Diverse Multilingual Data in AutoFormalization](https://mlsanity.com/paper/2502.15795/) (2025)
- [NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis](https://mlsanity.com/paper/2401.12131/) (2024)
- [OLViT: Multi-Modal State Tracking via Attention-Based Embeddings for Video-Grounded Dialog](https://mlsanity.com/paper/2402.13146/) (2024)
- [Logical forms complement probability in understanding language model (and human) performance](https://mlsanity.com/paper/2502.09589/) (2025)
- [Learning Temporal Rules from Noisy Timeseries Data](https://mlsanity.com/paper/2202.05403/) (2022)
- [OCTAL: Graph Representation Learning for LTL Model Checking](https://mlsanity.com/paper/2207.11649/) (2022)
- [Using Language Models For Knowledge Acquisition in Natural Language Reasoning Problems](https://mlsanity.com/paper/2304.01771/) (2023)

## Abstract (arXiv)

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.