ABSTRACT

Medical images, such as computed tomography (CT) and magnetic resonance imaging (MRI) scans, are routinely transformed and analyzed using computers and software. Medical images are increasingly processed and analyzed with artificial-intelligence and machine-learning methods, such as deep neural networks. In such safety-critical domains, stringent guarantees on the behaviors of these machine-learning methods are essential, but many recent studies have shown risks with these methods, such as lack of robustness and bias. Neural-network formal verification is emerging as an approach to provide guarantees on these machine-learning models to precisely characterize their behaviors. This project's novelties are to develop a neural-network formal-specification and -verification framework for medical-image analysis tasks, apply it to ensure specifications across the medical-image-analysis technology stack, and evaluate it on two specific medical-imaging analysis tasks. The first image-analysis task is the segmentation of brain lesions from MRIs of multiple-sclerosis patients, which is the process of automatically characterizing different regions of the MRIs into corresponding anatomic structures. The second image-analysis task is image synthesis for denoising optical-coherence-tomography (OCT) scans of the retina. The project's impacts are to enable medical-imaging analysis by enhancing confidence in the machine-learning models through formal verification. Beyond the development and application of these formal methods to medical-imaging analysis, the results of this project may enhance trustworthiness in other domains, such as perception and sensing components in autonomous systems.

Most neural-network verification methods developed so far are applicable only to simple computer-vision tasks, such as image classification, whereas medical image analysis typically requires more sophisticated generative computer-vision methods to solve more sophisticated tasks, such as semantic segmentation, instance segmentation, and image synthesis. Developing formal methods for these generative computer-vision tasks in the context of medical-imaging analysis is the core of this project. The first major objective of the project is to develop a robustness-specification framework, building on robustness to adversarial perturbations, specification mining, and metrics from computer vision used for generative tasks. The second major objective is to develop the formal-verification methods, building on reachability analysis of neural networks, specifically developing reachability methods for up-sampling layers used in generative models. The third major objective is to consider the robustness of generative models for image synthesis, such as those trained through generative-adversarial-network (GAN) processes. The fourth major objective is to evaluate these specification and verification methods on the MS lesion segmentation and OCT image-synthesis denoising tasks. The researchers will organize relevant competitions and challenges, such as continuing the Verification of Neural Networks Competition (VNN-COMP) and the IEEE ISBI Longitudinal MS Lesion Segmentation Challenge, and will develop benchmarks for the formal-methods, machine-learning, computer-vision, and medical-imaging-analysis research communities based on the research and results of this project.

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.

Please report errors in award information by writing to: awardsearch@nsf.gov.