Neural transition system abstraction for neural network dynamical system models and its application to Computational...

Area of Science:

• Computer Science
• Artificial Intelligence
• Formal Methods

Background:

• Data-driven models, particularly neural networks, often lack interpretability.
• Formal verification methods are crucial for ensuring system reliability and safety.
• Existing verification techniques may struggle with the complexity of neural network dynamics.

Purpose of the Study:

• To propose an explainable abstraction-based verification method for neural network models.
• To enhance the interpretability and user interaction in the verification process.
• To enable formal verification of system behavior against specifications.

Main Methods:

• State space partitioning using a data-driven process to abstract system dynamics.
• Employing set-valued reachability analysis to estimate subsystem relationships.
• Constructing a neural transition system abstraction from the neural network model.
• Verifying the abstracted model using Computational Tree Logic (CTL).

Main Results:

• The proposed method successfully abstracts complex system dynamics into understandable state labels.
• Formal verification of neural network models is achieved through the constructed abstraction.
• The framework demonstrates enhanced interpretability and validation capabilities.
• Examples with Maglev and handwritten models illustrate the framework's effectiveness.

Conclusions:

• The developed abstraction-based verification method significantly improves the interpretability of data-driven models.
• The framework provides a robust approach for formal verification of neural network behavior using CTL.
• This method facilitates validating complex systems against user-specified properties.