# Integrating Explanations in Learning LTL Specifications from Demonstrations

arXiv: https://arxiv.org/abs/2404.02872 · HTML: https://mlsanity.com/paper/2404.02872/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 15 of its 56 references that are in the map.
- First posted on arXiv 3 Apr 2024.

## Builds on (most cited first, 15 of 15)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [OpenAI Gym](https://mlsanity.com/paper/1606.01540/) (2016)
- [Siren's Song in the AI Ocean: A Survey on Hallucination in Large Language Models](https://mlsanity.com/paper/2309.01219/) (2023)
- [Omega-Regular Objectives in Model-Free Reinforcement Learning](https://mlsanity.com/paper/1810.00950/) (2018)
- [A Learning Based Approach to Control Synthesis of Markov Decision Processes for Linear Temporal Logic Specifications](https://mlsanity.com/paper/1409.5486/) (2014)
- [Learning Linear Temporal Properties](https://mlsanity.com/paper/1806.03953/) (2018)
- [Formal Specifications from Natural Language](https://mlsanity.com/paper/2206.01962/) (2022)
- [Policy Synthesis and Reinforcement Learning for Discounted LTL](https://mlsanity.com/paper/2305.17115/) (2023)
- [Multi-modal Program Inference: a Marriage of Pre-trainedLanguage Models and Component-based Synthesis](https://mlsanity.com/paper/2109.02445/) (2021)
- [Learning Interpretable Temporal Properties from Positive Examples Only](https://mlsanity.com/paper/2209.02650/) (2022)
- [Cook2LTL: Translating Cooking Recipes to LTL Formulae using Large Language Models](https://mlsanity.com/paper/2310.00163/) (2023)
- [Learning and Solving Regular Decision Processes](https://mlsanity.com/paper/2003.01008/) (2020)
- [Formal Consistency Checking over Specifications in Natural Languages](https://mlsanity.com/paper/1405.5003/) (2014)
- [Robust Linear Temporal Logic](https://mlsanity.com/paper/1510.08970/) (2015)

## Built on by (most cited first, 1 of 1)

- [Reward Shaping and Action Masking for Compositional Tasks using Behavior Trees and LLMs](https://mlsanity.com/paper/2605.05795/) (2026)

## Abstract (arXiv)

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.