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

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

doi:10.1145/3614407.3643699

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

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

^*Corresponding author for this work

Institute of Applied Information Processing and Communications (7050)

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

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 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. We implement our framework and demonstrate its utility on an illustrative car crash scenario.

Original language	English
Title of host publication	CSLAW 2024 - Proceedings of the 3rd Symposium on Computer Science and Law
Pages	73-85
Number of pages	13
ISBN (Electronic)	9798400703331
DOIs	https://doi.org/10.1145/3614407.3643699
Publication status	Published - 12 Mar 2024
Event	2024 Computer Science and Law Symposium: CSLAW 2024 - Boston, United States Duration: 12 Mar 2024 → 12 Mar 2024

Conference

Conference	2024 Computer Science and Law Symposium
Abbreviated title	CSLAW 2024
Country/Territory	United States
City	Boston
Period	12/03/24 → 12/03/24

Keywords

algorithmic decision making
algorithmic accountability
formal methods
SMT solving
symbolic execution

ASJC Scopus subject areas

Artificial Intelligence
Communication
Law
Computer Networks and Communications

Access to Document

10.1145/3614407.3643699Licence: CC BY 4.0

Cite this

Judson, S, Elacqua, M, Cano, F, Antonopoulos, T, Könighofer, B, Shapiro, S & Piskac, R 2024, 'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions. in CSLAW 2024 - Proceedings of the 3rd Symposium on Computer Science and Law. pp. 73-85, 2024 Computer Science and Law Symposium, Boston, United States, 12/03/24. https://doi.org/10.1145/3614407.3643699

@inproceedings{b2e5766cdb704dbca06bddb778b43f69,

title = "'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions",

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 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. We implement our framework and demonstrate its utility on an illustrative car crash scenario.",

keywords = "algorithmic decision making, algorithmic accountability, formal methods, SMT solving, symbolic execution",

author = "Samuel Judson and Matthew Elacqua and Filip Cano and Timos Antonopoulos and Bettina K{\"o}nighofer and Scott Shapiro and Ruzica Piskac",

year = "2024",

month = mar,

day = "12",

doi = "10.1145/3614407.3643699",

language = "English",

pages = "73--85",

booktitle = "CSLAW 2024 - Proceedings of the 3rd Symposium on Computer Science and Law",

note = "2024 Computer Science and Law Symposium : CSLAW 2024, CSLAW 2024 ; Conference date: 12-03-2024 Through 12-03-2024",

}

TY - GEN

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

AU - Judson, Samuel

AU - Elacqua, Matthew

AU - Cano, Filip

AU - Antonopoulos, Timos

AU - Könighofer, Bettina

AU - Shapiro, Scott

AU - Piskac, Ruzica

PY - 2024/3/12

Y1 - 2024/3/12

N2 - 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 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. We implement our framework and demonstrate its utility on an illustrative car crash scenario.

AB - 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 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. We implement our framework and demonstrate its utility on an illustrative car crash scenario.

KW - algorithmic decision making

KW - algorithmic accountability

KW - formal methods

KW - SMT solving

KW - symbolic execution

UR - http://www.scopus.com/inward/record.url?scp=85188688210&partnerID=8YFLogxK

U2 - 10.1145/3614407.3643699

DO - 10.1145/3614407.3643699

M3 - Conference paper

SP - 73

EP - 85

BT - CSLAW 2024 - Proceedings of the 3rd Symposium on Computer Science and Law

T2 - 2024 Computer Science and Law Symposium

Y2 - 12 March 2024 through 12 March 2024

ER -

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

Abstract

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this