AI Verification
First International Symposium, SAIV 2024, Montreal, QC, Canada, July 22-23, 2024, Proceedings
Published on 16. July 2024
IX, 189 pages
978-3-031-65112-0 (ISBN)
Description
This LNCS volume constitutes the proceedings of the First International Symposium on AI Verification, SAIV 2024, in Montreal, QC, Canada, during July 2024.
The scope of the topics was broadly categorized into two groups. The first group, formal methods for artificial intelligence, comprised: formal specifications for systems with AI components; formal methods for analyzing systems with AI components; formal synthesis methods of AI components; testing approaches for systems with AI components; statistical approaches for analyzing systems with AI components; and approaches for enhancing the explainability of systems with AI components. The second group, artificial intelligence for formal methods, comprised: AI methods for formal verification; AI methods for formal synthesis; AI methods for safe control; and AI methods for falsification.
More details
Series
Language
English
Place of publication
Cham
Switzerland
Publishing group
Springer International Publishing
Target group
Professional and scholarly
Product notice
Reflowable
Illustrations
IX, 189 p. 54 illus., 46 illus. in color.
File size
13,00 MB
ISBN-13
978-3-031-65112-0 (9783031651120)
DOI
10.1007/978-3-031-65112-0
Schweitzer Classification
Other editions
Additional editions
Guy Avni | Mirco Giacobbe | Taylor T. Johnson
AI Verification
First International Symposium, SAIV 2024, Montreal, QC, Canada, July 22-23, 2024, Proceedings
Book
07/2024
Springer
€139.09
Shipment within 15-20 days
Content
- Intro
- Preface
- Organization
- Contents
- Chronosymbolic Learning: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning
- 1 Introduction
- 2 Preliminaries
- 2.1 Constrained Horn Clauses
- 2.2 CHC Solving as a Symbolic Classification Problem
- 3 Chronosymbolic Learning
- 3.1 Architecture of Chronosymbolic Learning
- 3.2 Samples and Zones
- 3.3 Incorporate Zones Within Learning Iterations
- 3.4 Overall Algorithm
- 4 Design of Learner and Reasoner
- 4.1 Learner: Data-Driven CHC Solving
- 4.2 Reasoner: Zones Discovery
- 5 Experiments
- 5.1 Experimental Settings
- 5.2 Baselines
- 5.3 Performance Evaluation
- 5.4 Ablation Study
- 6 Related Work
- 7 Discussion and Future Work
- 8 Conclusion
- A Extended Preliminary
- A.1 Extended Related Work
- A.2 CHCs and Program Safety Verification
- A.3 Support Vector Machine
- A.4 Decision Tree
- B Solution Space Analysis
- C Implementation Details
- C.1 Learner: Data-Driven CHC Solving
- C.2 Reasoner: Zones Discovery
- C.3 Preprocessing of CHC Systems
- D Experimental Details
- D.1 Statistics About the Benchmarks
- D.2 Detailed Settings for Chronosymbolic-cover
- D.3 Results on Using Different Random Seeds in DT
- D.4 Running Time Analysis
- References
- Error Analysis of Shapley Value-Based Model Explanations: An Informative Perspective
- 1 Introduction
- 2 Background
- 2.1 Notation
- 2.2 Informative SVA
- 3 Observation Bias and Structural Bias Trade-Off
- 3.1 Overfitting and Underfitting of the RF
- 3.2 Explanation Error Decomposition
- 3.3 Over-Informative Explanation
- 3.4 Under-Informative Explanation
- 3.5 Explanation Error Analysis of Data-Smoothing Methods
- 3.6 Explanation Error Analysis of Distributional Assumptions-Based Methods
- 4 OOD Measurement of Distribution Drift
- 4.1 Distribution Drift and OOD Detection
- 5 Experiments
- 5.1 Distribution Drift Detection
- 5.2 Under-Informativeness Audit
- 5.3 Over-Informativeness Audit
- 6 Conclusions
- References
- Concept-Based Analysis of Neural Networks via Vision-Language Models
- 1 Introduction
- 2 Preliminaries
- 3 Conspec Specification Language
- 3.1 Syntax
- 3.2 Semantics
- 4 Vision-Language Models as Analysis Tools
- 5 Case Study
- 5.1 Dataset, Concepts, and Strength Predicates
- 5.2 Models
- 5.3 Extraction of Concept Representations
- 5.4 Statistical Validation of rep via Strength Predicates
- 5.5 Verification
- 6 Related Work
- 7 Conclusion
- A Proofs
- B Captions Used for Computing CLIP Text Embeddings
- C Verification of CLIP
- References
- Parallel Verification for -Equivalence of Neural Network Quantization
- 1 Introduction
- 2 Related Work
- 3 Preliminaries
- 3.1 Quantized Neural Networks (QNNs)
- 4 -Equivalence
- 5 MILP Encoding
- 6 Symbolic Interval Analysis
- 7 Parallelization
- 7.1 Process Management
- 7.2 Partitioning Strategies
- 8 Experiments
- 9 Efficiency
- 10 Verification Results
- 10.1 Local -Equivalence
- 10.2 Global -Equivalence
- 11 Conclusion
- References
- Verification of Neural Network Control Systems in Continuous Time
- 1 Introduction
- 2 Background
- 2.1 Fixed Vs. Continuous Actuation
- 2.2 Open-Loop Neural Network Verification
- 2.3 State-Based Neural Network Controller Verification
- 2.4 Image-Based Neural Network Controller Verification
- 3 Methodology
- 4 Evaluation
- 4.1 Autonomous Aircraft Taxiing System
- 4.2 Closed-Loop Verification
- 4.3 Verification of Abstraction Error
- 5 Related Work
- 6 Conclusion
- References
- A Preliminary Study to Examining Per-class Performance Bias via Robustness Distributions
- 1 Introduction
- 2 Background
- 3 Setup of Experiments
- 4 Results
- 4.1 Robustness Distributions
- 4.2 Per-class One-to-Any Verification
- 4.3 Per-class One-to-One Verification
- 5 Conclusions and Future Work
- A Overview of Used Networks
- B Kolmogorov-Smirnov Tests
- B.1 Robustness Distributions Aggregated
- B.2 One-to-Any KS Statistics per Network
- B.3 One-to-Any KS Statistics per Class
- B.4 One-to-One KS Statistics per Network
- B.5 One-to-One KS Statistics per Class
- References
- Clover: Closed-Loop Verifiable Code Generation
- 1 Introduction
- 2 Preliminaries: Deductive Program Verification
- 3 Clover
- 3.1 Clover Generation Phase
- 3.2 Clover Verification Phase
- 3.3 Consistency Checking Example
- 4 Evaluation
- 4.1 Dataset: CloverBench
- 4.2 Generation Phase
- 4.3 Verification Phase: Results on Ground-Truth Examples
- 4.4 Verification Phase: Results on MBPP-DFY-50
- 4.5 Verification Phase: Results on Adversarial Examples
- 4.6 A Preliminary Study with Verus
- 5 Related Work
- 6 Conclusion
- References
- Provable Repair of Vision Transformers
- 1 Introduction
- 2 Preliminaries
- 2.1 Provable Repair of Deep Neural Networks
- 2.2 Vision Transformers
- 2.3 Prior Approaches
- 2.4 StdLP Baseline
- 2.5 FTall Baseline
- 3 Approach
- 3.1 Last Layer Fine Tuning: PRoViTFT
- 3.2 Novel LP Formulation: PRoViTLP
- 3.3 PRoViTFT+LP
- 4 Experimental Evaluation
- 4.1 Experiment 1: Comparison with FTall
- 4.2 Experiment 2: Comparison with StdLP
- 4.3 Experiment 3: Comparison Across Architectures
- 5 Related Work
- 5.1 Formal Methods for Training and Verification
- 5.2 Provable Repair of DNNs
- 5.3 Transformer Editing
- 6 Conclusion
- A Experiment 2 Results
- B Experiment 3 Additional Results
- C Experiment 4: Comparison with StdLP on Reduced Vision Transformers
- D Experiment 5: Scalability Study
- References
- Iterative Counter-Example Guided Robustness Verification for Neural Networks
- 1 Introduction
- 2 Abstraction-Refinement Strategy
- 2.1 Robustness Verification Objective
- 2.2 Property-Based Abstraction
- 2.3 Inactive Neuron Based Abstraction Augmentation
- 2.4 Augmented Property Specification
- 2.5 Refinement of Abstraction
- 2.6 Iterative Abstraction-Verification-Refinement Steps
- 3 Preliminary Experimental Evaluation
- 4 Conclusion
- References
- Author Index
