2023/05/09 by Samuel Judson, Matthew Elacqua, Judson, Samuel +10 · 1 citation
Business, Management and Accounting · #Big Data and Business Intelligence #Computers and Society (cs.CY) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2305.05731
openalex publication_date 2023/05/09 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/01
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 A we use symbolic execution to represent its logic as a statement Π in the decidable theory QFFPBV. We implement our framework and demonstrate its utility on an illustrative car crash scenario.