Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Integrating Explanations in Learning LTL Specifications from Demonstrations

Ashutosh Gupta, John Komp, Abhay Singh Rajput, Krishna Shankaranarayanan, Ashutosh Trivedi, Namrita Varshney

TL;DR

This work tackles learning Linear Temporal Logic (LTL) specifications from demonstrations augmented with human explanations by coupling Large Language Models (LLMs) with optimization-based constraint solving. It introduces quantitative mining with two semantics—Robust and Discounted—to score candidate formulas over finite traces, and uses a template-based repair mechanism to synthesize high-fitness LTL formulas, implemented in the Janaka tool. Experiments on 17 case studies show that incorporating explanations and a repair-based workflow improves formula quality in many cases, with traces enhancing LLM responses and constraint solving providing formal guarantees. The proposed approach enables scalable, explanation-informed extraction of robust LTL specifications for safety-critical systems, bridging human intuition and formal guarantees through a hybrid synthesis pipeline.

Abstract

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. Both LLMs and optimization-based methods can extract LTL specifications from demonstrations; however, they have distinct limitations. LLMs can quickly generate solutions and incorporate human explanations, but their lack of consistency and reliability hampers their applicability in safety-critical domains. On the other hand, optimization-based methods do provide formal guarantees but cannot process natural language explanations and face scalability challenges. We present a principled approach to combining LLMs and optimization-based methods to faithfully translate human explanations and demonstrations into LTL specifications. We have implemented a tool called Janaka based on our approach. Our experiments demonstrate the effectiveness of combining explanations with demonstrations in learning LTL specifications through several case studies.

Integrating Explanations in Learning LTL Specifications from Demonstrations

TL;DR

This work tackles learning Linear Temporal Logic (LTL) specifications from demonstrations augmented with human explanations by coupling Large Language Models (LLMs) with optimization-based constraint solving. It introduces quantitative mining with two semantics—Robust and Discounted—to score candidate formulas over finite traces, and uses a template-based repair mechanism to synthesize high-fitness LTL formulas, implemented in the Janaka tool. Experiments on 17 case studies show that incorporating explanations and a repair-based workflow improves formula quality in many cases, with traces enhancing LLM responses and constraint solving providing formal guarantees. The proposed approach enables scalable, explanation-informed extraction of robust LTL specifications for safety-critical systems, bridging human intuition and formal guarantees through a hybrid synthesis pipeline.

Abstract

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. Both LLMs and optimization-based methods can extract LTL specifications from demonstrations; however, they have distinct limitations. LLMs can quickly generate solutions and incorporate human explanations, but their lack of consistency and reliability hampers their applicability in safety-critical domains. On the other hand, optimization-based methods do provide formal guarantees but cannot process natural language explanations and face scalability challenges. We present a principled approach to combining LLMs and optimization-based methods to faithfully translate human explanations and demonstrations into LTL specifications. We have implemented a tool called Janaka based on our approach. Our experiments demonstrate the effectiveness of combining explanations with demonstrations in learning LTL specifications through several case studies.
Paper Structure (20 sections, 2 theorems, 9 equations, 4 figures, 4 tables, 3 algorithms)

This paper contains 20 sections, 2 theorems, 9 equations, 4 figures, 4 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Motivating example.
  3. Problem Definition
  4. Qualitative Semantics for LTL
  5. Quantitative semantics for LTL
  6. Robust Semantics .
  7. Discounted Semantics .
  8. Mining LTL from Demonstrations and Explanations
  9. Quantitative Mining for LTL
  10. LTL Repair Algorithm
  11. Trace Constraints.
  12. Experiments
  13. LLM Setup
  14. Experimental Results
  15. Ablation Study
  16. ...and 5 more sections

Key Result

proposition 1

If $\alpha = 1$ then for every finite trace $w \in \Sigma^*$, we have that $[ \! [ {\varphi, w} ] \! ] = 1$ if and only if $w \models \varphi$.

Figures (4)

  • Figure 1: Our method for synthesizing LTL formulas from traces uses the intuition of an LLM to find possible answers and we correct them using our fitness-aware search.
  • Figure 2: Learning LTL specifications from explanations and demonstrations.
  • Figure 3: Template Generation Methods
  • Figure 4: The high-level architecture of $\textsf{Janaka }$.

Theorems & Definitions (4)

  • proposition 1: Qualitative Equivalence: Robust
  • proposition 2: Qualitative Equivalence: Discounted
  • definition 1: Qualitative Mining for LTL
  • definition 2: Quantitative Mining for LTL