DASS: Accountability from Attention, not Assumption

现代软件和网络物理系统在复杂的环境中面临着无限制的任务，这使得在发生伤害或伤害事件时的责任对社会和技术进程来说都是一个日益严峻的挑战。尽管众所周知的技术可以判断程序是否遵守形式属性，但这个过程提供的真实世界的保证取决于它的范围和精度。当每个代理根据其系统模型和对其状态的了解正确操作时，甚至可能发生危害。有必要了解自主代理人对损害的贡献，以便考虑反事实并核实这些代理人是否采取了适当的行动。哲学和法律使用诸如信念、愿望和意图之类的决策构件作为此类评估的基础，促使人们理解它们是如何在现代软件系统中产生的。该项目的新奇之处在于(I)使用形式推理来确保这些决策构件的机器模拟将被忠实地记录用于责任过程；以及(Ii)对如何使用这些构件来指导更符合责任评估的软件开发的调查。该项目的影响包括(I)开发形式化方法以确保保留信息的充分性和帮助开发人员达到该目的的编程语言构造，以及(Ii)构建有助于以适应性的、值中立的方式评估责任的框架。更具体地说，该项目的目的是评估如何使用认知和其他模式逻辑的工具来指导作为代理的行为、愿望、信念和意图的信息的形式化，并开发可验证的跟踪属性--可逆性--它保证以有利于回顾分析的方式记录关于这些决策构件的必要信息。此外，该项目致力于将信息如何指定与不同哲学流派对潜在文物的解释方式脱钩，例如道义论或功利主义伦理。这一奖项反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.