Teaching Temporal Logics to Neural Networks

By Bernd Finkbeiner, Christopher Hahn, Markus Norman Rabe, Frederik Schmitt. 2020

79 citations recorded by the source corpus.

We show that a deep neural network can learn the semantics of linear-time temporal logic (LTL). As a challenging task that requires deep understanding of the LTL semantics, we show that our network can solve the trace generation problem for LTL: given a satisfiable LTL formula, find a trace that satisfies the formula. We frame the trace generation problem for LTL as a translation task, i.e., to translate from formulas to satisfying traces, and train an off-the-shelf implementation of the Transformer, a recently introduced deep learning architecture proposed for solving natural language processing tasks. We provide a detailed analysis of our experimental results, comparing multiple hyperparameter settings and formula representations. After training for several hours on a single GPU the results were surprising: the Transformer returns the syntactically equivalent trace in 89% of the cases on a held-out test set. Most of the "mispredictions", however, (and overall more than 99% of the predicted traces) still satisfy the given LTL formula. In other words, the Transformer generalized from imperfect training data to the semantics of LTL.

Subfields: Artificial Intelligence, Model Architectures, Program Analysis & Verification

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Model Architectures

In Program Analysis & Verification

Citations in the corpus

Autoformalization with Large Language Models (2022, background): “Hahn et al. [18], Schmitt et al. [41], Kreber & Hahn [29] and Wu et al. [52] have shown that training on synthetic formulas can be successful for temporal logics and inequalities.”
Mathematical Reasoning via Self-supervised Skip-tree Training (2020, methodology): “Finkbeiner et al. [2020] explore the generalization properties of the Transformer architecture predicting the solutions to SAT formulas and temporal logic, but require a data generator that can solve formulas, which”
Memorizing Transformers (2022, unknown): “…in natural language processing (Devlin et al., 2019; Brown et al., 2020), mathematical reasoning (Polu & Sutskever, 2020; Wang et al., 2020a; Rabe et al., 2021; Li et al., 2021; Hahn et al., 2021; Cobbe et al., 2021), and program synthesis (Austin et al., 2021; Chen et al., 2021; Li et al., 2022).”
Language Modeling for Formal Mathematics (2020, background): “Finkbeiner et al. [2020] explore the generalization properties of Transformers predicting the solutions to formulas in linear-time temporal logic.”
On the Paradox of Learning to Reason from Data (2022, methodology): “For examples, SAT (Selsam et al., 2019), maxSAT (Wang et al., 2019), temporal logical problems (Hahn et al., 2021), DNF counting (Crouse et al., 2019), logical reasoning by learning the embedding of logical formula (Crouse et al., 2019; Abdelaziz et al., 2020) and mathematical problems (Saxton et…”
Conversational Neuro-Symbolic Commonsense Reasoning (2020, background): “Very recently, transformers were used for temporal logic [46] and to do multi-hop reasoning [47] using logical facts and rules stated in natural language.”
A Comprehensive Survey on Applications of Transformers for Deep Learning Tasks (2023, background): “, 2021) (Hahn et al., 2021) Sequence Generation 2021 Transformer (Encoder / Decoder) No NA Synthetic”
End-to-end symbolic regression with transformers (2022, unknown): “Language models, and especially Transformers [23], have been trained over synthetic datasets to solve various mathematical problems: integration [24], dynamical systems [25], linear algebra [26], formal logic [27] and theorem proving [28].”
Proof Artifact Co-training for Theorem Proving with Language Models (2021, background): “, 2021), Boolean satisfiability (Hahn et al., 2021), and inferring missing proof steps (Li et al.”