A study from MIT Lincoln Laboratory shows that although formal specifications are mathematically precise, they are not always interpretable by humans. Participants had difficulty validating AI behavior using these specifications, suggesting a discrepancy between theoretical claims and practical understanding. The findings highlight the need for more realistic assessments of AI explainability.
Some researchers believe that formal norms are a way for autonomous systems to "explain themselves" to humans. But a new study finds that we don't understand.
As autonomous systems and artificial intelligence become more common in daily life, new methods are emerging to help humans check whether these systems are behaving as expected. One approach is called "formal specification," which uses mathematical formulas that can be translated into natural language expressions. Some researchers claim that this approach can be used to illuminate decisions that AI will make in a human-interpretable way.
Researchers at MIT Lincoln Laboratory wanted to test this explainability claim. Their findings showed just the opposite: Formal specifications seemed impossible to interpret by humans. In the team's study, participants were asked to examine whether an AI agent's plans would succeed in a virtual game. When participants saw a formal description of the plan, less than half the time they were correct.
"This result is bad news for researchers who have been claiming that formal methods can provide interpretability for systems." Hosea Siu, a researcher in the laboratory's artificial intelligence technology group, said: "This may be true in some limited and abstract sense, but not for anything close to actual system verification." The group's paper has been accepted by the 2023 International Conference on Intelligent Robots and Systems held earlier this month.
The importance of explainability
Explainability is important because it allows humans to trust machines when they are used in the real world. If a robot or AI can explain its behavior, humans can decide whether it needs to be adjusted or whether it can be trusted to make fair decisions. An explainable system also allows technical users - not just developers - to understand and trust its capabilities. However, explainability has long been a difficult problem in the fields of artificial intelligence and autonomy. The machine learning process takes place in a "black box", so model developers often cannot explain why or how the system makes a certain decision.
"When researchers say 'our machine learning system is accurate,' we ask 'how accurate' and 'what data was used,' and if that information is not provided, we reject the claim. When researchers say 'our machine learning system is interpretable,' we are not doing that, and we need to start subjecting these claims to greater scrutiny," Siu said.
Translation Standards Challenges
In experiments, the researchers sought to determine whether formal specifications could make a system's behavior more explainable. Their focus is on people's ability to use these specifications to verify the system, that is, to understand whether the system always meets the user's goals.
Using formal specifications for this purpose is essentially a by-product of their original purpose. Formal specifications are part of a broader set of formal methods that use logical expressions as a mathematical framework to describe the behavior of a model. Because models are based on logical flows, engineers can use "model checkers" to mathematically prove facts about the system, including when the system is likely to accomplish a task and when it is unlikely to accomplish a task. Now, researchers are trying to use the same framework as a translational tool in humans.
"Researchers confuse the fact that formal specifications have precise semantics that humans can interpret. That's not the same thing," Siu said. "We realized that there was almost no checking that people actually understood the output."
In the team's experiment, participants were asked to verify a fairly simple set of behaviors with a robot playing a game of capture the flag, essentially answering "If the robot follows these rules exactly, does it always win?"
Participants included both formal methods experts and non-experts. They obtained the formal specification in three ways - "original" logic formulas, translations into formulas closer to natural language, and decision tree formats. In the field of artificial intelligence, decision trees are often thought of as a human-understandable way of demonstrating decision-making by an artificial intelligence or robot.
The result is that overall the validation performance is quite poor, with accuracy around 45% regardless of the representation.
Overconfidence and misunderstanding
People with previous formal discipline training performed only slightly better than novices. However, experts are more confident in their answers, whether they are correct or not. In general, people tend to over-confidence in the correctness of the specs put in front of them, which means they ignore the rule set that allows the game to fail. The researchers say this confirmation bias is especially important for system verification because people are more likely to overlook failure modes.
"We don't think this result means we should abandon using formal specifications to explain system behavior to people. But we do think more work needs to be done in designing how these specifications are presented to people and the workflows by which people use them," Siu added.
When thinking about why the experimental results were so bad, Siu realized that even the people using the formal methods were not trained to check the specifications as required by the experiment. Furthermore, it is difficult to think through all the possible consequences of a set of rules. Even so, the set of rules shown to participants was short, no more than a paragraph of text, "much shorter than the rules you would encounter in any real system," Siu said.
The team does not intend to tie their findings directly to human performance in real-world robot validations. Rather, their goal is to use these results as a starting point to consider what the formal logic community might be missing when making claims about interpretability, and how such claims might manifest in the real world.
Future Impact and Research
The research is part of a larger project Siu and teammates are working on to improve the relationship between robots and human operators, particularly military operators. The robot programming process often excludes operators. With similar goals of improving explainability and trust, the project is trying to have operators teach tasks directly to robots in a manner similar to how humans are trained. This process can both increase the operator's confidence in the robot and improve the robot's adaptability.
Ultimately, they hope the results of this study and their ongoing research will lead to better applications of autonomy as it becomes increasingly embedded in human lives and decision-making.
"Our findings demonstrate the need for human evaluation of certain systems and concepts before making too many claims about autonomy and AI's usefulness to humans," Siu added.