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

EAGER：通过形式推理和人工智能进行癌症诊断的因果分析

• 批准号: 2320050
• 负责人: Borzoo Bonakdarpour
• 金额: $ 24万
• 依托单位: Michigan State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-07-01 至 2024-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2320050&HistoricalAwards=false
• 关键词: EAGER; Causal; Analysis; through; Formal

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.

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