Zonotopes as specs

[rnbguy]

https://github.com/eth-sri/eran/blob/d5ea0b9dae4621e259ebcade5428e6860655941e/tf_verify/__main__.py#L278-L292

The example here uses upper bound and lower bound. My understanding is, internally Eran uses zonotopes(for transformation). But the input specs are always a hyper-box in Eran code. Is it possible to use a zonotope instead of using a simple hyper-box?

[GgnDpSngh]

Hi,

Sorry for the delay, yes the support for Zonotope inputs can be added. Let me know if this is required.

Cheers,

[rnbguy]

Yes. that'd be awesome. Hyperbox seems too strict to be used in a backend solver api.

[GgnDpSngh]

Hi,

How would you want to pass the Zonotope as Input, do you want to print your input Zonotope to a file in the form of a matrix?

Cheers, Gagandeep Singh

[rnbguy]

I don't need any parser. You can just expose some API. You can do whatever that's convenient for you. :)

Cheers.

[nikos-kekatos]

Hello!

We are also interested in using zonotopes as inputs to ERAN. What is the current status?

Thanks, Nikos

[GgnDpSngh]

Hi all,

We have added support for specifying Zonotopes as Inputs to ERAN. Use the following command:

python3 . --netname network_file --domain deepzono --zonotope zonotope_spec.

An example on the MNIST 6x100 network from the ERAN website would be: python3 . --netname mnist_relu_6_100.tf --domain deepzono --zonotope zonotope_example.txt

The first two lines in the Zonotope spec should specify the number of dimensions and the number of error terms per dimensions including the central error term. The following values in the file should be the coefficients for different error terms. The entry i*num_error_terms 0<=i<num_dimensions specifies the central error term for the i-th dimension.

I am attaching two example Zonotope specs for the MNIST networks both containing 784 dimensions. The first spec contains 10 error terms per dimension and second contains only one error term per dimension (thus corresponds to an image).

Let me know if you have any issues (note that you need to update the ELINA version on your system).

zonotope_example.txt zonotope_example2.txt

Cheers, Gagandeep Singh

[nikos-kekatos]

Hi Gagandeep,

thanks a lot for the update! So, I got your latest files and here is what I get.

$ python3 . --netname mnist_relu_6_100.tf --domain deepzono --dataset mnist is working fine while

$ python3 . --netname mnist_relu_6_100.tf --domain deepzono --dataset mnist --zonotope zonotope_example.txt

returns back an error. It gets stuck in an exception in zonoml.py:

_Problem with loading/calling "elina_abstract0_fromzonotope" from "libzonoml.so"

The error of the stack trace occurs in

_File "../ELINA/python_interface/zonoml.py", line 126, in elina_abstract0_fromzonotope return res UnboundLocalError: local variable 'res' referenced before assignment

Please note that I have updated my ELINA version and the $ _./elina_testzonoml seems to be working fine.

I would appreciate any feedback on this matter :).

Thanks again, Nikos

PS: I guess that it is not relevant but to avoid all the issues with the latest TensorFlow version I am using import tensorflow.compat.v1 as tf and _tf.disable_v2behavior().

[GgnDpSngh]

Hi Nikos,

It appears that the "C" compiler cannot locate the newly added "elina_abstract0_from_zonotope" function in the "libzonoml.so" shared object. Can you check whether "libzonoml.so" that the compiler uses (usually located in the folder "\usr\local\lib" or "\usr\lib") contains this function? You can check this by looking for the name of the function in the output of the following command:

nm -g /usr/local/lib/linzonoml.so

If you do not see the function then try installing ELINA again, otherwise try the command "sudo ldconfig".

Let me know if this helps.

Cheers, Gagandeep Singh

[nikos-kekatos]

Hi Gagandeep,

Thanks a lot, I checked your suggestions!

So, indeed the "elina_abstract0_from_zonotope" function is missing from the shared object.

I tried installing ELINA again but the problem remained with the last 10 or so commits. The macOS-equivalent command for the library caches $ sudo update_dyld_shared_cache does not change anything. Among many others, the $ nm returns _elina_abstract0_copy, _elina_abstract0_dimension, _elina_abstract0_permute_dimensions, _elina_abstract0_remove_dimensions

Any further suggestions would be highly appreciated.

Thanks, Nikos

PS: Note that I was not able to compile the latest version on macOS

ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
make[1]: *** [libfppoly.so] Error 1

[GgnDpSngh]

Hi Nikos,

Does the latest version of "ELINA/zonoml" folder compile on your machine? If yes, then the best way to get going would be to simply copy the newly generated "libzonoml.so" file to the default search directory of the compiler.

Cheers,

[antoniobruto]

Dear Gagandeep,

I have also installed everything without any errors (including the latest clone of ELINA). However, when using zonotopes, I see the same issue that was pointed out by Nikos, i.e. that the method elina_abstract0_from_zonotope is not present in libzonoml.so

Even tried doing as you suggested by re "making" the library from scratch but this did not add the method either.

Any alternate suggestions or discussions would be most appreciated. The traceback is included below:

Traceback (most recent call last): File "/usr/lib/python3.5/runpy.py", line 184, in _run_module_as_main "main", mod_spec) File "/usr/lib/python3.5/runpy.py", line 85, in _run_code exec(code, run_globals) File "./main.py", line 295, in perturbed_label, nn, nlb, nub = eran.analyze_zonotope(zonotope, domain, args.timeout_lp, args.timeout_milp, args.use_area_heuristic) File "./eran.py", line 111, in analyze_zonotope dominant_class, nlb, nub = analyzer.analyze() File "./analyzer.py", line 100, in analyze element, nlb, nub = self.get_abstract0() File "./analyzer.py", line 80, in get_abstract0 element = self.ir_list[0].transformer(self.man) File "./deepzono_nodes.py", line 259, in transformer element = elina_abstract0_from_zonotope(man, 0, zonotope_shape[0], self.num_error_terms, self.zonotope) File "../ELINA/python_interface/zonoml.py", line 126, in elina_abstract0_from_zonotope return res UnboundLocalError: local variable 'res' referenced before assignment

[LebronX]

Hi Gagandeep,

Thanks a lot, I checked your suggestions!

So, indeed the "elina_abstract0_from_zonotope" function is missing from the shared object.

I tried installing ELINA again but the problem remained with the last 10 or so commits. The macOS-equivalent command for the library caches $ sudo update_dyld_shared_cache does not change anything. Among many others, the $ nm returns _elina_abstract0_copy, _elina_abstract0_dimension, _elina_abstract0_permute_dimensions, _elina_abstract0_remove_dimensions

Any further suggestions would be highly appreciated.

Thanks, Nikos

PS: Note that I was not able to compile the latest version on macOS

ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
make[1]: *** [libfppoly.so] Error 1

Hi, I am also trying to install ERAN on macos, and now trying to compile ELINA. But I also have the same problem of libfppoly error. I would like to now did you solve this?

[GgnDpSngh]

Hi there,

Thanks for your interest in ERAN. I tried running the "deepzono" analysis with zonotope input on my Ubuntu machine and it worked. Have you checked whether "elina_abstract0_from_zonotope" exists in "ELINA/zonoml/libzonoml.so", if "zonoml" compiles, then it should have that method. You can then set the location from where the python interface loads "libzonoml.so" by specifying your custom path here:

https://github.com/eth-sri/ELINA/blob/40fd587fb5b08a9f4d733a4a3178ed7998332033/python_interface/zonoml_imports.py#L30

Please let me know if it works.

Cheers, Gagandeep Singh

[LebronX]

"elina_abstract0_from_zonotope" exists in "ELINA/zonoml/libzonoml.so"

Hi,

Thank you very much for the prompt reply!

"elina_abstract0_from_zonotope" indeed exists in "ELINA/zonoml/libzonoml.so".

But I don't understand what you mean by "You can then set the location from where the python interface loads "libzonoml.so" by specifying your custom path here". In zonoml_import.py, the path of zonoml_api is already "../zonoml/libzonoml.so", which is the correct location, no? Which location should I set?

Thanks

[LebronX]

The full error log:

cc -shared -Wcast-qual -Wswitch -Wall -Wextra -Wundef -Wcast-align -Wno-unused -U__STRICT_ANSI__ -fPIC -O3 -DNDEBUG -Werror-implicit-function-declaration -Wbad-function-cast -Wstrict-prototypes -Wno-strict-overflow -std=c99 -g -DNUM_LONGLONGRAT -DNUM_DOUBLE -DTHRESHOLD=0.75 -DTIMING -D_GNU_SOURCE -pthread -fno-tree-vectorize -m64 -march=native -ffp-contract=off -DGUROBI -I../elina_auxiliary -I../elina_linearize -I../elina_zonotope -I../partitions_api -I/home/gagandeepsi/gurobi903/linux64/include/ -I/usr/local/include/cddlib -o libfppoly.so fppoly.o backsubstitute.o compute_bounds.o expr.o relu_approx.o leakyrelu_approx.o round_approx.o clip_approx.o batch_normalization.o sign_approx.o s_curve_approx.o parabola_approx.o log_approx.o pool_approx.o lstm_approx.o maxpool_convex_hull.o -L../partitions_api -lpartitions -L../elina_auxiliary -lelinaux -L../elina_linearize -lelinalinearize -L../elina_zonotope -lzonotope -lmpfr -lgmp -lm -lpthread -lcdd -lgurobi90 ld: warning: ignoring file /usr/local/lib/libgurobi90.so, building for macOS-x86_64 but attempting to link with file built for unknown-unsupported file format ( 0x7F 0x45 0x4C 0x46 0x02 0x01 0x01 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 ) Undefined symbols for architecture x86_64: "_GRBaddconstr", referenced from: _substitute_spatial_gurobi in compute_bounds.o "_GRBemptyenv", referenced from: _substitute_spatial_gurobi in compute_bounds.o "_GRBfreeenv", referenced from: _substitute_spatial_gurobi in compute_bounds.o "_GRBfreemodel", referenced from: _substitute_spatial_gurobi in compute_bounds.o "_GRBgetdblattr", referenced from: _substitute_spatial_gurobi in compute_bounds.o "_GRBgeterrormsg", referenced from: _handle_gurobi_error in compute_bounds.o _substitute_spatial_gurobi in compute_bounds.o "_GRBgetintattr", referenced from: _substitute_spatial_gurobi in compute_bounds.o "_GRBnewmodel", referenced from: _substitute_spatial_gurobi in compute_bounds.o "_GRBoptimize", referenced from: _substitute_spatial_gurobi in compute_bounds.o "_GRBsetintattr", referenced from: _substitute_spatial_gurobi in compute_bounds.o "_GRBsetintparam", referenced from: _substitute_spatial_gurobi in compute_bounds.o "_GRBstartenv", referenced from: _substitute_spatial_gurobi in compute_bounds.o ld: symbol(s) not found for architecture x86_64 clang: error: linker command failed with exit code 1 (use -v to see invocation) make[1]: [libfppoly.so] Error 1 make: [c] Error 2

[GgnDpSngh]

Thanks for the details, I just wanted to check that the "libzonoml.so" you load has the required method. Based on the attached log, that you are trying to link libgurobi.so that was compiled on a different architecture, did you download Gurobi binaries or built from scratch?

Cheers, Gagandeep Singh

[LebronX]

Hi,

I follow Gurobi's website's download tutorial, so I think it is binary?

Thanks

[GgnDpSngh]

Did you run "make" and "setup.py"? If not, then it's binary and might not be compatible with your build system.

Cheers, Gagandeep Singh

[LebronX]

Hi,

I switch to a linux machine and now it works. I have one more question for the running example: where is the "nets" directory? I can only run the example of ACAS Xu, but not CIFAR-10 and MNIST.

Thanks

[GgnDpSngh]

I am glad that it worked, you can provide any MNIST or CIFAR10 network in onnx format or try any of the networks on the ERAN website (e.g. https://files.sri.inf.ethz.ch/eran/nets/tensorflow/mnist/mnist_relu_3_50.tf). You would have to generate your own Zonotope input, see an example specification for MNIST here: https://github.com/eth-sri/eran/blob/master/data/create_zonotope.py

Cheers, Gagandeep SIngh

[LebronX]

Hi,

Thanks for the reply!

I was talking about the example commands that you give on the readme. For example, this one: Maybe you could move the "nets" directory in this file website to data directory on the git repository so that when someone wants to try these examples, he can easily run the example commands.

Thank you so much for the helping again!