Learning to Estimate System Specifications in Linear Temporal Logic using Transformers and Mamba

• URL: http://arxiv.org/abs/2405.20917v1
• Date: Fri, 31 May 2024 15:21:53 GMT
• Title: Learning to Estimate System Specifications in Linear Temporal Logic using Transformers and Mamba
• Authors: İlker Işık, Ebru Aydin Gol, Ramazan Gokberk Cinbis,
• Abstract summary: specification mining involves extracting temporal logic formulae from system traces. We introduce autore models that can generate linear temporal logic formulae from traces. We devise a metric for the distinctiveness of the generated formulae and an algorithm to enforce the syntax constraints.
• Score: 6.991281327290525
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Temporal logic is a framework for representing and reasoning about propositions that evolve over time. It is commonly used for specifying requirements in various domains, including hardware and software systems, as well as robotics. Specification mining or formula generation involves extracting temporal logic formulae from system traces and has numerous applications, such as detecting bugs and improving interpretability. Although there has been a surge of deep learning-based methods for temporal logic satisfiability checking in recent years, the specification mining literature has been lagging behind in adopting deep learning methods despite their many advantages, such as scalability. In this paper, we introduce autoregressive models that can generate linear temporal logic formulae from traces, towards addressing the specification mining problem. We propose multiple architectures for this task: transformer encoder-decoder, decoder-only transformer, and Mamba, which is an emerging alternative to transformer models. Additionally, we devise a metric for quantifying the distinctiveness of the generated formulae and a straightforward algorithm to enforce the syntax constraints. Our experiments show that the proposed architectures yield promising results, generating correct and distinct formulae at a fraction of the compute cost needed for the combinatorial baseline.

Related papers

• Algorithmic Capabilities of Random Transformers [49.73113518329544]
  We investigate what functions can be learned by randomly transformers in which only the embedding layers are optimized. We find that these random transformers can perform a wide range of meaningful algorithmic tasks. Our results indicate that some algorithmic capabilities are present in transformers even before these models are trained.
  arXiv  Detail & Related papers  (2024-10-06T06:04:23Z)
• Simulating Petri nets with Boolean Matrix Logic Programming [4.762323642506732]
  We introduce a novel approach to deal with the limitations of high-level symbol manipulations. Within this framework, we propose two novel BMLP algorithms for a class of Petri nets known as elementary nets. We demonstrate empirically that BMLP algorithms can evaluate these programs 40 times faster than tabled B-Prolog, SWI-Prolog, XSB-Prolog and Clingo.
  arXiv  Detail & Related papers  (2024-05-18T23:17:00Z)
• Learning to Simulate: Generative Metamodeling via Quantile Regression [2.2518304637809714]
  We propose a new metamodeling concept, called generative metamodeling, which aims to construct a "fast simulator of the simulator" Once constructed, a generative metamodel can generate a large amount of random outputs as soon as the inputs are specified. We propose a new algorithm -- quantile-regression-based generative metamodeling (QRGMM) -- and study its convergence and rate of convergence.
  arXiv  Detail & Related papers  (2023-11-29T16:46:24Z)
• Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
  We discuss the problem of bounding partially identifiable queries, such as counterfactuals, in Pearlian structural causal models. A recently proposed iterated EM scheme yields an inner approximation of those bounds by sampling the initialisation parameters. We show how a single symbolic knowledge compilation allows us to obtain the circuit structure with symbolic parameters to be replaced by their actual values.
  arXiv  Detail & Related papers  (2023-10-05T07:10:40Z)
• Transformers as Statisticians: Provable In-Context Learning with In-Context Algorithm Selection [88.23337313766353]
  This work first provides a comprehensive statistical theory for transformers to perform ICL. We show that transformers can implement a broad class of standard machine learning algorithms in context. A emphsingle transformer can adaptively select different base ICL algorithms.
  arXiv  Detail & Related papers  (2023-06-07T17:59:31Z)
• Towards Invertible Semantic-Preserving Embeddings of Logical Formulae [1.0152838128195467]
  Learning and optimising logic requirements and rules has always been an important problem in Artificial Intelligence. Current methods are able to construct effective semantic-preserving embeddings via kernel methods, but the map they define is not invertible. In this work we address this problem, learning how to invert such an embedding leveraging deep architectures based on the Graph Variational Autoencoder framework.
  arXiv  Detail & Related papers  (2023-05-03T10:49:01Z)
• Error Correction Code Transformer [92.10654749898927]
  We propose to extend for the first time the Transformer architecture to the soft decoding of linear codes at arbitrary block lengths. We encode each channel's output dimension to high dimension for better representation of the bits information to be processed separately. The proposed approach demonstrates the extreme power and flexibility of Transformers and outperforms existing state-of-the-art neural decoders by large margins at a fraction of their time complexity.
  arXiv  Detail & Related papers  (2022-03-27T15:25:58Z)
• A Novel Anomaly Detection Algorithm for Hybrid Production Systems based on Deep Learning and Timed Automata [73.38551379469533]
  DAD:DeepAnomalyDetection is a new approach for automatic model learning and anomaly detection in hybrid production systems. It combines deep learning and timed automata for creating behavioral model from observations. The algorithm has been applied to few data sets including two from real systems and has shown promising results.
  arXiv  Detail & Related papers  (2020-10-29T08:27:43Z)
• Predictive Coding Approximates Backprop along Arbitrary Computation Graphs [68.8204255655161]
  We develop a strategy to translate core machine learning architectures into their predictive coding equivalents. Our models perform equivalently to backprop on challenging machine learning benchmarks. Our method raises the potential that standard machine learning algorithms could in principle be directly implemented in neural circuitry.
  arXiv  Detail & Related papers  (2020-06-07T15:35:47Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.