Recent work on formal approaches to specify or learn autonomous system behaviour is based on the idea that formal specifications are interpretable and beneficial for humans checking systems. Though often claimed, this assumption is rarely tested. 

Formal specifications

With the proliferation of autonomous systems and artificial intelligence in everyday life, novel approaches are being developed to assist humans in verifying that these systems are operating by expectations. Formal specifications are one approach that employs mathematical formulations capable of being converted into expressions in natural language. Some researchers assert this technique can specify an AI's decisions in human-comprehensible terms.

The researchers aimed to test such interpretability assertions. Their findings suggest that formal specifications need to be interpretable by humans. The team's study participants were asked to determine if an AI agent's plan would succeed in a virtual game. When given the formal plan specification, the participants were correct less than half the time.

Interpretability

Interpretability is crucial because it gives humans confidence in a real-world application of a machine. The ability of an AI or automaton to justify its actions would enable humans to determine whether the system requires modification or can be relied upon to render impartial judgments. An interpretable system empowers technology users to comprehend and place confidence in its functionalities, in addition to its developers. 

Nonetheless, interpretability has been an enduring obstacle in the domains of AI and autonomy. Since the machine learning process is a "black box," it is frequently impossible for model developers to clarify how or why a system arrived at a particular conclusion.

Experiment

In designing their experiment, the scholars aimed to ascertain whether implementing formal specifications enhanced the interpretability of a system's behaviour. Their primary concern was whether individuals could utilize these specifications to validate a system, i.e., determine whether it consistently fulfilled the user's objectives.

Formal specification application for this objective is an unintended consequence of its initial application. Formal specifications are a subset of a more extensive collection of formal methods that employ logical expressions to define the behaviour of a model within a mathematical framework. Due to the model's foundation in logical progression, "model checkers" enable engineers to mathematically validate system facts, such as the conditions under which task completion is feasible or infeasible. Presently, scholars are endeavouring to apply this identical framework as a tool for human translation.

Formal specifications training

Individuals with prior formal specifications training performed marginally better than those new to the subject. However, the experts expressed considerably greater assurance in their responses, irrespective of their accuracy. In general, individuals tended to place excessive confidence in the accuracy of specifications presented to them, resulting in disregarding rule sets and consequent game losses.  

The team does not intend to establish a direct correlation between their findings and human performance in practical robot validation scenarios. However, their objective is to utilize the results as an initial reference to scrutinize the aspects the formal logic community might be overlooking when asserting interpretability and the practical implications of such assertions.

Conclusion

This study was undertaken during a more extensive endeavour in which researchers strived to enhance the rapport between human operators and robotics, focusing on military applications. Robotics programming can frequently isolate operators from the proceedings. Implementing such a procedure may enhance the operator's trust in the robot and ability to adapt.

Furthermore, they hope that the findings of this study and their ongoing research will ultimately contribute to a more refined implementation of autonomy, which is increasingly pervasive in human existence and decision-making.

Image source: Unsplash