Towards a Maude-Based Approach for Formal Modeling Deep Neural Networks
摘要
Rapid evolution of Deep Learning (DL) and its underlying architecture, Deep Neural Networks (DNNs), presents both significant advances and ethical challenges. As DNNs become increasingly prevalent across various sectors, ensuring their reliability, interpretability, and robustness becomes paramount. However, this also poses considerable challenges, particularly in understanding their internal workings and ensuring that their behavior complies with ethical and legal standards. The objective of this work is to propose a new approach to respond to these challenges by integrating formal methods, notably exploiting the Maude language. Our method emphasizes the creation of multi-view models to capture different aspects of DNNs, thus facilitating comprehensive understanding and analysis. Through the application of Model Driven Engineering (MDE) principles and Maude language features, our approach enables the formalization of DNNs structures, initialization mechanisms, and processing. We demonstrate the utility of our approach by presenting a meta-model for DNNs and providing a detailed formal specification in Maude. Their dynamic behavior is described with rewriting rules to model operational dynamics. Our results indicate that the proposed approach provides a solid basis for understanding and modeling the behavior of DNNs, thereby contributing to their reliability and robustness in critical applications.