# Specification Generation for Neural Networks in Systems

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 16 of its 56 references that are in the map.
- First posted on arXiv 4 Dec 2024.

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

- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (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)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [Robust Physical-World Attacks on Deep Learning Models](https://mlsanity.com/paper/1707.08945/) (2017)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [Ithemal: Accurate, Portable and Fast Basic Block Throughput Estimation using Deep Neural Networks](https://mlsanity.com/paper/1808.07412/) (2018)
- [Robustness Certification of Generative Models](https://mlsanity.com/paper/2004.14756/) (2020)
- [Scalable Verification of GNN-based Job Schedulers](https://mlsanity.com/paper/2203.03153/) (2022)
- [Provable Defense Against Geometric Transformations](https://mlsanity.com/paper/2207.11177/) (2022)
- [Towards Reliable Neural Specifications](https://mlsanity.com/paper/2210.16114/) (2022)
- [When Machine Learning Meets Congestion Control: A Survey and Comparison](https://mlsanity.com/paper/2010.11397/) (2020)
- [Neural Network Branch-and-Bound for Neural Network Verification](https://mlsanity.com/paper/2107.12855/) (2021)
- [COMET: Neural Cost Model Explanation Framework](https://mlsanity.com/paper/2302.06836/) (2023)

## Abstract (arXiv)

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.