AutoSpec: Automated Generation of Neural Network Specifications

Each specification defines the expected model output for a given input space ( 2.1). The increasing adoption of neural networks in learning-augmented systems highlights the importance Specifically, researchers have relied on their domain knowledge of model safety and robustness, particularly and intuition about individual applications to manually in safety-critical domains. Despite progress in create specifications. For instance, in adaptive video streaming, the formal verification of neural networks, current where a neural network is employed to determine the practices require users to manually define model bitrate for the next video chunk based on recent network specifications--properties that dictate expected conditions, Eliyahu et al. (2021) define a specification as, model behavior in various scenarios. This manual "[if video] chunks were downloaded quickly (more quickly process, however, is prone to human error, limited than it takes to play a chunk), the DNN should eventually in scope, and time-consuming. In this paper, not choose the worst resolution." Similar manual specifications we introduce AutoSpec, the first framework to are devised for other learning-augmented systems, e.g., automatically generate comprehensive and accurate database indexes (Tan et al., 2021), memory allocators (Wei specifications for neural networks in learningaugmented et al., 2023), and job schedulers (Wu et al., 2022).