Description of neural network file format

[oGkgN]

Hi,

please provide a description of the .nnet format used by the various nnet/ACASXU_*.nnet files (which can be used as a reference for implementing custom parsers). I tried to figure out the format by reading the implementation of nnet/nnet.cpp, but I struggle at the part »load Min and Max values of inputs«.
Consider the first 5 non-comment lines of the file nnet/ACASXU_run2a_1_1_batch_2000.nnet:

7,5,5,50,
5,50,50,50,50,50,50,5,
0,
0.0,-3.141593,-3.141593,100.0,0.0,0.0,-3.0,
60760.0,3.141593,3.141593,1200.0,1200.0,100.0,3.0,

My observation so far is the following:
The first line contains (in that order) the number of layers [excluding the input layer] (7), the number of inputs/size of input layer (5), the number of outputs/size of output layer (5) and the size of the biggest layer of that network (50).
The next line provides the precise sizes of every (including the one for input) layer.
In the third line we have the 0/1 boolean value marking the network as symmetric/not symmetric.
But now I'm struggling: Considering this block of code from nnet/nnet.cpp

//Load Min and Max values of inputs
nnet->mins = new double[(nnet->inputSize)];
line = fgets(buffer,bufferSize,fstream);
record = strtok(line,",\n");
for (i = 0; i<(nnet->inputSize); i++)
{
    nnet->mins[i] = atof(record);
    record = strtok(NULL,",\n");
}

nnet->maxes = new double[(nnet->inputSize)];
line = fgets(buffer,bufferSize,fstream);
record = strtok(line,",\n");
for (i = 0; i<(nnet->inputSize); i++)
{
    nnet->maxes[i] = atof(record);
    record = strtok(NULL,",\n");
}

I expect the fourth and fifth line of have only 5 values, since the number of inputs is 5. Also, only five values are stored in the arrays mins and maxes. What am I missing? Might this even be a bug?

Kind regards.

[bunelr]

I have an implementation of another parser for these .nnet file here if you are interested.

When I wrote the parser, my assumption was that the two extra dimension corresponds to the two additional dimensions a_prev and \tau over which the network are discretized (See Appendix E in the Reluplex paper https://arxiv.org/pdf/1702.01135.pdf). In practice, these are not actually input to the neural network.

[kjulian3]

@bunelr is correct, the two extra dimensions correspond to a_prev and \tau. These dimensions were needed when one network was trained to represent the full state space, but when separate networks were trained on the different combinations of a_prev and \tau, those dimensions became unnecessary. Those extra values do not need to be included in these files. Thank you for pointing this out.