Towards Probability-based Safety Verification of Systems with Components from Machine Learning
Machine learning (ML) has recently created many new success stories. Hence, there is a strong motivation to use ML technology in software-intensive systems, including safety-critical systems. This raises the issue of safety verification of MLbased systems, which is currently thought to be infeasible or, at least, very hard. We think that it requires taking into account specific properties of ML technology such as: (i) Most ML approaches are inductive, which is both their power and their source of error. (ii) Neural networks (NN) resulting from deep learning are at the current state of the art not transparent. Consequently, there will always be errors remaining and, at least for deep NNs (DNNs), verification of their internal structure is extremely hard. In general, safety engineering cannot provide full guarantees that no harm will ever occur. That is why probabilities are used, e.g., for specifying a risk or a Tolerable Hazard Rate (THR). In this vision paper, we propose verification based on probabilities of errors both estimated by controlled experiments and output by the inductively learned classifier itself. Generalization error bounds may propagate to the probabilities of a hazard, which must not exceed a THR. As a result, the quantitatively determined bound on the probability of a classification error of an ML component in a safety-critical system contributes in a well-defined way to the latter's overall safety verification.
Code (0)
등록된 구현이 없습니다.
Tasks
BIG-bench Machine LearningSimilar Papers 제목 키워드 기반
Verification for Machine Learning, Autonomy, and Neural Networks Survey
This survey presents an overview of verification techniques for autonomous systems, with a focus on safety-critical autonomous cyber-physical systems (CPS) and subcomponents thereof. Autonomy in CPS is enabling by recent…
BIG-bench Machine LearningGeneral ClassificationSurveyNeuroCodeBench: a plain C neural network benchmark for software verification
Safety-critical systems with neural network components require strong guarantees. While existing neural network verification techniques have shown great progress towards this goal, they cannot prove the absence of softwa…
Density EstimationWhat, Indeed, is an Achievable Provable Guarantee for Learning-Enabled Safety Critical Systems
Machine learning has made remarkable advancements, but confidently utilising learning-enabled components in safety-critical domains still poses challenges. Among the challenges, it is known that a rigorous, yet practical…
A Review of Formal Methods applied to Machine Learning
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…
BIG-bench Machine LearningSufficient and Necessary Barrier-like Conditions for Safety and Reach-avoid Verification of Stochastic Discrete-time Systems
In this paper, we examine necessary and sufficient barrier-like conditions for infinite-horizon safety verification and reach-avoid verification of stochastic discrete-time systems, derived through a relaxation of Bellma…