“让汽车站上证人席”：基于SMT的决策调查预言机
计算机科学中的逻辑
2024-01-31 v2 计算机与社会
编程语言
摘要
在危害发生后进行有原则的责任追究，对于算法决策的可信设计与治理至关重要。法律理论提供了一种评估罪责的重要方法：让行为主体“站上证人席”，使其在交叉质询中接受对其行为与意图的审查。我们表明，在极小假设下，自动化推理可以如同法律事实发现的对抗过程一般严格审问算法行为。我们将问责过程（如审判或审查委员会）建模为反事实引导的逻辑探索与抽象精化 (CLEAR) 循环。我们使用符号执行与可满足性模理论 (SMT) 求解的形式化方法，来解答由人类调查者自适应提出的关于主体在事实与反事实情景中行为的查询。为此，对于决策算法 ，我们使用符号执行将其逻辑表示为可判定理论 \texttt{QF_FPBV} 中的语句 。我们实现了该框架，并在一个说明性的车祸场景中展示了其实用性。
引用
@article{arxiv.2305.05731,
title = {'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions},
author = {Samuel Judson and Matthew Elacqua and Filip Cano and Timos Antonopoulos and Bettina Könighofer and Scott J. Shapiro and Ruzica Piskac},
journal= {arXiv preprint arXiv:2305.05731},
year = {2024}
}