利用抽象-精化高效发现实际因果关系
Efficient Discovery of Actual Causality using Abstraction-Refinement
AI总结：
本文提出一种基于抽象-精化的SMT求解方法，用于高效发现迁移系统建模的计算系统中安全违规的实际原因，并在神经网络控制器、强化学习控制器和MPC控制器三个案例中验证了其有效性。
摘要：
因果关系是指一个事件对另一个事件的产生做出贡献的关系，其中原因对结果负有部分责任，而结果部分依赖于原因。在本文中，我们提出了一种新颖且有效的方法，用于对工程系统中事件的因果效应进行形式化推理，并应用于寻找嵌入式和信息物理系统中安全违规的根本原因。我们的动机来自Halpern和Pearl提出的实际因果关系概念，该概念关注特定事件的因果效应，而非试图对科学和自然现象做出一般性陈述的类型级因果关系。我们的第一个贡献是将以迁移系统建模的计算系统中实际因果关系的发现问题形式化为SMT求解问题。由于用于因果关系分析的数据集往往规模较大，为了解决自动化形式推理的可扩展性问题，我们的第二个贡献是一种基于抽象-精化的新技术，该技术允许在更小的抽象因果模型中识别实际原因。我们通过三个案例研究展示了我们方法的有效性（性能提升数个数量级），用于发现以下系统中安全违规的实际原因：（1）Mountain Car的神经网络控制器，（2）通过强化学习获得的Lunar Lander控制器，以及（3）F-16自动驾驶仪模拟器的MPC控制器。
英文摘要：
Causality is the relationship where one event contributes to the production of another, with the cause being partly responsible for the effect and the effect partly dependent on the cause. In this paper, we propose a novel and effective method to formally reason about the causal effect of events in engineered systems, with application for finding the root-cause of safety violations in embedded and cyber-physical systems. We are motivated by the notion of actual causality by Halpern and Pearl, which focuses on the causal effect of particular events rather than type-level causality, which attempts to make general statements about scientific and natural phenomena. Our first contribution is formulating discovery of actual causality in computing systems modeled by transition systems as an SMT solving problem. Since datasets for causality analysis tend to be large, in order to tackle the scalability problem of automated formal reasoning, our second contribution is a novel technique based on abstraction-refinement that allows identifying for actual causes within smaller abstract causal models. We demonstrate the effectiveness of our approach (by several orders of magnitude) using three case studies to find the actual cause of violations of safety in (1) a neural network controller for a Mountain Car, (2) a controller for a Lunar Lander obtained by reinforcement learning, and (3) an MPC controller for an F-16 autopilot simulator.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
