'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions

TL;DR

This paper introduces a formal framework using SMT-based symbolic execution to rigorously interrogate and analyze algorithmic decision-making behaviors, inspired by legal accountability processes, demonstrated on a car crash scenario.

Contribution

It presents a novel method combining symbolic execution and SMT solving to model and interrogate algorithmic decisions within an accountability framework inspired by legal procedures.

Findings

Framework effectively models algorithmic logic as SMT formulas

Enables counterfactual analysis of decisions

Demonstrated on a car crash scenario

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 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 $\Pi$ in the decidable theory $\texttt{QF_FPBV}$. We implement our framework and demonstrate its utility on an illustrative car crash scenario.