# AutoSpec: Automated Generation of Neural Network Specifications

arXiv: https://arxiv.org/abs/2409.10897 · HTML: https://mlsanity.com/paper/2409.10897/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 31 references that are in the map.
- First posted on arXiv 17 Sep 2024.

## Builds on (most cited first, 9 of 9)

- [The Case for Learned Index Structures](https://mlsanity.com/paper/1712.01208/) (2017)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Learning Scheduling Algorithms for Data Processing Clusters](https://mlsanity.com/paper/1810.01963/) (2018)
- [Intelligence and Learning in O-RAN for Data-driven NextG Cellular Networks](https://mlsanity.com/paper/2012.01263/) (2020)
- [Scalable Verification of GNN-based Job Schedulers](https://mlsanity.com/paper/2203.03153/) (2022)
- [Towards Reliable Neural Specifications](https://mlsanity.com/paper/2210.16114/) (2022)
- [Neural Network Compression of ACAS Xu Early Prototype is Unsafe: Closed-Loop Verification through Quantized State Backreachability](https://mlsanity.com/paper/2201.06626/) (2022)
- [DeepBeam: Deep Waveform Learning for Coordination-Free Beam Management in mmWave Networks](https://mlsanity.com/paper/2012.14350/) (2020)
- [Learning a Decision Tree Algorithm with Transformers](https://mlsanity.com/paper/2402.03774/) (2024)

## Built on by (most cited first, 2 of 2)

- [Intent-aligned Formal Specification Synthesis via Traceable Refinement](https://mlsanity.com/paper/2604.10392/) (2026)
- [Analyzing Symbolic Properties for DRL Agents in Systems and Networking](https://mlsanity.com/paper/2604.04914/) (2026)

## Abstract (arXiv)

The increasing adoption of neural networks in learning-augmented systems highlights the growing need for model safety and robustness, especially in safety-critical domains. While recent advances in neural network verification offer formal guarantees on worst-case behavior, existing approaches require users to manually define model specifications, an error-prone, incomplete, and time-consuming process. In this paper, we present AutoSpec, the first comprehensive framework for automatically generating and evaluating neural network specifications for learning-augmented systems. AutoSpec introduces a tree-based algorithm that adaptively partitions the input space to generate specification sets aligned with model behavior, as well as a statistical certification framework that provides rigorous accuracy guarantees for each specification. We also propose a principled evaluation framework that defines interpretable metrics for specification accuracy and coverage, establishing a benchmark for future research. Experiments across four diverse applications show that AutoSpec outperforms both manually defined specifications and existing baseline algorithms, improving the F1 score by up to 53% over human-defined specifications and 73% over the strongest baseline.
