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.

翻译：本文探究大型语言模型（LLMs）的最新进展是否有助于将人类解释转化为能够稳健支持从演示中学习线性时序逻辑（LTL）的格式。LLMs和基于优化的方法都能从演示中提取LTL规范，但它们各有局限。LLMs能快速生成解决方案并融入人类解释，但其一致性和可靠性不足限制了其在安全关键领域的适用性。而基于优化的方法虽能提供形式化保证，却无法处理自然语言解释且面临可扩展性挑战。我们提出了一种将LLMs与基于优化方法相结合的原则性方法，旨在忠实地将人类解释和演示转化为LTL规范。基于该方法，我们实现了一个名为Janaka的工具。实验通过多个案例研究证明了将解释与演示相结合学习LTL规范的有效性。