EAGER: Causal Analysis through Formal Reasoning and AI for Cancer Diagnostics

科学研究有两个目的：(1)发现一种自然现象之间以前未知的联系；(2)对这些现象之间的因果关系给出精确的机制解释。在这两者中，解释是实现全球影响最关键的。确定自然现象的原因不仅使我们能够预测它们未来的发生，而且还意味着我们可以预防或治疗这些事件的方法（例如，基因突变对癌症发展的影响）。在医疗领域尤其如此，错误的治疗可能导致灾难性的后果。事实上，医学领域主要侧重于确定相关性，而不是因果关系。这种根本原因分析和基于因果关系的预测模型对于更准确的诊断和及时选择适当的治疗类型至关重要。该项目的新颖和影响在于设计技术，将自动形式推理和人工智能（AI）结合起来，发现事件之间的因果关系，以回答有关某些医疗条件真正原因的深层问题。该项目建立了一个重要的基础设施，用于收集初步数据和设计概念验证技术，这些技术证明了该项目基于形式推理和人工智能提取健康和医疗领域因果结构的方法的可行性。该项目首先调查了两种不同的因果关系概念（Halpern-Pearl和Granger），并探讨了它们在医学领域的适用性。然后，该项目将提取因果结构的问题减少到解决自动推理上某些问题的决策过程中。为此，该项目利用现成的决策程序来解决量化布尔公式（QBF）和可满足模理论（SMT）的可满足性问题。在概率和预测设置中，该项目结合了概率系统的模型检查器，以对从医疗数据和格兰杰/概率因果关系生成的模型进行推理。最后，为了解决因果关系自动形式推理中的可扩展性问题，该项目将开发的技术与人工智能相结合，并在训练阶段将人工智能与形式推理相结合。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Scientific investigations have two purposes: (1) discovering previously unknown associations between a natural phenomenon, and (2) generating precise mechanistic explanations for how the phenomena are causally related. Among these two, explanation is the most critical to achieve global impact. Identifying the cause of natural phenomena not only enables us to predict their future occurrences, but also implies the means in which we may prevent or treat such events (e.g., the effect of genetic mutations on development of cancer). This is particularly true in the medical domain, where erroneous treatments can result in catastrophic consequences. Indeed, the medical domain mainly focuses on identifying correlations rather than causation. Such root-cause analysis and causality-based predictive modeling are critically needed for more accurate diagnosis and the timely selection of an appropriate type of therapy. The project's novelties and impact are designing techniques by combining automated formal reasoning and artificial intelligence (AI) to discover the causal relation between events to answer deep questions on real causes of certain medical conditions.The project builds a prominent infrastructure for collecting preliminary data and designing proof of concept techniques that demonstrate the viability of this project’s approach based on formal reasoning and AI to extract causal structures in health and medical domains. The project first investigates two different notions of causality (Halpern-Pearl and Granger) and explores their fitness in the medical domain. Then, the project reduces the problem of extracting causal structures to decision procedures that solve certain problems on automated reasoning. To this end, the project utilizes off-the-shelf decision procedures for solving the satisfiability problem for quantified Boolean formulas (QBF) and satisfiability modulo theory (SMT). In the probabilistic and predictive settings, the project incorporates model checkers for probabilistic systems to reason about models generated from medical data and Granger/probabilistic causality. Finally, in order to tackle the scalability issues in automated formal reasoning about causality, the project combines the developed techniques with AI, and augments AI with formal reasoning during the training phase.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.