Neural Network Verification

Project Overview

This project focuses on developing efficient and scalable verification algorithms for neural networks to ensure their safety and reliability in critical applications such as autonomous driving and medical diagnosis. The primary goal is to determine whether there exists an input that satisfies a given constraint and simultaneously violates a specified property. We aim to create verification techniques that work across various types of neural networks, including deep neural networks, quantized networks, and reinforcement learning models. Additionally, the project will explore training methods to improve network safety and robustness.

Objectives

  • Verification algorithms: develop a suite of verification algorithms for neural networks, including GPU-based, SMT-based, incremental verification, CEGAR (CounterExample-Guided Abstraction Refinement), possibly robustness analysis, PAC-based verification, and other techniques.
  • Algorithm efficiency: focus on scalability and efficiency, ensuring that the developed algorithms can handle large, complex models commonly found in safety-critical applications.
  • Safety and reliability: develop techniques specifically designed for verifying the safety and reliability of neural networks used in safety-critical systems such as autonomous vehicles and other high-stakes applications.
  • Application-specific verification: create specialized verification techniques tailored to the unique characteristics and constraints of different neural network architectures, such as deep neural networks and reinforcement learning-based models.
  • Training techniques: investigate training methods that can improve the safety and robustness of neural networks, making them easier to verify and more reliable in real-world scenarios.

Deliverables

  • Verification algorithms: a set of scalable and efficient algorithms for verifying the safety and reliability of various types of neural networks.
  • Toolchain: a comprehensive verification toolchain that includes implementation, documentation, and setup instructions.
  • Case Studies: demonstrations of the developed algorithms applied to real-world safety-critical systems like autonomous driving.