Structured Interactions with LLMs to Support LTL

Abstract

Prompting large language models (LLMs) to produce Linear Temporal Logic (LTL) explanations has been shown to assist students in LTL understanding tasks. Prior work has investigated LLM prompt improvements to ensure the correctness of the subsequent explanations. In this paper, we complete a replication investigating the extent to which using an LLM assists students in answering questions about LTL and find that LLM usage is associated with higher correctness scores, but LLM usage varied within subject populations. Based on the replication results, we propose an approach and prototype tooling for structured interactions between LLMs and students learning LTL. Finally, we evaluate our initial approach with a pilot study.