DASS: Accountability from Attention, not Assumption

点击翻译按钮获取中文摘要

Modern software and cyberphysical systems face open-ended tasks in complex environments, rendering accountability in the event of harm or injury an ever-growing challenge for both social and technical processes. Although well-understood techniques can judge whether programs obey formal properties, the real-world assurance that this process provides depends on its scope and precision. Harms can even occur when every agent operates correctly according to its model of the system and knowledge of its state. An understanding of the contribution of autonomous agents to a harm is necessary in order to consider counterfactuals and verify whether those agents acted appropriately. Philosophy and law employ decision artifacts such as beliefs, desires, and intentions as the basis for such assessments, motivating an understanding of how they arise within modern software systems. The project's novelties are (i) the use of formal reasoning to assure the machine analogues of these decision artifacts will be faithfully recorded for accountability processes; and (ii) an investigation of how these artifacts can be used to guide development of software more amenable to responsibility assessment. The project's impacts include (i) the development of formal methods to assure the sufficiency of retained information and programming languages constructs that assist developers to that end, and (ii) the construction of frameworks that contribute to the assessment of responsibility in an adaptable, value-neutral manner.More specifically, the aim of this project is to evaluate how the tools of epistemic and other modal logics can be used to guide formalization of the information underlying the actions, desires, beliefs and intentions of an agent, and to develop a verifiable trace property -- reversibility -- which guarantees that the necessary information regarding those decision artifacts is recorded in a manner conducive to retrospective analysis. Furthermore, this project strives to decouple how information is specified from how the underlying artifacts are interpreted by the different philosophical schools, such as deontological or utilitarian ethics.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.