PRG4CNN: A Probabilistic Model Checking-Driven Robustness Guarantee Framework for CNNs.

Area of Science:

• Artificial Intelligence
• Robotics
• Computer Vision

Background:

• Convolutional Neural Networks (CNNs) are vital for autonomous robots but often lack robustness against input perturbations.
• Existing formal verification methods for CNN robustness are time-consuming and focus on local properties.
• Probabilistic robustness offers a practical measure, but current verification is manual and lacks repair mechanisms.

Purpose of the Study:

• To develop an automated framework for guaranteeing probabilistic robustness of CNNs.
• To integrate robustness verification with automated repair for enhanced AI safety.
• To address the limitations of existing test-driven and local robustness verification approaches.

Main Methods:

• Proposed PRG4CNN, a probabilistic model checking-driven framework for CNN robustness.
• Modeled CNNs as Markov Decision Processes (MDPs) using model learning.
• Specified probabilistic robustness using Probabilistic Computational Tree Logic (PCTL) formulas.
• Implemented counterexample-guided sensitivity analysis for robustness repair.

Main Results:

• Demonstrated the effectiveness of PRG4CNN on various CNNs trained on the MNIST dataset.
• Achieved automated verification and repair of probabilistic robustness for CNNs.
• Showcased PRG4CNN as the first automated and complete framework for this task.

Conclusions:

• PRG4CNN provides an effective, automated solution for guaranteeing probabilistic robustness in CNNs.
• The framework enhances the reliability and safety of AI systems, particularly in robotics.
• This work advances the field of formal verification for deep neural networks.