Teaching Temporal Logics to Neural Networks
arXiv:2003.04218
Abstract
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.
References in corpus (17)
- Efficient Estimation of Word Representations in Vector Space
- Google's Neural Machine Translation System: Bridging the Gap between Human and Machine Translation
- Neural Message Passing for Quantum Chemistry
- Language Models are Few-Shot Learners
- DeepStack: Expert-Level Artificial Intelligence in No-Limit Poker
- Diffusion Convolutional Recurrent Neural Network: Data-Driven Traffic Forecasting
- Layer Normalization
- Structured Neural Summarization
- Learning-Assisted Automated Reasoning with Flyspeck
- Learning Program Embeddings to Propagate Feedback on Student Code
- Towards Verified Artificial Intelligence
- GamePad: A Learning Environment for Theorem Proving
- Generative Language Modeling for Automated Theorem Proving
- Enhancing the Transformer with Explicit Relational Encoding for Math Problem Solving
- HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
- Mathematical Reasoning via Self-supervised Skip-tree Training
- Can Neural Networks Understand Logical Entailment?