Integrating Explanations in Learning LTL Specifications from Demonstrations

要約

本稿では、大規模言語モデル（Large Language Models: LLM）の最近の進歩が、人間の説明を、実演から線形時間論理（Linear Temporal Logic: LTL）を学習するのに適した形式に変換するのに役立つかどうかを検討する。LLMも最適化ベースの手法もデモンストレーションからLTL仕様を抽出することができるが、これらには明確な限界がある。LLMは解を素早く生成し、人間の説明を取り入れることができるが、一貫性と信頼性の欠如がセーフティクリティカルな領域での適用を妨げている。一方、最適化ベースの手法は、形式的な保証を提供するが、自然言語による説明を処理できず、スケーラビリティの問題に直面する。我々は、LLMと最適化ベースの手法を組み合わせることで、人間の説明やデモンストレーションをLTL仕様に忠実に変換する原理的なアプローチを提案する。我々は、このアプローチに基づいてJanakaというツールを実装した。我々の実験は、いくつかのケーススタディを通して、LTL仕様の学習における説明と実演の組み合わせの有効性を実証している。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, DeepL