STL: Still Tricky Logic (for System Validation, Even When Showing Your Work)
Authors: Isabelle Hurley
Rohan R Paleja
Ashley Suh
Jaime Daniel Pena
Ho Chit Siu
Venue: NeurIPS 2024 poster (2024)
Keywords: Explainability
Formal Methods
Human Experiments
Robotics
Primary area: interpretability_and_explainability
TL;DR: Formal methods are not particularly "explainable" for system validation even when applying best practices from education research

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.

STL: Still Tricky Logic (for System Validation, Even When Showing Your Work)
Isabelle Hurley"
Rohan Paleja
Lincoln Laboratory
Lincoln Laboratory
Massachusetts Institute of Technology Lexington, MA 02421
Massachusetts Institute of Technology
Lexington, MA 02421
isabelle.
hww.hyulllll..m htabelle.hurrey@11.
mit. edu
rohan paleja@l1 mit.mit.e.. edu
Ashley Suh
Jaime D. Peña
Lincoln Laboratory
Lincoln Laboratory
Massachusetts Institute of Technology Lexington, MA 02421 ashley. suh@11 mim. edu
Massachusetts Institute of Technology
Lexington, MA 02421 jdpenaø11.mm edu
Ho Chit Siu Lincoln Laboratory
Massachusetts Institute of Technology Lexington, MA 02421 hochit. siuell mit. edu
Abstract
As learned control policies become increasingly common autonomous systems, there is increasing need to ensure that they are interpretable and can be checked by human stakcholders. Formal specifications have been proposed as ways produce numan-interpretalle 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 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% + 15% (mean + standard deviation), and that the three conditions 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.
1 Introduction
In recent years, research in robotics has made incredible strides and has been targeting applications across a variety of industries, including manufacturing, healthcare, household, and security. Across
"Corresponding author.
"DISTRIBUTION STATEMENT A. Approved for public release. Distribution is unlimited. This material is based upon work supported the Under Secretary Defense for Research and Engineering under Air Force Contract No. FA8702-15- 1-12-15---0001 Any opinions. findings. conclusions or recommendattins expressed in this material are those of the author(s) and do not necessarily reflect the views of the Under Secretary of Defense for Research and Engineering.
38th Conference on Neural Information Processing Systems (NcurIPS 2024).

---

these diverse use cases, a central envisioned capability is that of dynamic programming of robots, allowing an end-user - typically with less familiarity with the system than the original designer to modify the robotic system to suit their own purposes, such as in home robotics applications
37 40), agricultural monitoring [5) or Internet of Things devices [2 21]. However, prior to such a capability, robots must be able to perform tasks safely, and the programmer must be able to effectively ensure that the robot's behavior and its respective changes meet the intended goal.
In quality control, this process is commonly referred to as Verification & Validation (V&V). Specif- ically, properties and behaviors of robotic systems must meet a set of broader requirements (i.e., human safety. legal standards, etc.) and align with the intent of stakeholders. Depending on the techniques used to create robot behavior, the former (verification) can be accomplished via sampling and simulation, or even via mathematical proofs [I The latter (validation) is a process that determines whether the product "solves the right problems" and "satisf[ies] intended use and user needs" [1I, making it an inherently human-centered process of value alignment. Validation is key building block in creating robotic systems that are able to be dynamically reprogrammed and building common language between the user and robot
much less has been done on validation. Much of contemporary verification work relies on the use of formal methods, including languages such as linear temporal logic (LTL) and signal temporal logic (STL). There is also an assumption in the formal methods community that these methods are not only verifiable, but are also
While significant work has been performed on system verification 19
20
human- iimmannntterpettblle. and thus useful for validation due their semantics (e.g. 26 14 28 To 231). However, human validation of policies expressed in both L.TL and STL has shown to be empirically very difficult 17 38,, even as essential. Indeed, as Leveson observes, "virtually all accidents involving software stem from unsafe requirements, not implementation errors," and "software logic flaws stem from a lack of adequate requirements" (24).
Given the importance of validation and these difficulties in interpreting autonomous system behavior specified via formal logic, we propose the use of active learning, a popular educational practice, to improve humans' ability to validate formal logic policies. This active learning is distinct from active learning in the machine learning literature, and a focused activity (detailed in Section 2.2). Our primary research question is whether or not using active learning improves humans' policy validation rate. In this paper, we contribute 1) a (human) active learning method as a potential approach to improving humans' ability to interpret formal policies, leveraging tools common in formal methods, 2) an experimental protocol to measure the differences in system validation performance under varying active learning conditions, and 3) set of implications for improving human validation of autonomous systems. In short, formal specifications are not inherently human interpretable for system validation and while active learning approaches can improve human engagement with system validation task, this does not necessarily improve performance.
2 Background
2.1 Formal Methods for Interpretable Learning
Autonomous systems can be programmed in a variety of ways, including codifying domain expertise, extracting policies from demonstration 9 355, or synthesizing behavior via an objective function and constraints (25). Policies can be represented in a variety of forms, including neural networks, symbolic representations, and behavior trees. In this paper, we focus on a popular representation, temporal logic, subset of formal methods. Temporal logic has seen significant usage with autonomous systems
(e.g. 6 26 14 programming to those familiar with its use. Furthermore, these mathematically precise specifications allow for representing model behavior within a relatively concise format and verification to ensure the autonomous system behavior meets requirements. A more complete introduction to STL and its use in this experiment is in Appendix A.I
28
10 23) ) as it can represent high-level mission objectives, allowing for ease of
"Some definitions of validation, such as from system modeling 13] are slightly different, and in some cases there is disagreement about whether verification and validation are distinct activities. We take the software engineering standard definition from the IEEE []I], which distinguishes the two and is more appropriate for autonomous systems design.

---

Human stakeholders' ability to understand policies (to varying degrees) is increasingly important from legal, ethical, and usability perspectives, particularly if policies can be updated after system deployment, either in a centralized manner, or in user-initiated manner. Interpretability, and related terms such as transparency, explainability, and so on, are, however, often poorly defined, or indeed, simply left undefined in the research that claim to have created systems with these properties [27]. Miller et al.'s 2017 work showed that among a collection of papers from an Explainable Al workshop, most papers neither cited supporting social science literature to support their design choices, nor reached their conclusions with actual data showing any measure of interpretability; indeed "many models being used in explainable AI research are not building of explanation" " [32]. Sanneman and Shah propose the use of situation awareness to determine the informational needs driving requirements of explainable systems (36.. User informational needs map to the levels of perception, comprehension, or prediction of system behavior. For our purposes of system validation, a strong ability to predict behavior is the kind of interpretability required to ensure intent alignment.
current scientific understanding
Formal methods, which employ logical languages, are collection of system design techniques that rigorously tie semantic properties to mathematical models, and have been touted as a promising
approach to interpretable policies, in addition to their mathematical verifiability 66 26 4 28 The supposed link to interpretability (almost universally left unstated) is likely that if model behaviors can be tied specifically to meaningful, grounded concepts (such symbols and prepositions), and if models are small enough for humans to reasonably examine, then interpretability is achieved. Indeed, unlike "black box" methods such as deep neural networks, the semantics of formal logic ensures that their specification can always be expressed in natural language.
10 23
The major gap in these approaches to interpretabilityy is the lack of empirical evidence to their efficacy in the overwhelming majority of cases. For example 16 26) 14 28 IO. [3] all claim to have methods that learn human-interrpetabbl policies via formal methods. All provide empirical evidence that policies are learned, but all fail to provide any empirical evidence for the human-interpretabillyy of their policies. A more extensive 2023 survey of the last decade of temporal logic literature that specifically claimed interpretability saw that only approximately 10% cited any supporting work for the interpretability of their methods, none actually incorporated the cited methods into their work, and none checked their claims with actual humans [38]. Subsequent human experiments examining interpretabilityy for validation in that work showed less than 50% validation accuracy with signal temporal logic, even when using methods proposed by the literature (e.g. translation into language or decision trees). Formal methods experts only performed marginally better than complete novices. Those results match what is found in a broader 2023 review of the existing empirical work on explainable AI, where human performance has been extremely poor, even when self-reported understanding and trust increases 18).
While methods like translation into language may seem an intuitive way increase the interpretability of formal logic, empirical evidence does not demonstrate this improvement [38] 39). Vinter et al. [39 and Loomes and Vinter [29] showed that specifications rendered in natural language (even when containing logical operators) evoked inappropriate systemic biases in which readers substituted heuristic reasoning (commonly used in language) for logical reasoning (necessary for formal methods) during evaluation. Consequently, we do not provide a translation into natural language for this experiment.
In this paper, we aim to harness human active learning to bridge the gap between claims of inter- pretability and the actual understanding of users. Our goal is to provide users with deeper insight into the behavior of autonomous agents as specified by Signal Temporal Logic (STL). A detailed description of the STL format utilized for all specifications can be found in Appendix A.2
2.2 Human Active Learning for Validation
Following Miller et al.'s exhortation 32. we explore the utility of current scientific understanding of human learning in the process of interpreting robot policies for validation. Active learning as scoped by Bonwell and Eison, involves "instructional activities involving students in doing things and thinking about what they are doing," " and involves "higher-order thinking tasks as analysis, synthesis, and evaluation" (2) Common examples of active learning actívities in the classroom include note-taking, note synthesis, writing exercises, and discussion. Active learning has been shown to benefit learners by increasing their engagement in areas which require higher order thinking skills
3

---

like engineering [ and a 2014 metaanalysis found that across 225 studies conducted within STEM courses, active learning increased learner performance and decreased rates of class failure [16].
In systems where users work with programmed robots, active learning can be applied as a tool to increase user understanding over robot behavior. To enable this higher learning for validation, ask users to assess the contextual implications of given policy and evaluate how the allowed set of behaviors aligns with one's needs. Under the adapted Bloom's 's Taxonomy of (human) learning ([5), this assessment and evaluation would touch on higher levels of learning, specifically enabling the following dimensions of learning: Recognition, Assembly, Determination, and Judgement.
3 Methods
Providing humans with the ability to validate robot policies specified in STL is building block toward dynamic reprogramming of robots. In this section, we describe how to incorporate active learning to improve human's s ability to perform system validation.
3.1 Experimental Testbed: ManeuverGame
To investigate how pedagogical active learning practices can help improve humans' ability validate the policy of an autonomous system, we developed ManeuverGame, a software suite centered around policy evaluation for agents in a grid world game. ManeuverGame allows a user control an agent and navigate it through a map given configuration. Trajectories can be easily generated, saved and iterated upon for users explore the behavior constraints of a specification within the dynamics of a specific scenario. Thus, users can refine of their understanding of the policies by performing all aspects of Bloom's 's taxonomy 15 with given set of specifications. Figure d this process.
3.1.1 Active Learning For Validation Concept
Active learning and feedback be integrated into the process of system validation. We approach this by tasking learners to generate example behaviors that satisfy the specification's constraints in order to support their determinations of a specification's validity. If a behavior can be found that meets the specification but nonetheless violates the user's intent, then it demonstrates that the specification invalid. Figure (eeft) shows an example of specification used in this study.
Rather than solely tasking users with evaluating if a specification is valid or not, we investigate an active learning approach which breaks the validation of specifications into steps of first behavior exploration and secondly determination. In behavior exploration, users explore a subset of the allowed behaviors defined by the specification's constraints. In determination, users evaluate if the set of allowed behaviors contains only trajectories which match their intent or if it includes trajectories which violate their intent. Essentially, this approach asks users explore the set of behaviors and provide specific examples to "show their work" in making a specification determination.
Runtime verification is computational approach detect if system behaviors match specification [22]. Such techniques can be used to facilitate feedback about specific behaviors, since they are a lightweight alternative to other verification techniques like model checking and can be automatically generated from high level specifications (22). A runtime verification monitor takes in a finite trace (i.e. trajectory) and determines correctness property. It can be applied in the context of active learning for validation to give users feedback on example behaviors (trajectories).
We implement our experiment in the custom ManeuverGame interface (Figure D. An agent has specification that determines the trajectories it can generate, and the subject must determine if the specification will cause the agent to always win regardless of what trajectory is generated. The blue agent (circle) wins it reaches the green objective (triangle) within 30 steps, while avoiding being within one space of the static red players (diamond).
Where verification asks the question "does this product/behavior match with the set of requirements set out for it," validation probes "does this product operate in and only in the ways that I want it to?" In our experiment, "winning" serves as a clear objective stakeholder intent - essentially defining "the ways want it to" - that can be codified in programming. This approach replaces the more complex and less easily codified intents often held by robotics stakeholders, enabling us to explore the limitations and challenges of human validation in controlled environment.

---

01
Remember
02
Understand
03
Apply
04
Analyze
05
Evaluate
Create
Spediicction
brw 10 240000y47
Figure 1: Bloom's 'ss laxonomy applied to ManeuverGame. For given problem, subject must first recall the meaning of the information they'r re being presented with (c.g., a formal specification), and understand enables the subject to analyze different trajectories, both valid and invalid, under a trial-an sual-and-errow process. Evaluating the trajectories, a subject is able to hone in on specifications that are both valid and meet the specification, allowing them to create multiple such specifications. This process repeats itself for new problems.
the given context (grid world). Applying these concepts in ManeuverGame
Without presenting to the user task that can be checked automatically, we cannot objectively check the user's ability to evaluate the specification. Thus, while assessing whether specifications lead to winning can be framed as a verification problem, it provides clear representation of stakeholder intent, unlike the more complex intents that robotics stakeholders may have such as "complete the task safely" or "watch out for nearby cyclists." If such a simple intent cannot be easily validated, more difficult tasks are likely worse off.
4 Human-Subjects Study
We conducted a between-subjects experiment where human participants validated robot motion plans from provided trajectory specifications. 55 adult participants completed the experiment after providing informed consent. The protocol was approved by the MIT Committec the Use of Humans as Experimental Subjects and the United States Department of Defense Human Research Protection Office. Participants were recruited from the MIT Bchavioral Research Lab participant pool, which includes a diverse set of volunteers from the general public, along with a small number of targeted emails to recruit people with formal methods expertise. The pool was designed to reflect likely range of "end users" mond--ser-rprrgrammmal systems. Participants were compensated $15 USD for completion of the experiment plus $2 per correct validation, for total of up $35. Broadly, the experiment asked participants to determine whether provided temporal logic specification would always result in plans that would win capture-the-flagllik game in provided game configuration. Below, we detail the experiment procedure.
4.1 Procedure
All subjects are first provided with demographic survey focused relevant educational background (e.g., experience in logic, mathematics, robotics), with 5-point Likert scale questions and open-ended explanations. Next, subjects received introductory material via videos, text-based tutorials and interactive questions as described in Appendix A.3
Then, the participant shifted into the main experiment. During this phase, subjects were presented with a robot policy as a set of motion constraints (specifications) in STL alongside a starting map, and were asked to evaluate whether trajectories generated by the policy would always allow the blue agent to win the game (valid) or could result in losing (invalid), followed by their confidence in their answer. Each subject evaluated ten pairs of specifications and maps during the course of the experiment. For a sense of specification complexity across the evaluation tasks, the number of symbols in the specification varied from 43 to 97, and the abstract syntax tree (AST) depth ranged from 3 to
During evaluation, both Active Learning groups (AL-WF and AL-NF) were required to either provide three trajectories that 1) satisfied the specification and resulted in a blue team win before answering that specification was valid, or 2) provide one trajectory that satisfied the specification
5

---

but resulted in a blue team loss before answering that specification was invalid. The former required users explore potential implications of the specification, but does not represent an exhaustive search of the possibilities, while the latter is effectively proof by contradiction. While subjects are asked to provide trajectories that meet the specifications, the AL.-NF group was not provided real-time feedback about whether or not their trajectories were actually within specification") In the AL-WF condition runtime verification (using code from Cardona et al. [8) ensured that participant's provided trajectories matched the specification. Here, it is possible for users to get stuck if they are not able to think of trajectories that meet specification, since we do not let them proceed with specification-vioatiie
plans, unlike in AF-NF. Therefore, users were had the option to give up the question after three consecutive failed attempts at trajectory generations, and are asked to provide guess. Guessed answers were denoted as incorrect for the purpose of scoring.
control group performed the same task as the test groups, trajectories for their validation process nor were they given the option to do so on the interface. All users were provided with scratch paper, and is possible that subset of control users may have essentially executed similar workflow tracing on-screen with their finger or scratch paper.
were not required to provide
Finally, participants were asked comment on their approach to answering questions, their overall confidence, the presentation of specifications, and any features of the interface which helped or hindered their understanding. Participants could also provide free-response commentary on their thoughts on the experiment as whole.
4.2 Experiment Hypotheses
Here, we introduce our hypotheses, metrics assess each hypothesis, and statistical procedure. Our hypotheses are:
HI: Active learning increases the rate of correct responses in specification validation. This hypothesis is assessed by comparing the overall accuracy across conditions AL-NF and AL-WF, to the control.
H2: Active learning leads better calibration of confidence rating with response correctness in specification validation. This hypothesis is assessed by comparing the correlation coeffi- cient between confidence and validation accuracy across conditions AL-NF and AL,-FF, to the control.
H3: Increased rate of adherence to specifications in trajectory generation is correlated with increased rate of correct responses in specification validation in the AL-WF condition. This hypotheses is addressed by comparing the per-question rate of satisfactory trajectory generation with response correctness the AL-WF condition.
Omnibus tests were conducted examine the relationship between various subject-sppeific and specification-specci predictors and subjects' success at the validation task. The statistical models and further analysis procedures are detailed in Appendix [A.5) Additionally, we explicitly measured participant engagement and exclude users who "gave up" in our analysis. These representative cases were determined via criteria given in Appendix [A.7 indicated users did not actively interact with the experiment content. See Section 5.2 for more details on subjects' engagement.
5 Results
5.1 Validation Task Performance
In assessing H1, find that there was significant difference in the participants performance
among these groups (Table I F2, 42) = 0.0804, p = 0.453). Bartlett's test for homogeneity of variance in score across learning conditions revealed no significant differences (p = 0.744). Subjects' performance at the validation task was significantly better than random across all conditions (Table Ib. showing some minimal capability to validate system behaviors.
'A subset of four subjects from this experimental group were asked to perform experiment while speaking out loud to explain their thought process (the "think aloud" group). For these subjects, audio and screen recordings were taken, and their results not analyzed with the rest of the subjects.

---

Table 1: The overall accuracy (mean and standard deviation) for the Validation Task, along with statistical significance when compared against random chance (score of 50%) and associated Cohen's d effect size. Overall accuracy was 65 + 15%. AL-NF is active learning with no feedback, AL-WF active learning with feedback.
Condition
Accuracy
AL-NF
66 16%
0.007
0.90
AL-WF
= 16%
0.001
1.00
Control
13%
0.009
0.86
Validation Score vs. STEM Experience by Experimental Condition
Learning without Feedback
Active Learning without Feedback
Control
0.004
p 0.672
p 0.030
p 0.988
Points
STEM Experrence
STEM Experience
STEM Experience
Figure 2: STEM experience vs. validation score by experiment condition. Horizontal jitter was added to visually separate points. Linear fit is shown. Displayed r and p values were calculated using Spearman's coefficient.
However, the data did not indicate significant differences in subjects' overall performance based on the experimental condition, participant level of education, STEM background, or formal methods familiarity (all > 0.05). Further discussion of formal methods familiarity among our subject pool provided in Appendix A.. STEM experience appeared to be less influential the active learning conditions than in the control (Figure 2. The correlation between STEM experience and performance was r = 0.599 and p = 0.030, though not significant due the Bonferroni correction (a 0.05/3 0.016).
The data did not support significant differences in question correctness based on factors of level of education, familiarity with formal methods, STEM Background, experiment condition nor question specific factors of specification ground -ruth validity, specification complexity, nor the question sequence order as predictors of validation correctness (all p > 0.05).
In assessing H2, find that the comparison of participants average confidence levels between groups showed no significant difference (F(2,42) = 0.361, p = 0.699). Further analysis of confidence and calibration between subjects' confidence and correctness be found in Appendix A.6
5.2 Effective Engagement
Across each of the engagement mechanism conditions, some participants did not engage with the validation task (Table Behavior trends for von-engagement or gggvingg up" were identified post-hoc by analyzing the duration of users' engagement with questions for all groups, as well as the content of responses in active learning conditions. We identified and excluded eight participants who were determined to have given up on the task ("giving up" criteria in Section A.7)
Table 2: Participant count and engagement. AL-NF is active learning with no feedback, AL-WF is active learning with feedback. Time to completion (mean and standard deviation) does not include participants who gave up.
Condition
Number of Subjects
Number Giving Up
Time (minutes)
AL-NF
18
3
36.31 + 10.85
AL-WF
16
1
40.37 + 10.68
Control
17
4
19.92 9.07
7

---

Specification Satisfaction Trajectories by Validity when Resporse was Correct and Incorrect Valid
Invalid
%6 Satisfactory Trajectorie
30
p 6.25e-5
25
-1.08
1.31
68
10
Incorrect
Correct
Incorrect
Correct
Figure 3: Combined heat map and boxplot (same data) showing satisfaction of specification in trajectory generation by correctness for valid and invalid ground truth. Each datapoint represents one response to validation satisfaction question.
The two active learning conditions were not significantly different from each other (p = 0.29); however, they were both significantly greater than the control group 1.18 x 10 for AL-NF and AL-WF conditions respectively, both less than the Bonferroni threshold). The active learning conditions effectively extended users time of engagement with the task; however, as observed Table this extended time was not effective in improving performance at the system validation task during the experiment session.
3.20 10-5 and p
In AL-NF, certain users exhibited a tendency to fail the trajectory generation task by submitting trajectories that were completely uninformed by the specification (either of too short length or not at all adherent to the constraints).
Under AL-WF participants were forced to engage for longer durations as they could not answer without providing at least one satisfactory trajectory. While 108 of 506 total provided trajectories were rejected for not satisfying the specification, only eight of the 160 questions were answered with a "give-up" response, and those responses came from only five of the 16 total participants.
5.3 Trajectory Analysis
Under AL-NF participants could provide trajectories which did not meet the specification. These trajectories were further analyzed to interrogate how users arrived at their answers. 34% these trajectories did not actually meet the specification. Note that subjects were instructed only provide trajectories that met specifications, and that it was always possible to do so. These trajectories violated with the time bound, to the specification in variety of ways ranging from simple off by non-meaninguul trajectories. complete ignoring of parts of the specification, to the creation of short,
Participants' creation of trajectories that satisfy the specification is related to their correctness in validation task, however this effect is dependent on the ground truth validity of the specification. When the ground- -ruth of the specification is valid, correct responses more significantly more likely to be accompanied by trajectories which satisfy the specification (Figure 3 p = 6.25 10 10-5). Conversely, when the ground-truth of the specification is invalid, incorrect responses to be accompanied by satisfactory trajectories as shown work (Figure 3 = 4.03 x 10 (0-8). Proper trajectory generation indicates subjects' understanding of specification constraints, but the translation of this capacity to validation ability is not direct.
more likely
5.4 Subject Cognitive Process
Observations of subjects in the talk-aloud sub-group as well as the content of all subjects post- experiment comments provided insight in to the cognitive processes of the participants. In post experiment comments, 14 subjects (25% of the subject pool) expressed some degree of confusion and frustration with the process of system validation. Expressions varied in intensity from "it was little complicated for me," to describing the process as "overwhelming." "disorienting." " and "mind boggling." 57% of subjects who expressed such confusion participated in the AL-NF condition, five participated in the control condition and only one in the AL-WWF condition. Seven participants expressed confusion about the presentation and syntax of specifications with four participants specifi-

---

cally noting trouble with nesting, despite the fact the specification complexity metrics (AST depth and symbol count) were not found to significant factor in determining performance.
Six participants explicitly expressed some concept of safety (avoiding getting tagged) and liveness (reaching the goal). A notable instance of this stated "I imagined my robot was "suicidal" and was trying to get tagged. If there was no way to be tagged, then it remained to see if it could reach goal in under 30 steps (the other way lose)." The notion of the robot being "suicidal" suggests consideration of safety, where the participant is cognizant of potential hazards that the robot may encounter during its operation, while the emphasis on reaching the goal within a specified time frame suggests an awareness of ensuring that the robot remains active and progresses towards its objectives.
Discussion
6.1
Validation Accuracy
These findings suggest that formal specifications are not inherently human interpretable for validation and that inciting further cognitive engagement with required trajectory generation not a sufficient mechanism for improving interpretability over single session. While all conditions proved better than random chance, the operational significance of accuracy rates of between 60 and 70 percent for system validation would be unacceptable for most operational use cases of automation.
Our results indicated while tasking users to perform trace generations meeting specifications as step in performing system validation increases their time of engagement in the process, this step does not consistently improve task performance. While the validation question is asking users consider all possible trajectories allowed by a specification the process of generation may overly draw their focus to certain subset of the decision space.
The two active learning conditions may be improving the performance of participants with lower initial STEM experience (Figure 2 in comparison to the control, which would match previous work showing a dependence of active learning effects on initial levels of related experience [31 30), but there are too few low-STEM STEM-experience participants in our control group to test this hypothesis.
As noted by Vinter (39. individuals have difficulty working with formal specifications in myriad of ways and have a variety of preferences for specifications' verbosity. In our post-experiment commentary, 4 subjects noted trouble with operator nesting. The question with the lowest performance (32% correct) had a negation operator. Yet, other questions that included negation operators with equivalent or lower length and AST depth- - had typical correctness rates. While stringing concepts together, managing nested structures, and handling negation operators seem to present challenges, the impact of these factors on interpretability remains unclear. Our data do not provide sufficient support for conclusions about the causes or categories of these difficulties, though other works such as that by Booth et al. 3 examines the relationships between specific qualities of logical statements and human interpretability more directly. Exploration of various STL constructions on interpetability in conjunction with active learning practices could yield more nuanced insight into human comprehension of STL specifications.
Overall, the literature advocating for the use of formal methods for XAI seems to be dramatically underestimating usability issues, as well the informational needs of users. We note, however, that our particular choice of system validation as the goal of interpretability places particularly high informational need on the human, as prediction of all consequences of the policies must be accounted for [36].
6.2 Giving Up
The forced engagement of active learning notably frustrated participants. matching with common student feedback from educational settings despite improved performance [34 77 and in AI reliance studies where engagement elicited negative participant ratings despite more appropriate reliance levels 44. The most expressions of frustration came from the AL-NF group, which may be because there is increased workload, but not increased feedback. In contrast, the minimal expression of frustration and confusion from the AL-WF condition may be due part to the fact that frustrations were assuaged by the positive feedback subject received with successful saving of trajectories and

---

hints provided with negative feedback of failed saves. This result hints at way to improve user engagement and minimize frustration while maintaining potential active learning benefits.
6.3 Limitations
A limitation of this work is the relatively abstract setting of the validation scenario. In order to construct a concrete test case, we used a grid world and took set of "game-winning conditions" as the participants' intent, acting though they could not be easily codified. Having specific, simple set of "user intents" was required to ensure the objectivity of the validation ground truth. real-world setting would likely have more complex world dynamics, but also a more ill-defined set of stakeholder intentions that are actually difficult to translate appropriately to policies.
Another limitation, and a difference between this work and much of the active learning literature, that we are limited a single session of learning and testing. Studies exist that both show [ and do not show
33 a positive effect of active learning in single session, and much of the work
in this space showing strong effects over the course semester or more [[] [6]. may be that active learning only shows difference with the control condition over those periods, so multi-session studies should be conducted in the future.
Finally, our participants had a range of experience with formal methods, and included many complete novices, which would presumably not be the case with any operational validation scenario. However, previous work showed that formal methods expertise increases confidence in validation substantially, but only increases accuracy slightly, and critically, decouples accuracy from confidence (38). A more useful demographic to have here would likely be participants who are familiar with the task domain, though as previously noted, that would require a more defined validation task.
6.4 Implications and Recommendations
An observation about the approach towards validation is that the thought process is one of predicting and finding edge cases: situations in which the requirements are met, but the intent is violated. The more aligned the two are, the rarer these cases. This framing perhaps points to ways to ameliorate the situation, which some participants did indeed realize (Section 5.4). On the human side, priming and training in finding cases such cases may be useful, which may be explored in future work. Future experiments might also consider whether whether people trained in finding edge cases (e.g. lawyers, compliance officers, forensic accountants, etc) may perform better than laypeople or formal methods experts in checking formal policies. From the machine side, we may consider whether procedures that automatically show edge cases to human examiners may be helpful. Here, STL's quantitative semantics are attractive, as a diverse set of minimally-robut trajectories could represent conceptual edge cases that are worth examining, and may be generated automatically.
Similar 38 we again find that the common claims of formal methods interpretability to be unfounded for the issue of validation. Indeed the continued claims of "interpretable" methods without definition or evidence is akin claiming "accurate" learning methods without providing accuracy measures. These unsubtantiated and poorly-defined claims can have significant negative societal impact, as both researchers and potential users are driven towards unsupported methodologies. We recommend that the community define their claims more specifically, and provide evidence that the claims are met. At the same time, it is clear that interpretability cannot simply be considered from technological perspective - the needs of the user in the specific task context are of paramount importance, and is an underexplored area where significant improvements can be made (36).
7 Conclusion
This study is the first to our knowledge that attempts to unite research in human learning formal specification validation. Under conditions of just examining a specification, using active learning via trajectory generation, or using active learning with feedback on generated trajectories, all conditions are significantly better than random, but no condition is significantly different from any other, with an overall validation accuracy of 65% + 15%. These results continue to call into question common claims that formal specifications are inherently humann-nterppettable Further intervention and design of validation procedures on both human and machine sides are necessary to understand what methods actually work for the validation task, requirement for robot reprogramming after deployment.
10

---

References
[1] Divya Asok, A.M. Abirami, Nisha Angeline, and Raja Lavanya. Active Learning Environment for Achieving Higher-Order Thinking Skills in Engineering Education. In 2016 IEEE 4th International Conference on MOOCs, Innovation and Technology in Education (MITE), pages 47-53, Madurai, India, December 2016. IEEE.
[2] Charles C Bonwell and James A Eison. Active learning: Creating excitement in the classroom. 1991 ASHE-ERIC higher education reports. ERIC, 1991.
[3] Serena Booth, Christian Muise, and Julie Shah. Evaluating the Interpretability the Knowledge Compilation Map: Communicating Logical Statements Effectively. In Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, pages 5801-5807, Macao, China, 2019. International Joint Conferences on Artificial Intelligence Organization.
[4] Zana Buçinca, Maja Barbara Malaya, and Krzysztof Z Gajos. To trust or think: cognitive forcing functions can reduce overreliance on ai in ai-assisted decision-making, Proceedings of the ACM on Computer Interaction, (CSSCW1):-221,, 2021.
[5] Stephen SO Burgess, Mark Kranz, Neil E Turner, Rachel Cardell-Oliver, and Todd E Dawson. Harnessing wireless sensor technologies advance forest ecology and agricultural research. Agricultural and Forest Meteorology, 150(1):30-37, 2010.
[6] Alberto Camacho and Sheila A Mcllraith. Learning interpretable models expressed in linear temporal logic. In Proceedings of the International Conference on Automated Planning and Scheduling, volume 29, pages 621-630, 2019.
[7] Vincent E. Cangelosi and Gerald L. Usrey, Cognitive frustration and learning. Decision Sciences, 133-4):275-295, July 1970.
[8] Gustavo Cardona, Kevin Leahy, Makai Mann, and Cristian-loan Vasile. A flexible and efficient temporal logic tool for python: Pytelo. arXiv preprint arXiv:2310.087/4 14, 2023.
[9] Harish chaandar Ravichandar, Athanasios S. Polydoros, Sonia Chernova, and Aude Billard. Recent advances robot learning from demonstration. Annu. Rev. Control. Robotics Auton. Syst., 3:297-330, 2020.
[10] Glen Chou, Necmiye Ozay, and Dmitry Berenson. Learning temporal logic formulas from suboptimal demonstrations: theory and experiments. Autonomous Robots, 46(1):149-174, 2022.
[11] IEEE Computer Society. Software Engineering Standards Committee. IEEE Standard for Software Verification and Validation, volume 1012. IEFE, 1998.
[12) Fulvio Corno, Luigi De Russis, and Alberto Monge Roffarello. How do end-users program the internet things? Behaviour Information Technology, 41(9):1865-1877, 2022.
[13] National Research Council, Division on Engineering, Physical Sciences, Board on Mathemat- ical Sciences, Their Applications, Committee on Mathematical Foundations of Verification, and Uncertainty Quantification. Assessing the reliability of complex models: mathematical and statistical foundations of verification, validation, and uncertainty quantification. National Academies Press, 2012.
[14] Jonathan DeCastro, Karen Leung, Nikos Aréchiga, and Marco Pavone. Interpretable policies from formally-speciffeed temporal properties. In 2020 IEEE 23rd International Conference on Intelligent Transportation Systems (ITSC), pages 1-7. IEEE, 2020.
[15] Mary Forehand. Bloom's 's taxonomy. Emerging perspectives on learning, teaching, and technology, 41(4):47-56, 2010.
[16] Scott Freeman, Sarah L. Eddy, Miles McDonough, Michelle K. Smith, Nnadozie Okoroafor, Hannah Jordt, and Mary Pat Wenderoth. Active learning increases student performance in science, engineering, and mathematies. Proceedings of the National Academy of Sciences, (1(23):8410-8411 June 2014.

---

[17] Ben Greenman, Sam Saarinen, Tim Nelson, and Shriram Krishnamurthi. Little tricky logic: Misconceptions in the understanding of Itl. arXiv preprint arXiv:2211.01677 2022.
[18] Serhiy Kandul, Vincent Micheli, Juliane Beck, Markus Kneer, Thomas Burri, François Fleuret, and Markus Christen. Explainable ai: A review of the empirical literature. Available at SSRN 43252/9, 2023.
[19] Guy Katz, Clark W. Barrett, David L.. Dill, Kyle D. Julian, and Mykel J. Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. ArXiv, abs/1702.01 135, 2017.
[20] Fayhaa Hameedi Khlaif and Shawkat Sabah Khairullah. A survey formal verification approaches for dependable systems. ArXiv, 12s22204412913, 2022.
[21] Eun Kim, Xiangmin Fan, and Daniel Mosse. Empowering end users for social internet of things. In Proceedings of the Second International Conference on Internetoof-Things Design and Implementation, pages 71 71-82, 2017.
[22] Martin Leucker and Christian Schallhart. A brief account of runtime verification. The Journal of Logic and Algebruic Programming, 78(5):293-303, May 2009.
[23] Karen Leung, Nikos Aréchiga, and Marco Pavone. Backpropagation for parametric stl. In 2019 IEEE Intelligent Vehicles Symposium (/V), pages 185-192. IEEE, 2019.
[24] Nancy Leveson. Are you sure your software will not kill anyone? Communications of the ACM, 63(2):25-28, 2020.
[25] Sergey Levine, Chelsea Finn, Trevor Darrell, and P. Abbeel. End-to-end training of deep visuomotor policies. J. Mach. Learn. Res., 17:39:1-39:40, 2015.
[26] Danyang Li, Mingyu Cai, Cristian-Loan Vasile, and Roberto Tron. Learning signal temporal logic through neural network for interpretable classification. In 2023 American Control Conference (ACC), pages 1907-1914. IEEE, 2023.
[27] Zachary C Lipton. The mythos of model interpretability: In machine learning, the concept of interpretability is both important and slippery. Queue, 16(3):31-3) 2018.
[28] Wenliang Liu, Danyang Li, Erfan Aasi, Roberto Tron, and Calin Belta. Interpretable generative adversarial imitation learning. arXiv preprint arXiv:2402.10310. 2024.
[29] Martin Loomes and Rick Vinter. Formal methods: No cure for faulty reasoning. In Safer Systems: Proceedings of the Fifth Safety-critical Systems Symposium, Brighton 1997, pages 67-78. Springer, 1997.
[30] Danielle McNamara. Self-explanation and reading strategy training (sert) improves low- knowledge students' science course performance. Discourse Processes, 54(7):479-492, 2017.
[31] Danielle S McNamara and Jennifer L Scott. Training self explanation and reading strategies. In Proceedings of the Human Factors and Ergonomics Society Annual Meeting, volume 43, pages 1156-1160, SAGE Publications Sage CA: Los Angeles, CA, 1999.
[32] Tim Miller, Piers Howe, and Liz Sonenberg. Explainable ai: Beware of inmates running the asylum or: How learnt to stop worrying and love the social and behavioural sciences. arXiv preprint arXiv:
2017.
[33] Tenaha O'Reilly, Rachel Best, and Danielle S McNamara. Self-explanation reading training: Effects for low-knowledge readers. In Proceedings of the annual meeting of the cognitive science society, volume 26, 2004.
[34] David C Owens, Troy D Sadler, Angela T Barlow, and Cindi Smith-Walter Student motivation from and resistance to active learning rooted in essential science practices. Research Science Education, 50:253-277, 2020.
12

---

[35] Rohan Paleja, Andrew Silva, Letian Chen, and Matthew Gombolay. Interpretable and personal- ized apprenticeship scheduling: Learning interpretable scheduling policies from heterogeneous user demonstrations. In H. Larochelle, M. Ranzato, R. Hadsell, M.F. Balcan, and H. Lin, editors, Advances in Neural Information Processing Systems, volume 33, pages 6417-6428. Curran Associates, Inc., 2020.
[36] Lindsay Sanneman and Julie A Shah. The situation awareness framework for explainable ai (safe-ai) and human factors considerations for xai systems. International Journal of Human- Computer Interaction, 38(1 (8(18-20):1772-11233
2022.
[37] Joe Saunders, Dag Sverre Syrdal, Kheng Lee Koay, Nathan Burke, and Kerstin Dautenhahn. "teach me-show end-end-user personalization of smart home and companion robot. IEEE Transactions on Human-Machine Systems, (6(1):27-40) 2015.
[38] Ho Chit Siu, Kevin Leahy, and Makai Mann. Stl: Surprisingly tricky logic (for system validation). In 2023 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 8613-8620. IEEE, 2023.
[39] RJ Vinter, MJ Loomes, and D Korbrrot Seven lesser known myths of formal methods: uncovering the psychology of formal specification. 1996.
[40] Michel Weike, Kai Ruske, Reinhard Gerndt, and Tobias Doernbach. Enabling untrained users to shape real-world robot behavior using an intuitive visual programming tool human-robo interaction scenarios. In Proceedings of the 2024 International Symposium Technological Advances in
Interaction, pages 38 46, 2024.
[41] Regina MF Wong, Michael Lawson, and John Keeves. The effects of self-explanation training on students' problem solving in high-school mathematics. Learning and Instruction, 12(2):233-262, 2002.
A
Appendix
A.1 Signal Temporal Logic for Programming Autonomous Systems and Representing Behavior
The Signal Temporal Logic (STL) language specifies temporal properties of real-valued signals using signal predicates. A signal predicate is in the form fx((t) > a, where x(t) represents a signal that must follow the conditional specified within the predicate (i.e., larger than a). The syntax of signal temporal logic (STL) is formally defined as an aggregation of these primitives and temporal operators:
:: A F/GrygFielloUp
Here, the range = b] represents a time interval where the logic must hold True. G represents the Global operator, F represents the Finally operator, and U represents the Until operator. Formally,
At time if Gr((p) holds, then holds VI in L I.
At time f, if (1p) holds, then yp holds at some 1' f. Et+
At time t, if pUp'p' holds, then yp holds some time e + and Vt" e [t, t')'' holds.
Given an STL specification (i.e., a composition of formula and operators), set of acceptable robot behavior can be created. Our paper is concerned with helping users understand the set of possible behavior and allowing them ensure whether this set meets their specifications. For simplicity, we only use the F and G operators in this study, and not the U operator.
13

---

A.2
Specification Specifies
All specifications were expressed as location constraints. The basic structure of these constraints involved spatial variables X and Y, representing grid squares in the ManueverGame 2D gridworld. The relational operators <, ",>, 2, and = were employed to define spatial relationships. These atomic propositions were then combined using the following logical and temporal operators propositional logic operators: AND (Conjunction), OR (Disjunction), NOT (Negation) and temporal operators ALWAYS and EVENTUALLY. Time constraints were defined using language, specifically stating the intervals with the phrase "from time A to time B" for each temporal predicate. The logical and temporal operators were expressed in their linguistic form rather than symbolic notation. The resulting specification was ultimately of the form of STL, but with some increased clarity to those unfamiliar with STL.
All specifications were formulated as absolute positions rather than relational ones, which was intended make the task nontrivial (otherwise, statements such as "Eventually distance from goal 0 AND Globally distance from hostile > 2" could be used). The complexity of specifications was varied and measures of AST depth and specification length were captured. However, did not produce further classification of specification difficulty due to the ambiguity inherent to this this task. complete list of the specifications presented subjects is provided in the supplementary material.
A.3 Subject Introduction Process
Subjects were first introduced to the experiment through a series of short video clips that described the experiment flow, accompanied by supporting text-based tutorial. Subjects were introduced to the ManeuverGame interface and the rules of the game through a web-based tutorial integrated with the ManeuverGame software suite.
The introductory material gives clear visualizations of winning conditions and various loss conditions (the robot not reaching the goal within the time bound or the robot being "tagged" by the opponent).
The introduction section also provided explanations of STL notation and examples of creating trajectories that satisfy STL specifications. Concept check questions were provided to ensure participant understanding of the game mechanics, specification notation and the validation task. Additionally, practice validation questions were provided to give users practice interacting with the ManueverGame interface and experiment validation procedure.
A.4 Formal Methods Familiarity Representation and Analysis
Responses to the question of formal methods experience were recoded instances where participants' open-ended explanations showed that they did not actually understand what formal methods meant. In these instances we exclusively reduced the level of coded familiarity.
Formal methods familiarity was not found to be significant with either the original nor recoded values in the omnibus tests nor the post-hoc rank order correlation in Figure 4 However, formal- methods experts were underrepresented in our subject pool with the mean and standard deviation of participants' self-reported familiarity rating after recoding being 2.00 out of 5 1.26 and only 7 participants with self-rated familiarity > 3.
A.5 Statistical Models and Analysis
mixed-effects regression examined the participant based predictors of familiarity with formal methods, STEM experience, level of education and experiment condition with overall validation performance serving as the response variable. The regression was followed by independent two- sample t-tests for categorical variables, or Spearman's correlation for continuous variables if the omnibus returned significance.
Omnibus logistic regression analysis was performed on by-question basis with participant- based predictors of familiarity with formal methods, STEM experience, level of education, experiment condition as well as specification-basee predictors of specification ground truth validity, question sequence number, specification AST depth, specification symbol count and response variable of validation correctness.
14

---

Formal Methods Familiarity vs. Validation Score
10
Points
r= 0.196
0.209
self-reported familiarity with formal methods
Figure 4: Formal Methods Familiarity vs. Validation Score. Horizontal jitter was added to visually separate points. Displayed and p values were calculated using Spearman's 's coefficient but linear fit is shown.
Confidence when Correct and Incorrect by Condition
Active Learning without Feedback
Active Learning with Feedback
Control
p =
0.04 d 0.35
p 0.03 0.18
p 0.24
Confidence
2-
1.
Correct
Incorrect
Correct
Incorrect
Correct
Incorrect
Figure 5: Participant confidence in their answer when their answer was actually correct incorrect,
split by experimental condition.
A.6 Confidence Analysis
An examination of variance equality for confidence ratings yielded non-significant result (p 0.313). Independent t-tests between confidence values when responses were correct or incorrect (Figure indicated users' confidence not significantly different based on the correctness of their answer in any the conditions. The effect size the active learning without feedback condition is moderate though not significant with the Bonferroni threshold (Figure 5 p 0.040 > 0.05/3 0.016). Active learning without feedback could be a promising mechanism to improve users' confidence calibration.
Participants' average score across entirety of the experiment also did not appear to significantly correlated with their overall performance 7 Note the correlation between confidence and overall performance for control group was moderately positive though not significant with the Bonferroni correction (Figure 0.55, .05 0.05/3 0.016).
15

---

Participants' Confidence vs. Experience by Response Correctness
Correct
Incorrect
Confidence
0.320
0.030
0.0003
STEM Experience
STEM Experience
Figure 6: Participants' Average Confidence STEM Experience when Correct and Incorrect. Horizontal jitter is shown to visually separate points. The correlation was calculated using Spearman's coefficient, but a linear fit is shown.
Average Confidence vs. Score by Experimental Condition
Active Learning without Feedback
Active Learning with Feedback
Control
7-
Average Confidence
p 0.23
p
p
6-
2
2
6
10
2
3
7
Score
Score
Score
Figure Subject's average confidence across questions vs total validation score for each of the experimental learning conditions. A linear fit is shown but correlations were calculated using Spearman's coefficient. All the correlations were positive but none were found to significant with the Bonferroni correction (a 0.05/3 3 0.016).
There is a significant positive correlation between STEM experience and average confidence both when the question was answered correctly and incorrectly (Figure 6 The correlation is stronger on questions that were answered incorrectly (Figure r 0.530, 0.003) compared to when answered correctly (Figure r 0.320, p 0.03). Those with experience STEM fields may be more confident in their responses, but such confidence is substantiated by better performance.
A.7
Giving Up
The determination for giving was based upon users time spent completing the experiment as well their interaction with the experiment interface. Due the differing requirements subjects, different criteria were used to determine who gave up. The following criteria were applied to subjects in the three conditions:
Control:
< minute spent per question average
Active learning (no feedback):
2 minutes per validation question on average OR
at least 3 questions were answered with extremely short, nonsensical trajectories (e.g. < 3 time steps)
Active learning (with feedback):
16

---

2 minutes per validation question on average OR
choosing to give up (on the interface) on three or more questions
17

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: We claim that the evidence for single-session active learning helping people with system validation is lacking. Our data show the same.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or
NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
is fine to include aspirational goals as motivation as long as is clear that these goals are not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations the work performed by the authors?
Answer: [Yes]
Justification:
See discussion in Section 6.3
Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create separate "Limitations" section their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g.. independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution is low images are taken in low lighting. Or speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness.
While the authors might fear that complete honesty about limitations might used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't 't acknowledged judgment and recognize that individual actions in favor of transparency play impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
the paper. The authors should use their best
3. Theory Assumptions and Proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [NA]
18

---

Justification:
We do not present theoretical results.
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced the statement of any theorems.
The proofs can either appear the main paper or the supplemental material, but they appear in the supplemental material, the authors are encouraged to provide short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental Result Reproducibility
Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Question:
Answer: [Yes]
Justification: We present our methods in the paper and the information presented to subjects supplemental materials.
Guidelines:
The answer NA means that the paper does not include experiments. If the paper includes experiments, No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is novel architecture, describing the architecture fully might suffice, or if the contribution is a specific model and empirical evaluation, it may be necessary to either make possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g.. in the case of large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily a new algorithm, the paper should make it clear how reproduce that algorithm. (b) If the contribution is primarily
model architecture, the paper should describe the architecture clearly and fully.
(c) If the contribution is a new model (e.g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome describe the particular way they provide for reproducibility, In the case of closed-source models, it may be that access to the model is limited in some way (e.g., registered users), but it should be possible for other researchers to have some path to reproducing or verifying the results.
5. Open access to data and code
Question: Does the paper provide open access to the data and code, with sufficient instruc- tions to faithfully reproduce the main experimental results, as described in supplemental material?
19

---

Answer: [No]
Justification: While we believe we provide sufficient information to faithfully reproduce the main experimental results in our Methods section, we are not currently releasing the raw experiment data or code due to time constraints on ensuring removal of personally- identifiable information in the data, as well =code cleanup. We plan to release at least the experiment code before the end of the calendar year.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines (kttps://nips.co cc/
mublic/guides/ htaia///uuides/ooeeuubiiiss
for more details.
While encourage the release of code and data, we understand that this might not be possible, so "No" is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurIPS code and data submission guidelines (https
/ ptaips.cc/publii/guuudessss/ Cote://mdeeeSbmmiiiaa ssi onPolicy) for more details.
The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. only subset of experiments are reproducible, they should state which ones omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing much information possible in supplemental material (appended the paper) recommended, but including URLs to data and code permitted.
6. Experimental Setting/Details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary understand the results?
Answer: [NA]
Justification: The paper is about experiments, but not of the machine learning variety.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, as supplemental material.
7. Experiment Statistical Significance
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer: [Yes]
Justification: We present data distributions individual data points, box plots, and means and standard deviations where appropriate. Individual points and box plots allow us to avoid the assumption that the data symmetric, assumption that typical error bars make. We further report all our statistical testing on the data.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by emor bars, confi- dence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper.
20

---

The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).
should be clear whether the error bar is the standard deviation or the standard error of the mean.
OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that out of range (e.g. negative error rates).
If error bars reported in tables plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables the text.
8. Experiments Compute Resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time execution) needed to reproduce the experiments?
Question:
Answer: [NA]
Justification; The experiment was not primarily computational nature. While computation was required to run the human experiments and to perform runtime monitoring, such requirements were minimal, our policies were extremely small.
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs as well estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't make it into the paper).
9. Code Of Ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics httppp////nrrips....pppbtttttttt
Answer: [Yes]
Justification: We follow all NeurlPS ethical guidelines - in particular, our human experi- ments are appaappo with no notable risk of harm, and our subjects are appropriately compensated for their time.
Guidelines:
The answer NA means that the authors have reviewed the NeurIPS Code of Ethics.
If the authors answer No, they should explain the special circumstances that require a deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g., there a special consid- eration due to laws or regulations in their jurisdiction).
10. Broader Impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [Yes]
21

---

We describe the potential negative impacts of unsubstantiated claims of explainability, and point to some potential avenues of alleviating these issues for the system validation context. See Section 6.4
Justification:
Guidelines:
The answer NA means that there no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g.. deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology.
If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition attacks, mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility of ML).
11. Safeguards
Question: Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g.. pretrained language models, image generators, or scraped datasets)?
Answer: [NA]
Justification:
We do not release models.
Guidelines:
The answer NA means that the paper poses such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards is challenging, and many papers do not require this, but encourage authors to take this into account and make best. faith effort.
12. Licenses for existing assets
Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [Yes]
Justification: We credit the authors of the code used to calculate robustness in our monitor software in the Methods section.
Guidelines:
The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package dataset.
22

---

The authors should state which version of the asset is used and, if possible, include URL.
The name of the license (e.g., CC-BY 4.0) should be included for each asset. For scraped data from a particular source (e.g.. website), the copyright and terms of service of that source should be provided.
If assets released, the license, copyright information, and terms of in the package should be provided. For popular datasets, paperswi thcode com/ datasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if has changed) should be provided. this information not available online, the authors are encouraged to reach out to the asset's s creators.
13. New Assets
Question: Are new assets introduced in the paper well documented and the documentation provided alongside the assets?
Answer: [NA]
Justification:
We do not release new assets.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/code/model as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent obtained from people whose asset is used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsourcing and Research with Human Subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well as details about compensation (if any)?
Answer: [Yes]
Justification:
See Methods section and supplemental materials.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information
supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included the main paper.
According to the NeurIPS Code of Ethics, workers involved in data collection, curation, other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional Review Board (IRB) Approvals or Equivalent for Research with Human Subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [Yes]
Justification: See methods section for IRB information. No specific risks to subjects were expected reported.
Guidelines:
23

---

The answer NA means that the paper does not involve crowdsoureing nor research with
human subjects.
Depending on the country in which research is conducted, IRB approval (or equivalent)
may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and expect authors adhere the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review.
24


Reviews:
[{"review_id": "EzRRd4r6mz", "reviewer": "Reviewer_QXA3", "summary": "This paper examines the challenges of using Signal Temporal Logic (STL) for validating autonomous systems and finds that human validation accuracy remains loweven with active learning techniques. Using the ManeuverGame interface, the study tests three conditions—no active learning, active learning, and active learning with feedback—finding no significant improvement in validation performance. The research highlights the need for better validation techniques and human-computer interaction to enhance human interpretability and validation of STL-specified policies.", "questions": "Please refer to the weakness part:\n\n1. Justify why we need human supervision.\n\n2. Explain the criticism against interpretability.", "limitations": "This is about user-study which has no potential negative societal impact.", "rating": 5, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. The study employs a well-structured experimental design using the ManeuverGame interface, which effectively simulates real-world validation scenarios. This allows for a thorough assessment of human validation performance across different conditions\n\n2. The research provides valuable empirical evidence showing that active learning does not significantly enhance human validation accuracy, remaining around 65\\%. This insight is crucial for understanding the limitations of current formal methods in practical applications.\n\n3. The study highlights the cognitive challenges faced by humans in interpreting and validating STL-specified policies, pointing out areas for improvement in human-computer interaction.", "weaknesses": "1. In my understanding of formal method, if you want to verify a rather high-level specification (which I assume is what the authors mean by 'validate'): You either directly use a formal method enhanced synthesis for your policy (which is easily doable for their maneuver case study) or use model checking (which depends on what policy we care about), and no human supervision should be necessary. Could the author justify that?\n\n2. I think the criticism against interpretability is unfounded: They are not showing how they are interpreting the formulas for the users (which they can certainly do better with existing online monitors) and I think this is unfair for people who actually spend a lot of time developing monitors that are interpretable (such as the robust online monitors). Plus, few papers on monitoring are cited, which makes the paper seem to lack of comparision.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Human Supervision (Weakness 1, Question 1)\n\nWe appreciate the reviewer's comment regarding the lack of necessity for human supervision in our experiment and acknowledge that model checking could be used given the the concreteness of our objectives. As described in lines 155-158 of the manuscript, we wished to simulate real-world scenarios where human judgment is indispensable, particularly with stakeholder intents that are not easily codified into formal specifications. In the text, we explicitly acknowledge the reviewer's concern, but note that the task is a stand-in for the aforementioned human judgement scenarios. Unfortunately, without presenting to the user a task that can be checked automatically, we cannot objectively check the user's ability to evaluate the specification. Participants' failure to correctly understand the specifications in the context of the task is indicative of the difficulty they would encounter in more ambiguous and/or complex cases (line 158).\n\nWhile methods like model checking and  synthesis are indeed powerful, they fall short in capturing complex, context-dependent intents for autonomous systems, such as \"navigate safely\" or \"maintain user trust\". Where verification asks the question  \"does this product/behavior match with the set of requirements set out for it\"... validation probes \"does this product operate in and only in the ways that I want it to?\" In our experiment, \"winning\" serves as an objective stakeholder intent that can be codified in programming. This stands in for the more complex and less easily codified intents that robotics stakeholders often have and allows us to explore the limitations and challenges of human validation in a controlled environment, providing valuable insights that are applicable to more complex, real-world tasks.\n\nFor example, in an autonomous driving scenario it can be verified that a car is able to obey posted speed limits and this behavior can be verified in real time. However, validating that a vehicle is operating safely, obeying the flow of traffic, and properly responding to other drivers' intentions to merge are behaviors critical to its safe deployment that cannot so easily or directly be quantitatively checked. \n\n\nCritique of Interpretability (Weakness 2, Question 2)\n\nWe acknowledge the point regarding the our critique of interpretability claims and recognize the important work of researchers developing robust online monitors, such as Deshmukh et al. (2017), Zhang et al. (2023). However, upon review of such work, we still do not find empirical evidence that users performing interpretation are able to do so well using these systems. Such evidence cannot simply be provided in a software-only context without human studies. If the reviewer can point us to human studies with users interpreting formal specifications that demonstrate system usability, we would be happy to incorporate them into our discussion.\n\nOur findings indicate a gap in testing these systems with human participants to support interpretability claims. While many works have these claims (e.g. line 89), few support them with evidence from humans studies. This is not to say that existing efforts do not present interpretable techniques, but rather that there is a pressing need to validate these claims of interpretability with human operators, as argued by Miller et al. (2017) [28].\n\nMoreover, our study included a monitor in the third condition (active learning with feedback) where the robustness of users' trajectories was checked when users marked them as complete. Trajectories with negative robustness could not be saved and users were alerted that their submission was invalid and prompted to retry. However, our subject pool did not show significant improvement in validation performance even with this support. \n\nWe wish to emphasize the distinction between asserting a system's interpretability based on theoretical design principles and demonstrating it through empirical testing with human users. While theoretical claims rely on design principles to suggest interpretability, it is the empirical evaluation that provides concrete evidence of whether users can effectively understand and use the system. Even systems that appear to be interpretable at first glance, such as decision trees or translation into natural language, may not be actually interpretable, as shown in [33] as well as in Vinter et al. (1996) and Loomes and Vinter (1997), particularly for the difficult task of system validation, which requires understanding all potential edge cases.\n\nThe evidence we found and cited (lines 38-41, 92-98), along with Vinter et al. (1996) and Loomes and Vinter (1997) which actually involved users, point to a preponderance of evidence that methods claimed to be interpretable in the academic literature are often not so when users interact with them. If the reviewer is able to point us to user studies that demonstrate the interpretability of monitors (or other formal methods tools) that are designed to be human-interpretable, we would happily consider them in the context of this experiment.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "LksfUtkAcb", "reviewer": "Reviewer_67SW", "summary": "The paper presents the results of a human study exploring the intuitiveness and interpretability of formal logic—in this case, signal temporal logic (STL)—in expressing policies for autonomous systems. Specifically, the authors study the effect of active learning, a pedagogical approach for human learning, on understanding the semantics of STL. The experimental results show that active learning, with or without feedback, provides no significant improvement, and STL remains a challenging logic for humans to understand.", "questions": "- Would similar results be observed if natural language were used to express specifications? For instance, the specifications in Figure 1 do not have any STL-specific features that would complicate understanding.\n- Is it possible that participants' performance resulted from a lack of familiarity with the experimental setup rather than with the logic?\n- Which aspects of the logic do participants find challenging: modalities, time-tracking, or nesting of the operators?\n- How did the authors choose the class of specifications? Are they known to be particularly challenging, or do they express some practically relevant requirement?", "limitations": "The paper presents a human study to better understand the role of STL in interpreting robot policies. The study involved three groups of participants, differing in the active learning received. The results show no major differences in performance among these groups. While the user study is clearly of interest, it is not clear if natural language would have been a better candidate for the same task. It appears that the key challenge lies in understanding a conjunction of requirements and their effects.", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "+ The problem of understanding the role of formal logic in interpretable control is well motivated.\n+ The experimental setup, ManeuverGame, and the corresponding logic STL seem appropriate for the study.\n+ The user study appears to be well designed, with appropriate IRB approval.\n+ The results are surprising, especially regarding moderate changes in the results with respect to the formal methods/STEM background of the participants.", "weaknesses": "- In the absence of a list of exact formal specifications used in the study, it is difficult to understand why participants found it challenging to validate the specifications.\n- It is unclear whether the exercise tested participants' understanding of the domain or the logic.\n- The exact challenges in understanding STL are not clearly discussed.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "List of Specifications Used (Weakness 1)\n\nWe have included a full list of specifications and corresponding maps in the rebuttal's attached PDF. To clarify the nature of these specifications in the context of STL, we offer the following:\n\nAll specifications were expressed as location constraints. The basic structure of these constraints involved spatial variables X and Y, representing grid squares in 2D gridworld. The relational operators $<, >, \\leq, \\geq,$ and $=$ were employed to define spatial relationships. These atomic propositions were then combined using the following logical and temporal operators propositional logic operators: AND (Conjunction), OR (Disjunction), NOT (Negation) and temporal operators ALWAYS and EVENTUALLY.\n\nAll specifications were formulated as absolute positions rather than relational ones, which was intended to make the task nontrivial (otherwise, statements such as \"Eventually distance from goal = 0 AND Globally distance from hostile > 2\" could be used). While these specifications were intended to be relatively simple, the low rates of validation observed suggest that more intricate real-world systems, would likely encounter even more significant challenges. In examining the specific difficulties faced by subjects, a variety of failure causes were identified. Negation was highlighted as a significant challenge during the think-aloud portion of the experiment. Nesting was highlighted by 4 users in their post-experiment commentary as a challenge. Among the four specifications with the lowest performance (each with accuracy <50 percent), the main challenges presented by these specifications included time constraint alignment, operator coordination, negation handling, and nesting complexity. \n\nSubjects' Domain Knowledge vs STL Knowledge (Weakness 2 and Question 2)\n\nWe acknowledge the concern about the experimental setup testing participant's understanding of the experiment domain or the STL logic. The experiment utilized a gridworld representing a capture-the-flag scenario, chosen for its familiarity to a wide range of users. To address potential gaps in understanding, we included a comprehensive introductory section that thoroughly explained the game domain and its dynamics. This section typically required at least 20 minutes for most users to complete and featured a combination of text and animated explanations. This introduction not only provided text and animation explanations, but also interactive quizzes to ensure users correctly understood the game rules before they began gameplay. These quizzes evaluated users' understanding of movement through the gridword, all win and loss conditions, use of STL logic within the capture the game scenario, as well as use of the interface. All questions had to be correctly answered before subjects were able to progress through to the experiment task. Static versions of introductory material and quizzes are provided in the original supplementary material. \n\nChallenges in Subjects' Understanding (Weakness 3 and Question 3)\n\nWith regards to exact challenges in subjects' understanding of STL, our experimental format, which evaluated participants on only 10 specifications in the course of a single session, did not allow for in-depth analysis of the specific challenges they encountered in understanding the specifications. The work of Vinter et al. (1996) and Greenman et al. [15] which address the cognitive challenges people encounter in working with formal logic included much longer periods of evaluation such as over the course of multiple academic years. We appreciate the reviewer's observation that \"the key challenge lies in understanding a conjunction of requirements and their effects.\" It appears that many subjects struggled with evaluating the STL formulas due to misinterpretations of how different clauses, involving time and operator types, interact with one another. Future work expanding to a multi-session setup would allow for better understanding of specific challenges. \n\nTranslation into Natural Language (Question 1) \n\nWe acknowledge the reviewer's perspective regarding the potential benefits of translating formal methods into natural language for enhanced human interpretability. This viewpoint resonates with the initial intuition shared by the authors and many others in the field. However, we opted not to pursue language translation based on the findings from Vinter et al. (1996) and Vinter (1998). Their research revealed that specifications articulated in natural language—even those incorporating logical operators—can provoke systemic biases. Readers often revert to heuristic reasoning, which is common in everyday language use, rather than engaging in the logical reasoning that formal methods require during evaluations.\n\nConsequently, we believe that if natural language were employed to express specifications, subjects would likely make errors with similar or even greater frequency, albeit for slightly different reasons. The reliance on heuristic reasoning could lead to misinterpretations, undermining the very clarity and precision that natural language is intended to provide.\n\nFamiliarity with Domain (Question 2) (See Subjects' Domain Knowledge vs STL Knowledge, above)\n\nChallenging Aspects of Logic (Question 3) (See Challenges in Subjects' Understanding, above)\n\nChoice of the Class of Specifications (Question 4) \n\nWe chose the class of specifications and the scenario because gridworld movement (in our small environment) was something that we felt subjects could easily grasp. This assumption was validated by our pilot studies as well as by subjects' ability to answer questions in the introductory period that checked for their domain understanding. The simplicity of the validation task was a point of comparison against more complex and ambiguous validation tasks, which would be more difficult to perform. Poor performance here would likely indicate an inability to validate more real-world tasks (lines 155-158).", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "ZeQmu0w59q", "reviewer": "Reviewer_14rd", "summary": "This paper studies the claim of Signal Temporal Logic (STL) specifications being human interpretable and provides results from an experiment with human participants studying a potential active learning technique to improve explainability metrics. Results show that while human engagement is improved, system validation score changes are negligible.", "questions": "1. While the claim that STL is directly human interpretable can be brought into question, does it provide a useful middle ground towards interpretability for task descriptions? Could an STL specification be fed into a Large Language Model (LLM) tool to yield a description more favored by human participants? To this reviewer, intuitively,  a temporal logic specification is often more readable than any general neural network policy (viz. model parameters) or say a few “desired” trajectory samples.\n2. The example specification in Fig. 1 has several different time intervals considered (4 to 12, 15 to 30, etc). This may hinder “human interpretability” significantly as the user may need to parse the trajectories multiple times. Have different measures of difficulty been considered in the study such as a common set of time periods among the specifications or reduced number of AND clauses? A description of these difficulty classes may yield answers towards what parts of STL are difficult for the users.", "limitations": "- Primarily stated as a “negative result” paper, while showing that active learning may not help STL interpretability scores, a solution is not discussed.\n- STL specification difficulty classes were not defined or considered.", "rating": 4, "confidence": 3, "soundness": 2, "presentation": 3, "contribution": 1, "strengths": "The paper is written well and tackles an important topic that is ignored by many papers in STL and other temporal logics which claim human interpretability.", "weaknesses": "- The reviewer feels that this study, while important, may be a better fit for a more specialized venue.\n- The paper provides a study on the (mostly) unhelpful effects of active learning on the performance of the subjects (Table 1) but does not clearly indicate the usefulness of this knowledge or whether it significantly contributes to the community beyond what is already presented in [15, 33].", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Fit for NeurIPS (Weakness 1)\n\nAs the reviewer notes, our work tackles an important topic that is ignored by many studies in logic: validation of behavior via interpretable specifications. The implications of our work relate broadly to logic and XAI, and future work in this area will improve human-AI/human-robot interaction with logic-based systems. NeurIPS specifically has had a variety of work that employs formal logic, such as the following:\n\n- Differentiable Learning of Logical Rules for Knowledge Base Reasoning by Yang et al. (NeurIPS 2017)\n\n- Logical Neural Networks by Riegel et al. (NeurIPS 2020)\n\n- Interpretable and Explainable Logical Policies via Neurally Guided Symbolic Abstraction by Delfosse et al. (NeurIPS 2023)\n\nAs these works (among others) make interpretability claims about logic-based systems (and were accepted to NeurIPS), our work in empirically checks these claims, is essential. Quoting Professor Michael Carbin from the Charles Isbell NeurIPS 2020 keynote, \"The issue is not just correctness, but understanding the problem across the entire pipeline to understand what correctness is,\" which strongly mirrors our quotation of Professor Nancy Leveson (lines 39-41).\n\nContributions Beyond Greenman et al and Siu et al (Weakness 2)\n\nGreenman et al. is a study performed in a school setting with people trained in formal methods, seeking to understand misconceptions in LTL. While formal methods experts are important stakeholders in the validation process, they are not the only ones who need to understand the implications of specifications. Further, that work is concerned with general misconceptions, rather than the case of system validation.\n\nSiu et al. involved subjects with varying levels of familiarity with STL, but focused on methods that the formal methods and AI community believed were interpretable --- raw formal logic, decision trees, and natural language. That contrasts with the present study as we focus on methods demonstrated by the educational community (lines 104-119), heeding Miller's argument that the XAI community ought to draw from the work of experts in human learning in building our methods. Like Siu et al, our negative result calls into question the frequent claims being made about formal methods interpretability without evidence, and highlights the need to providing empirical evidence to support these claims, but we do so from the perspective that Miller takes.\n\nTranslation into Natural Language (Question 1)\n\nThe idea that a language translation might improve human interpretability seems intuitive, as the reviewer notes. However, much like the \"intuitive\" interpretability of other XAI methods that were not tested with users, close examination of the user study literature showed results to the contrary. We did not explore language translation because earlier findings with user studies (Vinter et al., 1996,  Vinter 1998) and not simply intuition, showed that specifications rendered in natural language evoked inappropriate systemic biases where readers substituted heuristic reasoning (commonly used in language) for logical reasoning (necessary for formal methods).\n\nComplexity of Time Periods (Question 2)\n\nWe agree that varying time intervals and multiple clauses may impact interpretability. We did not consider this kind of complexity, but note that in practice, creating any kind of autonomous system that only uses a single time interval or a minimal number of AND clauses severely limits the range of potential systems under consideration.\n\nNegative Result without a Demonstrated Solution (Limitation 1)\n\nMany papers in temporal logic assume human interpretability without empirical human evidence. While this work is a negative result, future work includes expanding to a multi-session setup in order to better resemble the structure of active learning pedagogy in classroom environments and perhaps also a focus on compliance based professions (lawyers, compliance officers etc.) who may have better training at identifying edge case failures. Moreover, future work should investigate how other machine-based solutions, such as automatically highlighting edge cases, could aid users in developing an accurate mental model of the limits of a specification. We refrain from endorsing a specific solution at this stage, emphasizing that thorough human subject studies are crucial to substantiate any claims about improving interpretability. Pushback against overreach of claims is a natural and appropriate part of the scientific discourse, as argued by in the XAI case by Miller et al, (2017) [28], particularly when others are not checking the claims as we do.\n\nSTL Difficulty Classes (Limitation 2) \n\nWe defined and considered specification complexity by the number of symbols (43 to 97) and the abstract syntax tree depth (3 to 5) (lines 182-184). The data did not support that these factors affected performance (line 242). We could have codified difficulty into classes, though how to classify these is unclear, and we are already using the field's standard measures of complexity. For context, the example in Figure 1 has 46 symbols and an AST depth of 3, an example that is on the simple end of our complexity spectrum. A full set of our specifications and maps is in the supplementary PDF.  \n\nAs noted by the Vinter studies, individuals have difficulty working with formal specifications in different ways and have a variety of preferences for specifications' verbosity. In our post-experiment commentary, 4 subjects noted trouble with operator nesting. The question with the lowest performance (32% correct) had a negation operator. Yet, other questions that included negation operators --- with equivalent or lower length and AST depth --- had typical correctness rates. This underscores the nuanced differences in how participants engage with formal specifications and the complexities associated with various specification constructions.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "TT2zrO8yjB", "reviewer": "Reviewer_d2Sv", "summary": "The paper investigates the efficacy of formal specifications (specifically, Signal Temporal Logic (STL)) for human validation of autonomous systems. The authors distinguish between *verification* (whether an implemented policy adheres to a formal specification of its behaviors) and *validation* (whether the system's specifications align with higher-level goals). They correctly assert that validation is an inherently human-centered and subjective process. While many existing explainable AI methods increase the system's explainability, humans still struggle to validate robot behaviors specified through formal methods. The main question addressed in the paper is *whether active learning methods can improve human performance in validating formal specifications.* \n\nThe paper conducts a comprehensive user study (n=55), dividing participants into three groups: no active learning (control), active learning with no live feedback (AL-NF), and active learning with live feedback (AL-WF). \n\nThe main conclusions can be summarized as follows:\n- There is no significant improvement in validation accuracy with active learning.\n- Active learning increases user engagement, and active learning with feedback reduces user frustration.\n- Active learning appears to have a greater impact on participants with lower STEM experience (sample size was however too small for definitive conclusions.)", "questions": "- Line198: Why the guessed answers were scored as incorrect? This seems to ignore potential role of feedbacks in increasing the chances of making a correct guess.", "limitations": "[As I mentioned in the Weaknesses section] The main limitation of the paper is that the experiments define system success as \"whether an agent can reach a goal in 30 steps\", which is a specific and objective task that can be verified through formal methods like model checking. In contrast, the introduction suggests an interest in higher-level, subjective human-centered goals, which are not directly addressed by the experiments.", "rating": 5, "confidence": 2, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "1. The paper correctly states that most human users are not capable of validating system behaviors using formal temporal specifications. It raises an interesting question about whether active learning methods can improve this capability. The experimental results are valuable as they show no significant improvement over the control group with active learning, which is surprising and definitely calls for further research at the intersection of human learning theories and formal system specification methodologies to bridge this gap.", "weaknesses": "1.  The main weakness of the paper is the mismatch between the claims made in the introduction and the focus of the experiments. The introduction argues that formal specifications are not suitable for explaining whether a system achieves higher-level, human-centered goals. However, the experiments measure the capacity of human users to infer the achievability of formally specified goals, specifically whether an agent can safely reach a goal in 30 steps. This task can be automatically checked using model checking techniques, such as providing the STL specification to a model checker to verify goal satisfaction and produce counter-examples if not satisfied. Although the authors mention this misalignment in the limitations section and correctly state that it is unavoidable to keep the success criteria objective and machine-checkable, the significant mismatch makes it difficult to draw conclusions regarding the efficacy of formal specifications in validating human-centered, higher-level goals. A short discussion of this mismatch in the introduction or later sections would have been beneficial.\n\n2. The introduction and related works sections do not discuss the state-of-the-art techniques for enhancing the validation process of formal temporal specifications. There is already work on improving the interpretability of temporal logic specifications, such as translation to natural language [1] and hierarchical specifications [2].\n\n\n[1] Cherukuri, H., Ferrari, A., Spoletini, P. (2022). Towards Explainable Formal Methods: From LTL to Natural Language with Neural Machine Translation. In: Gervasi, V., Vogelsang, A. (eds) Requirements Engineering: Foundation for Software Quality. REFSQ 2022. Lecture Notes in Computer Science, vol 13216. Springer, Cham. https://doi.org/10.1007/978-3-030-98464-9_7\n\n[2] X. Luo and C. Liu, “Simultaneous task allocation and planning for multi-robots under hierarchical temporal logic specifications,” arXiv preprint arXiv:2401.04003, 2023.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "High Level Objectives and Experiment Setup (Weakness 1 and Limitation)\n\nWe appreciate the reviewer's observations regarding the perceived incongruity between the high-level objectives delineated in our introduction and the specific experimental task employed in our study. Upon reflection, we recognize that there is an opportunity to further elucidate the distinction between verification and validation processes, and better explicate how our experimental paradigm aligns with real-world workflows and the broader implications of validation procedures.\n\nThe experimental task, which involves determining whether a given specification will result exclusively in trajectories allowing the agent to safely reach a goal within 30 steps, can be conceptualized and solved as a verification problem. However, we deliberately framed it as a validation problem, wherein the \"game rules\" of reaching the goal within 30 steps and avoiding the opponent serve as proxies for higher-level, human objectives. This methodological decision was made to facilitate an objective assessment of our hypotheses.\n\nWe acknowledge in the present paper that the utilization of these rules as surrogates for more complex, human-centered goals renders this experimental task equivalent to a verification task which could be solved with verification techniques such as model checking (lines 151-158). Nevertheless, our framing as a validation problem within the experimental setup allows us to explore the nuanced differences between verification and validation processes, particularly in contexts where system goals may be less explicitly defined or more subject to interpretation. This reframing enables us to investigate the cognitive processes and decision-making strategies employed by participants when confronted with a task that, while structurally similar to a verification problem, requires a more holistic evaluation of system behavior against broader objectives. As we note in line 158, the \"validation\" task we present in this study is simple enough that failure to perform well in this context bodes poorly for when it is to be replaced with a less explicitly-defined validation. This approach aligns with the validation challenges often encountered in real-world scenarios, where the assessment of system performance extends beyond mere compliance with specifications to encompass the fulfillment of overarching goals and stakeholder expectations. This work lays important groundwork for future research in bridging formal methods and human-centered validation processes.\n\nTheoretical Interpretability Improvements vs. Empirical Studies (Weakness 2)\n\nWe appreciate the reviewer providing further background works. Our main focus in this work is to fill in the gap in interpretability studies for STL validation that use real human validators. While Cherukuri et al. provides a mechanism for translation into natural language and evaluation of the translation quality with BLEU, we do not find such techniques to be within our scope on account of the fact that their claims for interpretability are not being tested with human subjects thinking through logical implications, but rather with natural language translations, which are not equivalent. Moreover, language translations of formal logic have not been shown to be an effective mechanism for improving human interpretability. Vinter et al. (1996) and Vinter (1998) showed that specifications rendered in natural language (even when containing logical operators) evoked inappropriate systemic biases in which readers substituted heuristic reasoning (commonly used in language) for logical reasoning (necessary for formal methods) during evaluation. This again highlights the difference between simply translating a specification back and forth between natural and logical languages, and correctly understanding the implications of the specifications (in either form). Neither rendering of the specification guarantees appropriate understanding.\n\nThe hierarchical structure for logic specifications presented in Luo and Liu offers an intriguing approach to formal method interpretability; however, the lack of empirical evaluation with human subjects limits our ability to assess its practical efficacy within the context of this work. Moreover, while this work effectively reduces the length of individual formulas, its applicability may be limited in contexts such as ours where formulas are already concise with at most total symbol count under 100 and at maximum 7 temporal clauses. \n\nWe appreciate the reviewer pointing us to recent work on improving the interpretability of temporal logic specifications, but must note that unlike the references we present in lines 38-41, alongside the Vinter work, the reviewer's references involve no human evaluators --- a requirement for making strong claims about human-interpretability. The Cherukuri and Luo works may very well be helpful in improving interpretability, but human evidence of their efficacy is yet to be seen.\n\n\nQuestion on scoring guesses (Question 1)\n\nThe opportunity to guess was only provided to subjects after they choose to \"give up\" and told that their response would be recorded as incorrect. This opportunity was provided following multiple failures to provide trajectories that met the specification as described in lines 196 and 197 of the manuscript.\n\nLimitation\n(See response to High Level Objectives and Experiment Setup.)", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:
We thank the reviewers for their critical assessment of our work. As a note, we appreciate one of the reviewers pointing out that we did not include the example formulas and maps show to subjects. We have included this content in the rebuttal's attached PDF and will also include it in the final manuscript.

Contribution to XAI

This work builds upon Miller et al's (2017) work which advocates for the critical need to ground explainability work in cognitive science and human information processing [28]. Our study distinguishes itself not only within the formal methods community but also in the broader XAI field by leveraging well-established educational practices and theories. This approach offers a novel perspective on explainability, bridging the gap between AI systems and human comprehension. 

Many interpretability studies claim human interpretability without providing empirical evidence, our work evaluates claims of human understanding with real humans. Despite producing a negative result, our study underscores the importance of empirical research involving human subjects. This outcome reinforces the understanding that intuitive solutions in XAI may not always align with actual human comprehension.


Why not natural language?

Although natural language is often perceived as more intuitive for human understanding, it also presents its own set of challenges and biases. For this, we point to the work of Vinter et al. (1996), Loomes and Vinter (1997), and Vinter (1998) which evaluated the use of natural language translations of formal logic. We will address this oversight and incorporate a discussion of their findings into the final manuscript. Ironically, the time in which Vinter performed his experiments was one in which natural language was the standard approach to specifications, and the general push in computer science was to move towards the use of formal specifications for greater human understanding.

We refer to the following works in our responses:

Loomes, Martin, and Rick Vinter. "Formal methods: No cure for faulty reasoning." Safer Systems: Proceedings of the Fifth Safety-critical Systems Symposium, Brighton 1997. London: Springer London, 1997.

RJ Vinter, MJ Loomes, and D Kornbrot. Seven lesser known myths of formal methods:
uncovering the psychology of formal specification. 1996.

Vinter, Ricky Jay. "Evaluating formal specifications: a cognitive approach." (1998).

Jyotirmoy V. Deshmukh, Alexandre Donzé, Shromona Ghosh, Xiaoqing Jin, Garvit Juniwal, and Sanjit A. Seshia. Robust online monitoring of signal temporal logic. Form. Methods Syst. Des., 51(1):5–30, aug 2017

Zhenya Zhang, Jie An, Paolo Arcaini, and Ichiro Hasuo. Online Causation Monitoring of Signal Temporal Logic. In Constantin Enea and Akash Lal, editors, Computer Aided Verification, pages 62–84, Cham, 2023. Springer Nature Switzerland.

Meta-review: The paper investigates the question of the interpretability of STL formulas and identifies that they remain hard for users to correctly interpret. They also show that popular pedagogical methods like active learning don’t seem to completely correct the issue. The paper also shows how factors like STEM education do not seem to affect the outcome as strongly as one would expect. These results are interesting and relevant given the popularity of learned logical specifications to summarize agent behavior.

There were some common concerns that were raised by multiple reviewers. First off, multiple reviewers were thrown off by the obvious connection between the problem being studied and formal verification. After all, one could employ model-checking to verify if the system would ever invalidate the given specification. I would encourage the authors to provide a clear discussion of the goals of this study and how they differ from model checking. Then, there is the question of the influence of the form in which the formulas are presented. While natural language is one method, other forms could also be employed. The authors do point to some initial negative results, particularly in relation to natural language. It would be useful to consider this dimension as part of future work. Finally, there is the question of the significance of the results. While I do agree that a negative result on its own is quite useful, it might be worth considering why these issues arise in the first place and what a potential solution might look like. Or are the authors of the opinion that formal specification, at least STL, is a dead end as a method in XAI? A discussion along these lines might be a helpful addition to the paper.  This also connects to similarities and differences between the results in the paper and the one presented by Siu et al. 2023. The authors did provide a pretty detailed argument in their responses. I would recommend the authors also include a version of it in the paper.

In conclusion, I would recommend that the paper be accepted.
Decision: Accept (poster)