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

Authors: isabelle  hurley
rohan  paleja
ashley  suh
jaime d peña
ho  chit
Venue: NeurIPS_cc_2024_Conference
Published: 2024-05-15 16:38:07

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.

Main paper: 
 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 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 [12, 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). Specifically, 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 [13, 11] . The latter (validation) is a process that determines whether the product "solves the right problems" and "satisf[ies] intended use and user needs" [11] , making it an inherently human-centered process of value alignment. Validation is a key building block in creating robotic systems that are able to be dynamically reprogrammed and building a common language between the user and robot. 3While significant work has been performed on system verification [19, 20] , 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 human-interpretable, and thus useful for validation due to their semantics (e.g. [6, 26, 14, 28, 10, 23] ). However, human validation of policies expressed in both LTL and STL has shown to be empirically very difficult [17, 38] , even as it is 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 is a human-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) a 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 a system validation task, this does not necessarily improve performance. 
formal methods for interpretable learning: 
 Autonomous systems can be programmed in a variety of ways, including codifying domain expertise, extracting policies from demonstration [9, 35] , 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, a subset of formal methods. Temporal logic has seen significant usage with autonomous systems (e.g. [6, 26, 14, 28, 10, 23] ) as it can represent high-level mission objectives, allowing for ease of 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.1.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 a 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 AI 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 on current scientific understanding 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.Formal methods, which employ logical languages, are a 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 [6, 26, 14, 28, 10, 23] . The supposed link to interpretability (almost universally left unstated) is likely that if model behaviors can be tied specifically to meaningful, grounded concepts (such as 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.The major gap in these approaches to interpretability is the lack of empirical evidence to their efficacy in the overwhelming majority of cases. For example [6, 26, 14, 28, 10, 23] all claim to have methods that learn human-interpretable policies via formal methods. All provide empirical evidence that policies are learned, but all fail to provide any empirical evidence for the human-interpretability 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 interpretability 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 to 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 interpretability and the actual understanding of users. Our goal is to provide users with a 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.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 activities 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 like engineering [1] 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, we ask users to assess the contextual implications of a given policy and evaluate how the allowed set of behaviors aligns with one's needs. Under the adapted Bloom's Taxonomy of (human) learning [15] , this assessment and evaluation would touch on higher levels of learning, specifically enabling the following dimensions of learning: Recognition, Assembly, Determination, and Judgement. 
methods: 
 Providing humans with the ability to validate robot policies specified in STL is a building block toward dynamic reprogramming of robots. In this section, we describe how to incorporate active learning to improve a human's ability to perform system validation.To investigate how pedagogical active learning practices can help improve humans' ability to 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 to control an agent and navigate it through a map given configuration. Trajectories can be easily generated, saved and iterated upon for users to 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 taxonomy [15] with given set of specifications. Figure 1 depicts this process.Active learning and feedback can 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 is invalid. Figure 1 (left) shows an example of a 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 to explore the set of behaviors and provide specific examples to "show their work" in making a specification determination.Runtime verification is a computational approach to detect if system behaviors match a 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. a trajectory) and determines a 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 1 ). An agent has a 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 if 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 I 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 a controlled environment. [15] applied to ManeuverGame. For a given problem, a subject must first recall the meaning of the information they're being presented with (e.g., a formal specification), and understand it in the given context (grid world). Applying these concepts in ManeuverGame enables the subject to analyze different trajectories, both valid and invalid, under a trial-and-error 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.Without presenting to the user a 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 a 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.Question: For each theoretical result, does the paper provide the full set of assumptions and a complete (and correct) proof? Answer: [NA]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 personallyidentifiable information in the data, as well as =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. • Providing as much information as possible in supplemental material (appended to the paper) is recommended, but including URLs to data and code is permitted. 
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 Committee on the Use of Humans as Experimental Subjects and the United States Department of Defense Human Research Protection Office. Participants were recruited from the MIT Behavioral 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 a likely range of "end users" of end-user-reprogrammable systems. Participants were compensated $15 USD for completion of the experiment plus $2 per correct validation, for a total of up to $35. Broadly, the experiment asked participants to determine whether a provided temporal logic specification would always result in plans that would win a capture-the-flag-like game in a provided game configuration. Below, we detail the experiment procedure.All subjects are first provided with a demographic survey focused on 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 5.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 a specification was valid, or 2) provide one trajectory that satisfied the specification but resulted in a blue team loss before answering that a specification was invalid. The former required users to explore potential implications of the specification, but does not represent an exhaustive search of the possibilities, while the latter is effectively a 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 4 . 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-violating plans, unlike in AF-NF. Therefore, users were had the option to give up on the question after three consecutive failed attempts at trajectory generations, and are asked to provide a guess. Guessed answers were denoted as incorrect for the purpose of scoring.A control group performed the same task as the test groups, but were not required to provide 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 it is possible that a subset of control users may have essentially executed a similar workflow tracing on-screen with their finger or on scratch paper.Finally, participants were asked to 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 a whole.Here, we introduce our hypotheses, metrics to assess each hypothesis, and statistical procedure.Our hypotheses are:• H1: 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 to better calibration of confidence rating with response correctness in specification validation. This hypothesis is assessed by comparing the correlation coefficient between confidence and validation accuracy across conditions AL-NF and AL-WF, 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 in the AL-WF condition.Omnibus tests were conducted to examine the relationship between various subject-specific and specification-specific 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 and indicated users did not actively interact with the experiment content. See Section 5.2 for more details on subjects' engagement. 
validation task performance: 
 In assessing H1, we find that there was no significant difference in the participants performance among these groups (Table 1 , F (2, 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 1 ), showing some minimal capability to validate system behaviors. 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 p > 0.05). Further discussion of formal methods familiarity among our subject pool is provided in Appendix A.5. STEM experience appeared to be less influential in 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 to 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-truth validity, specification complexity, nor the question sequence order as predictors of validation correctness (all p > 0.05).In assessing H2, we 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 can be found in Appendix A.6.Across each of the engagement mechanism conditions, some participants did not engage with the validation task (Table 2 ). Behavior trends for non-engagement or "giving 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). 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 (p = 3.20 × 10 -5 and p = 1.18 × 10 -6 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 in Table 1 this extended time was not effective in improving performance at the system validation task during the experiment session.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 a 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.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% of these trajectories did not actually meet the specification. Note that subjects were instructed to only provide trajectories that met specifications, and that it was always possible to do so. These trajectories violated the specification in a variety of ways ranging from simple off by one errors with the time bound, to complete ignoring of parts of the specification, to the creation of short, non-meaningful trajectories.Participants' creation of trajectories that satisfy the specification is related to their correctness in the validation task, however this effect is dependent on the ground truth validity of the specification. When the ground-truth of the specification is valid, correct responses are more significantly more likely to be accompanied by trajectories which satisfy the specification (Figure 3 , p = 6.25 × 10 -5 ).Conversely, when the ground-truth of the specification is invalid, incorrect responses are more likely to be accompanied by satisfactory trajectories as shown work (Figure 3 , p = 4.03 × 10 -8 ). Proper trajectory generation indicates subjects' understanding of specification constraints, but the translation of this capacity to validation ability is not direct.Observations of subjects in the talk-aloud sub-group as well as the content of all subjects postexperiment 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 a 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-WF 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 be a 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 to lose)." The notion of the robot being "suicidal" suggests a 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.6 Discussion 
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 is not a sufficient mechanism for improving interpretability over a 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 a 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 to consider all possible trajectories allowed by a specification the process of generation may overly draw their focus to a 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-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 as 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] .The forced engagement of active learning notably frustrated participants, matching with common student feedback from educational settings despite improved performance [34, 7] , and in AI reliance studies where engagement elicited negative participant ratings despite more appropriate reliance levels [4] . 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 in 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 a way to improve user engagement and minimize frustration while maintaining potential active learning benefits.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 a set of "game-winning conditions" as the participants' intent, acting as though they could not be easily codified. Having a specific, simple set of "user intents" was required to ensure the objectivity of the validation ground truth. A 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, is that we are limited to a single session of learning and testing. Studies exist that both show [41] and do not show [33] a positive effect of active learning in a single session, and much of the work in this space showing strong effects is over the course of a semester or more [1, 16] . It may be that active learning only shows a 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.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-robust trajectories could represent conceptual edge cases that are worth examining, and may be generated automatically.Similar to [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 to 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 a 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] .Question: Does the paper specify all the training and test details (e.g., data splits, hyperparameters, how they were chosen, type of optimizer, etc.) necessary to 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 to a 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, or as supplemental material. 
conclusion: 
 This study is the first to our knowledge that attempts to unite research in human learning to 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 human-interpretable. 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, a requirement for robot reprogramming after deployment.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.Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?Answer: [Yes] Justification: We present data distributions as 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 are symmetric, an assumption that typical error bars make. We further report all of 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 error bars, confidence intervals, or statistical significance tests, at least for the experiments that support the main claims of the paper.• 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). • It should be clear whether the error bar is the standard deviation or the standard error of the mean. Justification: The experiment was not primarily computational in nature. While computation was required to run the human experiments and to perform runtime monitoring, such requirements were minimal, as 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 as 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). 
code of ethics: 
 Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics https://neurips.cc/public/EthicsGuidelines? 
broader impacts: 
 Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?Answer: [Yes] Justification: 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. Guidelines:• The answer NA means that there is no societal impact of the work performed.• If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact. • Examples of negative societal impacts include potential malicious or 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 as 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 to attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of ML). 
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 no such risks.• Released models that have a 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 to 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 we encourage authors to take this into account and make a best faith effort. 12. Licenses for existing assets Question: 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? 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 or dataset.• The answer NA means that the paper does not involve crowdsourcing 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 we expect authors to adhere to 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. 
 
 Appendix: Responses to the question of formal methods experience were recoded in 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, formalmethods 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 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 twosample t-tests for categorical variables, or a Spearman's correlation for continuous variables if the omnibus returned significance.Omnibus logistic regression analysis was performed on a by-question basis with participant-based predictors of familiarity with formal methods, STEM experience, level of education, experiment condition as well as specification-based predictors of specification ground truth validity, question sequence number, specification AST depth, specification symbol count and a response variable of validation correctness.An examination of variance equality for confidence ratings yielded a non-significant result (p = 0.313). Independent t-tests between confidence values when responses were correct or incorrect (Figure 5 ) indicated users' confidence was not significantly different based on the correctness of their answer in any of the conditions. The effect size of 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 the entirety of the experiment also did not appear to be 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 7 r = 0.55, .05 > 0.05/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 6 , r = 0.530, p = 0.003) compared to when answered correctly (Figure 6 , r = 0.320, p = 0.03). Those with experience in STEM fields may be more confident in their responses, but such confidence is substantiated by better performance. Horizontal jitter is shown to visually separate points. The correlation was calculated using Spearman's coefficient, but a linear fit is shown.Figure 7 : Subject's average confidence across all 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 of the correlations were positive but none were found to be significant with the Bonferroni correction (a = 0.05/3 = 0.016).The determination for giving up was based upon users time spent completing the experiment as well as their interaction with the experiment interface. Due to the differing requirements on subjects, different criteria were used to determine who gave up. The following criteria were applied to subjects in the three conditions:Control:• < 1 minute spent per question on averageActive 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):• < 2 minutes per validation question on average OR • choosing to give up (on the interface) on three or more questionsNeurIPS Paper Checklist 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 a separate "Limitations" section in 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 on 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 a few datasets or with a 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, a facial recognition algorithm may perform poorly when image resolution is low or images are taken in low lighting. Or a 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 be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an important role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.Justification: We follow all NeurIPS ethical guidelines -in particular, our human experiments are IRB-approved, with no notable risk of harm, and our subjects are appropriately compensated for their time.Guidelines:• The answer NA means that the authors have not 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., if there is a special consideration due to laws or regulations in their jurisdiction).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[11], which distinguishes the two and is more appropriate for autonomous systems design.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 were not analyzed with the rest of the subjects. 


Decision: 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.

Reviews: review: paper_summary: paper_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.
strength_weakness: strength_weakness: 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?

2. 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.
questions: questions: Please refer to the weakness part:

1. Justify why we need human supervision.

2. Explain the criticism against interpretability.
limitations: limitations: This is about user-study which has no potential negative societal impact.
paper_summary: paper_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.
strength_weakness: strength_weakness: - 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.
- It is unclear whether the exercise tested participants' understanding of the domain or the logic.
- The exact challenges in understanding STL are not clearly discussed.
questions: 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.
- Is it possible that participants' performance resulted from a lack of familiarity with the experimental setup rather than with the logic?
- Which aspects of the logic do participants find challenging: modalities, time-tracking, or nesting of the operators?
- 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: 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.
paper_summary: paper_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.
strength_weakness: strength_weakness: - The reviewer feels that this study, while important, may be a better fit for a more specialized venue.
- 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].
questions: 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.
2. 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: limitations: - Primarily stated as a “negative result” paper, while showing that active learning may not help STL interpretability scores, a solution is not discussed.
- STL specification difficulty classes were not defined or considered.
paper_summary: paper_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.* 

The 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). 

The main conclusions can be summarized as follows:
- There is no significant improvement in validation accuracy with active learning.
- Active learning increases user engagement, and active learning with feedback reduces user frustration.
- Active learning appears to have a greater impact on participants with lower STEM experience (sample size was however too small for definitive conclusions.)
strength_weakness: strength_weakness: 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.

2. 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].


[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

[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.
questions: 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: 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.

Comments: title: Re: suitability for NeurIPS
Re: Comparison to Siu et al. 2023
Re: Comment on Siu et al.
Thanks for your response.
comment: I thank the authors for their responses to my questions. I am satisfied with the answers provided.
Thank you for the comment. Since the suitability for NeurIPS is a new concern that was not brought up in the initial review, we would like to address that issue specifically. As we responded to reviewer 14rd when the same suitability concern was stated:

"...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:

Differentiable Learning of Logical Rules for Knowledge Base Reasoning by Yang et al. (NeurIPS 2017)

Logical Neural Networks by Riegel et al. (NeurIPS 2020)

Interpretable and Explainable Logical Policies via Neurally Guided Symbolic Abstraction by Delfosse et al. (NeurIPS 2023)

As 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)."
We thank the reviewer and the area chair for the comments, and wish to clarify our contributions in comparison to Siu et al. 2023.

Siu et al 2023 and this work are both concerned with the validation of STL formulas and both return negative results on humans' ability to validate such formulas to a high degree of accuracy. However, while Siu et al explored methods asserted as interpretable by the AI community - raw STL, decision trees, and natural language - this work takes a different approach with a far more involved procedure required of our human participants. One of Miller et al's [28] critiques of the XAI space was that it frequently proposed methods without grounding them in studies about how humans actually learn. That critique also applies to the methods used by the Siu et al. experiment, since those were based on the largely unfounded assumptions of the XAI community.

In contrast, our active (human) learning approach (background in lines 105-119) is one that is based on the education literature, not the AI literature, and has been studied in human learning contexts for decades [1, 2, 13, 14], with [14] in particular showing that active learning increased learner performance and decreased failure rates across a metaanalysis of 255 studies on active learning (line 113). Active learning requires far more participant engagement than non-active learning. While what we present to participants is similar to Siu et al's experiment, Siu et al's experiment did not require participants to actually execute a related task and show examples of their thought process (lines 107-108). In contrast, our two active learning conditions (lines 185-198) required participants to demonstrate their understanding of the specifications by providing example trajectories that justified their validation decision, a task that was not part of the Siu et al. work. Essentially, while Siu et al's participants could just answer the validation question without thinking about it if they so chose, our active learning participants were forced to use methods that are shown by the education literature to improve human understanding.

Particularly in response to the reviewer's concern about the contribution of this work vs Siu et al. given the similar findings: The fact that subjects' validation accuracy did not change sufficiently to be detectable for the task of system validation in this case likely speaks more to the difficulty of the interpretation and validation of specifications than it does to the efficacy of active learning (which again, has decades of empirical research behind it).
 
There is significant differences between the present work and Siu et al.'s experiment, with the application of empirically-demonstrated human learning procedures being the fundamental driver. Siu et al's work was a step in the right direction of asking for empirical evidence of interpretability for validation, but by using methods established empirically in the human learning literature and not asserted in the AI literature, the present work shows to a much greater degree the depth of work required to make the claims of AI interpretability meaningful for this kind of use case.
Dear Authors,

Could you comment on how you would differentiate your work from [33] Siu et al.? This would really help future discussions.
Thank you for your response. All of my questions have been answered, and I don't have any further inquiries. I am maintaining a score of 5. My main concerns remain the limited scope of contributions and the paper's suitability for NeurIPS.
I thank the authors for their response and their rebuttal PDF explaining the specifications considered. Based on reading the other reviews as well, I am optimistic that the community will be interested in the results presented. 

However, I am still uncertain whether the presented study, in its current form, will be useful to XAI researchers without further in-depth exploration of what makes certain parts of STL challenging for human evaluators. Since the presented work is a step in the right direction, I will raise my score accordingly. Nevertheless, I remain skeptical about how useful the work is compared to Siu et al. [33], given that STL was a subset of the logic descriptions they considered.
Thank the author for answering my questions, my concern has been solved and. I have updated my score accordingly.