Capturing Dependencies Within Machine Learning via a Formal Process Model
Fabian Ritz and Thomy Phan and Andreas Sedlmeier and Philipp Altmann and Jan Wieghardt and Reiner Schmid and Horst Sauer and Cornel Klein and Claudia Linnhoff-Popien and Thomas Gabor.International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), pages 249--265, 2022.
[abstract] [bibtex] [doi] [pdf]
The development of Machine Learning (ML) models is more than just a special case of software development (SD): ML models acquire properties and fulfill requirements even without direct human interaction in a seemingly uncontrollable manner. Nonetheless, the underlying processes can be described in a formal way. We define a comprehensive SD process model for ML that encompasses most tasks and artifacts described in the literature in a consistent way. In addition to the production of the necessary artifacts, we also focus on generating and validating fitting descriptions in the form of specifications. We stress the importance of further evolving the ML model throughout its life-cycle even after initial training and testing. Thus, we provide various interaction points with standard SD processes in which ML often is an encapsulated task. Further, our SD process model allows to formulate ML as a (meta-) optimization problem. If automated rigorously, it can be used to realize self-adaptive autonomous systems. Finally, our SD process model features a description of time that allows to reason about the progress within ML development processes. This might lead to further applications of formal methods within the field of ML.
@inproceedings{ ritzISoLA22, author = "Fabian Ritz and Thomy Phan and Andreas Sedlmeier and Philipp Altmann and Jan Wieghardt and Reiner Schmid and Horst Sauer and Cornel Klein and Claudia Linnhoff-Popien and Thomas Gabor", title = "Capturing Dependencies Within Machine Learning via a Formal Process Model", year = "2022", abstract = "The development of Machine Learning (ML) models is more than just a special case of software development (SD): ML models acquire properties and fulfill requirements even without direct human interaction in a seemingly uncontrollable manner. Nonetheless, the underlying processes can be described in a formal way. We define a comprehensive SD process model for ML that encompasses most tasks and artifacts described in the literature in a consistent way. In addition to the production of the necessary artifacts, we also focus on generating and validating fitting descriptions in the form of specifications. We stress the importance of further evolving the ML model throughout its life-cycle even after initial training and testing. Thus, we provide various interaction points with standard SD processes in which ML often is an encapsulated task. Further, our SD process model allows to formulate ML as a (meta-) optimization problem. If automated rigorously, it can be used to realize self-adaptive autonomous systems. Finally, our SD process model features a description of time that allows to reason about the progress within ML development processes. This might lead to further applications of formal methods within the field of ML.", url = "https://link.springer.com/chapter/10.1007/978-3-031-19759-8_16", eprint = "https://thomyphan.github.io/files/2022-isola-preprint.pdf", publisher = "Springer Nature Switzerland", booktitle = "International Symposium on Leveraging Applications of Formal Methods, Verification and Validation", pages = "249--265", doi = "https://doi.org/10.1007/978-3-031-19759-8_16" }
Related Articles
- T. Gabor et al., “The Holy Grail of Quantum Artificial Intelligence: Major Challenges in Accelerating the Machine Learning Pipeline”, QSE 2020
- T. Gabor et al., “The Scenario Coevolution Paradigm: Adaptive Quality Assurance for Adaptive Systems”, STTT 2020