'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions
'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions
复制标题
“将汽车搁置”：基于 SMT 的预言机用于调查决策
DOI：
--
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
R. Piskac
中科院分区：
文献类型：
--
作者：
Samuel Judson;Matthew Elacqua;Filip Cano Córdoba;Timos Antonopoulos;Bettina Könighofer;Scott J. Shapiro;R. Piskac
在危害后，有原则的问责制对于算法决策的值得信赖的设计和治理至关重要。法律理论提供了一种评估罪魁祸首的至关重要方法：将代理人“在看台上”，以对其行为和意图进行盘问。我们表明，在最少的假设下，自动推理可以像在法律事实发现的对抗过程一样严格审问算法行为。我们将责任过程（例如试验或审查委员会）建模为反事实引导的逻辑探索和抽象改进（清晰）循环。我们使用正式的符号执行和满足性模量理论（SMT）的方法来解除有关人类研究者自适应提出的事实和反事实场景中的代理行为的查询。为了这样做，对于决策算法$ \ mathcal {a} $，我们使用符号执行将其逻辑表示为确定理论中的语句$ \ pi $，$ \ texttt {qf_fpbv} $。我们实施我们的框架，并在说明性的车祸场景中演示其实用性。
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 $\Pi$ in the decidable theory $\texttt{QF_FPBV}$. We implement our framework and demonstrate its utility on an illustrative car crash scenario.
登录
查看更多内容
DOI：
10.1007/978-3-030-81685-8_9
发表时间：
2021
期刊：
--
影响因子：
--
作者：
M. Christakis;Hasan Ferit Eniser;H. Hermanns;J. Hoffmann;Yugesh Kothari;Jianlin Li;J. Navas;Valentin Wüstholz
通讯作者：
M. Christakis;Hasan Ferit Eniser;H. Hermanns;J. Hoffmann;Yugesh Kothari;Jianlin Li;J. Navas;Valentin Wüstholz
DOI：
10.1109/ase.2017.8115670
发表时间：
2017-10
期刊：
2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE)
影响因子：
--
作者：
D. Liew;Daniel Schemmel;Cristian Cadar;Alastair F. Donaldson;Rafael Zähl;Klaus Wehrle
通讯作者：
D. Liew;Daniel Schemmel;Cristian Cadar;Alastair F. Donaldson;Rafael Zähl;Klaus Wehrle
DOI：
10.1109/icdcs.2019.00117
发表时间：
2019-07
期刊：
2019 IEEE 39th International Conference on Distributed Computing Systems (ICDCS)
影响因子：
--
作者：
Man-Ki Yoon;Zhong Shao
通讯作者：
Man-Ki Yoon;Zhong Shao
DOI：
10.24963/ijcai.2023/42
发表时间：
2023
期刊：
International Joint Conferences on Artificial Intelligence Organization
影响因子：
--
作者：
Cano Córdoba, Filip;Judson, Samuel;Antonopoulos, Timos;Bjørner, Katrine;Shoemaker, Nicholas;Shapiro, Scott J.;Piskac, Ruzica;Könighofer, Bettina
通讯作者：
Könighofer, Bettina