@inproceedings{96bbb59dcea64e7dabb373148862ac32,
title = "soid: A Tool for Legal Accountability for Automated Decision Making",
abstract = "We present soid, a tool for interrogating the decision making of autonomous agents using SMT-based automated reasoning. Relying on the Z3 SMT solver and KLEE symbolic execution engine, soid allows investigators to receive rigorously proven answers to factual and counterfactual queries about agent behavior, enabling effective legal and engineering accountability for harmful or otherwise incorrect decisions. We evaluate soid qualitatively and quantitatively on a pair of examples, i) a buggy implementation of a classic decision tree inference benchmark from the explainable AI (XAI) literature; and ii) a car crash in a simulated physics environment. For the latter, we also contribute the \soidgui{}, a domain-specific, web-based example interface for legal and other practitioners to specify factual and counterfactual queries without requiring sophisticated programming or formal methods expertise.",
keywords = "SMT solving, Accountable software systems, CS & Law",
author = "Samuel Judson and Matthew Elacqua and Filip Cano and Timos Antonopoulos and Bettina K{\"o}nighofer and Shapiro, {Scott J.} and Ruzica Piskac",
year = "2024",
doi = "10.1007/978-3-031-65630-9_12",
language = "English",
isbn = "978-3-031-65629-3",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer, Cham",
pages = "233–246",
editor = "Arie Gurfinkel and Vijay Ganesh",
booktitle = "Computer Aided Verification - 36th International Conference, CAV 2024, Proceedings",
note = "36th International Conference on Computer Aided Verification : CAV 2024, CAV 2024 ; Conference date: 22-07-2024 Through 27-07-2024",
}