Scalable Anytime Algorithms for Learning Formulas in Linear Temporal Logic

• URL: http://arxiv.org/abs/2110.06726v1
• Date: Wed, 13 Oct 2021 13:57:31 GMT
• Title: Scalable Anytime Algorithms for Learning Formulas in Linear Temporal Logic
• Authors: Ritam Raha, Rajarshi Roy, Nathana\"el Fijalkow, Daniel Neider
• Abstract summary: We consider the problem of learning formulas for classifying traces. Existing solutions suffer from two limitations: they do not scale beyond small formulas, and they may exhaust computational resources without returning any result. We introduce a new algorithm addressing both issues: our algorithm is able to construct formulas an order of magnitude larger than previous methods, and it is anytime.
• Score: 2.631744051718347
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Linear temporal logic (LTL) is a specification language for finite sequences (called traces) widely used in program verification, motion planning in robotics, process mining, and many other areas. We consider the problem of learning LTL formulas for classifying traces; despite a growing interest of the research community, existing solutions suffer from two limitations: they do not scale beyond small formulas, and they may exhaust computational resources without returning any result. We introduce a new algorithm addressing both issues: our algorithm is able to construct formulas an order of magnitude larger than previous methods, and it is anytime, meaning that it in most cases successfully outputs a formula, albeit possibly not of minimal size. We evaluate the performances of our algorithm using an open source implementation against publicly available benchmarks.

Related papers

• When can you trust feature selection? -- I: A condition-based analysis of LASSO and generalised hardness of approximation [49.1574468325115]
  We show how no (randomised) algorithm can determine the correct support sets (with probability $> 1/2$) of minimisers of LASSO when reading approximate input. For ill-posed inputs, the algorithm runs forever, hence, it will never produce a wrong answer. For any algorithm defined on an open set containing a point with infinite condition number, there is an input for which the algorithm will either run forever or produce a wrong answer.
  arXiv  Detail & Related papers  (2023-12-18T18:29:01Z)
• Algorithm of Thoughts: Enhancing Exploration of Ideas in Large Language Models [17.059322033670124]
  We propose a novel strategy that propels Large Language Models through algorithmic reasoning pathways. Our results suggest that instructing an LLM using an algorithm can lead to performance surpassing that of the algorithm itself.
  arXiv  Detail & Related papers  (2023-08-20T22:36:23Z)
• Machine Learning for Online Algorithm Selection under Censored Feedback [71.6879432974126]
  In online algorithm selection (OAS), instances of an algorithmic problem class are presented to an agent one after another, and the agent has to quickly select a presumably best algorithm from a fixed set of candidate algorithms. For decision problems such as satisfiability (SAT), quality typically refers to the algorithm's runtime. In this work, we revisit multi-armed bandit algorithms for OAS and discuss their capability of dealing with the problem. We adapt them towards runtime-oriented losses, allowing for partially censored data while keeping a space- and time-complexity independent of the time horizon.
  arXiv  Detail & Related papers  (2021-09-13T18:10:52Z)
• Learning Linear Temporal Properties from Noisy Data: A MaxSAT Approach [22.46055650237819]
  We devise two algorithms for inferring concise formulas even in the presence of noise. Our first algorithm infers minimal formulas by reducing the inference problem to a problem in satisfiability. Our second learning algorithm relies on the first algorithm to derive a decision tree over formulas based on a decision tree learning algorithm.
  arXiv  Detail & Related papers  (2021-04-30T16:06:03Z)
• Algorithmic Solution for Systems of Linear Equations, in $\mathcal{O}(mn)$ time [0.0]
  We present a novel algorithm attaining excessively fast, the sought solution of linear systems of equations. The execution time is very short compared with state-of-the-art methods. The paper also comprises a theoretical proof for the algorithmic convergence.
  arXiv  Detail & Related papers  (2021-04-26T13:40:31Z)
• Evolving Reinforcement Learning Algorithms [186.62294652057062]
  We propose a method for meta-learning reinforcement learning algorithms. The learned algorithms are domain-agnostic and can generalize to new environments not seen during training. We highlight two learned algorithms which obtain good generalization performance over other classical control tasks, gridworld type tasks, and Atari games.
  arXiv  Detail & Related papers  (2021-01-08T18:55:07Z)
• Towards Optimally Efficient Tree Search with Deep Learning [76.64632985696237]
  This paper investigates the classical integer least-squares problem which estimates signals integer from linear models. The problem is NP-hard and often arises in diverse applications such as signal processing, bioinformatics, communications and machine learning. We propose a general hyper-accelerated tree search (HATS) algorithm by employing a deep neural network to estimate the optimal estimation for the underlying simplified memory-bounded A* algorithm.
  arXiv  Detail & Related papers  (2021-01-07T08:00:02Z)
• Parallel Scheduling Self-attention Mechanism: Generalization and Optimization [0.76146285961466]
  We propose a general scheduling algorithm, which is derived from the optimum scheduling for small instances solved by a satisfiability checking(SAT) solver. Strategies for further optimization on skipping redundant computations are put forward as well, with which reductions of almost 25% and 50% of the original computations are respectively achieved. The proposed algorithms are applicable regardless of problem sizes, as long as the number of input vectors is divisible to the number of computing units available in the architecture.
  arXiv  Detail & Related papers  (2020-12-02T12:04:16Z)
• Strong Generalization and Efficiency in Neural Programs [69.18742158883869]
  We study the problem of learning efficient algorithms that strongly generalize in the framework of neural program induction. By carefully designing the input / output interfaces of the neural model and through imitation, we are able to learn models that produce correct results for arbitrary input sizes.
  arXiv  Detail & Related papers  (2020-07-07T17:03:02Z)
• Run2Survive: A Decision-theoretic Approach to Algorithm Selection based on Survival Analysis [75.64261155172856]
  survival analysis (SA) naturally supports censored data and offers appropriate ways to use such data for learning distributional models of algorithm runtime. We leverage such models as a basis of a sophisticated decision-theoretic approach to algorithm selection, which we dub Run2Survive. In an extensive experimental study with the standard benchmark ASlib, our approach is shown to be highly competitive and in many cases even superior to state-of-the-art AS approaches.
  arXiv  Detail & Related papers  (2020-07-06T15:20:17Z)
• Learning Interpretable Models in the Property Specification Language [6.875312133832079]
  We develop a learning algorithm for formulas in the IEEE standard temporal logic PSL. Our work is motivated by the fact that many natural properties, such as an event happening at every n-th point in time, cannot be expressed in speak.
  arXiv  Detail & Related papers  (2020-02-10T11:42:50Z)

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.