Specification Generation for Neural Networks in Systems

TL;DR

This work tackles the trustworthiness problem of neural networks deployed in computer systems by automatically generating expressive specifications from traditional reference algorithms. It formalizes specifications as Hoare-style preconditions and postconditions ${\varphi_{\mathcal{S}}}$, ${\psi_{\mathcal{S}}}$ over inputs ${\mathcal{X}}$ and outputs ${\mathcal{Y}}$, and introduces SpecTRA to cluster observations of reference behaviors into concise specs. Applied to adaptive bitrate streaming (Pensieve) and congestion control (Aurora), SpecTRA yields high-coverage, interpretable specifications and uncovers previously unknown vulnerabilities in state-of-the-art networks. The framework supports verification-driven development and offers a practical route to more reliable NN components in dynamic systems.

Abstract

Specifications - precise mathematical representations of correct domain-specific behaviors - are crucial to guarantee the trustworthiness of computer systems. With the increasing development of neural networks as computer system components, specifications gain more importance as they can be used to regulate the behaviors of these black-box models. Traditionally, specifications are designed by domain experts based on their intuition of correct behavior. However, this is labor-intensive and hence not a scalable approach as computer system applications diversify. We hypothesize that the traditional (aka reference) algorithms that neural networks replace for higher performance can act as effective proxies for correct behaviors of the models, when available. This is because they have been used and tested for long enough to encode several aspects of the trustworthy/correct behaviors in the underlying domain. Driven by our hypothesis, we develop a novel automated framework, SpecTRA to generate specifications for neural networks using references. We formulate specification generation as an optimization problem and solve it with observations of reference behaviors. SpecTRA clusters similar observations into compact specifications. We present specifications generated by SpecTRA for neural networks in adaptive bit rate and congestion control algorithms. Our specifications show evidence of being correct and matching intuition. Moreover, we use our specifications to show several unknown vulnerabilities of the SOTA models for computer systems.

Figures (32)

• Figure 1: (Overview of SpecTRA) Observations from all the references (a) are given as input to our specification generation algorithm, SpecTRA. For illustration purposes, a 2-D feature space is considered and each input is classified in either the red or black class by the corresponding reference algorithm. SpecTRA takes the observations and from them develops a set of likely specifications (e). To generate the specifications, SpecTRA first partitions the input space into input regions and from them identifies the regions which have several observations for each reference separately (b) to form the important input regions for the reference. These important regions are combined into interesting behavior input regions (c) according to Definition \ref{['def:nontrivialbeh']}. Clusters are identified in the interesting behavior regions with the same output set according to density (d). These clusters form the specifications (e) that map the inputs in each cluster to the corresponding output set of the cluster.
• Figure 2: Ablation study for hyperparameters affecting the specifications
• Figure : 1
• Figure : 2
• Figure : 3

Theorems & Definitions (2)

• Definition 1
• Definition 2