Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Samuel Judson, Matthew Elacqua, Filip Cano, Timos Antonopoulos, Bettina Könighofer, Scott J. Shapiro, Ruzica Piskac

TL;DR

It is shown that under minimal assumptions automated reasoning can rigorously interrogate algorithmic behaviors as in the adversarial process of legal fact finding.

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

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

TL;DR

It is shown that under minimal assumptions automated reasoning can rigorously interrogate algorithmic behaviors as in the adversarial process of legal fact finding.

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 we use symbolic execution to represent its logic as a statement in the decidable theory . We implement our framework and demonstrate its utility on an illustrative car crash scenario.
Paper Structure (43 sections, 2 theorems, 17 equations, 9 figures, 2 tables, 1 algorithm)

This paper contains 43 sections, 2 theorems, 17 equations, 9 figures, 2 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Contribution
  3. Outline.
  4. Related Work
  5. Motivation
  6. Legal Accountability for ADMs
  7. Technical Background
  8. Programs and Traces
  9. SMT-based Program Analysis
  10. SMT Solving.
  11. Symbolic Execution.
  12. Counterfactual Reasoning
  13. Formalism.
  14. Formal Reasoning for Accountability
  15. Counterfactual-Guided Logic Exploration
  16. ...and 28 more sections

Key Result

Theorem 5.5

Let $q_i = ((\varphi, \psi), \beta)$ be a factual query, and let $(\tau^f, \, t, \, \varphi, \, \psi)$ be a corresponding factual scenario. Then is valid iff $\tau^f \models \varphi(\hat{E}) \land \psi(\hat{S}) \to_{\mathcal{A}, t, \ell} \beta(\hat{D})$.

Figures (9)

  • Figure 1: A broadside car crash rendered in the $\textsf{soid}$ GUI.
  • Figure 2: Longitudinal Proper Response Guard (see Def. 4.1 of shalev2017formal) written in C. Although not used by the simulated self-driving cars of our case study, this sort of decision functionality is representative of what $\textsf{soid}$ is designed to investigate.
  • Figure 3: Counterfactual-guided Abstraction Refinement of the code in Figure \ref{['fig:long-pr-example']}. A factual query $q_1$ and a pair of counterfactual queries, $q_2, \, q_3$, all with the same $\beta$, produce the diagrammed symbolic traces and the resultant abstraction $\hat{A}$ at bottom right. Concrete states are rendered with a typewriter font, while symbolic states are rendered in Garamond.
  • Figure 4: Still of the $\textsf{soid}$ GUI (with a small section cut out for brevity). At top left is the critical moment from the program logs as chosen by the investigator. At bottom right are the counterfactual conditions the investigator has specified.
  • Figure 5: Our decision tree example. At top, the relevant decision subtree for a misclassification based on health data, with the incorrect path taken in red -- and the correct branch missed in blue -- as the unit conversion bug leads to a significantly smaller BMI input than is correct. At bottom, the (otherwise correct) decision tree inference logic in C.
  • ...and 4 more figures

Theorems & Definitions (10)

  • Definition 3.1
  • Definition 3.2
  • Definition 5.1
  • Definition 5.2
  • Definition 5.3
  • Definition 5.4
  • Theorem 5.5
  • proof
  • Theorem 5.6
  • proof