The test data of acas xu is missing

[dgl-prc]

Hi, acasxu_test.csv is missing, so one can not run the ERAN to verify the acas xu net.

FileNotFoundError: [Errno 2] No such file or directory: '../data/acasxu_test.csv'

I have googled the ACAS Xu dataset but only found 45 pretrained models.

are the acas xu training and test dataset generated by yourself according to the acas xu system? could you shed light on how to get the acas xu data?

[GgnDpSngh]

Hi there,

I have added instructions for running ACASXu with ERAN in the README. Currently, properties 5-10 are supported. As an example, the command for property 9 with deepzono would be:

python3 . --netname ../data/acasxu/nets/ACASXU_run2a_3_3_batch_2000.onnx --dataset acasxu --domain deepzono --specnumber 9

Cheers, Gagandeep Singh

[dgl-prc]

Many thanks! BTW, did you train the ACASXU model by yourself? I would like to verify an ACASXU model trained by myself, but don't know where to get the training/test set? could you give me a hint about where to get the dataset if you know about it?

[GgnDpSngh]

Hi there,

The ACASXu dataset is not publicly available so we use the networks provided officially converted in ONNX format. The paper below tries to learn their own ACASXu networks by sampling from existing networks: https://arxiv.org/abs/1907.10662

Cheers, Gagandeep Singh

[dgl-prc]

What a kind person you are!
Thanks again.

Best wishes to you, Guoliang

[dgl-prc]

Hi, when I run the ACAS Xu, the following error is reported.

  File "/usr/lib/python3.6/runpy.py", line 193, in _run_module_as_main
    "__main__", mod_spec)
  File "/usr/lib/python3.6/runpy.py", line 85, in _run_code
    exec(code, run_globals)
  File "./__main__.py", line 432, in <module>
    _,nn,nlb,nub = eran.analyze_box(specLB, specUB, init_domain(domain), config.timeout_lp, config.timeout_milp, config.use_default_heuristic, constraints)
  File "./eran.py", line 74, in analyze_box
    execute_list, output_info = self.optimizer.get_deeppoly(nn, specLB, specUB, lexpr_weights, lexpr_cst, lexpr_dim, uexpr_weights, uexpr_cst, uexpr_dim, expr_size)
  File "./optimizer.py", line 373, in get_deeppoly
    lexpr_weights, lexpr_cst, lexpr_dim, uexpr_weights, uexpr_cst, uexpr_dim, expr_size))
  File "./deeppoly_nodes.py", line 124, in __init__
    add_input_output_information_deeppoly(self, input_names, output_name, output_shape)
  File "./deeppoly_nodes.py", line 62, in add_input_output_information_deeppoly
    self.output_length = reduce((lambda x, y: x*y), output_shape[1:len(output_shape)])
TypeError: reduce() of empty sequence with no initial value

It seems that output_shape is wrong. I logged the value of output_shape, which was [5], so I conjectured that the correct output_shape should be [1,5]. So I changed the code of function _onnxshape_tointlist in onnx_translator.py as follows:

def onnxshape_to_intlist(onnxshape):
    """
    ONNX has its own wrapper for shapes. Our optimizer expects a list of ints.

    Arguments
    ---------
    onnxshape : TensorShapeProto

    Return
    ------
    output : list
        list of ints corresponding to onnxshape
    """
    result = list(map(lambda j: 1 if j.dim_value is None else int(j.dim_value), onnxshape.dim))
    # No shape means a single value
    if not result:
        return [1]
    # convert NCHW to NHWC
    if len(result) == 4:
        return [result[0], result[2], result[3], result[1]]
        # try to fix the bug of ACAS Xu
    if len(result) == 1:
        return [1, result[0]]
    return result

However, it reported a new error: "Segmentation fault (core dumped)".

How to fix this bug?

[GgnDpSngh]

Hi there,

What exact command did you run?

Cheers,

[dgl-prc]

This is my command:

python . --netname ../data/acasxu/nets/ACASXU_run2a_3_3_batch_2000.onnx --dataset acasxu --domain deeppoly --specnumber 7

[GgnDpSngh]

I ran the command you mentioned and it worked for me, can you check if you are running the latest version of ERAN?

Cheers,

[dgl-prc]

It worked after I completely updated all the files. I probably forgot to update some files before... Thank you so much.

[dgl-prc]

On the same machine, the verification of MNIST could be done within 5min, but that of ACASXU has been running for 16 hours. Is it normal that the verification of ACASXU takes so long time?

The command is:

python . --netname ../data/acasxu/nets/ACASXU_run2a_3_3_batch_2000.onnx --dataset acasxu --domain deeppoly --specnumber 7

Cheers,

[GgnDpSngh]

It can happen, you can set the "max_depth" parameter here to < 10 and also add the option --complete True for faster verification:

https://github.com/eth-sri/eran/blob/7421d04a0a16881e14886f66df48ef8d1c6596d8/tf_verify/__main__.py#L203

Cheers,

[dgl-prc]

Got it. Many thanks~

Cheers,

[dgl-prc]

Just report a potential bug.

The multiprocessing may not work when verifying with the option "--complete True". I set "max_depth" to 2, and verify the ACASXu model with the option "--complete False" and "--complete True" respectively, but only succeed when with the option "--complete False". The command I used is:

python . --netname ../data/acasxu/nets/ACASXU_run2a_3_3_batch_2000.onnx --dataset acasxu --domain deeppoly --specnumber 9 --complete True

With the option "--complete False", the result of the verification is:

This network has 300 neurons.
AcasXu property 9 Failed for Box 0 out of 1
936.1339559555054 seconds
Total time needed: 936.1339712142944 seconds

With the option "--complete True", the result of the verification is:

Traceback (most recent call last):
  File "/usr/lib/python3.6/runpy.py", line 193, in _run_module_as_main
    "__main__", mod_spec)
  File "/usr/lib/python3.6/runpy.py", line 85, in _run_code
    exec(code, run_globals)
  File "./__main__.py", line 499, in <module>
    res = pool.starmap(acasxu_recursive, multi_bounds)
  File "/usr/lib/python3.6/multiprocessing/pool.py", line 274, in starmap
    return self._map_async(func, iterable, starmapstar, chunksize).get()
  File "/usr/lib/python3.6/multiprocessing/pool.py", line 644, in get
    raise self._value
multiprocessing.pool.MaybeEncodingError: Error sending result: '<multiprocessing.pool.ExceptionWithTraceback object at 0x7f890c034da0>'. Reason: 'TypeError("can't pickle PyCapsule objects",)'

I thus managed to verify the ACASXu without multiprocessing when option "--complete" is Ture, and succeeded. The output is shown as follows.

This network has 300 neurons.
Using license file /home/my_server/project/eran/gurobi902/gurobi.lic
Academic license - for non-commercial use only
397.3860023021698 seconds
Total time needed: 397.3860216140747 seconds

[GgnDpSngh]

Hi there,

I noticed this as well now, I have been trying to get rid of it. In the meantime, I have optimized the analysis for ACASXu and also added support for all 10 ACASXu properties. The analysis should be faster than before.

Cheers,

[GgnDpSngh]

I made a fix, did not observe the above exception for me, maybe check if you also do not get the error.

Cheers,

[dgl-prc]

I made a fix, did not observe the above exception for me, maybe check if you also do not get the error.

Cheers,

Great! I have tested the first 5 properties with multiprocessing and did not get the error! The command I used is like:

python . --netname ../data/acasxu/nets/ACASXU_run2a_1_1_batch_2000.onnx --dataset acasxu --domain deeppoly --specnumber 1 --complete True