FMitF: Track I: Generative Neural Network Verification in Medical Imaging Analysis

医学图像，如计算机断层扫描(CT)和磁共振成像(MRI)扫描，通常使用计算机和软件进行转换和分析。医学图像越来越多地使用人工智能和机器学习方法进行处理和分析，例如深度神经网络。在这样的安全关键领域，对这些机器学习方法的行为进行严格的保证是必不可少的，但最近的许多研究表明，这些方法存在风险，例如缺乏健壮性和偏差。神经网络形式验证正在成为一种方法，可以为这些机器学习模型提供保证，以准确地描述它们的行为。该项目的创新之处在于为医学图像分析任务开发了一个神经网络形式规范和验证框架，将其应用于确保整个医学图像分析技术堆栈的规范，并在两个特定的医学图像分析任务中对其进行评估。第一个图像分析任务是从多发性硬化症患者的磁共振成像中分割出大脑病变，这是一个自动将磁共振成像的不同区域表征为相应的解剖结构的过程。第二个图像分析任务是图像合成，用于对视网膜的光学相干断层扫描(OCT)进行去噪。该项目的影响是通过正式验证增强对机器学习模型的信心，从而实现医学成像分析。除了这些形式化方法在医学成像分析中的开发和应用之外，该项目的结果还可以提高其他领域的可信度，例如自主系统中的感知和传感组件。到目前为止，大多数神经网络验证方法只适用于简单的计算机视觉任务，如图像分类，而医学图像分析通常需要更复杂的生成性计算机视觉方法来解决更复杂的任务，如语义分割、实例分割和图像合成。在医学成像分析的背景下，为这些生成性计算机视觉任务开发形式化方法是该项目的核心。该项目的第一个主要目标是开发一个健壮性规范框架，建立在对对抗性扰动、规范挖掘和用于生成性任务的计算机视觉的度量的健壮性基础上。第二个主要目标是以神经网络的可达性分析为基础，开发形式验证方法，特别是为生成模型中使用的上采样层开发可达性方法。第三个主要目标是考虑用于图像合成的生成模型的稳健性，例如通过生成-对抗-网络(GAN)过程训练的生成模型。第四个主要目标是评估这些规范和验证方法在MS病变分割和OCT图像合成去噪任务中的应用。研究人员将组织相关的竞赛和挑战，如继续神经网络验证竞赛(VNN-COMP)和IEEE ISBI MS病变纵向分割挑战赛，并将根据该项目的研究和结果为正式方法、机器学习、计算机视觉和医学成像分析研究社区制定基准。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.