Explaining Multi-stage Tasks by Learning Temporal Logic Formulas from Suboptimal Demonstrations

• URL: http://arxiv.org/abs/2006.02411v1
• Date: Wed, 3 Jun 2020 17:40:14 GMT
• Title: Explaining Multi-stage Tasks by Learning Temporal Logic Formulas from Suboptimal Demonstrations
• Authors: Glen Chou, Necmiye Ozay, Dmitry Berenson
• Abstract summary: We present a method for learning multi-stage tasks from demonstrations by learning the logical structure and atomic propositions of a consistent linear temporal logic (LTL) formula. The learner is given successful but potentially suboptimal demonstrations, where the demonstrator is optimizing a cost function while satisfying the formula, and the cost function is uncertain to the learner. Our algorithm uses the Karush-Kuhn-Tucker (KKT) optimality conditions of the demonstrations together with a counter-example-guided falsification strategy to learn the atomic proposition parameters.
• Score: 6.950510860295866
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present a method for learning multi-stage tasks from demonstrations by learning the logical structure and atomic propositions of a consistent linear temporal logic (LTL) formula. The learner is given successful but potentially suboptimal demonstrations, where the demonstrator is optimizing a cost function while satisfying the LTL formula, and the cost function is uncertain to the learner. Our algorithm uses the Karush-Kuhn-Tucker (KKT) optimality conditions of the demonstrations together with a counterexample-guided falsification strategy to learn the atomic proposition parameters and logical structure of the LTL formula, respectively. We provide theoretical guarantees on the conservativeness of the recovered atomic proposition sets, as well as completeness in the search for finding an LTL formula consistent with the demonstrations. We evaluate our method on high-dimensional nonlinear systems by learning LTL formulas explaining multi-stage tasks on 7-DOF arm and quadrotor systems and show that it outperforms competing methods for learning LTL formulas from positive examples.

Related papers

• RoSTE: An Efficient Quantization-Aware Supervised Fine-Tuning Approach for Large Language Models [95.32315448601241]
  We propose an algorithm named Rotated Straight-Through-Estimator (RoSTE) RoSTE combines quantization-aware supervised fine-tuning (QA-SFT) with an adaptive rotation strategy to reduce activation outliers. Our findings reveal that the prediction error is directly proportional to the quantization error of the converged weights, which can be effectively managed through an optimized rotation configuration.
  arXiv  Detail & Related papers  (2025-02-13T06:44:33Z)
• Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization [4.2518927441106]
  Main bottleneck in existing methods is a computationally expensive quantifier elimination step. We propose a template-based Skolemization approach, where we automatically synthesize linear/polynomial Skolem functions in order to eliminate quantifiers in the formula. Our method offers a range of appealing theoretical properties combined with a strong practical performance.
  arXiv  Detail & Related papers  (2024-12-18T14:37:15Z)
• Constrained LTL Specification Learning from Examples [8.544277223210894]
  We propose a new type of learning problem called constrained learning. In addition to positive and negative examples, the user can specify one or more constraints over the properties of the formula. An experimental evaluation demonstrates that ATLAS is able to solve new types of learning problems while performing better than or competitively with the state-of-the-art tools in learning.
  arXiv  Detail & Related papers  (2024-12-03T23:15:27Z)
• TLINet: Differentiable Neural Network Temporal Logic Inference [10.36033062385604]
  This paper introduces TLINet, a neural-symbolic framework for learning STL formulas. In contrast to existing approaches, we introduce approximation methods for max operator designed specifically for temporal logic-based gradient techniques. Our framework not only learns the structure but also the parameters of STL formulas, allowing flexible combinations of operators and various logical structures.
  arXiv  Detail & Related papers  (2024-05-03T16:38:14Z)
• Integrating Explanations in Learning LTL Specifications from Demonstrations [6.070833893646998]
  This paper investigates whether recent advances in Large Language Models (LLMs) can assist in translating human explanations into a format that can robustly support learning Linear Temporal Logic (LTL) from demonstrations. We present a principled approach combining LLMs and optimization-based methods to faithfully translate human explanations and demonstrations into specifications.
  arXiv  Detail & Related papers  (2024-04-03T17:09:00Z)
• The Common Stability Mechanism behind most Self-Supervised Learning Approaches [64.40701218561921]
  We provide a framework to explain the stability mechanism of different self-supervised learning techniques. We discuss the working mechanism of contrastive techniques like SimCLR, non-contrastive techniques like BYOL, SWAV, SimSiam, Barlow Twins, and DINO. We formulate different hypotheses and test them using the Imagenet100 dataset.
  arXiv  Detail & Related papers  (2024-02-22T20:36:24Z)
• Faithful Explanations of Black-box NLP Models Using LLM-generated Counterfactuals [67.64770842323966]
  Causal explanations of predictions of NLP systems are essential to ensure safety and establish trust. Existing methods often fall short of explaining model predictions effectively or efficiently. We propose two approaches for counterfactual (CF) approximation.
  arXiv  Detail & Related papers  (2023-10-01T07:31:04Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  This paper studies Linear Temporal Logic over Finite Traces (LTLf) proposition letters are replaced with first-order formulas interpreted over arbitrary theories. The resulting logic, called Satisfiability Modulo Theories (LTLfMT), is semi-decidable.
  arXiv  Detail & Related papers  (2022-04-28T17:57:33Z)
• Reinforcement Learning from Partial Observation: Linear Function Approximation with Provable Sample Efficiency [111.83670279016599]
  We study reinforcement learning for partially observed decision processes (POMDPs) with infinite observation and state spaces. We make the first attempt at partial observability and function approximation for a class of POMDPs with a linear structure.
  arXiv  Detail & Related papers  (2022-04-20T21:15:38Z)
• Formal Synthesis of Lyapunov Neural Networks [61.79595926825511]
  We propose an automatic and formally sound method for synthesising Lyapunov functions. We employ a counterexample-guided approach where a numerical learner and a symbolic verifier interact to construct provably correct Lyapunov neural networks. Our method synthesises Lyapunov functions faster and over wider spatial domains than the alternatives, yet providing stronger or equal guarantees.
  arXiv  Detail & Related papers  (2020-03-19T17:21:02Z)

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.