Differentiable Inference of Temporal Logic Formulas
- URL: http://arxiv.org/abs/2208.05440v1
- Date: Wed, 10 Aug 2022 16:52:23 GMT
- Title: Differentiable Inference of Temporal Logic Formulas
- Authors: Nicole Fronda and Houssam Abbas
- Abstract summary: We demonstrate the first Recurrent Neural Network architecture for learning Signal Temporal Logic formulas.
We present the first systematic comparison of formula inference methods.
- Score: 1.370633147306388
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We demonstrate the first Recurrent Neural Network architecture for learning
Signal Temporal Logic formulas, and present the first systematic comparison of
formula inference methods. Legacy systems embed much expert knowledge which is
not explicitly formalized. There is great interest in learning formal
specifications that characterize the ideal behavior of such systems -- that is,
formulas in temporal logic that are satisfied by the system's output signals.
Such specifications can be used to better understand the system's behavior and
improve design of its next iteration. Previous inference methods either assumed
certain formula templates, or did a heuristic enumeration of all possible
templates. This work proposes a neural network architecture that infers the
formula structure via gradient descent, eliminating the need for imposing any
specific templates. It combines learning of formula structure and parameters in
one optimization. Through systematic comparison, we demonstrate that this
method achieves similar or better mis-classification rates (MCR) than
enumerative and lattice methods. We also observe that different formulas can
achieve similar MCR, empirically demonstrating the under-determinism of the
problem of temporal logic inference.
Related papers
- Expressive Symbolic Regression for Interpretable Models of Discrete-Time Dynamical Systems [0.0]
Symbolic Artificial Neural Network-Trained Expressions (SymANNTEx) architecture for this task.
We show that our modified SymANNTEx model properly identifies single-state maps and achieves moderate success in approximating a dual-state attractor.
arXiv Detail & Related papers (2024-06-05T05:05:29Z) - Learning to Estimate System Specifications in Linear Temporal Logic using Transformers and Mamba [6.991281327290525]
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.
arXiv Detail & Related papers (2024-05-31T15:21:53Z) - A Neural Rewriting System to Solve Algorithmic Problems [47.129504708849446]
We propose a modular architecture designed to learn a general procedure for solving nested mathematical formulas.
Inspired by rewriting systems, a classic framework in symbolic artificial intelligence, we include in the architecture three specialized and interacting modules.
We benchmark our system against the Neural Data Router, a recent model specialized for systematic generalization, and a state-of-the-art large language model (GPT-4) probed with advanced prompting strategies.
arXiv Detail & Related papers (2024-02-27T10:57:07Z) - 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) - A Recursive Bateson-Inspired Model for the Generation of Semantic Formal
Concepts from Spatial Sensory Data [77.34726150561087]
This paper presents a new symbolic-only method for the generation of hierarchical concept structures from complex sensory data.
The approach is based on Bateson's notion of difference as the key to the genesis of an idea or a concept.
The model is able to produce fairly rich yet human-readable conceptual representations without training.
arXiv Detail & Related papers (2023-07-16T15:59:13Z) - A Recursively Recurrent Neural Network (R2N2) Architecture for Learning
Iterative Algorithms [64.3064050603721]
We generalize Runge-Kutta neural network to a recurrent neural network (R2N2) superstructure for the design of customized iterative algorithms.
We demonstrate that regular training of the weight parameters inside the proposed superstructure on input/output data of various computational problem classes yields similar iterations to Krylov solvers for linear equation systems, Newton-Krylov solvers for nonlinear equation systems, and Runge-Kutta solvers for ordinary differential equations.
arXiv Detail & Related papers (2022-11-22T16:30:33Z) - Identifiability and Asymptotics in Learning Homogeneous Linear ODE Systems from Discrete Observations [114.17826109037048]
Ordinary Differential Equations (ODEs) have recently gained a lot of attention in machine learning.
theoretical aspects, e.g., identifiability and properties of statistical estimation are still obscure.
This paper derives a sufficient condition for the identifiability of homogeneous linear ODE systems from a sequence of equally-spaced error-free observations sampled from a single trajectory.
arXiv Detail & Related papers (2022-10-12T06:46:38Z) - Refining Labelled Systems for Modal and Constructive Logics with
Applications [0.0]
This thesis serves as a means of transforming the semantics of a modal and/or constructive logic into an 'economical' proof system.
The refinement method connects two proof-theoretic paradigms: labelled and nested sequent calculi.
The introduced refined labelled calculi will be used to provide the first proof-search algorithms for deontic STIT logics.
arXiv Detail & Related papers (2021-07-30T08:27:15Z) - Uncertainty-Aware Signal Temporal logic [21.626420725274208]
Existing temporal logic inference methods mostly neglect uncertainties in the data.
We propose two uncertainty-aware signal temporal logic (STL) inference approaches to classify the undesired behaviors and desired behaviors of a system.
arXiv Detail & Related papers (2021-05-24T21:26:57Z) - Provably Efficient Neural Estimation of Structural Equation Model: An
Adversarial Approach [144.21892195917758]
We study estimation in a class of generalized Structural equation models (SEMs)
We formulate the linear operator equation as a min-max game, where both players are parameterized by neural networks (NNs), and learn the parameters of these neural networks using a gradient descent.
For the first time we provide a tractable estimation procedure for SEMs based on NNs with provable convergence and without the need for sample splitting.
arXiv Detail & Related papers (2020-07-02T17:55: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.