Software Verification and Formal Methods for ML-Enabled Autonomous Systems (Lecture Notes in Computer Science)

✍ Scribed by Omri Isac (editor), Radoslav Ivanov (editor), Guy Katz (editor), Nina Narodytska (editor), Laura Nenzi (editor)

• Publisher: Springer
• Year: 2022
• Tongue: English
• Leaves: 213
• Category: Library

✦ Synopsis

This book constitutes the refereed proceedings of the 5th International Workshop on Software Verification and Formal Methods for ML-Enables Autonomous Systems, FoMLAS 2022, and the 15th International Workshop on Numerical Software Verification, NSV 2022, which took place in Haifa, Israel, in July/August 2022.
The volume contains 8 full papers from the FoMLAS 2022 workshop and 3 full papers from the NSV 2022 workshop. The FoMLAS workshop is dedicated to the development of novel formal methods techniques to discussing on how formal methods can be used to increase predictability, explainability, and accountability of ML-enabled autonomous systems. NSV 2022 is focusing on the challenges of the verification of cyber-physical systems with machine learning components.

✦ Table of Contents

FoMLAS 2022 Preface
FoMLAS 2022 Organization
NSV 2022 Preface
NSV 2022 Organization
Contents
FoMLAS 2022
VPN: Verification of Poisoning in Neural Networks-12pt
1 Introduction
2 Model Poisoning as a Safety Property
2.1 Model Poisoning Formulation
2.2 Checking for Poisoning
2.3 Achieving Scalability via Attack Transferability
3 Evaluation
3.1 Setup
3.2 Results on MNIST
3.3 Results on GTSRB
3.4 Results on Clean Models
4 Conclusion
References
A Cascade of Checkers for Run-time Certification of Local Robustness
1 Introduction
2 Background
3 Ensuring Local Robustness
3.1 Local Robustness via Training
3.2 Run-time Checks for Local Robustness
4 A Cascade of Run-time Local Robustness Checkers
5 Case Studies
5.1 MNIST
5.2 SafeSCAD
6 Conclusion
References
CEG4N: Counter-Example Guided Neural Network Quantization Refinement
1 Introduction
2 Preliminaries
2.1 Neural Network
2.2 Quantization
2.3 NNQuantization
2.4 NNEquivalence
2.5 Verification of NNProperties
3 Counter-Example Guided Neural Network Quantization Refinement (CEG4N)
3.1 Robust Quantization as a Minimization Problem
3.2 The CEG4NFramework Implementation
4 Experimental Evaluation
4.1 Description of the Benchmarks
4.2 Setup
4.3 Objectives
4.4 Results
4.5 Limitations
5 Conclusion
A Appendices
A.1 Implementation of NNs in Python.
A.2 Implementation of NNs abstract models in C.
A.3 Encoding of Equivalence Properties
A.4 Genetic Algorithm Parameters Definition
References
Minimal Multi-Layer Modifications of Deep Neural Networks
1 Introduction
2 Background
3 3M-DNN: Finding Multi-Layer DNN Changes
3.1 The Search Level
3.2 The Single-Layer Modification Level
4 Implementation
5 Evaluation
6 Related Work
7 Conclusion and Future Work
References
Differentiable Logics for Neural Network Training and Verification
1 Introduction
2 Differentiable Logic and Constraint Cased Loss Functions
3 Property Based Approach
4 Conclusions and Future Work
4.1 Conclusions
4.2 Future Work and Design Space
References
Neural Networks in Imandra: Matrix Representation as a Verification Choice-12pt
1 Motivation
2 Matrices in Neural Network Formalisation
3 Matrices as Lists of Lists
4 Matrices as Functions
5 Real-Valued Matrices; Records and Arrays
5.1 Algebraic Data Types for Real-Valued Matrices
5.2 Real-Valued Matrix Indices
5.3 Records
6 Conclusions
References
Self-correcting Neural Networks for Safe Classification
1 Introduction
2 Problem Setting
2.1 Background
2.2 Problem Definition
3 Self-correcting Transformer
3.1 Overview
3.2 Algorithmic Details of SC-Layer
3.3 Key Properties
3.4 Complexity
3.5 Differentiability of SC-Layer
4 Vectorizing Self-correction
5 Evaluation
5.1 ACAS Xu
5.2 Collision Detection
5.3 Scaling to Larger Domains
5.4 Handling Arbitrary, Complex Constraints
6 Related Work
7 Conclusion and Future Directions
A Appendix 1: Proofs
B Appendix 2: Vectorizing Self-Correction
B.1 Stable Topological Sort
B.2 Cycle Detection
B.3 Prioritizing Root Vertices
C Appendix 3: Generation of Synthetic Data
References
Formal Specification for Learning-Enabled Autonomous Systems
1 Introduction
2 Formal Specifications
2.1 Event-Based Abstraction
3 Use Case Specifications from Learning-Enabled Autonomous Systems
3.1 Automated Valet Parking System
3.2 A Medical Autonomous System
4 Related Work
5 Concluding Remarks
References
NSV 2022
Verified Numerical Methods for Ordinary Differential Equations
1 Introduction
2 Main Result
3 Verified Error Bounds
3.1 Local Discretization Error
3.2 Propagation of Errors
3.3 Global Discretization Error
3.4 Local Round-Off Error
3.5 Global Round-Off Error
3.6 Total Global Error
4 Program Verification
5 Composing the Main Theorems
6 Soundness
7 Related Work
8 Conclusion and Future Work
References
Neural Network Precision Tuning Using Stochastic Arithmetic
1 Introduction
2 Preliminary
2.1 Neural Networks
2.2 Floating-Point Arithmetic
2.3 Discrete Stochastic Arithmetic (DSA)
2.4 The PROMISE Software
3 Methodology
4 Experimental Results
4.1 Sine Neural Network
4.2 MNIST Neural Network
4.3 CIFAR Neural Network
4.4 Inverted Pendulum
5 Conclusion and Perspectives
Appendix A Sine Neural Network
Appendix A.1 Type Distribution for Sine Approximation with Input Value 2.37 Considering One Type per Neuron
Appendix A.2 Type Distribution for Sine Approximation with Input Value 2.37 Considering One Type per Layer
Appendix B MNIST Neural Network
Appendix B.1 Type Distribution for MNIST with Test_data[61] Input Considering One Type per Layer
Appendix B.2 Type Distribution for MNIST with Test_data[91] Input Considering one type per neuron
Appendix B.3 Type Distribution for MNIST with Test_data[91] Input Considering One Type per Layer
Appendix C CIFAR Neural Network
Appendix C.1 Type Distribution for CIFAR with Test_data[386] Input Considering One Type per Layer
Appendix C.2 Type Distribution for CIFAR with Test_data[731] Input Considering One Type per Neuron
Appendix C.3 Type Distribution for CIFAR with Test_data[731] Input Considering One Type per Layer
Appendix D Inverted pendulum
Appendix D.1 Type Distribution for the Inverted Pendulum with Input (0.5,0.5) Considering One Type per Layer
Appendix D.2 Type Distribution for the Inverted Pendulum with Input (-3,-6) Considering One Type per Neuron
Appendix D.3 Type Distribution for the Inverted Pendulum with Input (-3,-6) Considering One Type per Layer
References
MLTL Multi-type (MLTLM): A Logic for Reasoning About Signals of Different Types
1 Introduction
2 Preliminaries
2.1 Signals and Trajectories
2.2 MLTL
2.3 R2U2
3 Mission-Time Temporal Logic Multi-type (MLTLM)
3.1 Equivalent MLTLM Formula for Every MLTL Formula
3.2 Evaluation of MLTLM Formula
3.3 Examples of Projections
3.4 Example Specifications Across Timescales
4 Equisatisfiable Formula in MLTL and an Implementation of an MLTLM Monitor with the Modulo-Reduction Projection
4.1 The Translator
4.2 An Efficient MLTLM Engine
4.3 Optimization Results
5 Conclusion
References
Author Index