Reachability-based Temporal Logic Verification for Reliable LLM-guided Human-Autonomy Teaming

TL;DR

This paper introduces a reachability-based framework that uses signal temporal logic to verify and improve the reliability of human-autonomy teaming guided by large language models, ensuring safe and effective communication.

Contribution

It presents a novel STL feasibility filter that decomposes complex commands for parallel feasibility checking and feedback, enhancing reliability in human-autonomy interactions.

Findings

Successfully filters infeasible subformulas

Provides informative feedback for command modification

Enables safer human-autonomy teaming

Abstract

We propose a reachability-based framework for reliable LLM-guided human-autonomy teaming (HAT) using signal temporal logic (STL). In the proposed framework, LLM is leveraged as a translator that transfers natural language commands given by a human operator into corresponding STL specifications or vice versa. An STL feasibility filter (SFF) is proposed to check the feasibility of the generated STL. The SFF first decomposes the complex and nested LLM translation into a set of simpler subformulas for parallelization and informative feedback generation. The reachability analysis method is then applied to verify if each subformula is feasible for a target dynamical system: if feasible, perform mission planning, otherwise, reject it. The proposed SFF can identify infeasible subformulas, more than simply providing the boolean verification results for the whole STL, thereby facilitating the feedback generation of LLM to request modification of the command to the human. Consequently, the proposed framework can allow more reliable HAT by enabling safe and informative communication between the human operator and the autonomous agent. Our experiments demonstrate that the proposed framework can successfully filter out infeasible subformulas and generate informative feedback based on such information.