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

High Level Objectives and Experiment Setup (Weakness 1 and Limitation)

We 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.

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

We 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.

Theoretical Interpretability Improvements vs. Empirical Studies (Weakness 2)

We 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.

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

We 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.

Question on scoring guesses (Question 1)

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

Limitation (See response to High Level Objectives and Experiment Setup.)

Fit for NeurIPS (Weakness 1)

As 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:

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

Contributions Beyond Greenman et al and Siu et al (Weakness 2)

Greenman 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.

Siu 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.

Translation into Natural Language (Question 1)

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

Complexity of Time Periods (Question 2)

We 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.

Negative Result without a Demonstrated Solution (Limitation 1)

Many 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.

STL Difficulty Classes (Limitation 2)

We 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.

As 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.

List of Specifications Used (Weakness 1)

We 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:

All 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.

All 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.

Subjects' Domain Knowledge vs STL Knowledge (Weakness 2 and Question 2)

We 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.

Challenges in Subjects' Understanding (Weakness 3 and Question 3)

With 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.

Translation into Natural Language (Question 1)

We 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.

Consequently, 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.

Familiarity with Domain (Question 2) (See Subjects' Domain Knowledge vs STL Knowledge, above)

Challenging Aspects of Logic (Question 3) (See Challenges in Subjects' Understanding, above)

Choice of the Class of Specifications (Question 4)

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

Human Supervision (Weakness 1, Question 1)

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

While 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.

For 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.

Critique of Interpretability (Weakness 2, Question 2)

We 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.

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

Moreover, 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.

We 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.

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