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\% \pm 20\%$ (mean $\pm$ 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.

翻译：近期开发形式化方法技术以描述或学习自主系统行为的大量工作，都基于一个前提：在检验系统时，形式化规约对人类而言是可解释且有用的。尽管这一假设经常被提及，却鲜少得到检验。我们开展了一项人类实验（N=62），参与者包括事先熟悉和不熟悉形式化方法的人员，要求他们验证一组信号时态逻辑（STL）约束是否能确保智能体免受伤害，并使其在网格世界夺旗场景中完成任务。验证准确率为 $45\% \pm 20\%$（均值 $\pm$ 标准差）。研究发现，规约的真实有效性、受试者对形式化方法的熟悉程度以及教育水平是决定验证正确性的显著因素。参与者表现出肯定偏差，导致有效规约的准确率显著提高，但无效规约的准确率显著降低。此外，参与者（尤其是熟悉形式化方法者）往往对自己的答案过度自信，且无论实际正确性如何，其自信程度均相似。我们的数据并不支持“形式化规约在系统验证中具有有意义的人类可解释性”这一观点。我们建议对数据展示和验证培训进行人因工程改进，并在可解释性声明重新进入形式化方法文献之前对其进行检验。