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

Michigan State University, East Lansing MI

Investigators

Abstract

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.