Kavli Affiliate: Johannes Lehmann
| First 5 Authors: Christel Baier, Roxane van den Bossche, Sascha Klüppelholz, Johannes Lehmann, Jakob Piribauer
| Summary:
To improve reliability and the understanding of AI systems, there is
increasing interest in the use of formal methods, e.g. model checking. Model
checking tools produce a counterexample when a model does not satisfy a
property. Understanding these counterexamples is critical for efficient
debugging, as it allows the developer to focus on the parts of the program that
caused the issue.
To this end, we present a new technique that ascribes a responsibility value
to each state in a transition system that does not satisfy a given safety
property. The value is higher if the non-deterministic choices in a state have
more power to change the outcome, given the behaviour observed in the
counterexample. For this, we employ a concept from cooperative game theory —
namely general power indices, such as the Shapley value — to compute the
responsibility of the states.
We present an optimistic and pessimistic version of responsibility that
differ in how they treat the states that do not lie on the counterexample. We
give a characterisation of optimistic responsibility that leads to an efficient
algorithm for it and show computational hardness of the pessimistic version. We
also present a tool to compute responsibility and show how a stochastic
algorithm can be used to approximate responsibility in larger models. These
methods can be deployed in the design phase, at runtime and at inspection time
to gain insights on causal relations within the behavior of AI systems.
| Search Query: ArXiv Query: search_query=au:”Johannes Lehmann”&id_list=&start=0&max_results=3