shaddadi / veritex Goto Github PK
View Code? Open in Web Editor NEWLicense: BSD 3-Clause "New" or "Revised" License
License: BSD 3-Clause "New" or "Revised" License
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'
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.
Again, your code is well modular already. I don't feel many issues there.
Here is minor feedback for examples/Demo/main_demo.py
veritex/examples/Demo/main_demo.py
Lines 66 to 69 in 920eb72
veritex/examples/Demo/main_demo.py
Lines 85 to 87 in 920eb72
dnn0.set_property(property1)
veritex/examples/Demo/main_demo.py
Lines 92 to 93 in 920eb72
veritex/examples/Demo/main_demo.py
Lines 107 to 110 in 920eb72
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.
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.
It would be useful to have all the outputs stored in a log file, particularly for debugging purposes in case some issue occurs.
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 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]))
What tables and figures are generated? Where are they stored? It would be nice to include this in the readme file.
Windows does not allow <> as a filename.
AcasNetID<1,7>-normed-train.pt
Add he simplest example in example.
just
We know Demo is also simple. but more simpler one!
Documentation looking much better already. May want to add file level documentation as follows:
veritex/veritex/methods/reachplot.py
Lines 1 to 8 in c22386b
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'
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!"
You did not upload it because those are generated when we run ACASXu example.
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
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
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 nnet module is missing.
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.
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
veritex/veritex/methods/repair.py
Line 28 in cabe690
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.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.