NN4SysBench: Characterizing Neural Network Verification for Computer Systems

Shuyi Lin; Haoyu He; Tianhao Wei; Kaidi Xu; Huan Zhang; Gagandeep Singh; Changliu Liu; Cheng Tan

NN4SysBench: Characterizing Neural Network Verification for Computer Systems

Shuyi Lin
, Haoyu He
, Tianhao Wei
, Kaidi Xu
, Huan Zhang
, Gagandeep Singh
, Changliu Liu
, Cheng Tan

Research output: Chapters, Conference Papers, Creative and Literary Works › RGC 32 - Refereed conference paper (with host publication) › peer-review

1 Citation (Scopus)

Abstract

We present NN4SysBench, a benchmark suite for neural network verification that is composed of applications from the domain of computer systems. We call these neural networks for computer systems or NN4Sys. NN4Sys is booming: there are many proposals for using neural networks in computer systems-for example, databases, OSes, and networked systems-many of which are safety-critical. Neural network verification is a technique to formally verify whether neural networks satisfy safety properties. We however observe that NN4Sys has some unique characteristics that today's verification tools overlook and have limited support. Therefore, this benchmark suite aims at bridging the gap between NN4Sys and the verification by using impactful NN4Sys applications as benchmarks to illustrate computer systems' unique challenges. We also build a compatible version of NN4SysBench, so that today's verifiers can also work on these benchmarks with approximately the same verification difficulties. The code is available here: https://github.com/Khoury-srg/NN4SysBench. © 2024 Neural information processing systems foundation. All rights reserved.

Original language	English
Title of host publication	NIPS '24: Proceedings of the 38th International Conference on Neural Information Processing Systems
Publisher	Curran Associates Inc.
Pages	91390-91404
ISBN (Electronic)	9798331314385
Publication status	Published - Dec 2024
Externally published	Yes
Event	38th Annual Conference on Neural Information Processing Systems (NeurIPS 2024) - Vancouver Convention Center, Vancouver, Canada Duration: 10 Dec 2024 → 15 Dec 2024 https://neurips.cc/ https://proceedings.neurips.cc/

Publication series

Name	Advances in Neural Information Processing Systems
Volume	37
ISSN (Print)	1049-5258

Conference

Conference	38th Annual Conference on Neural Information Processing Systems (NeurIPS 2024)
Abbreviated title	NeurIPS 2024
Place	Canada
City	Vancouver
Period	10/12/24 → 15/12/24
Internet address	https://neurips.cc/ https://proceedings.neurips.cc/

Funding

This work has been partially supported by Khoury apprenticeship program. Cheng Tan is supported in part by NSF CAREER #2237295. Huan Zhang is supported in part by the AI2050 program at Schmidt Sciences (AI 2050 Early Career Fellowship) and NSF (IIS-2331967).

Access Output

Other Access Options

Check CityUHK Library

Permanent Link

Right click to copy link

Cite this

Lin, S., He, H., Wei, T., Xu, K., Zhang, H., Singh, G., Liu, C., & Tan, C. (2024). NN4SysBench: Characterizing Neural Network Verification for Computer Systems. In NIPS '24: Proceedings of the 38th International Conference on Neural Information Processing Systems (pp. 91390-91404). (Advances in Neural Information Processing Systems; Vol. 37). Curran Associates Inc.. http://dl.acm.org/doi/10.5555/3737916.3740816

@inproceedings{5a926e100dc8459395f83780500b7f1b,

title = "NN4SysBench: Characterizing Neural Network Verification for Computer Systems",

abstract = "We present NN4SysBench, a benchmark suite for neural network verification that is composed of applications from the domain of computer systems. We call these neural networks for computer systems or NN4Sys. NN4Sys is booming: there are many proposals for using neural networks in computer systems-for example, databases, OSes, and networked systems-many of which are safety-critical. Neural network verification is a technique to formally verify whether neural networks satisfy safety properties. We however observe that NN4Sys has some unique characteristics that today's verification tools overlook and have limited support. Therefore, this benchmark suite aims at bridging the gap between NN4Sys and the verification by using impactful NN4Sys applications as benchmarks to illustrate computer systems' unique challenges. We also build a compatible version of NN4SysBench, so that today's verifiers can also work on these benchmarks with approximately the same verification difficulties. The code is available here: https://github.com/Khoury-srg/NN4SysBench. {\textcopyright} 2024 Neural information processing systems foundation. All rights reserved.",

author = "Shuyi Lin and Haoyu He and Tianhao Wei and Kaidi Xu and Huan Zhang and Gagandeep Singh and Changliu Liu and Cheng Tan",

year = "2024",

month = dec,

language = "English",

series = "Advances in Neural Information Processing Systems",

publisher = "Curran Associates Inc.",

pages = "91390--91404",

booktitle = "NIPS '24: Proceedings of the 38th International Conference on Neural Information Processing Systems",

address = "United States",

note = "38th Annual Conference on Neural Information Processing Systems (NeurIPS 2024), NeurIPS 2024 ; Conference date: 10-12-2024 Through 15-12-2024",

url = "https://neurips.cc/, https://proceedings.neurips.cc/",

}

Lin, S, He, H, Wei, T, Xu, K, Zhang, H, Singh, G, Liu, C & Tan, C 2024, NN4SysBench: Characterizing Neural Network Verification for Computer Systems. in NIPS '24: Proceedings of the 38th International Conference on Neural Information Processing Systems. Advances in Neural Information Processing Systems, vol. 37, Curran Associates Inc., pp. 91390-91404, 38th Annual Conference on Neural Information Processing Systems (NeurIPS 2024), Vancouver, Canada, 10/12/24. <http://dl.acm.org/doi/10.5555/3737916.3740816>

NN4SysBench: Characterizing Neural Network Verification for Computer Systems. / Lin, Shuyi; He, Haoyu; Wei, Tianhao et al.
NIPS '24: Proceedings of the 38th International Conference on Neural Information Processing Systems. Curran Associates Inc., 2024. p. 91390-91404 (Advances in Neural Information Processing Systems; Vol. 37).

Research output: Chapters, Conference Papers, Creative and Literary Works › RGC 32 - Refereed conference paper (with host publication) › peer-review

TY - GEN

T1 - NN4SysBench

T2 - 38th Annual Conference on Neural Information Processing Systems (NeurIPS 2024)

AU - Lin, Shuyi

AU - He, Haoyu

AU - Wei, Tianhao

AU - Xu, Kaidi

AU - Zhang, Huan

AU - Singh, Gagandeep

AU - Liu, Changliu

AU - Tan, Cheng

PY - 2024/12

Y1 - 2024/12

N2 - We present NN4SysBench, a benchmark suite for neural network verification that is composed of applications from the domain of computer systems. We call these neural networks for computer systems or NN4Sys. NN4Sys is booming: there are many proposals for using neural networks in computer systems-for example, databases, OSes, and networked systems-many of which are safety-critical. Neural network verification is a technique to formally verify whether neural networks satisfy safety properties. We however observe that NN4Sys has some unique characteristics that today's verification tools overlook and have limited support. Therefore, this benchmark suite aims at bridging the gap between NN4Sys and the verification by using impactful NN4Sys applications as benchmarks to illustrate computer systems' unique challenges. We also build a compatible version of NN4SysBench, so that today's verifiers can also work on these benchmarks with approximately the same verification difficulties. The code is available here: https://github.com/Khoury-srg/NN4SysBench. © 2024 Neural information processing systems foundation. All rights reserved.

AB - We present NN4SysBench, a benchmark suite for neural network verification that is composed of applications from the domain of computer systems. We call these neural networks for computer systems or NN4Sys. NN4Sys is booming: there are many proposals for using neural networks in computer systems-for example, databases, OSes, and networked systems-many of which are safety-critical. Neural network verification is a technique to formally verify whether neural networks satisfy safety properties. We however observe that NN4Sys has some unique characteristics that today's verification tools overlook and have limited support. Therefore, this benchmark suite aims at bridging the gap between NN4Sys and the verification by using impactful NN4Sys applications as benchmarks to illustrate computer systems' unique challenges. We also build a compatible version of NN4SysBench, so that today's verifiers can also work on these benchmarks with approximately the same verification difficulties. The code is available here: https://github.com/Khoury-srg/NN4SysBench. © 2024 Neural information processing systems foundation. All rights reserved.

UR - https://www.scopus.com/pages/publications/105000511862

UR - https://www.scopus.com/record/pubmetrics.uri?eid=2-s2.0-105000511862&origin=recordpage

M3 - RGC 32 - Refereed conference paper (with host publication)

T3 - Advances in Neural Information Processing Systems

SP - 91390

EP - 91404

BT - NIPS '24: Proceedings of the 38th International Conference on Neural Information Processing Systems

PB - Curran Associates Inc.

Y2 - 10 December 2024 through 15 December 2024

ER -

NN4SysBench: Characterizing Neural Network Verification for Computer Systems

Abstract

Publication series

Conference

Funding

Access Output

Other Access Options

Permanent Link

Other Files and Links

Fingerprint

Cite this