Towards Reliable Neural Specifications

Authors: Chuqin Geng, Nham Le, Xiaojie Xu, Zhaoyue Wang, Arie Gurfinkel, Xujie Si

ICML 2023 | Conference PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Experimental We conduct thorough experimental evaluations from both statistical and formal verification perspectives. Particularly, we show that a single NAP is sufficient for certifying a significant fraction of unseen inputs.
Researcher Affiliation Academia 1Mc Gill University 2Mila Quebec AI Institute 3University of Waterloo 4University of Toronto.
Pseudocode Yes Algorithm 1 NAP Mining Algorithm
Open Source Code No The paper does not provide a statement about releasing its own source code or a link to a code repository for the methodology described.
Open Datasets Yes Our experiments are based on benchmarks from VNNCOMP (2021) the annual neural network verification competition. We use 2 of the datasets from the competition: MNIST and CIFAR10.
Dataset Splits No The paper mentions using 'training images' and 'testing images' for its main experiments but does not explicitly describe a separate validation dataset split or specific percentages for training/test splits for the main MNIST and CIFAR10 experiments.
Hardware Specification Yes Experiments are done on a machine with an Intel(R) Xeon(R) CPU E5-2686 and 480GBs of RAM.
Software Dependencies No The paper mentions using 'Marabou' as a neural network verifier but does not provide specific version numbers for Marabou or any other software dependencies.
Experiment Setup Yes For MNIST, we use the two largest models mnistfc 256x4 and mnistfc 256x6, a 4and 6-layers fully connected network with 256 neurons for each layer, respectively. For CIFAR10, we use the convolutional neural net cifar10 small.onnx with 2568 Re LUs. Timeouts for MNIST and CIFAR10 are 10 and 30 minutes, respectively.