AI Verification : First International Symposium, SAIV 2024, Montreal, QC, Canada, July 22–23, 2024, Proceedings / edited by Guy Avni, Mirco Giacobbe, Taylor T. Johnson, Guy Katz, Anna Lukina, Nina Narodytska, Christian Schilling.

Format:

Book

Author/Creator:

Avni, Guy.

Contributor:

Giacobbe, Mirco.

Johnson, Taylor T.

Katz, Guy.

Lukina, Anna.

Narodytska, Nina.

Schilling, Christian.

Series:

Lecture Notes in Computer Science, 1611-3349 ; 14846

Language:

English

Subjects (All):

Artificial intelligence.

Artificial Intelligence.

Local Subjects:

Artificial Intelligence.

Physical Description:

1 online resource (197 pages)

Edition:

1st ed. 2024.

Place of Publication:

Cham : Springer Nature Switzerland : Imprint: Springer, 2024.

Summary:

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.

Contents:

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

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

Concept-Based Analysis of Neural Networks via Vision-Language Models

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

7 Conclusion

A Proofs

B Captions Used for Computing CLIP Text Embeddings

C Verification of CLIP

Parallel Verification for -Equivalence of Neural Network Quantization

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

Verification of Neural Network Control Systems in Continuous Time

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

A Preliminary Study to Examining Per-class Performance Bias via Robustness Distributions

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

Clover: Closed-Loop Verifiable Code Generation

2 Preliminaries: Deductive Program Verification

3 Clover

3.1 Clover Generation Phase

3.2 Clover Verification Phase

3.3 Consistency Checking Example

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

Provable Repair of Vision Transformers

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.1 Formal Methods for Training and Verification

5.2 Provable Repair of DNNs

5.3 Transformer Editing

A Experiment 2 Results

B Experiment 3 Additional Results

C Experiment 4: Comparison with StdLP on Reduced Vision Transformers

D Experiment 5: Scalability Study

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

Author Index.

Notes:

Description based on publisher supplied metadata and other sources.

ISBN:

9783031651120

OCLC:

1449630148