-
Analyzing Intentional Behavior in Autonomous Agents under Uncertainty
Authors:
Filip Cano Córdoba,
Samuel Judson,
Timos Antonopoulos,
Katrine Bjørner,
Nicholas Shoemaker,
Scott J. Shapiro,
Ruzica Piskac,
Bettina Könighofer
Abstract:
Principled accountability for autonomous decision-making in uncertain environments requires distinguishing intentional outcomes from negligent designs from actual accidents. We propose analyzing the behavior of autonomous agents through a quantitative measure of the evidence of intentional behavior. We model an uncertain environment as a Markov Decision Process (MDP). For a given scenario, we rely…
▽ More
Principled accountability for autonomous decision-making in uncertain environments requires distinguishing intentional outcomes from negligent designs from actual accidents. We propose analyzing the behavior of autonomous agents through a quantitative measure of the evidence of intentional behavior. We model an uncertain environment as a Markov Decision Process (MDP). For a given scenario, we rely on probabilistic model checking to compute the ability of the agent to influence reaching a certain event. We call this the scope of agency. We say that there is evidence of intentional behavior if the scope of agency is high and the decisions of the agent are close to being optimal for reaching the event. Our method applies counterfactual reasoning to automatically generate relevant scenarios that can be analyzed to increase the confidence of our assessment. In a case study, we show how our method can distinguish between 'intentional' and 'accidental' traffic collisions.
△ Less
Submitted 4 July, 2023;
originally announced July 2023.
-
'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions
Authors:
Samuel Judson,
Matthew Elacqua,
Filip Cano,
Timos Antonopoulos,
Bettina Könighofer,
Scott J. Shapiro,
Ruzica Piskac
Abstract:
Principled accountability in the aftermath of harms is essential to the trustworthy design and governance of algorithmic decision making. Legal theory offers a paramount method for assessing culpability: putting the agent 'on the stand' to subject their actions and intentions to cross-examination. We show that under minimal assumptions automated reasoning can rigorously interrogate algorithmic beh…
▽ More
Principled accountability in the aftermath of harms is essential to the trustworthy design and governance of algorithmic decision making. Legal theory offers a paramount method for assessing culpability: putting the agent 'on the stand' to subject their actions and intentions to cross-examination. We show that under minimal assumptions automated reasoning can rigorously interrogate algorithmic behaviors as in the adversarial process of legal fact finding. We model accountability processes, such as trials or review boards, as Counterfactual-Guided Logic Exploration and Abstraction Refinement (CLEAR) loops. We use the formal methods of symbolic execution and satisfiability modulo theories (SMT) solving to discharge queries about agent behavior in factual and counterfactual scenarios, as adaptively formulated by a human investigator. In order to do so, for a decision algorithm $\mathcal{A}$ we use symbolic execution to represent its logic as a statement $Π$ in the decidable theory $\texttt{QF_FPBV}$. We implement our framework and demonstrate its utility on an illustrative car crash scenario.
△ Less
Submitted 29 January, 2024; v1 submitted 9 May, 2023;
originally announced May 2023.
-
On Heuristic Models, Assumptions, and Parameters
Authors:
Samuel Judson,
Joan Feigenbaum
Abstract:
Insightful interdisciplinary collaboration is essential to the principled governance of complex technologies, like those produced by modern computing research and development. Technical research on the interaction between computation and society often focuses on how researchers model social and physical systems. These models underlie how computer scientists specify problems and propose algorithmic…
▽ More
Insightful interdisciplinary collaboration is essential to the principled governance of complex technologies, like those produced by modern computing research and development. Technical research on the interaction between computation and society often focuses on how researchers model social and physical systems. These models underlie how computer scientists specify problems and propose algorithmic solutions. However, the social effects of computing can depend just as much on obscure and opaque technical caveats, choices, and qualifiers. Such artifacts are products of the particular algorithmic techniques and theory applied to solve a problem once modeled, and their nature can imperil thorough sociotechnical scrutiny of the often discretionary decisions made to manage them. We describe three classes of objects used to encode these choices and qualifiers: heuristic models, assumptions, and parameters. We raise six reasons these objects may be hazardous to comprehensive analysis of computing and argue they deserve deliberate consideration as researchers explain scientific work.
△ Less
Submitted 16 August, 2023; v1 submitted 18 January, 2022;
originally announced January 2022.
