STL: Still Tricky Logic (for System Validation, Even When Showing Your Work)

TL;DR

This paper investigates whether active learning can improve human validation of formal specifications in autonomous systems, finding limited success and highlighting ongoing challenges in interpretability.

Contribution

It applies active learning to enhance human validation of signal temporal logic specifications, revealing current limitations and suggesting future research directions.

Findings

Validation accuracy around 65% with high variability

Active learning conditions did not significantly outperform no active learning

Formal specifications alone may not suffice for effective human interpretability

Abstract

As learned control policies become increasingly common in autonomous systems, there is increasing need to ensure that they are interpretable and can be checked by human stakeholders. Formal specifications have been proposed as ways to produce human-interpretable policies for autonomous systems that can still be learned from examples. Previous work showed that despite claims of interpretability, humans are unable to use formal specifications presented in a variety of ways to validate even simple robot behaviors. This work uses active learning, a standard pedagogical method, to attempt to improve humans' ability to validate policies in signal temporal logic (STL). Results show that overall validation accuracy is not high, at $65\% \pm 15\%$ (mean $\pm$ standard deviation), and that the three conditions of no active learning, active learning, and active learning with feedback do not significantly differ from each other. Our results suggest that the utility of formal specifications for human interpretability is still unsupported but point to other avenues of development which may enable improvements in system validation.