# STL: Surprisingly Tricky Logic (for System Validation)

arXiv: https://arxiv.org/abs/2305.17258 · HTML: https://mlsanity.com/paper/2305.17258/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 27 references that are in the map.
- First posted on arXiv 26 May 2023.

## Builds on (most cited first, 8 of 8)

- [Techniques for Interpretable Machine Learning](https://mlsanity.com/paper/1808.00033/) (2018)
- [Explainable AI: Beware of Inmates Running the Asylum Or: How I Learnt to Stop Worrying and Love the Social and Behavioural Sciences](https://mlsanity.com/paper/1712.00547/) (2017)
- [Interpretable Classification of Time-Series Data using Efficient Enumerative Techniques](https://mlsanity.com/paper/1907.10265/) (2019)
- [Interpretable Apprenticeship Learning with Temporal Logic Specifications](https://mlsanity.com/paper/1710.10532/) (2017)
- [Classification of Time-Series Data Using Boosted Decision Trees](https://mlsanity.com/paper/2110.00581/) (2021)
- [Designing Environments Conducive to Interpretable Robot Behavior](https://mlsanity.com/paper/2007.00820/) (2020)
- [Little Tricky Logic: Misconceptions in the Understanding of LTL](https://mlsanity.com/paper/2211.01677/) (2022)
- [Inferring Temporal Logic Properties from Data using Boosted Decision Trees](https://mlsanity.com/paper/2105.11508/) (2021)

## Built on by (most cited first, 2 of 2)

- [Fewer Than 1% of Explainable AI Papers Validate Explainability with Humans](https://mlsanity.com/paper/2503.16507/) (2025)
- [Military AI Needs Technically-Informed Regulation to Safeguard AI Research and its Applications](https://mlsanity.com/paper/2505.18371/) (2025)

## Abstract (arXiv)

Much of the recent work developing formal methods techniques to specify or learn the behavior of autonomous systems is predicated on a belief that formal specifications are interpretable and useful for humans when checking systems. Though frequently asserted, this assumption is rarely tested. We performed a human experiment (N = 62) with a mix of people who were and were not familiar with formal methods beforehand, asking them to validate whether a set of signal temporal logic (STL) constraints would keep an agent out of harm and allow it to complete a task in a gridworld capture-the-flag setting. Validation accuracy was 45% ± 20% (mean ± standard deviation). The ground-truth validity of a specification, subjects' familiarity with formal methods, and subjects' level of education were found to be significant factors in determining validation correctness. Participants exhibited an affirmation bias, causing significantly increased accuracy on valid specifications, but significantly decreased accuracy on invalid specifications. Additionally, participants, particularly those familiar with formal methods, tended to be overconfident in their answers, and be similarly confident regardless of actual correctness. Our data do not support the belief that formal specifications are inherently human-interpretable to a meaningful degree for system validation. We recommend ergonomic improvements to data presentation and validation training, which should be tested before claims of interpretability make their way back into the formal methods literature.