A Review of Formal Methods applied to Machine Learning

• URL: http://arxiv.org/abs/2104.02466v1
• Date: Tue, 6 Apr 2021 12:48:17 GMT
• Title: A Review of Formal Methods applied to Machine Learning
• Authors: Caterina Urban and Antoine Min\'e
• Abstract summary: We review state-of-the-art formal methods applied to the emerging field of the verification of machine learning systems. We first recall established formal methods and their current use in an exemplar safety-critical field, avionic software. We then provide a comprehensive and detailed review of the formal methods developed so far for machine learning, highlighting their strengths and limitations.
• Score: 0.6853165736531939
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We review state-of-the-art formal methods applied to the emerging field of the verification of machine learning systems. Formal methods can provide rigorous correctness guarantees on hardware and software systems. Thanks to the availability of mature tools, their use is well established in the industry, and in particular to check safety-critical applications as they undergo a stringent certification process. As machine learning is becoming more popular, machine-learned components are now considered for inclusion in critical systems. This raises the question of their safety and their verification. Yet, established formal methods are limited to classic, i.e. non machine-learned software. Applying formal methods to verify systems that include machine learning has only been considered recently and poses novel challenges in soundness, precision, and scalability. We first recall established formal methods and their current use in an exemplar safety-critical field, avionic software, with a focus on abstract interpretation based techniques as they provide a high level of scalability. This provides a golden standard and sets high expectations for machine learning verification. We then provide a comprehensive and detailed review of the formal methods developed so far for machine learning, highlighting their strengths and limitations. The large majority of them verify trained neural networks and employ either SMT, optimization, or abstract interpretation techniques. We also discuss methods for support vector machines and decision tree ensembles, as well as methods targeting training and data preparation, which are critical but often neglected aspects of machine learning. Finally, we offer perspectives for future research directions towards the formal verification of machine learning systems.

Related papers

• Formal Methods for Autonomous Systems [21.989467515686858]
  Formal methods have played a key role in establishing the correctness of safety-critical systems. Main building blocks of formal methods are models and specifications. We consider correct-by-construction synthesis under various formulations.
  arXiv  Detail & Related papers  (2023-11-02T14:18:43Z)
• Formal and Practical Elements for the Certification of Machine Learning Systems [0.9217021281095907]
  We show how parameters of machine learning models are not hand-coded nor derived from physics but learned from data. As a result, requirements cannot be directly traced to lines of code, hindering the current bottom-up aerospace certification paradigm. Based on a scalable statistical verifier, our proposed framework is model-agnostic and tool-independent.
  arXiv  Detail & Related papers  (2023-10-05T00:20:59Z)
• Lessons from Formally Verified Deployed Software Systems (Extended version) [65.69802414600832]
  This article examines a range of projects, in various application areas, that have produced formally verified systems and deployed them for actual use. It considers the technologies used, the form of verification applied, the results obtained, and the lessons that the software industry should draw regarding its ability to benefit from formal verification techniques and tools.
  arXiv  Detail & Related papers  (2023-01-05T18:18:46Z)
• A Survey of Machine Unlearning [56.017968863854186]
  Recent regulations now require that, on request, private information about a user must be removed from computer systems. ML models often remember' the old data. Recent works on machine unlearning have not been able to completely solve the problem.
  arXiv  Detail & Related papers  (2022-09-06T08:51:53Z)
• An Overview and Prospective Outlook on Robust Training and Certification of Machine Learning Models [12.012612885618436]
  As learning algorithms become more popular in data-driven control systems, their robustness to data uncertainty must be ensured in order to maintain reliable safety-critical operations. We begin by reviewing common formalisms for such robustness, and then move on to discuss popular and state-of-the-art techniques for training robust machine learning models.
  arXiv  Detail & Related papers  (2022-08-15T23:09:54Z)
• Learning Physical Concepts in Cyber-Physical Systems: A Case Study [72.74318982275052]
  We provide an overview of the current state of research regarding methods for learning physical concepts in time series data. We also analyze the most important methods from the current state of the art using the example of a three-tank system.
  arXiv  Detail & Related papers  (2021-11-28T14:24:52Z)
• A Practical Tutorial on Explainable AI Techniques [5.671062637797752]
  This tutorial is meant to be the go-to handbook for any audience with a computer science background. It aims at getting intuitive insights of machine learning models, accompanied with straight, fast, and intuitive explanations out of the box.
  arXiv  Detail & Related papers  (2021-11-13T17:47:31Z)
• Multi Agent System for Machine Learning Under Uncertainty in Cyber Physical Manufacturing System [78.60415450507706]
  Recent advancements in predictive machine learning has led to its application in various use cases in manufacturing. Most research focused on maximising predictive accuracy without addressing the uncertainty associated with it. In this paper, we determine the sources of uncertainty in machine learning and establish the success criteria of a machine learning system to function well under uncertainty.
  arXiv  Detail & Related papers  (2021-07-28T10:28:05Z)
• Trusted Artificial Intelligence: Towards Certification of Machine Learning Applications [5.7576910363986]
  The T"UV AUSTRIA Group in cooperation with the Institute for Machine Learning at the Johannes Kepler University Linz proposes a certification process. The holistic approach attempts to evaluate and verify the aspects of secure software development, functional requirements, data quality, data protection, and ethics. The audit catalog can be applied to low-risk applications within the scope of supervised learning.
  arXiv  Detail & Related papers  (2021-03-31T08:59:55Z)
• Technology Readiness Levels for Machine Learning Systems [107.56979560568232]
  Development and deployment of machine learning systems can be executed easily with modern tools, but the process is typically rushed and means-to-an-end. We have developed a proven systems engineering approach for machine learning development and deployment. Our "Machine Learning Technology Readiness Levels" framework defines a principled process to ensure robust, reliable, and responsible systems.
  arXiv  Detail & Related papers  (2021-01-11T15:54:48Z)
• Towards CRISP-ML(Q): A Machine Learning Process Model with Quality Assurance Methodology [53.063411515511056]
  We propose a process model for the development of machine learning applications. The first phase combines business and data understanding as data availability oftentimes affects the feasibility of the project. The sixth phase covers state-of-the-art approaches for monitoring and maintenance of a machine learning applications.
  arXiv  Detail & Related papers  (2020-03-11T08:25:49Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.