Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

AutoSpec: Automated Generation of Neural Network Specifications

Shuowei Jin, Francis Y. Yan, Cheng Tan, Anuj Kalia, Xenofon Foukas, Z. Morley Mao

TL;DR

This paper introduces AutoSpec, the first framework to automatically generate comprehensive and accurate specifications for neural networks in learning-augmented systems and proposes the first set of metrics for assessing the accuracy and coverage of model specifications, establishing a benchmark for future comparisons.

Abstract

The increasing adoption of neural networks in learning-augmented systems highlights the importance of model safety and robustness, particularly in safety-critical domains. Despite progress in the formal verification of neural networks, current practices require users to manually define model specifications -- properties that dictate expected model behavior in various scenarios. This manual process, however, is prone to human error, limited in scope, and time-consuming. In this paper, we introduce AutoSpec, the first framework to automatically generate comprehensive and accurate specifications for neural networks in learning-augmented systems. We also propose the first set of metrics for assessing the accuracy and coverage of model specifications, establishing a benchmark for future comparisons. Our evaluation across four distinct applications shows that AutoSpec outperforms human-defined specifications as well as two baseline approaches introduced in this study.

AutoSpec: Automated Generation of Neural Network Specifications

TL;DR

This paper introduces AutoSpec, the first framework to automatically generate comprehensive and accurate specifications for neural networks in learning-augmented systems and proposes the first set of metrics for assessing the accuracy and coverage of model specifications, establishing a benchmark for future comparisons.

Abstract

The increasing adoption of neural networks in learning-augmented systems highlights the importance of model safety and robustness, particularly in safety-critical domains. Despite progress in the formal verification of neural networks, current practices require users to manually define model specifications -- properties that dictate expected model behavior in various scenarios. This manual process, however, is prone to human error, limited in scope, and time-consuming. In this paper, we introduce AutoSpec, the first framework to automatically generate comprehensive and accurate specifications for neural networks in learning-augmented systems. We also propose the first set of metrics for assessing the accuracy and coverage of model specifications, establishing a benchmark for future comparisons. Our evaluation across four distinct applications shows that AutoSpec outperforms human-defined specifications as well as two baseline approaches introduced in this study.
Paper Structure (23 sections, 2 equations, 8 figures, 3 tables, 4 algorithms)

This paper contains 23 sections, 2 equations, 8 figures, 3 tables, 4 algorithms.

Table of Contents

  1. Introduction
  2. Background and Related Work
  3. Providing Worst-Case Guarantees via Verification
  4. Automated Specification Generation
  5. Specification Quality Evaluation
  6. Specification Evaluation
  7. Specification Generation Algorithms
  8. Problem Statement
  9. Grid-based Generation
  10. Clustering-based Generation
  11. AutoSpec: Tree Traversing Generation
  12. Experimental Evaluation
  13. AutoSpec's performance
  14. Comparison with human-defined specifications
  15. Verifying DNNs with generated specifications
  16. ...and 8 more sections

Figures (8)

  • Figure 1: AutoSpec's workflow: AutoSpec starts by splitting the input data into specification generation and evaluation datasets. AutoSpec employs a specification generation algorithm (§\ref{['s:specgen']}) to generate candidate specifications. These specifications are assessed on the evaluation dataset (§\ref{['s:speceval']}), producing a set of quality metrics that describe their comprehensiveness and accuracy.
  • Figure 2: Visualization of the specification set generated by different algorithms.
  • Figure 3: Specification visualization on spec gen dataset.
  • Figure 4: Specification visualization on spec eval dataset.
  • Figure 5: Human-defined specifications vs. AutoSpec-generated specifications.
  • ...and 3 more figures