shaddadi / veritex Goto Github PK

Windows does not allow <> as a filename.
AcasNetID<1,7>-normed-train.pt

It would be nice to have some indication for progress as you are running the reproduce_results scripts. For example, 30% of networks verified or xx/yy verified.

The following image is generated:

When running main_demo.py, the following error is reported for each iteration:

Process Process-375:
Traceback (most recent call last):
File "/usr/local/lib/python3.7/multiprocessing/process.py", line 297, in _bootstrap
self.run()
File "/usr/local/lib/python3.7/multiprocessing/process.py", line 99, in run
self._target(*self._args, **self._kwargs)
File "/veritex/veritex/methods/worker.py", line 66, in main_func
self.state_spawn_depth_first(tuple_state)
File "/veritex/veritex/methods/worker.py", line 368, in state_spawn_depth_first
self.state_spawn_depth_first(next_tuple_states[0])
File "/veritex/veritex/methods/worker.py", line 368, in state_spawn_depth_first
self.state_spawn_depth_first(next_tuple_states[0])
File "/veritex/veritex/methods/worker.py", line 368, in state_spawn_depth_first
self.state_spawn_depth_first(next_tuple_states[0])
[Previous line repeated 8 more times]
File "/veritex/veritex/methods/worker.py", line 348, in state_spawn_depth_first
self.collect_results(next_tuple_states[0][0])
File "/veritex/veritex/methods/worker.py", line 333, in collect_results
unsafe_inputs = self.dnn.backtrack(vfl)
File "/veritex/veritex/networks/ffnn.py", line 79, in backtrack
elements = np.dot(np.dot(As_unsafe,vfl_set.M), vfl_set.vertices.T) + np.dot(As_unsafe, vfl_set.b) +ds_unsafe
TypeError: Concatenation operation is not implemented for NumPy arrays, use np.concatenate() instead. Please do not rely on this error; it may not be given on all Python implementations.
Process Process-378:
Traceback (most recent call last):
File "/usr/local/lib/python3.7/multiprocessing/process.py", line 297, in _bootstrap
self.run()
File "/usr/local/lib/python3.7/multiprocessing/process.py", line 99, in run
self._target(*self._args, **self._kwargs)
File "/veritex/veritex/methods/worker.py", line 66, in main_func
self.state_spawn_depth_first(tuple_state)
File "/veritex/veritex/methods/worker.py", line 368, in state_spawn_depth_first
self.state_spawn_depth_first(next_tuple_states[0])
File "/veritex/veritex/methods/worker.py", line 368, in state_spawn_depth_first
self.state_spawn_depth_first(next_tuple_states[0])
File "/veritex/veritex/methods/worker.py", line 368, in state_spawn_depth_first
self.state_spawn_depth_first(next_tuple_states[0])
[Previous line repeated 8 more times]
File "/veritex/veritex/methods/worker.py", line 348, in state_spawn_depth_first
self.collect_results(next_tuple_states[0][0])
File "/veritex/veritex/methods/worker.py", line 333, in collect_results
unsafe_inputs = self.dnn.backtrack(vfl)
File "/veritex/veritex/networks/ffnn.py", line 79, in backtrack
elements = np.dot(np.dot(As_unsafe,vfl_set.M), vfl_set.vertices.T) + np.dot(As_unsafe, vfl_set.b) +ds_unsafe
TypeError: Concatenation operation is not implemented for NumPy arrays, use np.concatenate() instead. Please do not rely on this error; it may not be given on all Python implementations.

I get the following error when running this script:
Traceback (most recent call last):
File "/usr/local/lib/python3.7/multiprocessing/process.py", line 297, in _bootstrap
self.run()
File "/usr/local/lib/python3.7/multiprocessing/process.py", line 99, in run
self._target(*self._args, **self._kwargs)
File "/home/veritex/src/veritex/methods/worker.py", line 104, in main_func
self.state_spawn_depth_first(tuple_state)
File "/home/veritex/src/veritex/methods/worker.py", line 364, in state_spawn_depth_first
self.state_spawn_depth_first(next_tuple_states[0])
File "/home/veritex/src/veritex/methods/worker.py", line 364, in state_spawn_depth_first
self.state_spawn_depth_first(next_tuple_states[0])
File "/home/veritex/src/veritex/methods/worker.py", line 364, in state_spawn_depth_first
self.state_spawn_depth_first(next_tuple_states[0])
[Previous line repeated 7 more times]
File "/home/veritex/src/veritex/methods/worker.py", line 358, in state_spawn_depth_first
self.collect_results(next_tuple_states[0][0])
File "/home/veritex/src/veritex/methods/worker.py", line 338, in collect_results
unsafe_inputs = self.dnn.backtrack(s) # in FVIM or Flattice
File "/home/veritex/src/veritex/networks/ffnn.py", line 164, in backtrack
for i in range(len(self.property.unsafe_domains)):
AttributeError: 'NoneType' object has no attribute 'unsafe_domains'

What tables and figures are generated? Where are they stored? It would be nice to include this in the readme file.

We have already had requirement.txt.
However if we consider developer user, maybe setup.py which allows install this repo. as Python pkg would be better.

Documentation looking much better already. May want to add file level documentation as follows:

It would be useful to have all the outputs stored in a log file, particularly for debugging purposes in case some issue occurs.

When running the tool on Mac M1, I get errors related to imports of torch.ao.quantization. The error is not showing by changing all instances of "torch.ao.quantization" to "torch.quantization". This is likely a pytorch issue.

I understand you make some list by
acasxu_repair_list.py
At least, we may merge the codes repair_propertyX.py into repair_property.py.
I know you need repair_propertyX.py as function pointer for property_ls. You can keep this. but still you may call marged code repair_property.py internal of repair_propertyX.py.

repair_all_nnets.py and repair_sub_nnets.py are almost same. just marge it and make shell script to call all setting or sub setting.

Nice! I was able to run the script on Windows under your new instructions.

Here is the table that is generated. This is consistent with the results in the paper. Fix typo Successe -> Success.

Table2&3.txt

Next I will run the longer script.

I tried it with python 3.8, 2.7 However because of other lib issues, it works only 3.7

You did not upload it because those are generated when we run ACASXu example.

The code itself seems to be good.
Anyway, what is the difference of each verify_pX_vnnlib.py?
I feel we may make one function for that and call them from .sh with different argument instead of many copy of .py

I ran Reproduce_results2.py for several hours. Here is the log (partial since buffer on powershell is limited).

I got the following error: "The number of repaired instances is not correct!"

log.txt

Something like this:

def add_binary(a, b):
'''
Returns the sum of two decimal numbers in binary digits.

        Parameters:
                a (int): A decimal integer
                b (int): Another decimal integer

        Returns:
                binary_sum (str): Binary string of the sum of a and b
'''
binary_sum = bin(a+b)[2:]
return binary_sum

print(add_binary.doc)

There is a minor typo in the tool name of setup.py. I noticed this when installing. Is this for a reason, e.g., already used name or something? Otherwise I would suggest fixing as veritex, as it may confuse users to see veritx.

https://github.com/Shaddadi/veritex/blob/master/setup.py#L11

There are two warnings that pop up.
...
[2022-05-03 20:00:16,693][INFO] After 25 epochs / 0m 29s (29.440 seconds), with 0.9774 accuracy on test set.
[2022-05-03 20:00:16,693][INFO] Eventually the trained network got certified? True
[2022-05-03 20:00:16,694][INFO] === Avg <epochs, train_time, certified, accuracy> for 35 networks:
[2022-05-03 20:00:16,694][INFO] tensor([25.2857, 28.8715, 0.9714, 0.9473])
[2022-05-03 20:00:16,695][INFO] Total Cost Time: 1010.9472537349939s.

figure2_generator.py:54: UserWarning: Attempted to set non-positive bottom ylim on a log-scaled axis.
Invalid limit will be ignored.
plt.ylim([0, 116])
/usr/local/lib/python3.7/site-packages/onnx2pytorch/convert/operations.py:154: UserWarning: The given NumPy array is not writeable, and PyTorch does not support non-writeable tensors. This means you can write to the underlying (supposedly non-writeable) NumPy array using the tensor. You may want to copy the array to protect its data or make it writeable before converting it to a tensor. This type of warning will be suppressed for the rest of this program. (Triggered internally at ../torch/csrc/utils/tensor_numpy.cpp:189.)
weight = torch.from_numpy(numpy_helper.to_array(params[0]))

I reran on my Ubuntu computer via docker as a final check using the last version. Installation appeared okay via docker with latest instructions.

install-taylor-ubuntu-2022-05-06.txt

I was UNABLE to successfully run the copy to host command. I kept getting a file permission error for some reason. This should get corrected, as otherwise the artifact might fail as not being functional. For some reason I did not have this problem on a Windows host.

johnsott@lh-lambda-quad:~/veritex-results-2022-05-06$ sudo docker cp cav_veritex:/veritex/cav22_artifact/results/. .
open /home/johnsott/veritex-results-2022-05-06/Figure2.png: permission denied

root@c7d71a98cd96:/veritex/cav22_artifact/results# ls
 Figure2.png
'Table2&3.txt'
'figure3(a)_original_reach_property_1_2_dims_0_1.png'
'figure3(b)_veritex_reach_property_1_2_dims_0_1.png'
'figure3(c)_art_reach_property_1_2_dims_0_1.png'
'figure3(d)_original_reach_property_3_4_dims_0_1.png'
'figure3(e)_veritex_reach_property_3_4_dims_0_1.png'
'figure3(f)_art_reach_property_3_4_dims_0_1.png'
'figure4(a)_original_reach_property_1_2_dims_0_1.png'
'figure4(b)_veritex_reach_property_1_2_dims_0_1.png'
'figure4(c)_original_reach_property_1_2_dims_0_2.png'
'figure4(d)_veritex_reach_property_1_2_dims_0_2.png'

Again, your code is well modular already. I don't feel many issues there.
Here is minor feedback for examples/Demo/main_demo.py

dnn0.set_property(property1)

Add he simplest example in example.

just

• load very small NN (like 3 layer)
• Setup FNN
• run it with out parallel processing. (single)

We know Demo is also simple. but more simpler one!

The nnet module is missing.