'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914657959149568 |
|---|---|
| author | Judson, Samuel Elacqua, Matthew Cano, Filip Antonopoulos, Timos Könighofer, Bettina Shapiro, Scott J. Piskac, Ruzica |
| author_facet | Judson, Samuel Elacqua, Matthew Cano, Filip Antonopoulos, Timos Könighofer, Bettina Shapiro, Scott J. Piskac, Ruzica |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2305_05731 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | 'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions Judson, Samuel Elacqua, Matthew Cano, Filip Antonopoulos, Timos Könighofer, Bettina Shapiro, Scott J. Piskac, Ruzica Logic in Computer Science Computers and Society Programming Languages 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. |
| title | 'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions |
| topic | Logic in Computer Science Computers and Society Programming Languages |
| url | https://arxiv.org/abs/2305.05731 |