verified-intelligence / alpha-beta-crown Goto Github PK
View Code? Open in Web Editor NEWalpha-beta-CROWN: An Efficient, Scalable and GPU Accelerated Neural Network Verifier (winner of VNN-COMP 2021, 2022, and 2023)
License: Other
alpha-beta-CROWN: An Efficient, Scalable and GPU Accelerated Neural Network Verifier (winner of VNN-COMP 2021, 2022, and 2023)
License: Other
Hi,
I am running abcrown on a self-defined pytorch model, where I replaced the model_ori
as the following model, where all L_i are nn.Linear layers.:
class SVDNetBig(nn.Module):
def __init__(self, L1, L2, L3, L4, L5, L6, L7):
super(SVDNetBig, self).__init__()
self.flatten = nn.Flatten()
self.L1 = L1
self.L1R = nn.ReLU(inplace = True)
self.L2 = L2
self.L2R = nn.ReLU(inplace = True)
self.L3 = L3
self.L3R = nn.ReLU(inplace = True)
self.L4 = L4
self.L4R = nn.ReLU(inplace = True)
self.L5 = L5
self.L5R = nn.ReLU(inplace = True)
self.L6 = L6
self.L6R = nn.ReLU(inplace = True)
self.L7 = L7
def forward(self, x):
out = torch.sub(x, torch.tensor([[[[0.1307000070810318]]]], device = x.device))
out = torch.div(out, torch.tensor([[[[0.30810001492500305]]]], device = x.device))
out = self.flatten(out)
out = self.L1(out)
out = self.L1R(out)
out = self.L2(out)
out = self.L2R(out)
out = self.L3(out)
out = self.L3R(out)
out = self.L4(out)
out = self.L4R(out)
out = self.L5(out)
out = self.L5R(out)
out = self.L6(out)
out = self.L6R(out)
out = self.L7(out)
return out
The generated BoundedModule
is defined as follows:
BoundedModule(
(/0): BoundInput(name="/0")
(/1): BoundParams(name="/1")
(/2): BoundParams(name="/2")
(/3): BoundParams(name="/3")
(/4): BoundParams(name="/4")
(/5): BoundParams(name="/5")
(/6): BoundParams(name="/6")
(/7): BoundParams(name="/7")
(/8): BoundParams(name="/8")
(/9): BoundParams(name="/9")
(/10): BoundParams(name="/10")
(/11): BoundParams(name="/11")
(/12): BoundParams(name="/12")
(/13): BoundParams(name="/13")
(/14): BoundParams(name="/14")
(/15): BoundConstant(name="/15")
(/16): BoundSub(name="/16")
(/17): BoundConstant(name="/17")
(/18): BoundDiv(name="/18")
(/19): BoundFlatten(name="/19")
(/input): BoundLinear(name="/input")
(/21): BoundRelu(name="/21")
(/input.3): BoundLinear(name="/input.3")
(/23): BoundRelu(name="/23")
(/input.7): BoundLinear(name="/input.7")
(/25): BoundRelu(name="/25")
(/input.11): BoundLinear(name="/input.11")
(/27): BoundRelu(name="/27")
(/input.15): BoundLinear(name="/input.15")
(/29): BoundRelu(name="/29")
(/input.19): BoundLinear(name="/input.19")
(/31): BoundRelu(name="/31")
(/32): BoundLinear(name="/32")
)
However, calling model.build_the_model()
gives me IndexError
:
File "/home/alpha-beta-CROWN/complete_verifier/auto_LiRPA/backward_bound.py", line 156, in backward_general
A, lower_b, upper_b = l.bound_backward(l.lA, l.uA, *l.inputs)
File "/home/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/bivariate.py", line 562, in bound_backward
uA_y = _bound_oneside(last_uA, y, sign=-1)
File "/home/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/bivariate.py", line 550, in _bound_oneside
return self.broadcast_backward(sign * last_A, w)
File "/home/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/base.py", line 282, in broadcast_backward
if shape[i] == 1 and A.shape[i + 1] != 1 and i != batch_dim:
IndexError: tuple index out of range
File "/home/alpha-beta-CROWN/complete_verifier/auto_LiRPA/backward_bound.py", line 156, in backward_general
A, lower_b, upper_b = l.bound_backward(l.lA, l.uA, *l.inputs)
File "/home/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/bivariate.py", line 562, in bound_backward
uA_y = _bound_oneside(last_uA, y, sign=-1)
File "/home/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/bivariate.py", line 550, in _bound_oneside
return self.broadcast_backward(sign * last_A, w)
File "/home/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/base.py", line 282, in broadcast_backward
if shape[i] == 1 and A.shape[i + 1] != 1 and i != batch_dim:
IndexError: tuple index out of range
Any insights on how to solve the issue? Thank you so much for your reply!
Hi,
I tried to run abcrown on the network built by myself.
A special thing about my network is that it is like "residual linear", where I have a "
Add" node but its inputs are two "Gemm" nodes (unlike residual block which is two Conv nodes as inputs of "Add")
The input of the network is [1, 1, 28, 28] , and I set the input shape in .yaml as well.
model:
input_shape: [1, 1, 28, 28]
But during execution, it gave me:
File "alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 857, in check_prior_bounds
node.inputs[i], prior_checked=True)
File "alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 946, in compute_intermediate_bounds
ref_intermediate_lb, ref_intermediate_ub)
File "alpha-beta-CROWN/complete_verifier/auto_LiRPA/backward_bound.py", line 346, in get_sparse_C
num_channel = node.output_shape[-3]
IndexError: tuple index out of range
I thought auto-LiRPA can handle any DAG? I am not sure what leads to the problem.
Could you please kindly give me some advice?
Thanks and regards,
Yuyi
Hi, I figured CROWN does not support having the ReLU function as last year (it throws some error), so I thought I could add an identity Linear layer after ReLU as follows:
class MyModel(nn.ModuleList):
def __init__(self, device=torch.device("cpu")):
super(MyModel, self).__init__()
self.to(device)
self.af = nn.ReLU()
self.lin1 = nn.Linear(19, 32)
self.lin2 = nn.Linear(32, 32)
self.out = nn.Linear(32, 15)
self.c2d_1 = torch.nn.Conv1d(1, 24, 15)
self.c2d_2 = torch.nn.Conv1d(24, 12, 1)
self.c2d_3 = torch.nn.Conv1d(12, 6, 1)
self.c2d_4 = torch.nn.Conv1d(6, 3, 1)
self.c2d_5 = torch.nn.Conv1d(3, 1, 1)
self.eye = torch.nn.Linear(1, 1)
self.eye.weight = torch.nn.Parameter(torch.ones_like(self.eye.weight))
self.eye.bias = torch.nn.Parameter(torch.tensor([0.], requires_grad=True))
def forward(self, obs):
obs = self.af(self.lin1(obs))
obs = self.af(self.lin2(obs))
logits = self.out(obs)
after_conv1 = self.af(self.c2d_1(logits))
after_conv2 = self.af(self.c2d_2(after_conv1))
after_conv3 = self.af(self.c2d_3(after_conv2))
after_conv4 = self.af(self.c2d_4(after_conv3))
after_conv5 = self.af(self.c2d_5(after_conv4))
return self.eye(after_conv5)[0]
Nonetheless, it gives me the following error:
Traceback (most recent call last):
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 612, in <module>
abcrown.main()
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 591, in main
verified_status = self.complete_verifier(
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 416, in complete_verifier
l, nodes, ret = self.bab(
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 241, in bab
result = general_bab(
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/bab.py", line 340, in general_bab
global_lb = act_split_round(
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/bab.py", line 165, in act_split_round
split_domain(net, domains, d, batch, impl_params=impl_params,
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/bab.py", line 70, in split_domain
branching_heuristic.get_branching_decisions(
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/torch/autograd/grad_mode.py", line 27, in decorate_context
return func(*args, **kwargs)
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/heuristics/kfsb.py", line 143, in get_branching_decisions
k_ret_lbs = self.net.update_bounds(
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 303, in update_bounds
lb, _, = self.net.compute_bounds(
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 1206, in compute_bounds
return self._compute_bounds_main(C=C,
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 1311, in _compute_bounds_main
ret = self.backward_general(
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/backward_bound.py", line 324, in backward_general
lb, ub = concretize(self, batch_size, output_dim, lb, ub,
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/backward_bound.py", line 671, in concretize
lA = roots[i].lA.reshape(output_dim, batch_size, -1).transpose(0, 1) if bound_lower else None
RuntimeError: shape '[1, 4, -1]' is invalid for input of size 1
P.S: the error is gone when I remove this line of parameter setting:
self.eye.weight = torch.nn.Parameter(torch.ones_like(self.eye.weight))
It seems that input linear constraint (e.g., x_1 > x_2) is not supported. I got the following error message.
File "alpha-beta-CROWN/complete_verifier/read_vnnlib.py", line 80, in update_rv_tuple
f"input constraints must be box ({op} {first} {second})"
AssertionError: input constraints must be box
Is there a plan to support input linear constraint in the near future?
I have read the paper《Efficient neural network robustness certification with general activation functions》(proposed CROWN),I have a question:
Why should back propagate to the first layer to calculate Global bounds by Λ(0) and Ω(0)?will the Global bounds obtained this way be more accurate?
When I test a robustness property using this tool, the result of program return 'unsafe', but I can not find the corresponding adversarial example.
Hello and fantastic work on developing your tool!
I am just beginning to try it out, and want to try running it on a Mac OS computer. I have the impression that your environment.yaml file is for linux rather than Mac OS. I am wondering if you happen to already have an environment.yml file that works for Mac OS. (If not and I reach one that works, I will be happy to share it.)
When I verify a CROWN-ibp pre-trained model using alpha-beta-CROWN, it consistenly shows Result: image x prediction is incorrect, skipped.
As a result the overall verified acc. is very low depsite CROWN-verified acc. is relatively normal.
I guess that's batch-norm support problem, because in the printed log I see two new warnings:
/home/zhangheng/anaconda3/envs/alpha-beta-crown/lib/python3.7/site-packages/torch/nn/functional.py:2113: TracerWarning: Converting a tensor to a Python boolean might cause the trace to be incorrect. We can't record the data flow of Python values, so this value will be treated as a constant in the future. This means that the trace might not generalize to other inputs!
if size_prods == 1:
/home/zhangheng/anaconda3/envs/alpha-beta-crown/lib/python3.7/site-packages/torch/onnx/symbolic_helper.py:680: UserWarning: ONNX export mode is set to inference mode, but operator batch_norm is set to training mode. The model will be exported in inference, as specified by the export mode.
training_mode + ", as specified by the export mode.")
I tried some scripts without batchnorm included in exp_configs
folder, there are no these two warnings.
Here are the log file, please have a look, thank you!
Hi,
I followed your instructions online to run robustness verification on ERAN benchmark, eg:
python robustness_verifier.py --config exp_configs/mnist_conv_small.yaml
but change the epsilon from 0.12 to 0.11.
I also used the same parameter configuration in mnist_6_100.yaml to run on ERAN mnist_3_100 and mnist_5_100.
Since alpha-beta-CROWN should be a complete tool for ReLU-activated networks, I am confused that there are still some images with inconclusive results.
May I ask why this is the case? And how may I run it with complete behavior?
Thank you so much for your help!
When I try to execute the below command:
conda env create -f complete_verifier/environment.yml
I face this issue:
Collecting package metadata (repodata.json): done
Solving environment: failed
ResolvePackageNotFound:
For your information, I am working on Windows OS.
Hi,
I just noticed that when running on the same network and the same property, the visited subdomains could be different.
all nodes are split!!
9651 domains visited
Result: timeout
Time: 111.90976047515869
all nodes are split!!
9777 domains visited
Result: timeout
Time: 112.87935328483582
all nodes are split!!
9790 domains visited
Result: timeout
Time: 114.08122301101685
For example, I presented the printouts of 3 executions given the same config (I set the attack as skip, and the bab timeout as 360)
Even though all nodes are split, I wonder why different numbers of domains were visited for different execution.
What leads to this randomness of domains?
I would be grateful if you could share some insights.
Thanks and regards,
Yuyi
Thanks for adding the support for conv1d in the new release.
I get the following error when I have a sequence of two conv1d in my network architecture:
class MyModel(nn.ModuleList):
def __init__(self, device=torch.device("cpu")):
super(MyModel, self).__init__()
self.to(device)
self.af = nn.ReLU()
self.lin1 = nn.Linear(19, 15)
self.c1d_1 = torch.nn.Conv1d(1, 24, 15)
self.c1d_2 = torch.nn.Conv1d(24, 1, 1)
def forward(self, obs):
lin1 = self.af(self.lin1(obs))
after_conv1 = self.af(self.c1d_1(lin1.unsqueeze(dim=0)))
after_conv2 = self.af(self.c1d_2(after_conv1))
return after_conv2[0]
The error:
Traceback (most recent call last):
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 612, in <module>
abcrown.main()
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 591, in main
verified_status = self.complete_verifier(
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 416, in complete_verifier
l, nodes, ret = self.bab(
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 241, in bab
result = general_bab(
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/bab.py", line 246, in general_bab
global_lb, ret = net.build(
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 455, in build
lb, ub, aux_reference_bounds = self.net.init_alpha(
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/optimized_bounds.py", line 766, in init_alpha
l, u = self.compute_bounds(
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 1206, in compute_bounds
return self._compute_bounds_main(C=C,
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 1303, in _compute_bounds_main
self.check_prior_bounds(final)
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
self.check_prior_bounds(n)
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
self.check_prior_bounds(n)
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
self.check_prior_bounds(n)
[Previous line repeated 3 more times]
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 804, in check_prior_bounds
self.compute_intermediate_bounds(
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 910, in compute_intermediate_bounds
node.lower, node.upper = self.backward_general(
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/backward_bound.py", line 337, in backward_general
lb = lb.view(batch_size, *output_shape) if bound_lower else None
RuntimeError: view size is not compatible with input tensor's size and stride (at least one dimension spans across two contiguous subspaces). Use .reshape(...) instead.
I tried the solutions I found online (replacing view by reshape AND adding contiguous() before view()), but it throws another error:
Traceback (most recent call last):
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 612, in <module>
abcrown.main()
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 591, in main
verified_status = self.complete_verifier(
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 416, in complete_verifier
l, nodes, ret = self.bab(
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 241, in bab
result = general_bab(
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/bab.py", line 246, in general_bab
global_lb, ret = net.build(
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 455, in build
lb, ub, aux_reference_bounds = self.net.init_alpha(
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/optimized_bounds.py", line 766, in init_alpha
l, u = self.compute_bounds(
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 1206, in compute_bounds
return self._compute_bounds_main(C=C,
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 1303, in _compute_bounds_main
self.check_prior_bounds(final)
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
self.check_prior_bounds(n)
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
self.check_prior_bounds(n)
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
self.check_prior_bounds(n)
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 804, in check_prior_bounds
self.compute_intermediate_bounds(
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 915, in compute_intermediate_bounds
self.restore_sparse_bounds(
File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/backward_bound.py", line 584, in restore_sparse_bounds
lower[:, unstable_idx] = new_lower.view(batch_size, -1)
RuntimeError: shape mismatch: value tensor of shape [1331] cannot be broadcast to indexing result of shape [1, 11]
Describe the bug
Hi, when I reproduced the results for SDP models with GCP-CROWN, an error occurred.
To Reproduce
run 'python abcrown.py --config exp_configs/GCP-CROWN/mnist_cnn_a_adv.yaml'
Traceback (most recent call last):
File "/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/abcrown.py", line 609, in
abcrown.main()
File "/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/abcrown.py", line 588, in main
verified_status = self.complete_verifier(
File "/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/abcrown.py", line 399, in complete_verifier
l, nodes, ret = self.bab(
File "/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/abcrown.py", line 242, in bab
result = general_bab(
File "/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/bab.py", line 269, in general_bab
net.set_cuts(model_incomplete.A_saved, x, ret['lower_bounds'], ret['upper_bounds'])
File "/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/cuts/cut_verification.py", line 269, in set_cuts
cuts = add_input_cuts(self, A, number_cuts=number_cuts, device=self.net.device)
File "/home/ictt/miniconda3/envs/alpha-beta-crown2/lib/python3.9/site-packages/torch/autograd/grad_mode.py", line 27, in decorate_context
return func(*args, **kwargs)
File "/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/cuts/implied_cuts.py", line 237, in add_input_cuts
assert last_A.matmul(center) - last_A.abs().matmul(diff) + last_b < 0
AssertionError
mip solver model built in 0.6189 seconds.
lower bounds for all target labels: [1.9055490493774414, 0.5247936248779297, -2.302560329437256, -1.420586109161377, -0.5922765731811523, -0.33838844299316406, -1.5372157096862793, 1.1211633682250977, 0.47852492332458496]
Starting MIP solver for these labels: [2, 3, 4, 5, 6]
start creating model mps for candidates: ['lay/16_2', 'lay/16_3', 'lay/16_4', 'lay/16_5', 'lay/16_6']
parallel save mip model to /home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/cuts/CPLEX_cuts/cplexmip_lay-16_starttime=1708308422_idx=1_spec=2_30843038.mps
parallel save mip model to /home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/cuts/CPLEX_cuts/cplexmip_lay-16_starttime=1708308422_idx=1_spec=3_30843038.mps
parallel save mip model to /home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/cuts/CPLEX_cuts/cplexmip_lay-16_starttime=1708308422_idx=1_spec=4_30843038.mps
parallel save mip model to /home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/cuts/CPLEX_cuts/cplexmip_lay-16_starttime=1708308422_idx=1_spec=5_30843038.mps
parallel save mip model to /home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/cuts/CPLEX_cuts/cplexmip_lay-16_starttime=1708308422_idx=1_spec=6_30843038.mps
parallel mps save finish
/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/lp_mip_solver.py:1146: ResourceWarning: unclosed file <_io.TextIOWrapper name='/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/cuts/CPLEX_cuts/cplexmip_lay-16_starttime=1708308422_idx=1_spec=2_30843038.log' mode='w' encoding='ANSI_X3.4-1968'>
proc, logfile = run_get_cuts_subprocess(model_filename_stamped)
ResourceWarning: Enable tracemalloc to get the object allocation traceback
Process Process-2:
Traceback (most recent call last):
File "/home/ictt/miniconda3/envs/alpha-beta-crown2/lib/python3.9/multiprocessing/managers.py", line 802, in _callmethod
conn = self._tls.connection
AttributeError: 'ForkAwareLocal' object has no attribute 'connection'
During handling of the above exception, another exception occurred:
Traceback (most recent call last):
File "/home/ictt/miniconda3/envs/alpha-beta-crown2/lib/python3.9/multiprocessing/process.py", line 315, in _bootstrap
self.run()
File "/home/ictt/miniconda3/envs/alpha-beta-crown2/lib/python3.9/multiprocessing/process.py", line 108, in run
self._target(*self._args, **self._kwargs)
File "/home/ictt/miniconda3/envs/alpha-beta-crown2/lib/python3.9/site-packages/torch/autograd/grad_mode.py", line 27, in decorate_context
return func(*args, **kwargs)
File "/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/lp_mip_solver.py", line 1042, in construct_mip_with_model
build_the_model_mip(model, labels_to_verify=None, save_mps=save_mps, process_dict=process_dict, x=x, intermediate_bounds=intermediate_bounds)
File "/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/lp_mip_solver.py", line 1152, in build_the_model_mip
raise e
File "/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/lp_mip_solver.py", line 1147, in build_the_model_mip
processes[pidx] = {'pid': proc.pid, '_logfile': logfile, '_fname_stamped': model_filename_stamped, 'c': model_c_row}
File "", line 2, in setitem
File "/home/ictt/miniconda3/envs/alpha-beta-crown2/lib/python3.9/multiprocessing/managers.py", line 806, in _callmethod
self._connect()
File "/home/ictt/miniconda3/envs/alpha-beta-crown2/lib/python3.9/multiprocessing/managers.py", line 793, in _connect
conn = self._Client(self._token.address, authkey=self._authkey)
File "/home/ictt/miniconda3/envs/alpha-beta-crown2/lib/python3.9/multiprocessing/connection.py", line 502, in Client
c = SocketClient(address)
File "/home/ictt/miniconda3/envs/alpha-beta-crown2/lib/python3.9/multiprocessing/connection.py", line 630, in SocketClient
s.connect(address)
FileNotFoundError: [Errno 2] No such file or directory
/home/ictt/miniconda3/envs/alpha-beta-crown2/lib/python3.9/subprocess.py:1052: ResourceWarning: subprocess 4172529 is still running
_warn("subprocess %s is still running" % self.pid,
ResourceWarning: Enable tracemalloc to get the object allocation traceback
System configuration:
NVIDIA TITAN RTX 24G.
environment_pyt111.yaml
How to solve the problem?
Hi, I am using alpha-beta-CROWN to certify a model, called CNN7, on CIFAR10 dataset. However, I met "CUDA out of memory error":
torch.cuda.OutOfMemoryError: CUDA out of memory. Tried to allocate 10.11 GiB (GPU 0; 23.65 GiB total capacity; 8.18 GiB already allocated; 8.91 GiB free; 13.24 GiB reserved in total by PyTorch) If reserved memory is >> allocated memory try setting max_split_size_mb to avoid fragmentation. See documentation for Memory Management and PYTORCH_CUDA_ALLOC_CONF
As shown above, the memory of my GPU card is 24GB.
The structure of CNN7 is as follows:
Sequential(
(0): Conv2d(3, 64, kernel_size=(3, 3), stride=(1, 1), padding=(1, 1))
(1): ReLU()
(2): Conv2d(64, 64, kernel_size=(3, 3), stride=(1, 1), padding=(1, 1))
(3): ReLU()
(4): Conv2d(64, 128, kernel_size=(3, 3), stride=(2, 2), padding=(1, 1))
(5): ReLU()
(6): Conv2d(128, 128, kernel_size=(3, 3), stride=(1, 1), padding=(1, 1))
(7): ReLU()
(8): Conv2d(128, 128, kernel_size=(3, 3), stride=(1, 1), padding=(1, 1))
(9): ReLU()
(10): Flatten(start_dim=1, end_dim=-1)
(11): Linear(in_features=32768, out_features=512, bias=True)
(12): ReLU()
(13): Linear(in_features=512, out_features=10, bias=True)
)
I am considering if CNN7 model is too big to be certified by alpha-beta-CROWN.
So is there any way for me to certify CNN7 using alpha-beta-CROWN (without a GPU card with larger memory)?
Hi,
When I tried to evaluate both the lower and upper bound of a NN by calling the bab() method in /complete_verifier/bab_verification_general.py, it has an assertion error in the compute_bounds()
method in auto_LiRPA/bound_general.py.
It seems that we cannot have return_A == True
when calling compute_bounds()
since method == crown-optimized
(was set here). However, it seems that in this build_the_model_with_refined_bounds() method, return_A
is set to True
if we want to get_upper_bound
.
Thanks for helping.
Zhilu
Firstly, thank you for your amazing work and for sharing it with us.
I try to use your framework to run robustness tests on a very simple convnet for classification task. The implementation is as following:
import pickle
def load_pickled_data(file, columns):
"""
Loads pickled training and test data.
Parameters
----------
file :
Name of the pickle file.
columns : list of strings
List of columns in pickled data we're interested in.
Returns
-------
A tuple of datasets for given columns.
"""
with open(file, mode='rb') as f:
dataset = pickle.load(f)
return tuple(map(lambda c: dataset[c], columns))
import torch
import numpy as np
from typing import Tuple
class TSRDataset(torch.utils.data.Dataset):
def __init__(self, pickled_X: np.array, pickled_y: np.array, transform=None) -> None:
super(TSRDataset).__init__()
self.X_ = pickled_X
self.y_ = pickled_y
# # 4. Make function to load images
# def load_image(self, index: int) -> Image.Image:
# "Opens an image via a path and returns it."
# image_path = self.paths[index]
# return Image.open(image_path)
def __len__(self) -> int:
"Returns the total number of samples."
return len(self.X_)
# Overwrite the __getitem__() method (required for subclasses of torch.utils.data.Dataset)
def __getitem__(self, index: int) -> Tuple[torch.Tensor, int]:
"Returns one sample of data, data and label (X, y)."
img = self.X_[index]
class_idx = self.y_[index]
return img, class_idx # return data, label (X, y)
import torch.nn as nn
class CNN(nn.Module):
def __init__(self, params):
super(CNN, self).__init__()
self.conv1 = nn.Conv2d(in_channels=1, out_channels=params.conv1_d, kernel_size=params.conv1_k, stride=1, padding=self.get_pad(params.conv1_k, 1))
self.conv2 = nn.Conv2d(in_channels=params.conv1_d, out_channels=params.conv2_d, kernel_size=params.conv2_k, stride=1, padding=self.get_pad(params.conv2_k, 1))
self.conv3 = nn.Conv2d(in_channels=params.conv2_d, out_channels=params.conv3_d, kernel_size=params.conv3_k, stride=1, padding=self.get_pad(params.conv3_k, 1))
self.fc4 = nn.Linear(in_features=3584, out_features=params.fc4_size)
self.out = nn.Linear(in_features=params.fc4_size, out_features=params.num_classes)
self.params = params
def get_pad(self, ksize, stride):
in_height = in_width = 32
stride_height = stride_width = stride
strides = [stride_height, stride_width]
filter_height = filter_width = ksize
if (in_height % strides[0] == 0):
pad_along_height = max(filter_height - stride_height, 0)
else:
pad_along_height = max(filter_height - (in_height % stride_height), 0)
if (in_width % strides[1] == 0):
pad_along_width = max(filter_width - stride_width, 0)
else:
pad_along_width = max(filter_width - (in_width % stride_width), 0)
pad_top = pad_along_height // 2
pad_bottom = pad_along_height - pad_top
pad_left = pad_along_width // 2
pad_right = pad_along_width - pad_left
return [pad_left, pad_right]
def forward(self, x, is_training=True):
# Convolutions
x = self.conv1(x)
x = nn.functional.relu(x)
x = nn.functional.max_pool2d(x, kernel_size=2, stride=2, padding=self.get_pad(2,2))
# x = nn.functional.dropout(x, p=self.params.conv1_p, training=is_training)
x1 = x.clone()
x = self.conv2(x)
x = nn.functional.relu(x)
x = nn.functional.max_pool2d(x, kernel_size=2, stride=2, padding=self.get_pad(2,2))
# x = nn.functional.dropout(x, p=self.params.conv2_p, training=is_training)
x2 = x.clone()
x = self.conv3(x)
x = nn.functional.relu(x)
x = nn.functional.max_pool2d(x, kernel_size=2, stride=2, padding=self.get_pad(2,2))
# x = nn.functional.dropout(x, p=self.params.conv3_p, training=is_training)
x3 = x.clone()
# Fully connected
x1 = nn.functional.max_pool2d(x1, kernel_size=4, stride=4, padding=self.get_pad(4,4))
x1 = torch.flatten(x1, 1, -1)
x2 = nn.functional.max_pool2d(x2, kernel_size=2, stride=2, padding=self.get_pad(2,2))
x2 = torch.flatten(x2, 1, -1)
x3 = torch.flatten(x3, 1, -1)
x = torch.cat((x1, x2, x3), dim=-1)
x = self.fc4(x)
x = nn.functional.relu(x)
# x = nn.functional.dropout(x, p=self.params.fc4_p, training=is_training)
x = self.out(x)
return x
def get_model():
from collections import namedtuple
Parameters = namedtuple('Parameters', [
# Data parameters
'num_classes', 'image_size',
# Training parameters
'batch_size', 'max_epochs', 'log_epoch', 'print_epoch',
# Optimisations
'learning_rate_decay', 'learning_rate',
'l2_reg_enabled', 'l2_lambda',
'early_stopping_enabled', 'early_stopping_patience',
'resume_training',
# Layers architecture
'conv1_k', 'conv1_d', 'conv1_p',
'conv2_k', 'conv2_d', 'conv2_p',
'conv3_k', 'conv3_d', 'conv3_p',
'fc4_size', 'fc4_p'
])
parameters = Parameters(
# Data parameters
num_classes = 43,
image_size = (32, 32),
# Training parameters
batch_size = 256,
max_epochs = 30,
log_epoch = 1,
print_epoch = 1,
# Optimisations
learning_rate_decay = True,
learning_rate = 0.001,
l2_reg_enabled = False,
l2_lambda = 0.0001,
early_stopping_enabled = True,
early_stopping_patience = 25,
resume_training = False,
# Layers architecture
conv1_k = 5, conv1_d = 32, conv1_p = 0.9,
conv2_k = 5, conv2_d = 64, conv2_p = 0.8,
conv3_k = 5, conv3_d = 128, conv3_p = 0.7,
fc4_size = 1024, fc4_p = 0.5
)
return CNN(parameters)
def tsr_data(eps):
"""Example dataloader. For MNIST and CIFAR you can actually use existing ones in utils.py."""
assert eps is not None
data_path = '/kaggle/input/reqnew/train_extended_preprocessed.p'
X_test, y_test = load_pickled_data(data_path, columns = ['features', 'labels'])
# You can access the mean and std stored in config file.
mean = torch.tensor(np.mean(X_test, axis=(0,1,2)))
std = torch.tensor(np.std(X_test, axis=(0,1,2)))
# normalize = transforms.Normalize(mean=mean, std=std)
test_data = TSRDataset(X_test, y_test, transform=None)
# Load entire dataset.
testloader = torch.utils.data.DataLoader(test_data,\
batch_size=10000, shuffle=False, num_workers=0)
X, labels = next(iter(testloader))
# Set data_max and data_min to be None if no clip. For CIFAR-10 we clip to [0,1].
data_max = torch.reshape((1. - mean) / std, (1, -1, 1, 1))
data_min = torch.reshape((0. - mean) / std, (1, -1, 1, 1))
if eps is None:
raise ValueError('You must specify an epsilon')
# Rescale epsilon.
ret_eps = torch.reshape(eps / std, (1, -1, 1, 1))
return torch.tensor(X).permute((0,3,1,2)), torch.argmax(torch.tensor(labels), dim=-1), data_max, data_min, ret_eps
My loaded data is actually an np array of shape [N, H, W, C] where C is 1 since it is in grayscale. The labels are classes that range from 0 to 42.
When I run alpha-beta-CROWN with the attached configuration, I got the following output:
/kaggle/working
Configurations:
general:
device: cuda
seed: 100
conv_mode: patches
deterministic: false
double_fp: false
loss_reduction_func: sum
record_bounds: false
sparse_alpha: true
save_adv_example: false
precompile_jit: false
complete_verifier: bab
enable_incomplete_verification: true
csv_name: null
results_file: out.txt
root_path: ''
model:
name: 'Customized("custom_model_data", "get_model")'
path: /kaggle/working/model_torch.pt
onnx_path: null
onnx_path_prefix: ''
cache_onnx_conversion: false
onnx_quirks: null
input_shape: null
onnx_loader: default_onnx_and_vnnlib_loader
onnx_optimization_flags: none
data:
start: 0
end: 10
select_instance: null
num_outputs: 43
mean: 0.0
std: 1.0
pkl_path: null
dataset: 'Customized("custom_model_data", "tsr_data")'
data_filter_path: null
data_idx_file: null
specification:
type: lp
robustness_type: verified-acc
norm: .inf
epsilon: 0.00784313725
vnnlib_path: null
vnnlib_path_prefix: ''
solver:
batch_size: 256
min_batch_size_ratio: 0.1
use_float64_in_last_iteration: false
early_stop_patience: 10
start_save_best: 0.5
bound_prop_method: alpha-crown
prune_after_crown: false
crown:
batch_size: 1000000000
max_crown_size: 1000000000
alpha-crown:
alpha: true
lr_alpha: 0.1
iteration: 100
share_slopes: false
no_joint_opt: false
lr_decay: 0.98
full_conv_alpha: true
beta-crown:
lr_alpha: 0.01
lr_beta: 0.05
lr_decay: 0.98
optimizer: adam
iteration: 20
beta: true
beta_warmup: true
enable_opt_interm_bounds: false
all_node_split_LP: false
forward:
refine: false
dynamic: false
max_dim: 10000
multi_class:
multi_class_method: allclass_domain
label_batch_size: 32
skip_with_refined_bound: true
mip:
parallel_solvers: null
solver_threads: 1
refine_neuron_timeout: 15
refine_neuron_time_percentage: 0.8
early_stop: true
adv_warmup: true
mip_solver: gurobi
bab:
initial_max_domains: 1
max_domains: .inf
decision_thresh: 0
timeout: 300
timeout_scale: 1
override_timeout: null
get_upper_bound: false
dfs_percent: 0.0
pruning_in_iteration: true
pruning_in_iteration_ratio: 0.2
sort_targets: false
batched_domain_list: true
optimized_intermediate_layers: ''
interm_transfer: true
cut:
enabled: false
bab_cut: false
lp_cut: false
method: null
lr: 0.01
lr_decay: 1.0
iteration: 100
bab_iteration: -1
early_stop_patience: -1
lr_beta: 0.02
number_cuts: 50
topk_cuts_in_filter: 100
batch_size_primal: 100
max_num: 1000000000
patches_cut: false
cplex_cuts: false
cplex_cuts_wait: 0
cplex_cuts_revpickup: true
cut_reference_bounds: true
fix_intermediate_bounds: false
branching:
method: kfsb
candidates: 3
reduceop: min
sb_coeff_thresh: 0.001
input_split:
enable: false
enhanced_bound_prop_method: alpha-crown
enhanced_branching_method: naive
enhanced_bound_patience: 100000000.0
attack_patience: 100000000.0
adv_check: 0
sort_domain_interval: -1
attack:
enabled: false
beam_candidates: 8
beam_depth: 7
max_dive_fix_ratio: 0.8
min_local_free_ratio: 0.2
mip_start_iteration: 5
mip_timeout: 30.0
adv_pool_threshold: null
refined_mip_attacker: false
refined_batch_size: null
attack:
pgd_order: before
pgd_steps: 100
pgd_restarts: 100
pgd_early_stop: true
pgd_lr_decay: 0.99
pgd_alpha: auto
pgd_loss_mode: null
enable_mip_attack: false
cex_path: ./test_cex.txt
attack_mode: PGD
gama_lambda: 10.0
gama_decay: 0.9
check_clean: false
input_split:
pgd_steps: 100
pgd_restarts: 30
pgd_alpha: auto
input_split_enhanced:
pgd_steps: 200
pgd_restarts: 5000000
pgd_alpha: auto
input_split_check_adv:
pgd_steps: 5
pgd_restarts: 5
pgd_alpha: auto
debug:
lp_test: null
Experiments at Fri May 5 09:26:50 2023 on b2ccc2a2c33d
CNN(
(conv1): Conv2d(1, 32, kernel_size=(5, 5), stride=(1, 1), padding=(2, 2))
(conv2): Conv2d(32, 64, kernel_size=(5, 5), stride=(1, 1), padding=(2, 2))
(conv3): Conv2d(64, 128, kernel_size=(5, 5), stride=(1, 1), padding=(2, 2))
(fc4): Linear(in_features=3584, out_features=1024, bias=True)
(out): Linear(in_features=1024, out_features=43, bias=True)
)
/kaggle/working/alpha-beta-CROWN/complete_verifier/custom_model_data.py:211: UserWarning: To copy construct from a tensor, it is recommended to use sourceTensor.clone().detach() or sourceTensor.clone().detach().requires_grad_(True), rather than torch.tensor(sourceTensor).
return torch.tensor(X).permute((0,3,1,2)), torch.argmax(torch.tensor(labels), dim=-1), data_max, data_min, ret_eps
Internal results will be saved to Verified_ret_[Customized_model]_start=0_end=10_iter=20_b=256_timeout=300_branching=kfsb-min-3_lra-init=0.1_lra=0.01_lrb=0.05_PGD=before_cplex_cuts=False_multiclass=allclass_domain.npy.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% idx: 0, vnnlib ID: 0 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Attack parameters: initialization=uniform, steps=100, restarts=100, alpha=0.007461458444595337, initialization=uniform, GAMA=False
Model output of first 5 examples:
tensor([[-26.63533783, -5.86781883, -4.54763603, -21.69909477, -20.81317139,
-0.61611140, -16.72828102, -13.13037777, -18.94099617, -26.45909882,
-4.61056852, -12.54259109, -0.75518376, -16.09009552, -2.99634385,
-11.60897160, -17.43187332, -9.52975750, -18.21758842, -29.91522217,
-33.70221329, -23.20652962, -18.36230087, -25.41592407, -33.91773987,
-21.16673660, -17.64099312, -39.80070496, -35.47123337, -31.05479431,
-22.17935181, -18.36315536, -43.14264679, -13.38010883, 12.96510029,
-20.21791458, -4.28863621, -6.38604784, 41.21236038, -6.59563351,
4.28117037, -27.70765305, -9.50008297]], device='cuda:0')
Adv example prediction (first 2 examples and 2 restarts):
tensor([[[-26.52582550, -3.93510056, -6.41698170, -20.35298538, -20.99528694,
-6.70625925, -16.09720039, -15.72246552, -17.80824852, -23.99833107,
-11.98600864, -10.19097519, 2.43953228, -9.03533268, -2.28550172,
-9.02405930, -19.05975914, -7.56664610, -19.64624596, -25.21205711,
-34.47130585, -25.68278313, -19.72745895, -25.75965881, -34.31901932,
-21.08712769, -16.40643311, -36.51839066, -30.18853760, -27.88558769,
-23.38009453, -19.63435936, -35.52644348, -10.87827301, 20.88450241,
-9.49922180, -2.24221802, 1.64629138, 29.64516830, -7.80061817,
5.89254475, -24.37758255, -11.45957851],
[-26.52582741, -3.93510199, -6.41698503, -20.35298538, -20.99528885,
-6.70626211, -16.09720039, -15.72246647, -17.80824661, -23.99833107,
-11.98601246, -10.19097233, 2.43953443, -9.03533077, -2.28550124,
-9.02405930, -19.05976105, -7.56664419, -19.64624596, -25.21205330,
-34.47130585, -25.68278503, -19.72745895, -25.75965881, -34.31901550,
-21.08712578, -16.40643501, -36.51838684, -30.18853188, -27.88558388,
-23.38009453, -19.63436317, -35.52643967, -10.87827301, 20.88450432,
-9.49921989, -2.24221563, 1.64629233, 29.64516640, -7.80062008,
5.89254475, -24.37757874, -11.45957756]]], device='cuda:0')
PGD attack margin (first 2 examles and 10 specs):
tensor([[[56.17099380, 33.58026886, 36.06214905, 49.99815369, 50.64045715,
36.35142899, 45.74237061, 45.36763382, 47.45341492, 53.64349747]]],
device='cuda:0')
number of violation: 0
Attack finished in 16.8530 seconds.
PGD attack failed
/kaggle/working/alpha-beta-CROWN/auto_LiRPA/parse_graph.py:147: FutureWarning: 'torch.onnx.symbolic_helper._set_opset_version' is deprecated in version 1.13 and will be removed in version 1.14. Please remove its usage and avoid setting internal variables directly.
_set_opset_version(12)
/kaggle/working/alpha-beta-CROWN/auto_LiRPA/parse_graph.py:45: FutureWarning: 'torch.onnx._patch_torch._node_getitem' is deprecated in version 1.13 and will be removed in version 1.14. Please Internally use '_node_get' in symbolic_helper instead..
attrs = {k: n[k] for k in n.attributeNames()}
Model prediction is: tensor([[-26.63533783, -5.86781883, -4.54763603, -21.69909477, -20.81317139,
-0.61611140, -16.72828102, -13.13037777, -18.94099617, -26.45909882,
-4.61056852, -12.54259109, -0.75518376, -16.09009552, -2.99634385,
-11.60897160, -17.43187332, -9.52975750, -18.21758842, -29.91522217,
-33.70221329, -23.20652962, -18.36230087, -25.41592407, -33.91773987,
-21.16673660, -17.64099312, -39.80070496, -35.47123337, -31.05479431,
-22.17935181, -18.36315536, -43.14264679, -13.38010883, 12.96510029,
-20.21791458, -4.28863621, -6.38604784, 41.21236038, -6.59563351,
4.28117037, -27.70765305, -9.50008297]], device='cuda:0')
/kaggle/working/alpha-beta-CROWN/auto_LiRPA/bound_general.py:946: UserWarning: Creating an identity matrix with size 8192x8192 for node BoundMaxPool(name="/input"). This may indicate poor performance for bound computation. If you see this message on a small network please submit a bug report.
ref_intermediate_lb, ref_intermediate_ub)
/kaggle/working/alpha-beta-CROWN/auto_LiRPA/bound_general.py:946: UserWarning: Creating an identity matrix with size 4096x4096 for node BoundMaxPool(name="/input.4"). This may indicate poor performance for bound computation. If you see this message on a small network please submit a bug report.
ref_intermediate_lb, ref_intermediate_ub)
layer /12 using sparse-features alpha with shape [11222]; unstable size 11222; total size 32768 (torch.Size([1, 32, 32, 32]))
layer /12 start_node /input using full alpha with unstable size None total_size 8192 output_shape torch.Size([32, 16, 16])
layer /12 start_node /x.3 using full alpha with unstable size 64 total_size 64 output_shape 64
layer /12 start_node /input.4 using full alpha with unstable size None total_size 4096 output_shape torch.Size([64, 8, 8])
layer /12 start_node /x.7 using full alpha with unstable size 128 total_size 128 output_shape 128
layer /12 start_node /x.11 using full alpha with unstable size 1024 total_size 1024 output_shape torch.Size([1024])
layer /12 start_node /28 using full alpha with unstable size None total_size 42 output_shape 42
Traceback (most recent call last):
File "/kaggle/working/alpha-beta-CROWN/complete_verifier/abcrown.py", line 647, in <module>
main()
File "/kaggle/working/alpha-beta-CROWN/complete_verifier/abcrown.py", line 535, in main
incomplete_verifier(model_ori, x, data_ub=data_max, data_lb=data_min, vnnlib=vnnlib)
File "/kaggle/working/alpha-beta-CROWN/complete_verifier/abcrown.py", line 69, in incomplete_verifier
domain, x, data_lb, data_ub, vnnlib, stop_criterion_func=stop_criterion_min(arguments.Config["bab"]["decision_thresh"]))
File "/kaggle/working/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 1069, in build_the_model
(self.x,), share_slopes=share_slopes, c=self.c, bound_upper=False)
File "/kaggle/working/alpha-beta-CROWN/auto_LiRPA/optimized_bounds.py", line 1050, in init_slope
final_node_name=final_node_name)
File "/kaggle/working/alpha-beta-CROWN/auto_LiRPA/backward_bound.py", line 760, in get_alpha_crown_start_nodes
assert not sparse_intermediate_bounds or use_sparse_conv is False # Double check our assumption holds. If this fails, then we created wrong shapes for alpha.
AssertionError
To solve this issue, I tried to change full_conv_alpha, conv_mode, or share_alpha parameters but I got another error with those:
/kaggle/working
/opt/conda/lib/python3.7/site-packages/onnx/mapping.py:27: DeprecationWarning: `np.object` is a deprecated alias for the builtin `object`. To silence this warning, use `object` by itself. Doing this will not modify any behavior and is safe.
Deprecated in NumPy 1.20; for more details and guidance: https://numpy.org/devdocs/release/1.20.0-notes.html#deprecations
int(TensorProto.STRING): np.dtype(np.object)
Configurations:
general:
device: cuda
seed: 100
conv_mode: matrix
deterministic: false
double_fp: false
loss_reduction_func: sum
record_bounds: false
sparse_alpha: false
save_adv_example: false
precompile_jit: false
complete_verifier: bab
enable_incomplete_verification: true
csv_name: null
results_file: out.txt
root_path: ''
model:
name: 'Customized("custom_model_data", "get_model")'
path: /kaggle/working/model_torch.pt
onnx_path: null
onnx_path_prefix: ''
cache_onnx_conversion: false
onnx_quirks: null
input_shape: null
onnx_loader: default_onnx_and_vnnlib_loader
onnx_optimization_flags: none
data:
start: 0
end: 10
select_instance: null
num_outputs: 43
mean: 0.0
std: 1.0
pkl_path: null
dataset: 'Customized("custom_model_data", "tsr_data")'
data_filter_path: null
data_idx_file: null
specification:
type: lp
robustness_type: verified-acc
norm: .inf
epsilon: 0.00784313725
vnnlib_path: null
vnnlib_path_prefix: ''
solver:
batch_size: 256
min_batch_size_ratio: 0.1
use_float64_in_last_iteration: false
early_stop_patience: 10
start_save_best: 0.5
bound_prop_method: alpha-crown
prune_after_crown: false
crown:
batch_size: 1000000000
max_crown_size: 1000000000
alpha-crown:
alpha: true
lr_alpha: 0.1
iteration: 100
share_slopes: false
no_joint_opt: false
lr_decay: 0.98
full_conv_alpha: false
beta-crown:
lr_alpha: 0.01
lr_beta: 0.05
lr_decay: 0.98
optimizer: adam
iteration: 20
beta: true
beta_warmup: true
enable_opt_interm_bounds: false
all_node_split_LP: false
forward:
refine: false
dynamic: false
max_dim: 10000
multi_class:
multi_class_method: allclass_domain
label_batch_size: 32
skip_with_refined_bound: true
mip:
parallel_solvers: null
solver_threads: 1
refine_neuron_timeout: 15
refine_neuron_time_percentage: 0.8
early_stop: true
adv_warmup: true
mip_solver: gurobi
bab:
initial_max_domains: 1
max_domains: .inf
decision_thresh: 0
timeout: 300
timeout_scale: 1
override_timeout: null
get_upper_bound: false
dfs_percent: 0.0
pruning_in_iteration: true
pruning_in_iteration_ratio: 0.2
sort_targets: false
batched_domain_list: true
optimized_intermediate_layers: ''
interm_transfer: true
cut:
enabled: false
bab_cut: false
lp_cut: false
method: null
lr: 0.01
lr_decay: 1.0
iteration: 100
bab_iteration: -1
early_stop_patience: -1
lr_beta: 0.02
number_cuts: 50
topk_cuts_in_filter: 100
batch_size_primal: 100
max_num: 1000000000
patches_cut: false
cplex_cuts: false
cplex_cuts_wait: 0
cplex_cuts_revpickup: true
cut_reference_bounds: true
fix_intermediate_bounds: false
branching:
method: kfsb
candidates: 3
reduceop: min
sb_coeff_thresh: 0.001
input_split:
enable: false
enhanced_bound_prop_method: alpha-crown
enhanced_branching_method: naive
enhanced_bound_patience: 100000000.0
attack_patience: 100000000.0
adv_check: 0
sort_domain_interval: -1
attack:
enabled: false
beam_candidates: 8
beam_depth: 7
max_dive_fix_ratio: 0.8
min_local_free_ratio: 0.2
mip_start_iteration: 5
mip_timeout: 30.0
adv_pool_threshold: null
refined_mip_attacker: false
refined_batch_size: null
attack:
pgd_order: before
pgd_steps: 100
pgd_restarts: 100
pgd_early_stop: true
pgd_lr_decay: 0.99
pgd_alpha: auto
pgd_loss_mode: null
enable_mip_attack: false
cex_path: ./test_cex.txt
attack_mode: PGD
gama_lambda: 10.0
gama_decay: 0.9
check_clean: false
input_split:
pgd_steps: 100
pgd_restarts: 30
pgd_alpha: auto
input_split_enhanced:
pgd_steps: 200
pgd_restarts: 5000000
pgd_alpha: auto
input_split_check_adv:
pgd_steps: 5
pgd_restarts: 5
pgd_alpha: auto
debug:
lp_test: null
Experiments at Mon May 1 17:49:40 2023 on d2707ae0421e
CNN(
(conv1): Conv2d(1, 32, kernel_size=(5, 5), stride=(1, 1), padding=(2, 2))
(conv2): Conv2d(32, 64, kernel_size=(5, 5), stride=(1, 1), padding=(2, 2))
(conv3): Conv2d(64, 128, kernel_size=(5, 5), stride=(1, 1), padding=(2, 2))
(fc4): Linear(in_features=3584, out_features=1024, bias=True)
(out): Linear(in_features=1024, out_features=43, bias=True)
)
/kaggle/working/alpha-beta-CROWN/complete_verifier/custom_model_data.py:211: UserWarning: To copy construct from a tensor, it is recommended to use sourceTensor.clone().detach() or sourceTensor.clone().detach().requires_grad_(True), rather than torch.tensor(sourceTensor).
return torch.tensor(X).permute((0,3,1,2)), torch.argmax(torch.tensor(labels), dim=-1), data_max, data_min, ret_eps
Internal results will be saved to Verified_ret_[Customized_model]_start=0_end=10_iter=20_b=256_timeout=300_branching=kfsb-min-3_lra-init=0.1_lra=0.01_lrb=0.05_PGD=before_cplex_cuts=False_multiclass=allclass_domain.npy.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% idx: 0, vnnlib ID: 0 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Attack parameters: initialization=uniform, steps=100, restarts=100, alpha=0.007461458444595337, initialization=uniform, GAMA=False
Model output of first 5 examples:
tensor([[-26.63533783, -5.86781883, -4.54763603, -21.69909477, -20.81317139,
-0.61611140, -16.72828102, -13.13037777, -18.94099617, -26.45909882,
-4.61056852, -12.54259109, -0.75518376, -16.09009552, -2.99634385,
-11.60897160, -17.43187332, -9.52975750, -18.21758842, -29.91522217,
-33.70221329, -23.20652962, -18.36230087, -25.41592407, -33.91773987,
-21.16673660, -17.64099312, -39.80070496, -35.47123337, -31.05479431,
-22.17935181, -18.36315536, -43.14264679, -13.38010883, 12.96510029,
-20.21791458, -4.28863621, -6.38604784, 41.21236038, -6.59563351,
4.28117037, -27.70765305, -9.50008297]], device='cuda:0')
Adv example prediction (first 2 examples and 2 restarts):
tensor([[[-26.52582550, -3.93510056, -6.41698170, -20.35298538, -20.99528694,
-6.70625925, -16.09720039, -15.72246552, -17.80824852, -23.99833107,
-11.98600864, -10.19097519, 2.43953228, -9.03533268, -2.28550172,
-9.02405930, -19.05975914, -7.56664610, -19.64624596, -25.21205711,
-34.47130585, -25.68278313, -19.72745895, -25.75965881, -34.31901932,
-21.08712769, -16.40643311, -36.51839066, -30.18853760, -27.88558769,
-23.38009453, -19.63435936, -35.52644348, -10.87827301, 20.88450241,
-9.49922180, -2.24221802, 1.64629138, 29.64516830, -7.80061817,
5.89254475, -24.37758255, -11.45957851],
[-26.52582741, -3.93510199, -6.41698503, -20.35298538, -20.99528885,
-6.70626211, -16.09720039, -15.72246647, -17.80824661, -23.99833107,
-11.98601246, -10.19097233, 2.43953443, -9.03533077, -2.28550124,
-9.02405930, -19.05976105, -7.56664419, -19.64624596, -25.21205330,
-34.47130585, -25.68278503, -19.72745895, -25.75965881, -34.31901550,
-21.08712578, -16.40643501, -36.51838684, -30.18853188, -27.88558388,
-23.38009453, -19.63436317, -35.52643967, -10.87827301, 20.88450432,
-9.49921989, -2.24221563, 1.64629233, 29.64516640, -7.80062008,
5.89254475, -24.37757874, -11.45957756]]], device='cuda:0')
PGD attack margin (first 2 examles and 10 specs):
tensor([[[56.17099380, 33.58026886, 36.06214905, 49.99815369, 50.64045715,
36.35142899, 45.74237061, 45.36763382, 47.45341492, 53.64349747]]],
device='cuda:0')
number of violation: 0
Attack finished in 13.5393 seconds.
PGD attack failed
/kaggle/working/alpha-beta-CROWN/auto_LiRPA/parse_graph.py:147: FutureWarning: 'torch.onnx.symbolic_helper._set_opset_version' is deprecated in version 1.13 and will be removed in version 1.14. Please remove its usage and avoid setting internal variables directly.
_set_opset_version(12)
/kaggle/working/alpha-beta-CROWN/auto_LiRPA/parse_graph.py:45: FutureWarning: 'torch.onnx._patch_torch._node_getitem' is deprecated in version 1.13 and will be removed in version 1.14. Please Internally use '_node_get' in symbolic_helper instead..
attrs = {k: n[k] for k in n.attributeNames()}
Model prediction is: tensor([[-26.63533783, -5.86781883, -4.54763603, -21.69909477, -20.81317139,
-0.61611140, -16.72828102, -13.13037777, -18.94099617, -26.45909882,
-4.61056852, -12.54259109, -0.75518376, -16.09009552, -2.99634385,
-11.60897160, -17.43187332, -9.52975750, -18.21758842, -29.91522217,
-33.70221329, -23.20652962, -18.36230087, -25.41592407, -33.91773987,
-21.16673660, -17.64099312, -39.80070496, -35.47123337, -31.05479431,
-22.17935181, -18.36315536, -43.14264679, -13.38010883, 12.96510029,
-20.21791458, -4.28863621, -6.38604784, 41.21236038, -6.59563351,
4.28117037, -27.70765305, -9.50008297]], device='cuda:0')
/kaggle/working/alpha-beta-CROWN/auto_LiRPA/bound_general.py:946: UserWarning: Creating an identity matrix with size 8192x8192 for node BoundMaxPool(name="/input"). This may indicate poor performance for bound computation. If you see this message on a small network please submit a bug report.
ref_intermediate_lb, ref_intermediate_ub)
/kaggle/working/alpha-beta-CROWN/auto_LiRPA/bound_general.py:946: UserWarning: Creating an identity matrix with size 16384x16384 for node BoundConv(name="/x.3"). This may indicate poor performance for bound computation. If you see this message on a small network please submit a bug report.
ref_intermediate_lb, ref_intermediate_ub)
/kaggle/working/alpha-beta-CROWN/auto_LiRPA/bound_general.py:946: UserWarning: Creating an identity matrix with size 4096x4096 for node BoundMaxPool(name="/input.4"). This may indicate poor performance for bound computation. If you see this message on a small network please submit a bug report.
ref_intermediate_lb, ref_intermediate_ub)
/kaggle/working/alpha-beta-CROWN/auto_LiRPA/bound_general.py:946: UserWarning: Creating an identity matrix with size 8192x8192 for node BoundConv(name="/x.7"). This may indicate poor performance for bound computation. If you see this message on a small network please submit a bug report.
ref_intermediate_lb, ref_intermediate_ub)
layer /12 start_node /input using full alpha with unstable size None total_size 8192 output_shape torch.Size([32, 16, 16])
layer /12 start_node /x.3 using full alpha with unstable size None total_size 16384 output_shape torch.Size([64, 16, 16])
layer /12 start_node /input.4 using full alpha with unstable size None total_size 4096 output_shape torch.Size([64, 8, 8])
layer /12 start_node /x.7 using full alpha with unstable size None total_size 8192 output_shape torch.Size([128, 8, 8])
layer /12 start_node /x.11 using full alpha with unstable size 1024 total_size 1024 output_shape torch.Size([1024])
layer /12 start_node /28 using full alpha with unstable size None total_size 42 output_shape 42
Traceback (most recent call last):
File "/kaggle/working/alpha-beta-CROWN/complete_verifier/abcrown.py", line 647, in <module>
main()
File "/kaggle/working/alpha-beta-CROWN/complete_verifier/abcrown.py", line 535, in main
incomplete_verifier(model_ori, x, data_ub=data_max, data_lb=data_min, vnnlib=vnnlib)
File "/kaggle/working/alpha-beta-CROWN/complete_verifier/abcrown.py", line 69, in incomplete_verifier
domain, x, data_lb, data_ub, vnnlib, stop_criterion_func=stop_criterion_min(arguments.Config["bab"]["decision_thresh"]))
File "/kaggle/working/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 1069, in build_the_model
(self.x,), share_slopes=share_slopes, c=self.c, bound_upper=False)
File "/kaggle/working/alpha-beta-CROWN/auto_LiRPA/optimized_bounds.py", line 1054, in init_slope
node.init_opt_parameters(start_nodes)
File "/kaggle/working/alpha-beta-CROWN/auto_LiRPA/operators/pooling.py", line 54, in init_opt_parameters
dtype=torch.float, device=ref.device, requires_grad=True)
TypeError: empty(): argument 'size' must be tuple of SymInts, but found element of type torch.Size at pos 2
I could not solve the problem and I guess the second one is not the way to go. I am in need of your help.
Sorry for the long text. Thanks in advance
I trained several adv trained models based on the origin github repo of Madry and Trades, even with the defination in alpha-beta-CROWN/complete_verifier/model_defs.py
.
When I use robustness_verifier.py
to validate these models, an same error raised for all of them.
The error caused by the code assert type(last_lA) == torch.Tensor or type(last_uA) == torch.Tensor
in auto_LiRPA/operators/convolution.py
-> class BoundMaxPool
-> function bound_backward
.
When I check the type of last_lA
, I found it is patches not tensor, so cannot pass the assert check.
I then checked the demos in exp_configs
, I want to use a model and config provided by you to reproduce the error but I found unfortunately that it seems no model contains the MaxPool layer. If you need me to provide a model for reproducing this problem, I will be happy to do so.
Hi there,
I tried to verify a customized model using alpha-beta-crown, but I got an error I could not figure out how to fix. I'd appreciate it if you could have a look at it.
yaml file:
general:
enable_incomplete_verification: False
loss_reduction_func: max
conv_mode: matrix
model:
name: cmars
input_shape: 19
specification:
vnnlib_path: cmars/vnnlib/large_1/N8/h32/basic.vnnlib
attack:
pgd_order: skip
solver:
batch_size: 500000
bound_prop_method: forward+backward
beta-crown:
iteration: 10
bab:
initial_max_domains: 100
branching:
method: naive # Split on input space.
input_split:
enable: True
adv_check: .inf
The model is defined in model_defs.py:
def cmars() -> nn.Sequential:
return nn.Sequential(
nn.Linear(19, 32),
nn.ReLU(),
nn.Linear(32, 32),
nn.ReLU(),
nn.Linear(32, 140),
nn.ReLU(),
nn.Linear(140, 1),
)
basic.vnnlib
(declare-const X_0 Real)
(declare-const X_1 Real)
(declare-const X_2 Real)
(declare-const X_3 Real)
(declare-const X_4 Real)
(declare-const X_5 Real)
(declare-const X_6 Real)
(declare-const X_7 Real)
(declare-const X_8 Real)
(declare-const X_9 Real)
(declare-const X_10 Real)
(declare-const X_11 Real)
(declare-const X_12 Real)
(declare-const X_13 Real)
(declare-const X_14 Real)
(declare-const X_15 Real)
(declare-const X_16 Real)
(declare-const X_17 Real)
(declare-const X_18 Real)
(declare-const Y_0 Real)
(assert (or
(and (<= X_0 0.11281310021877289) (>= X_0 0.08347102999687195) (<= X_1 -0.04856841638684273) (>= X_1 -0.07791049033403397) (<= X_2 -0.004555195104330778) (>= X_2 -0.033897269517183304) (<= X_3 0.06879998743534088) (>= X_3 0.03945791721343994) (<= X_4 0.1568262130022049) (>= X_4 0.12748414278030396) (<= X_5 0.2448524385690689) (>= X_5 0.21551036834716797) (<= X_6 0.2595234811306) (>= X_6 0.23018139600753784) (<= X_7 0.33287864923477173) (>= X_7 0.303536593914032) (<= X_8 0.42090487480163574) (>= X_8 0.391562819480896) (<= X_9 0.42090487480163574) (>= X_9 0.391562819480896) (<= X_10 0.391562819480896) (>= X_10 0.36222073435783386) (<= X_11 0.47958904504776) (>= X_11 0.4502469599246979) (<= X_12 0.6262993812561035) (>= X_12 0.5969573259353638) (<= X_13 0.6996545791625977) (>= X_13 0.6703125238418579) (<= X_14 0.7143256068229675) (>= X_14 0.6849835515022278) (<= X_15 0.6262993812561035) (>= X_15 0.5969573259353638) (<= X_16 0.5529442429542542) (>= X_16 0.5236021280288696) (<= X_17 0.4502469599246979) (>= X_17 0.42090487480163574) (<= X_18 0.4942600727081299) (>= X_18 0.46491798758506775) (>= Y_0 0))
))
The error:
Traceback (most recent call last):
File "abcrown.py", line 661, in <module>
main()
File "abcrown.py", line 584, in main
refined_betas=refined_betas, attack_images=all_adv_candidates, attack_margins=attack_margins)
File "abcrown.py", line 410, in complete_verifier
rhs=rhs, timeout=timeout, attack_images=this_spec_attack_images)
File "abcrown.py", line 200, in bab
rhs=rhs, timeout=timeout, branching_method=arguments.Config["bab"]["branching"]["method"])
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/batch_branch_and_bound_input_split.py", line 164, in input_bab_parallel
bounding_method=bounding_method,
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 1141, in build_the_model
x=(x,), C=self.c, method=bounding_method, cutter=self.cutter, bound_upper=False)
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1319, in compute_bounds
self.check_prior_bounds(final)
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 847, in check_prior_bounds
self.check_prior_bounds(n)
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 847, in check_prior_bounds
self.check_prior_bounds(n)
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 847, in check_prior_bounds
self.check_prior_bounds(n)
[Previous line repeated 6 more times]
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 855, in check_prior_bounds
node.inputs[i], prior_checked=True)
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 883, in compute_intermediate_bounds
node=node, concretize=True)
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/forward_bound.py", line 32, in forward_general
self.forward_general(node=l_pre, offset=offset)
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/forward_bound.py", line 40, in forward_general
linear = node.linear = node.bound_forward(self.dim_in, *inp)
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/linear.py", line 651, in bound_forward
y.upper.transpose(-1, -2) if y.upper is not None else None
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/linear.py", line 509, in bound_forward
lw, lb, uw, ub = BoundLinear.bound_forward_mul(x.lw, x_lb, x.uw, x_ub, w)
RuntimeError: The following operation failed in the TorchScript interpreter.
Traceback of TorchScript (most recent call last):
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/linear.py", line 457, in bound_forward_mul
def bound_forward_mul(x_lw: Tensor, x_lb: Tensor, x_uw: Tensor, x_ub: Tensor, w: Tensor):
w_pos, w_neg = w.clamp(min=0), w.clamp(max=0)
lw = x_lw.matmul(w_pos) + x_uw.matmul(w_neg)
~~~~~~~~~~~ <--- HERE
uw = x_uw.matmul(w_pos) + x_lw.matmul(w_neg)
lb = x_lb.matmul(w_pos) + x_ub.matmul(w_neg)
RuntimeError: mat1 and mat2 shapes cannot be multiplied (19x1 and 19x32)
Describe the bug
The adverse example is output in a binary file out.txt. Is there a way to read it?
Additional context
This is not really a bug, but a usability issue.
Hi, I am trying to simulate the conv1d operation using unsqueeze+conv2d (as conv1d is not already supported), but I get this error that I cannot fix. When I remove the convolutional layer, I do not get the error, so the error should have something to do with conv2d. I'd appreciate your help.
The error:
Model prediction is: tensor([0.17936328], device='cuda:0')
initial forward+backward bounds (first 10): tensor([-0.18187992], device='cuda:0')
Traceback (most recent call last):
File "abcrown.py", line 666, in <module>
main()
File "abcrown.py", line 589, in main
refined_betas=refined_betas, attack_images=all_adv_candidates, attack_margins=attack_margins)
File "abcrown.py", line 410, in complete_verifier
rhs=rhs, timeout=timeout, attack_images=this_spec_attack_images)
File "abcrown.py", line 200, in bab
rhs=rhs, timeout=timeout, branching_method=arguments.Config["bab"]["branching"]["method"])
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/batch_branch_and_bound_input_split.py", line 297, in input_bab_parallel
stop_func=stop_func,
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/batch_branch_and_bound_input_split.py", line 71, in batch_verification_input_split
stop_criterion_func=stop_func(thresholds),
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 1518, in get_lower_bound_naive
bound_upper=False, return_A=True, needed_A_dict=needed_A_dict)
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1328, in compute_bounds
unstable_idx=alpha_idx, update_mask=update_mask)
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/backward_bound.py", line 221, in backward_general
lb = lb.view(batch_size, *output_shape) if bound_lower else None
RuntimeError: shape '[8192, 1]' is invalid for input of size 67108864
The model:
class MyModel(nn.ModuleList):
def __init__(self, device=torch.device("cpu")):
super(MyModel, self).__init__()
self.to(device)
self.af = nn.ReLU()
self.lin1 = nn.Linear(19, 32)
self.lin2 = nn.Linear(32, 32)
self.lin3 = nn.Linear(32, 15)
self.conv2d = nn.Conv2d(
in_channels=1, out_channels=1, kernel_size=(1, 15)
)
def forward(self, obs):
lin1 = self.af(self.lin1(obs))
lin2 = self.af(self.lin2(lin1))
lin3 = self.lin3(lin2).unsqueeze(0).unsqueeze(0)
conved = self.conv2d(lin3)
return conved[0][0]
YAML file:
general:
enable_incomplete_verification: False
loss_reduction_func: max
conv_mode: matrix
model:
name: cmars
input_shape: [1, 19]
specification:
vnnlib_path: /home/mzi/sys-rl-verif/verif-slicing/cmars/vnnlib/large_1/N8/h32/basic-a1.vnnlib
attack:
pgd_order: skip
solver:
bound_prop_method: forward+backward
bab:
method: sb
input_split:
enable: True
adv_check: .inf
VNNLib property is as that in my previous question.
basic.vnnlib
(declare-const X_0 Real)
(declare-const X_1 Real)
(declare-const X_2 Real)
(declare-const X_3 Real)
(declare-const X_4 Real)
(declare-const X_5 Real)
(declare-const X_6 Real)
(declare-const X_7 Real)
(declare-const X_8 Real)
(declare-const X_9 Real)
(declare-const X_10 Real)
(declare-const X_11 Real)
(declare-const X_12 Real)
(declare-const X_13 Real)
(declare-const X_14 Real)
(declare-const X_15 Real)
(declare-const X_16 Real)
(declare-const X_17 Real)
(declare-const X_18 Real)
(declare-const Y_0 Real)
(assert (or
(and (<= X_0 0.11281310021877289) (>= X_0 0.08347102999687195) (<= X_1 -0.04856841638684273) (>= X_1 -0.07791049033403397) (<= X_2 -0.004555195104330778) (>= X_2 -0.033897269517183304) (<= X_3 0.06879998743534088) (>= X_3 0.03945791721343994) (<= X_4 0.1568262130022049) (>= X_4 0.12748414278030396) (<= X_5 0.2448524385690689) (>= X_5 0.21551036834716797) (<= X_6 0.2595234811306) (>= X_6 0.23018139600753784) (<= X_7 0.33287864923477173) (>= X_7 0.303536593914032) (<= X_8 0.42090487480163574) (>= X_8 0.391562819480896) (<= X_9 0.42090487480163574) (>= X_9 0.391562819480896) (<= X_10 0.391562819480896) (>= X_10 0.36222073435783386) (<= X_11 0.47958904504776) (>= X_11 0.4502469599246979) (<= X_12 0.6262993812561035) (>= X_12 0.5969573259353638) (<= X_13 0.6996545791625977) (>= X_13 0.6703125238418579) (<= X_14 0.7143256068229675) (>= X_14 0.6849835515022278) (<= X_15 0.6262993812561035) (>= X_15 0.5969573259353638) (<= X_16 0.5529442429542542) (>= X_16 0.5236021280288696) (<= X_17 0.4502469599246979) (>= X_17 0.42090487480163574) (<= X_18 0.4942600727081299) (>= X_18 0.46491798758506775) (>= Y_0 0))
))
When creating conda environment using environment.yml, I am getting the following error:
Collecting package metadata (repodata.json): done
Solving environment: |
Found conflicts! Looking for incompatible packages.
failed
UnsatisfiableError: The following specifications were found to be incompatible with each other:
Package icu conflicts for:
fontconfig==2.13.1=h6c09931_0 -> libxml2[version='>=2.9.10,<2.10.0a0'] -> icu[version='>=58.2,<59.0a0']
matplotlib==3.5.1=py37h06a4308_1 -> pyqt -> qt=5.9 -> icu[version='>=58.2,<59.0a0']
gst-plugins-base==1.14.0=h8213a91_2 -> gstreamer[version='>=1.14.0,<2.0a0'] -> gettext -> libxml2[version='>=2.9.10,<2.10.0a0'] -> icu[version='>=58.2,<59.0a0']
keras==2.4.3=hd3eb1b0_0 -> tensorflow -> tensorflow-base==2.5.0=mkl_py37h35b2a3d_0 -> icu[version='>=68.1,<69.0a0']
scikit-image==0.19.2=py37h51133e4_0 -> networkx[version='>=2.2'] -> matplotlib[version='>=3.3'] -> matplotlib-base[version='>=3.5.1,<3.5.2.0a0'] -> icu[version='>=58.2,<59.0a0']
icu==58.2=he6710b0_3
pyqt==5.9.2=py37h05f1152_2 -> qt=5.9 -> icu[version='>=58.2,<59.0a0']
qt==5.9.7=h5867ecd_1 -> icu[version='>=58.2,<59.0a0']
libxml2==2.9.14=h74e7548_0 -> icu[version='>=58.2,<59.0a0']
keras-base==2.4.3=pyhd3eb1b0_0 -> tensorflow[version='>=2.2'] -> tensorflow-base==2.5.0=mkl_py37h35b2a3d_0 -> icu[version='>=68.1,<69.0a0']
How to deal with it? Thank you!
Describe the bug
I tried to use MIP to check my properties, but I am experimenting some problems. I first tried MIP using the example provided in the documentation in the MIP section. I pulled the vnncomp2022_benchmarks repository, executed the Tiny MNIST fully connected networks configuration, and it worked successfully! However, when I adapted this previous configuration file to work with my properties, I get an assertion error. After debugging, I tried setting the sparse_alpha: false to bypass that assertion error, and it worked, but I got a Gurobi length miss-match error.
To Reproduce
I created a small zip file containing a minimum example to reproduce the bug. This zip file contains a yaml configuration, a vnnlib property, a model, error logs (with and without the sparse_alpha set to false), and the instructions for reproducing the problem. The zip file can be found at https://drive.google.com/file/d/1bUXpezrTdKAhfxj2im8oQcqM2JzV9v3I/view?usp=share_link
System configuration:
Hello, I notice that alpha-beta-crown is available for Sigmoid, Tanh activation functions. I use this code to verify model from ERAN. The CNN model with Sigmoid activation function has run smoothly, while for CNN model with Tanh activation function
Traceback (most recent call last):
File "abcrown.py", line 650, in <module>
main()
File "abcrown.py", line 538, in main
incomplete_verifier(model_ori, x, data_ub=data_max, data_lb=data_min, vnnlib=vnnlib)
File "abcrown.py", line 72, in incomplete_verifier
domain, x, data_lb, data_ub, vnnlib, stop_criterion_func=stop_criterion_min(arguments.Config["bab"]["decision_thresh"]))
File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 1122, in build_the_model
bound_upper=False, aux_reference_bounds=aux_reference_bounds, cutter=self.cutter)
File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1170, in compute_bounds
cutter=cutter, decision_thresh=decision_thresh)
File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/optimized_bounds.py", line 592, in get_optimized_bounds
update_mask=preserve_mask)
File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1321, in compute_bounds
self.check_prior_bounds(final)
File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 849, in check_prior_bounds
self.check_prior_bounds(n)
File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 857, in check_prior_bounds
node.inputs[i], prior_checked=True)
File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 959, in compute_intermediate_bounds
unstable_size=unstable_size)
File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/backward_bound.py", line 154, in backward_general
l.lA, l.uA, *l.inputs, start_shape=start_shape, start_node=node)
File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/activation.py", line 258, in bound_backward
lA, lbias = _bound_oneside(last_lA, sign=-1)
File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/activation.py", line 255, in _bound_oneside
A_prod, _bias = multiply_by_A_signs(last_A, w_pos, w_neg, b_pos, b_neg)
File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/clampmult.py", line 122, in multiply_by_A_signs
return ClampedMultiplication.apply(A, d_pos, d_neg, b_pos, b_neg, False)
File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/clampmult.py", line 101, in forward
return ClampedMultiplication.clamp_mutiply_forward(A, d_pos, d_neg, b_pos, b_neg, patches_mode)
RuntimeError: The following operation failed in the TorchScript interpreter.
Traceback of TorchScript (most recent call last):
File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/clampmult.py", line 42, in clamp_mutiply_forward
A_pos = A.clamp(min=0)
A_neg = A.clamp(max=0)
A_new = d_pos * A_pos + d_neg * A_neg
~~~~~~~~~~~~~ <--- HERE
bias_pos = bias_neg = torch.tensor(0.)
if b_pos is not None:
RuntimeError: The size of tensor a (1000) must match the size of tensor b (304) at non-singleton dimension 0
The command to run is:
python abcrown.py --onnx_path onnx/mnist/convMedGTANH__Point.onnx --dataset MNIST --epsilon 0.02 --device cpu --complete_verifier skip --no_full_conv_alpha --end 100
I have fixed the code like Sigmoid in backward_bound.py:
if (sparse_intermediate_bounds and isinstance(node, (BoundRelu, BoundSigmoid))
and nj.name != final_node_name and not share_slopes):
to
if (sparse_intermediate_bounds and isinstance(node, (BoundRelu, BoundSigmoid, BoundTanh))
and nj.name != final_node_name and not share_slopes):
How to deal with it? Thank you!
Dear alpha-beta-CROWN Team,
I hope this message finds you well. I've been working on running your latest version of Alpha-Beta-CROWN, but I've encountered a PackagesNotFoundError while executing the following command:
conda create -f complete_verifier/environment.yaml --name alpha-beta-crown
The following command will also show the same error:
conda create -f complete_verifier/environment_2022.yaml --name alpha-beta-crown
conda create -f complete_verifier/environment_pyt111.yaml --name alpha-beta-crown
conda create -f complete_verifier/environment_pyt200.yaml --name alpha-beta-crown
conda create -f complete_verifier/environment_pyt201.yaml --name alpha-beta-crown
The error message I received is as follows:
Collecting package metadata (current_repodata.json): done
Solving environment: failed with repodata from current_repodata.json, will retry with next repodata source.
Collecting package metadata (repodata.json): done
Solving environment: failed
PackagesNotFoundError: The following packages are not available from current channels:
- complete_verifier/environment.yaml
Current channels:
- https://repo.anaconda.com/pkgs/main/linux-64
- https://repo.anaconda.com/pkgs/main/noarch
- https://repo.anaconda.com/pkgs/r/linux-64
- https://repo.anaconda.com/pkgs/r/noarch
- https://conda.anaconda.org/conda-forge/linux-64
- https://conda.anaconda.org/conda-forge/noarch
To search for alternate channels that may provide the conda package you're
looking for, navigate to
https://anaconda.org
and use the search bar at the top of the page.
I would greatly appreciate your guidance and support to help me overcome this issue.
Thank you in advance for your help.
System configuration:
SiLU is a popular activation function. It is used in the YOLOv5 networks. Can you support it?
Hi, thanks for your great work in this field. I was trying to use the abcrown.py
file with a ResNet18 adversarially pretrained model (from the Fast Adversarial Training repo). But I'm seeing intermediate outputs like
Result: unknown in 121.7578 seconds
Is this concerning or should I let it run completely before checking the results? Because it is taking quite some time (reached 800 out of 1000 samples on CIFAR10 in ~20 hours). Also, I had to change the config file to use
crown:
batch_size: 8
max_crown_size: 8
because the default batch size and max crown size were 10^8 which caused an out-of-memory error even on a 24GB GPU. Does that seem reasonable or will there be a problem with the evaluation (like not being comparable to the reported results in your papers)?
Describe the bug
Calling the main script to display help by
python abcrown.py --help
fails with
ValueError: unsupported format character ')' (0x29) at index 17
To Reproduce
Just use above command on current main.
System configuration:
Fix
The error seems to come from the use of "%" in a help message: l.291 in arguments.py
self.add_argument('--mip_refine_timeout', type=float, default=0.8,
help='Percentage (x100%) of time used for improving all intermediate layer bounds using mip. Default to be 0.8*timeout.',
hierarchy=h + ["refine_neuron_time_percentage"])
Doubling % fixes the error (https://stackoverflow.com/questions/20480018/valueerror-unsupported-format-character)
I want to use ab-crown to verify neural networks with localrobustness property with the l-1 and l-2 norms. When I do this I get "Only Linf-norm attack is supported, the pgd_order will be changed to skip"
To Reproduce
Please provide us with the following to receive timely help:
python alpha-beta-CROWN/complete_verifier/abcrown.py --config "./config_ffnnRELU__Point_6_500.onnx_image_1.yaml"
Model files, especially when the bug is only triggered on specific models.
norm_bug.zip
*/miniconda3/envs/alpba-beta-crown/lib/python3.7/site-packages/onnx2pytorch/convert/layer.py:30: UserWarning: The given NumPy array is not writable, and PyTorch does not support non-writable tensors. This means writing to this tensor will result in undefined behavior. You may want to copy the array to protect its data or make it writable before converting it to a tensor. This type of warning will be suppressed for the rest of this program. (Triggered internally at /opt/conda/conda-bld/pytorch_1646755953518/work/torch/csrc/utils/tensor_numpy.cpp:178.)
layer.weight.data = torch.from_numpy(numpy_helper.to_array(weight))
*/miniconda3/envs/alpba-beta-crown/lib/python3.7/site-packages/onnx2pytorch/convert/model.py:154: UserWarning: Using experimental implementation that allows 'batch_size > 1'.Batchnorm layers could potentially produce false outputs.
"Using experimental implementation that allows 'batch_size > 1'."
*/miniconda3/envs/alpba-beta-crown/lib/python3.7/site-packages/onnx2pytorch/operations/reshape.py:36: TracerWarning: Converting a tensor to a Python boolean might cause the trace to be incorrect. We can't record the data flow of Python values, so this value will be treated as a constant in the future. This means that the trace might not generalize to other inputs!
if (shape[0] == 1 and (len(shape) == 4 or len(shape) == 2)
*/miniconda3/envs/alpba-beta-crown/lib/python3.7/site-packages/onnx2pytorch/operations/reshape.py:55: TracerWarning: Iterating over a tensor might cause the trace to be incorrect. Passing a tensor of different shape won't change the number of iterations executed (and might lead to errors or silently give incorrect results).
shape = [x if x != 0 else input.size(i) for i, x in enumerate(shape)]
Configurations:
general:
device: cuda
seed: 100
conv_mode: patches
deterministic: false
double_fp: false
loss_reduction_func: sum
record_bounds: false
sparse_alpha: true
save_adv_example: false
precompile_jit: false
complete_verifier: bab
enable_incomplete_verification: true
csv_name: null
results_file: out.txt
root_path: ''
model:
name: null
path: null
onnx_path: ./ffnnRELU__Point_6_500.onnx
onnx_path_prefix: ''
cache_onnx_conversion: false
onnx_quirks: null
input_shape: null
onnx_loader: default_onnx_and_vnnlib_loader
onnx_optimization_flags: none
data:
start: 0
end: 10000
select_instance: null
num_outputs: 10
mean: 0.0
std: 1.0
pkl_path: null
dataset: CIFAR
data_filter_path: null
data_idx_file: null
specification:
type: lp
robustness_type: verified-acc
norm: 2
epsilon: null
vnnlib_path: ./mnist_train_property_1_eps_0.127.vnnlib
vnnlib_path_prefix: ''
solver:
batch_size: 4096
min_batch_size_ratio: 0.1
use_float64_in_last_iteration: false
early_stop_patience: 10
start_save_best: 0.5
bound_prop_method: alpha-crown
prune_after_crown: false
crown:
batch_size: 1000000000
max_crown_size: 1000000000
alpha-crown:
alpha: true
lr_alpha: 0.1
iteration: 100
share_slopes: false
no_joint_opt: false
lr_decay: 0.98
full_conv_alpha: true
beta-crown:
lr_alpha: 0.01
lr_beta: 0.03
lr_decay: 0.98
optimizer: adam
iteration: 20
beta: true
beta_warmup: true
enable_opt_interm_bounds: false
all_node_split_LP: false
forward:
refine: false
dynamic: false
max_dim: 10000
multi_class:
multi_class_method: allclass_domain
label_batch_size: 32
skip_with_refined_bound: true
mip:
parallel_solvers: 8
solver_threads: 4
refine_neuron_timeout: 15
refine_neuron_time_percentage: 0.8
early_stop: true
adv_warmup: true
mip_solver: gurobi
bab:
initial_max_domains: 1
max_domains: .inf
decision_thresh: 0
timeout: 1200
timeout_scale: 1
override_timeout: null
get_upper_bound: false
dfs_percent: 0.0
pruning_in_iteration: true
pruning_in_iteration_ratio: 0.2
sort_targets: false
batched_domain_list: true
optimized_intermediate_layers: ''
interm_transfer: true
cut:
enabled: false
bab_cut: false
lp_cut: false
method: null
lr: 0.01
lr_decay: 1.0
iteration: 100
bab_iteration: -1
early_stop_patience: -1
lr_beta: 0.02
number_cuts: 50
topk_cuts_in_filter: 100
batch_size_primal: 100
max_num: 1000000000
patches_cut: false
cplex_cuts: false
cplex_cuts_wait: 0
cplex_cuts_revpickup: true
cut_reference_bounds: true
fix_intermediate_bounds: false
branching:
method: kfsb
candidates: 5
reduceop: max
sb_coeff_thresh: 0.001
input_split:
enable: false
enhanced_bound_prop_method: alpha-crown
enhanced_branching_method: naive
enhanced_bound_patience: 100000000.0
attack_patience: 100000000.0
adv_check: 0
sort_domain_interval: -1
attack:
enabled: false
beam_candidates: 8
beam_depth: 7
max_dive_fix_ratio: 0.8
min_local_free_ratio: 0.2
mip_start_iteration: 5
mip_timeout: 30.0
adv_pool_threshold: null
refined_mip_attacker: false
refined_batch_size: null
attack:
pgd_order: before
pgd_steps: 100
pgd_restarts: 30
pgd_early_stop: true
pgd_lr_decay: 0.99
pgd_alpha: auto
pgd_loss_mode: null
enable_mip_attack: false
cex_path: ./test_cex.txt
attack_mode: PGD
gama_lambda: 10.0
gama_decay: 0.9
check_clean: false
input_split:
pgd_steps: 100
pgd_restarts: 30
pgd_alpha: auto
input_split_enhanced:
pgd_steps: 200
pgd_restarts: 5000000
pgd_alpha: auto
input_split_check_adv:
pgd_steps: 5
pgd_restarts: 5
pgd_alpha: auto
debug:
lp_test: null
Experiments at Mon Aug 28 12:52:53 2023 on ethnode33
Only Linf-norm attack is supported, the pgd_order will be changed to skip
Internal results will be saved to out.txt.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% idx: 0, vnnlib ID: 0 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Using onnx ./ffnnRELU__Point_6_500.onnx
Using vnnlib ./mnist_train_property_1_eps_0.127.vnnlib
Precompiled vnnlib file found at ./mnist_train_property_1_eps_0.127.vnnlib.compiled
Loading onnx ./ffnnRELU__Point_6_500.onnx wih quirks {}
Model prediction is: tensor([[ 10.79480839, -32.92673492, -10.14999199, -17.28115654, -19.48822784,
-11.00737000, -5.19352055, -12.42144966, -11.82566643, -15.57086086]],
device='cuda:0')
Traceback (most recent call last):
File "alpha-beta-CROWN/complete_verifier/abcrown.py", line 647, in
main()
File "alpha-beta-CROWN/complete_verifier/abcrown.py", line 535, in main
incomplete_verifier(model_ori, x, data_ub=data_max, data_lb=data_min, vnnlib=vnnlib)
File "alpha-beta-CROWN/complete_verifier/abcrown.py", line 69, in incomplete_verifier
domain, x, data_lb, data_ub, vnnlib, stop_criterion_func=stop_criterion_min(arguments.Config["bab"]["decision_thresh"]))
File "./alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 1069, in build_the_model
(self.x,), share_slopes=share_slopes, c=self.c, bound_upper=False)
File "/home/bosmanaw/verona/VERONA/alpha-beta-CROWN/complete_verifier/auto_LiRPA/optimized_bounds.py", line 1023, in init_slope
intermediate_layer_bounds=intermediate_layer_bounds)
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1321, in compute_bounds
self.check_prior_bounds(final)
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 849, in check_prior_bounds
self.check_prior_bounds(n)
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 849, in check_prior_bounds
self.check_prior_bounds(n)
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 849, in check_prior_bounds
self.check_prior_bounds(n)
[Previous line repeated 8 more times]
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 857, in check_prior_bounds
node.inputs[i], prior_checked=True)
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 935, in compute_intermediate_bounds
node=node, delete_bounds_after_use=True)
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/interval_bound.py", line 31, in IBP_general
n, delete_bounds_after_use=delete_bounds_after_use)
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/interval_bound.py", line 31, in IBP_general
n, delete_bounds_after_use=delete_bounds_after_use)
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/interval_bound.py", line 31, in IBP_general
n, delete_bounds_after_use=delete_bounds_after_use)
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/interval_bound.py", line 42, in IBP_general
node.interval = node.interval_propagate(*inp)
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/convolution.py", line 283, in interval_propagate
deviation = torch.mul(weight, weight).sum((1, 2, 3)).sqrt() * eps
TypeError: unsupported operand type(s) for *: 'Tensor' and 'NoneType'
Without the above information, you might not be able to receive timely help from us.
System configuration:
OS:
Python version:
Pytorch Version:
Have you tried to reproduce the problem in a cleanly created conda/virtualenv environment using official installation instructions and the latest code on the main branch?: YES
Hi,
I wonder how do you handle vgg16 networks in your system.
And I noticed from prepare_instance.sh that you would call up dnnv to convert the maxpooling layer to relu.
So may I double-check that when your system verifies on vgg16, it verified on the converted network?
Thank you so much for your reply!
Best regards,
Yuyi
Hi,
I tried the following simple network to make sure I correctly understood alpha-beta-CROWN behavior.
Case 1:
(assert (or
(and (>= X_0 -1.0) (<= X_0 1.0) (>= X_1 0.5) (<= X_1 0.5) (<= Y_0 -0.6))
))
The true interval of y_0 is [-0.5, 0.5]. alpha-beta-CROWN returned safe.
Case 2:
(assert (or
(and (>= X_0 -1.0) (<= X_0 1.0) (>= X_1 0.5) (<= X_1 0.5) (>= Y_0 0.0))
))
The true interval of y_0 is [-0.5, 0.5]. alpha-beta-CROWN returned unknown.
The result of case 1 is as I expected, but I expected the result of case 2 to be unsafe as alpha-beta-crown is sound and complete. Please correct me if I am wrong but when two possible cases of the only Relu node are investigated and the corresponding bounds are calculated, I think we can give a definite response with regard to the violation or satisfaction of the defined property.
Here are the yaml config yaml.txt and the model model.txt in case you need them.
Hello,
I am having some incompatibility issues at the moment with the alpha-beta-CROWN tool running the experiments for the VNNCOMP21 competition.
I have created a conda environment with python 3.8 and I have installed the packages manually using the installation script provided. The command to install onnx2pytorch from Github did not work: git+git://github.com/Sarimuko/onnx2pytorch@8879f72c41ba960ff6495ae754d885eac2ebf656#egg=onnx2pytorch
So, I installed the pip package available for onnx2python (last version is 0.4.1). This package showed to have some incompatibilities with the pytorch version 1.8.2 (the last available at the pytorch-lts channel). Then I replaced this version by the pytorch version 1.11 for CUDA from the pytorch channel in Anaconda. Like this, the code worked but it still fails in some of the predefined benchmarks of the competition due to some of the torch modules that seem to be incompatible in some way with the code.
My questions are:
Is there a pip package version for onnx2pytorch that matches (or being similar) the one of git+git://github.com/Sarimuko/onnx2pytorch@8879f72c41ba960ff6495ae754d885eac2ebf656#egg=onnx2pytorch?
Do you know what is the latest version of pytorch compatible with the alpha-beta-CROWN code?
I have attached the images with the command introduced to run the code, the errors obtained and the pytorch, onnx, CUDA, onnx2pytorch versions installed.
Thank you in advance.
Hi,
I tried to run exp_configs/vnncomp22/vggnet16.yaml without any changes, but I got the following NotImplementedError.
I'd appreciate it if you could look into this.
Traceback (most recent call last):
File "abcrown.py", line 656, in <module>
main()
File "abcrown.py", line 579, in main
refined_betas=refined_betas, attack_images=all_adv_candidates, attack_margins=attack_margins)
File "abcrown.py", line 410, in complete_verifier
rhs=rhs, timeout=timeout, attack_images=this_spec_attack_images)
File "abcrown.py", line 200, in bab
rhs=rhs, timeout=timeout, branching_method=arguments.Config["bab"]["branching"]["method"])
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/batch_branch_and_bound_input_split.py", line 164, in input_bab_parallel
bounding_method=bounding_method,
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 1141, in build_the_model
x=(x,), C=self.c, method=bounding_method, cutter=self.cutter, bound_upper=False)
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1319, in compute_bounds
self.check_prior_bounds(final)
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 847, in check_prior_bounds
self.check_prior_bounds(n)
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 847, in check_prior_bounds
self.check_prior_bounds(n)
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 847, in check_prior_bounds
self.check_prior_bounds(n)
[Previous line repeated 29 more times]
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 855, in check_prior_bounds
node.inputs[i], prior_checked=True)
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 883, in compute_intermediate_bounds
node=node, concretize=True)
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/forward_bound.py", line 16, in forward_general
return self.forward_general_dynamic(C, node, concretize, offset)
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/forward_bound.py", line 156, in forward_general_dynamic
linear_inp = self.forward_general_dynamic(node=l_pre, offset=offset)
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/forward_bound.py", line 168, in forward_general_dynamic
*inp, max_dim=max_dim, offset=offset)
File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/base.py", line 228, in bound_dynamic_forward
raise NotImplementedError(f'bound_dynamic_forward is not implemented for {self}.')
NotImplementedError: bound_dynamic_forward is not implemented for BoundMaxPool(name="/input.8").
Hi, I was wondering if alpha-beta-CROWN already supports BaB verification of networks with heaviside activation functions.
Dear alpha-beta-CROWN Team,
I would like to extend my gratitude for your excellent work.
Your sample code works perfectly when we run it.
However, I'm writing to report an issue that I encountered
while attempting to run your sample code with a custom model using the following command:
python abcrown.py --config exp_configs/mnist_S.yaml
To provide some context, I added a custom model definition in model_defs.py, which looks as follows:
def conv_S():
model = nn.Sequential(
nn.Conv2d(1, 16, 4, stride=2, padding=1),
nn.ReLU(),
nn.MaxPool2d(2),
nn.Conv2d(16, 32, 4, stride=2, padding=1),
nn.ReLU(),
nn.MaxPool2d(2),
Flatten(),
nn.Linear(32, 24),
nn.ReLU(),
nn.Linear(24, 10)
)
return model
At this point, the code executes perfectly in idx 0 to 12 but has a result in idx 13,
it encounters the following issue:
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% idx: 13, vnnlib ID: 13 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Attack parameters: initialization=uniform, steps=100, restarts=100, alpha=0.025000005960464478, initialization=uniform, GAMA=False
Model output of first 5 examples:
tensor([[ 9.34262276, -7.84992790, 1.48994040, -5.32939434, -1.97707677,
0.06667299, 0.49797791, -3.03078222, 2.04741216, -0.75792819]],
device='cuda:0')
Adv example prediction (first 2 examples and 2 restarts):
tensor([[[ 6.48601294, -7.30414724, 0.62207073, -3.60429788, -2.02184796,
-0.06410425, -1.29587710, -2.43488121, 4.11566591, 1.92593360],
[ 6.48601294, -7.30414724, 0.62207073, -3.60429788, -2.02184796,
-0.06410425, -1.29587710, -2.43488121, 4.11566591, 1.92593360]]],
device='cuda:0')
PGD attack margin (first 2 examles and 10 specs):
tensor([[[13.79016018, 5.86394215, 10.09031105, 8.50786114, 6.55011702,
7.78188992, 8.92089462, 2.37034702, 4.56007957]]],
device='cuda:0')
number of violation: 0
Attack finished in 0.3795 seconds.
PGD attack failed
/home/user/anaconda3/envs/alpha-beta-crown/lib/python3.7/site-packages/torch/nn/functional.py:749: UserWarning: Note that order of the arguments: ceil_mode and return_indices will changeto match the args list in nn.MaxPool2d in a future release.
warnings.warn("Note that order of the arguments: ceil_mode and return_indices will change"
Model prediction is: tensor([[ 9.34262276, -7.84992790, 1.48994040, -5.32939434, -1.97707677,
0.06667299, 0.49797791, -3.03078222, 2.04741216, -0.75792819]],
device='cuda:0')
layer /10 using sparse-features alpha with shape [1178]; unstable size 1178; total size 3136 (torch.Size([1, 16, 14, 14]))
layer /10 start_node /input.8 using sparse-spec alpha with unstable size 166 total_size 288 output_shape (32, 3, 3)
layer /10 start_node /input.12 using sparse-spec alpha with unstable size 21 total_size 24 output_shape torch.Size([24])
layer /10 start_node /25 using full alpha with unstable size None total_size 9 output_shape 9
Traceback (most recent call last):
File "abcrown.py", line 647, in <module>
main()
File "abcrown.py", line 535, in main
incomplete_verifier(model_ori, x, data_ub=data_max, data_lb=data_min, vnnlib=vnnlib)
File "abcrown.py", line 69, in incomplete_verifier
domain, x, data_lb, data_ub, vnnlib, stop_criterion_func=stop_criterion_min(arguments.Config["bab"]["decision_thresh"]))
File "/home/user/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 1069, in build_the_model
(self.x,), share_slopes=share_slopes, c=self.c, bound_upper=False)
File "/home/user/alpha-beta-CROWN/complete_verifier/auto_LiRPA/optimized_bounds.py", line 1050, in init_slope
final_node_name=final_node_name)
File "/home/user/alpha-beta-CROWN/complete_verifier/auto_LiRPA/backward_bound.py", line 760, in get_alpha_crown_start_nodes
assert not sparse_intermediate_bounds or use_sparse_conv is False # Double check our assumption holds. If this fails, then we created wrong shapes for alpha.
AssertionError
It would be greatly appreciated if you could provide guidance or support to help me overcome this problem.
For your convenience, I have prepared our materials, including mnist_S.yaml, ConvS-custom.pth and model_defs.py, with
wget -O materials.rar https://www.dropbox.com/scl/fi/pnn7ob5focdhr6r3kr843/materials.rar?rlkey=9vp37h1gkxrhf8t2gf8fthqsg&dl=1
unrar x marerials.rar
Thank you in advance for your assistance.
System configuration:
error:
in "patches.py" line 380, in inplace_unfold
assert len(kernel_size) == 2 and len(padding) == 4 and len(stride) == 2
I just add my model in model_defs.py, but it will report the error above.
My model contains Conv2d, BatchNorm2d, ReLU, MaxPool2d and Dropout. Besides, my dataset's shape is (6000, 1, 1024, 2).
What are the possible reasons for such an error? Will the difference between the two dimensions of the dataset have an effect on the comparison?
Describe the bug
Running with any configuration file in exp_configs/bab_attack/
fails with error
To Reproduce
Please provide us with the following to receive timely help:
conda activate alpha-beta-crown
python abcrown.py --config exp_configs/bab_attack/cifar_cnn_a_adv.yaml
Just running the official reposity with the given configuration file is failing for bab attack.
Output:
/home/yusuf/miniconda3/envs/alpha-beta-crown/lib/python3.9/site-packages/pkg_resources/__init__.py:121: DeprecationWarning: pkg_resources is deprecated as an API
warnings.warn("pkg_resources is deprecated as an API", DeprecationWarning)
/home/yusuf/miniconda3/envs/alpha-beta-crown/lib/python3.9/site-packages/pkg_resources/__init__.py:2870: DeprecationWarning: Deprecated call to `pkg_resources.declare_namespace('google')`.
Implementing implicit namespace packages (as specified in PEP 420) is preferred to `pkg_resources.declare_namespace`. See https://setuptools.pypa.io/en/latest/references/keywords.html#keyword-namespace-packages
declare_namespace(pkg)
/home/yusuf/miniconda3/envs/alpha-beta-crown/lib/python3.9/site-packages/torchvision/io/image.py:13: UserWarning: Failed to load image Python extension: /home/yusuf/miniconda3/envs/alpha-beta-crown/lib/python3.9/site-packages/torchvision/image.so: undefined symbol: _ZNK3c1010TensorImpl36is_contiguous_nondefault_policy_implENS_12MemoryFormatE
warn(f"Failed to load image Python extension: {e}")
Configurations:
general:
device: cuda
seed: 100
conv_mode: patches
deterministic: false
double_fp: false
loss_reduction_func: sum
sparse_alpha: true
sparse_interm: true
save_adv_example: false
eval_adv_example: false
show_adv_example: false
precompile_jit: false
complete_verifier: bab
enable_incomplete_verification: true
csv_name: null
results_file: out.txt
root_path: ''
deterministic_opt: false
graph_optimizer: 'Customized("custom_graph_optimizer", "default_optimizer")'
no_batchdim_buffers: false
save_output: false
output_file: out.pkl
model:
name: cnn_4layer_adv
path: models/sdp/cifar_cnn_a_adv.model
onnx_path: null
onnx_path_prefix: ''
cache_onnx_conversion: false
debug_onnx: false
onnx_quirks: null
input_shape: null
onnx_loader: default_onnx_and_vnnlib_loader
onnx_optimization_flags: none
onnx_vnnlib_joint_optimization_flags: none
check_optmized: false
flatten_final_output: false
optimize_graph: null
data:
start: 537
end: 538
select_instance: null
num_outputs: 10
mean: [0.4914, 0.4824, 0.4467]
std: [0.2471, 0.2435, 0.2616]
pkl_path: null
dataset: CIFAR
data_filter_path: null
data_idx_file: null
specification:
type: lp
robustness_type: verified-acc
norm: .inf
epsilon: 0.00784313725
epsilon_min: 0.0
vnnlib_path: null
vnnlib_path_prefix: ''
rhs_offset: null
solver:
batch_size: 8192
auto_enlarge_batch_size: false
min_batch_size_ratio: 0.1
use_float64_in_last_iteration: false
early_stop_patience: 10
start_save_best: 0.5
bound_prop_method: alpha-crown
init_bound_prop_method: same
prune_after_crown: false
crown:
batch_size: 1000000000
max_crown_size: 1000000000
alpha-crown:
alpha: true
lr_alpha: 0.1
iteration: 100
share_alphas: false
lr_decay: 0.98
full_conv_alpha: true
max_coeff_mul: .inf
matmul_share_alphas: false
apply_output_constraints_to: []
disable_optimization: []
beta-crown:
lr_alpha: 0.01
lr_beta: 0.05
lr_decay: 0.999
optimizer: adam
iteration: 100
beta: true
beta_warmup: true
enable_opt_interm_bounds: false
all_node_split_LP: false
forward:
refine: false
dynamic: false
max_dim: 10000
multi_class:
label_batch_size: 32
skip_with_refined_bound: true
mip:
parallel_solvers: 8
solver_threads: 1
refine_neuron_timeout: 15
refine_neuron_time_percentage: 0.8
early_stop: true
adv_warmup: true
mip_solver: gurobi
skip_unsafe: false
bab:
initial_max_domains: 1
max_domains: 5000000
decision_thresh: 0
timeout: 1800
timeout_scale: 1
override_timeout: null
get_upper_bound: true
dfs_percent: 0.0
pruning_in_iteration: true
pruning_in_iteration_ratio: 0.2
sort_targets: false
batched_domain_list: true
optimized_interm: ''
interm_transfer: true
recompute_interm: false
sort_domain_interval: -1
vanilla_crown: false
cut:
enabled: false
implication: false
bab_cut: false
lp_cut: false
method: null
lr: 0.01
lr_decay: 1.0
iteration: 100
bab_iteration: -1
early_stop_patience: -1
lr_beta: 0.02
number_cuts: 50
topk_cuts_in_filter: 1000
batch_size_primal: 100
max_num: 1000000000
patches_cut: false
cplex_cuts: false
cplex_cuts_wait: 0
cplex_cuts_revpickup: true
cut_reference_bounds: true
fix_intermediate_bounds: false
branching:
method: kfsb
candidates: 3
reduceop: max
enable_intermediate_bound_opt: false
branching_input_and_activation: false
branching_input_and_activation_order: [input, relu]
branching_input_iterations: 30
branching_relu_iterations: 50
sb_coeff_thresh: 0.001
nonlinear_split:
method: shortcut
branching_point_method: uniform
num_branches: 2
branching_point_refinement: false
filter: false
filter_beta: false
filter_batch_size: 10000
filter_iterations: 25
shortlist_size: 500
loose_tanh_threshold: null
new_input_split:
enable: false
batch_size: 2
rounds: 1
init_alpha_batch_size: 8192
full_alpha: false
input_split:
enable: false
enhanced_bound_prop_method: alpha-crown
enhanced_branching_method: naive
enhanced_bound_patience: 100000000.0
attack_patience: 100000000.0
adv_check: 0
split_partitions: 2
sb_margin_weight: 1.0
sb_primary_spec: null
sb_primary_spec_iter: 1
sb_sum: false
bf_backup_thresh: -1
bf_rhs_offset: 0
bf_zero_crossing_score: false
ibp_enhancement: false
catch_assertion: false
compare_with_old_bounds: false
update_rhs_with_attack: false
attack:
enabled: true
beam_candidates: 128
beam_depth: 6
max_dive_fix_ratio: 0.5
min_local_free_ratio: 0.5
mip_start_iteration: 2
mip_timeout: 360
adv_pool_threshold: null
refined_mip_attacker: true
refined_batch_size: null
attack:
pgd_order: before
pgd_steps: 100
pgd_restarts: 100
pgd_batch_size: 100000000
pgd_early_stop: true
pgd_lr_decay: 0.99
pgd_alpha: auto
pgd_loss_mode: null
enable_mip_attack: false
adv_saver: default_adv_saver
early_stop_condition: default_early_stop_condition
adv_example_finalizer: default_adv_example_finalizer
pgd_loss: default_pgd_loss
cex_path: ./test_cex.txt
attack_mode: diverse_pgd
attack_tolerance: 0.0
attack_func: attack_with_general_specs
gama_lambda: 10.0
gama_decay: 0.9
check_clean: false
input_split:
pgd_steps: 100
pgd_restarts: 30
pgd_alpha: auto
input_split_enhanced:
pgd_steps: 200
pgd_restarts: 500000
pgd_alpha: auto
input_split_check_adv:
pgd_steps: 5
pgd_restarts: 5
pgd_alpha: auto
max_num_domains: 10
debug:
view_model: false
lp_test: null
rescale_vnnlib_ptb: null
test_optimized_bounds: false
test_optimized_bounds_after_n_iterations: 0
Experiments at Tue Feb 20 22:08:43 2024 on potato
Sequential(
(0): Conv2d(3, 16, kernel_size=(4, 4), stride=(2, 2), padding=(1, 1))
(1): ReLU()
(2): Conv2d(16, 32, kernel_size=(4, 4), stride=(2, 2), padding=(1, 1))
(3): ReLU()
(4): Flatten(start_dim=1, end_dim=-1)
(5): Linear(in_features=2048, out_features=100, bias=True)
(6): ReLU()
(7): Linear(in_features=100, out_features=10, bias=True)
)
Parameters:
0.weight: shape torch.Size([16, 3, 4, 4])
0.bias: shape torch.Size([16])
2.weight: shape torch.Size([32, 16, 4, 4])
2.bias: shape torch.Size([32])
5.weight: shape torch.Size([100, 2048])
5.bias: shape torch.Size([100])
7.weight: shape torch.Size([10, 100])
7.bias: shape torch.Size([10])
Trying generic MNIST/CIFAR data loader.
Files already downloaded and verified
Internal results will be saved to out.txt.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% idx: 0, vnnlib ID: 537 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Attack parameters: initialization=uniform, steps=100, restarts=100, alpha=0.008052505552768707, initialization=uniform, GAMA=False
Model output of first 5 examples:
tensor([[ -7.39000368, -13.28085136, -4.82924271, -7.23044920, -5.35508966,
-8.15784931, -6.39428473, -8.74342728, -11.18965244, -12.32971764]],
device='cuda:0')
100%|████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████| 1/1 [00:00<00:00, 2.07it/s]
Adv example prediction (first 2 examples and 2 restarts):
tensor([[[ -6.71217108, -12.28457832, -4.12656498, -6.24762297, -4.17495298,
-7.11022472, -5.33284330, -7.67359495, -10.33115959, -11.30035210],
[ -6.71217108, -12.28457832, -4.12656498, -6.24762297, -4.17495298,
-7.11022472, -5.33284330, -7.67359495, -10.33115959, -11.30035210]]],
device='cuda:0')
PGD attack margin (first 2 examles and 10 specs):
tensor([[[2.58560610, 8.15801334, 2.12105799, 0.04838800, 2.98365974,
1.20627832, 3.54702997, 6.20459461, 7.17378712]]], device='cuda:0')
number of violation: 0
Attack finished in 1.0545 seconds.
PGD attack failed
/home/yusuf/Desktop/abc_fresh/complete_verifier/auto_LiRPA/parse_graph.py:154: FutureWarning: 'torch.onnx.symbolic_helper._set_opset_version' is deprecated in version 1.13 and will be removed in version 1.14. Please remove its usage and avoid setting internal variables directly.
_set_opset_version(12)
Model: BoundedModule(
(/input.1): BoundInput(name=/input.1, inputs=[], perturbed=True)
(/1): BoundParams(name=/1, inputs=[], perturbed=False)
(/2): BoundParams(name=/2, inputs=[], perturbed=False)
(/3): BoundParams(name=/3, inputs=[], perturbed=False)
(/4): BoundParams(name=/4, inputs=[], perturbed=False)
(/5): BoundParams(name=/5, inputs=[], perturbed=False)
(/6): BoundParams(name=/6, inputs=[], perturbed=False)
(/7): BoundParams(name=/7, inputs=[], perturbed=False)
(/8): BoundParams(name=/8, inputs=[], perturbed=False)
(/input): BoundConv(name=/input, inputs=[/input.1, /1, /2], perturbed=True)
(/input.4): BoundRelu(name=/input.4, inputs=[/input], perturbed=True)
(/input.8): BoundConv(name=/input.8, inputs=[/input.4, /3, /4], perturbed=True)
(/12): BoundRelu(name=/12, inputs=[/input.8], perturbed=True)
(/13): BoundFlatten(name=/13, inputs=[/12], perturbed=True)
(/input.12): BoundLinear(name=/input.12, inputs=[/13, /5, /6], perturbed=True)
(/15): BoundRelu(name=/15, inputs=[/input.12], perturbed=True)
(/16): BoundLinear(name=/16, inputs=[/15, /7, /8], perturbed=True)
)
Original output: tensor([[ -7.39000368, -13.28085136, -4.82924271, -7.23044920, -5.35508966,
-8.15784931, -6.39428473, -8.74342632, -11.18965340, -12.32971668]],
device='cuda:0')
Split layers:
BoundConv(name=/input, inputs=[/input.1, /1, /2], perturbed=True): [(BoundRelu(name=/input.4, inputs=[/input], perturbed=True), 0)]
BoundConv(name=/input.8, inputs=[/input.4, /3, /4], perturbed=True): [(BoundRelu(name=/12, inputs=[/input.8], perturbed=True), 0)]
BoundLinear(name=/input.12, inputs=[/13, /5, /6], perturbed=True): [(BoundRelu(name=/15, inputs=[/input.12], perturbed=True), 0)]
Nonlinear functions:
BoundRelu(name=/input.4, inputs=[/input], perturbed=True)
BoundRelu(name=/12, inputs=[/input.8], perturbed=True)
BoundRelu(name=/15, inputs=[/input.12], perturbed=True)
layer /input.4 using sparse-features alpha with shape [686]; unstable size 686; total size 4096 ([1, 16, 16, 16])
layer /input.4 start_node /input.8 using sparse-spec alpha [2, 458, 1, 686] with unstable size 457 total_size 2048 output_shape (32, 8, 8)
layer /input.4 start_node /input.12 using sparse-spec alpha [2, 25, 1, 686] with unstable size 24 total_size 100 output_shape torch.Size([100])
layer /input.4 start_node /16 using full alpha [2, 9, 1, 686] with unstable size None total_size 9 output_shape 9
layer /12 using sparse-features alpha with shape [457]; unstable size 457; total size 2048 ([1, 32, 8, 8])
layer /12 start_node /input.12 using sparse-spec alpha [2, 25, 1, 457] with unstable size 24 total_size 100 output_shape torch.Size([100])
layer /12 start_node /16 using full alpha [2, 9, 1, 457] with unstable size None total_size 9 output_shape 9
layer /15 using sparse-features alpha with shape [24]; unstable size 24; total size 100 ([1, 100])
layer /15 start_node /16 using full alpha [2, 9, 1, 24] with unstable size None total_size 9 output_shape 9
Optimizable variables initialized.
initial CROWN bounds: tensor([[ 0.77253890, 5.35441875, 0.88030529, -0.71995872, 1.51813030,
-0.45570922, 1.82640553, 3.47526670, 4.63339520]], device='cuda:0') None
best_l after optimization: 18.567962646484375
alpha/beta optimization time: 2.470933437347412
initial alpha-crown bounds: tensor([[ 0.91563702, 5.49638367, 1.00899839, -0.58640003, 1.65252423,
-0.34389973, 2.01817369, 3.65779972, 4.74874640]], device='cuda:0')
Worst class: (+ rhs) -0.586400032043457
Total VNNLIB file length: 9, max property batch size: 1, total number of batches: 9
lA shape: [torch.Size([9, 1, 16, 16, 16]), torch.Size([9, 1, 32, 8, 8]), torch.Size([9, 1, 100])]
Properties batch 0, size 1
Remaining timeout: 1795.2805857658386
##### Instance 0 first 10 spec matrices:
tensor([[[ 0., 0., 1., 0., -1., 0., 0., 0., 0., 0.]]])
thresholds: tensor([0.], device='cuda:0') ######
Remaining spec index tensor([0], device='cuda:0') with bounds tensor([[-0.58640003]], device='cuda:0') need to verify.
Model prediction is: tensor([ -7.39000368, -13.28085136, -4.82924271, -7.23044920, -5.35508966,
-8.15784931, -6.39428473, -8.74342632, -11.18965340, -12.32971668],
device='cuda:0')
build_with_refined_bounds batch [1/1]
setting alpha for layer /input.4 start_node /16 with alignment adjustment
setting alpha for layer /12 start_node /16 with alignment adjustment
setting alpha for layer /15 start_node /16 with alignment adjustment
all alpha initialized
true A is required, we do a full backward CROWN pass to obtain it
(alpha-)CROWN with fixed intermediate bounds: tensor([[-0.58639872]], device='cuda:0') tensor([[1.64917374]], device='cuda:0')
Intermediate layers: /input,/input.8,/input.12,/16
Keeping alphas for these layers: ['/16']
Keeping alphas for these layers: ['/16']
Traceback (most recent call last):
File "/home/yusuf/Desktop/abc_fresh/complete_verifier/abcrown.py", line 612, in <module>
abcrown.main()
File "/home/yusuf/Desktop/abc_fresh/complete_verifier/abcrown.py", line 591, in main
verified_status = self.complete_verifier(
File "/home/yusuf/Desktop/abc_fresh/complete_verifier/abcrown.py", line 398, in complete_verifier
l, nodes, ret = self.bab(
File "/home/yusuf/Desktop/abc_fresh/complete_verifier/abcrown.py", line 241, in bab
result = general_bab(
File "/home/yusuf/Desktop/abc_fresh/complete_verifier/bab.py", line 302, in general_bab
domains = DomainClass(
File "/home/yusuf/Desktop/abc_fresh/complete_verifier/attack/domains.py", line 206, in __init__
candidate_domains = [to_cpu(ReLUDomain(
File "/home/yusuf/Desktop/abc_fresh/complete_verifier/attack/domains.py", line 206, in <listcomp>
candidate_domains = [to_cpu(ReLUDomain(
File "/home/yusuf/Desktop/abc_fresh/complete_verifier/attack/domains.py", line 94, in to_cpu
self.lA = [lA.to(device='cpu', non_blocking=True) for lA in self.lA]
File "/home/yusuf/Desktop/abc_fresh/complete_verifier/attack/domains.py", line 94, in <listcomp>
self.lA = [lA.to(device='cpu', non_blocking=True) for lA in self.lA]
AttributeError: 'str' object has no attribute 'to'
System configuration:
Describe the bug
When verifying an onnx network with latest version of ab-crown we get an ONNXRuntime error, that does not exist when running inference with the model.
This is regarding a squeeze layer.
We have tried using the recommended version of onnx and onnxruntime, as well as the most recent versions available.
To Reproduce
A minimum example is attached in "music_bugreport.zip
music_bugreport.zip
provided in zip
complete output in txt file in zip.
reproduce the problem by activating your environment and then running python alpha-beta-CROWN/complete_verifier/abcrown.py --config "vgg16.onnx/config_vgg16.onnx_image_instance0.npy.yaml"
Without the above information, you might not be able to receive timely help from us.
System configuration:
Screenshots
If applicable, add screenshots to help explain your problem.
Additional context
Add any other context about the problem here.
Dear,
I am very impressed when reading your papers regarding the theorems where you solve the constrained problems with efficient algorithms that run on GPU.
In the theorem proofs, I notice that the original constrained problem includes constraints x(i) = W(i)x(i-1)+b(i), which only captures fully-connected/convolutional/... layers's behavior.
But for an Add layer in residual networks in ONNX model, its function is like x(i) = x(i-1)+x(i-k). I fail to see how this theorem extends to residual networks, but I did observe residual networks in your experiments.
So I wonder if there is a theorem behind handling the residual networks? And is this theorem (if any) just a customization of your existing theorem?
Thank you in advance for your clarification!
Hi,
I tried to use your tool to analyze mnist_relu_6_100.onnx from ERAN system (https://files.sri.inf.ethz.ch/eran/nets/onnx/mnist/mnist_relu_6_100.onnx).
I used command python abcrown.py --config exp_configs/mnist_6_100.yaml
The yaml is as follows:
general:
complete_verifier: bab-refine
model:
name: mnist_6_100
path: models/eran/mnist_relu_6_100.onnx
data:
dataset: MNIST_ERAN_UN
std: [1.0]
mean: [0.0]
specification:
epsilon: 0.025
attack:
pgd_order: after
solver:
batch_size: 1024
beta-crown:
iteration: 20
mip:
parallel_solvers: 16
refine_neuron_time_percentage: 0.8
bab:
timeout: 1000
branching:
reduceop: max
It returned me:
Traceback (most recent call last):
File "abcrown.py", line 650, in <module>
main()
File "abcrown.py", line 553, in main
verified_status, init_global_lb, lower_bounds, upper_bounds, refined_betas = mip(saved_bounds=saved_bounds)
File "abcrown.py", line 145, in mip
score=score, stop_criterion_func=stop_criterion_min(1e-4))
File "/home/yuyi/alpha-beta-CROWN/complete_verifier/lp_mip_solver.py", line 1968, in build_the_model_mip_refine
raise NotImplementedError
NotImplementedError
Could you please advise me why would this happen?
Thanks and regards,
Yuyi
I am new to this tool. When I am running the example, I notice that the incomplete verifier will compute the upper bound and lower bound at each ReLU layer. At each ReLU layer, I see the ub and lb value, but at the last, the ub value will become infinity. Although I know this tool only focuses on the lower bound to verify whether the specification is satisfied or not, is it feasible to use this tool to compute the upper bound?
Hi,
I tried to run MNIST_ERAN dataset with network mnist_convSmallRELU__Point.
And I tried to increase the execution time with the hope that it would return more conclusive images.
I update the config as follows:
bab: timeout: 2000 branching: reduceop: max
But the program still terminates very quickly, with average execution time 3.06 seconds for each image.
I wonder why the verification process still terminates early with 2000 seconds timeout?
Thanks for your help!
Best regards,
Veronica
While I am aware that AB Crown only works with Ubuntu, I am wondering if a NVIDIA GPU is a requirement. I believe this may be possible to enable while using a VM, although my attempts have not been successful. Any guidance on that would be wonderful, but in the meantime I am wondering if there is any way to utilize the tool without the CUDA?
Here is my output when running the command: python abcrown.py --config exp_configs/mnist_6_100.yaml
I receive the same output on my VM which runs Kubuntu 23.04, which I attempted to install CUDA on.
/Users/lizsotomayor/miniconda3/envs/alpha-beta-crown/lib/python3.7/site-packages/onnx/mapping.py:27: DeprecationWarning: `np.object` is a deprecated alias for the builtin `object`. To silence this warning, use `object` by itself. Doing this will not modify any behavior and is safe.
Deprecated in NumPy 1.20; for more details and guidance: https://numpy.org/devdocs/release/1.20.0-notes.html#deprecations
int(TensorProto.STRING): np.dtype(np.object)
Configurations:
general:
device: cuda
seed: 100
conv_mode: patches
deterministic: false
double_fp: false
loss_reduction_func: sum
record_bounds: false
sparse_alpha: true
save_adv_example: false
precompile_jit: false
complete_verifier: bab-refine
enable_incomplete_verification: true
csv_name: null
results_file: out.txt
root_path: ''
model:
name: mnist_6_100
path: models/eran/mnist_6_100_nat.pth
onnx_path: null
onnx_path_prefix: ''
cache_onnx_conversion: false
onnx_quirks: null
input_shape: null
onnx_loader: default_onnx_and_vnnlib_loader
onnx_optimization_flags: none
data:
start: 0
end: 10000
select_instance: null
num_outputs: 10
mean: [0.0]
std: [1.0]
pkl_path: null
dataset: MNIST_ERAN_UN
data_filter_path: null
data_idx_file: null
specification:
type: lp
robustness_type: verified-acc
norm: .inf
epsilon: 0.026
vnnlib_path: null
vnnlib_path_prefix: ''
solver:
batch_size: 1024
min_batch_size_ratio: 0.1
use_float64_in_last_iteration: false
early_stop_patience: 10
start_save_best: 0.5
bound_prop_method: alpha-crown
prune_after_crown: false
crown:
batch_size: 1000000000
max_crown_size: 1000000000
alpha-crown:
alpha: true
lr_alpha: 0.1
iteration: 100
share_slopes: false
no_joint_opt: false
lr_decay: 0.98
full_conv_alpha: true
beta-crown:
lr_alpha: 0.01
lr_beta: 0.05
lr_decay: 0.98
optimizer: adam
iteration: 20
beta: true
beta_warmup: true
enable_opt_interm_bounds: false
all_node_split_LP: false
forward:
refine: false
dynamic: false
max_dim: 10000
multi_class:
multi_class_method: allclass_domain
label_batch_size: 32
skip_with_refined_bound: true
mip:
parallel_solvers: 16
solver_threads: 1
refine_neuron_timeout: 15
refine_neuron_time_percentage: 0.8
early_stop: true
adv_warmup: true
mip_solver: gurobi
bab:
initial_max_domains: 1
max_domains: .inf
decision_thresh: 0
timeout: 300
timeout_scale: 1
override_timeout: null
get_upper_bound: false
dfs_percent: 0.0
pruning_in_iteration: true
pruning_in_iteration_ratio: 0.2
sort_targets: false
batched_domain_list: true
optimized_intermediate_layers: ''
interm_transfer: true
cut:
enabled: false
bab_cut: false
lp_cut: false
method: null
lr: 0.01
lr_decay: 1.0
iteration: 100
bab_iteration: -1
early_stop_patience: -1
lr_beta: 0.02
number_cuts: 50
topk_cuts_in_filter: 100
batch_size_primal: 100
max_num: 1000000000
patches_cut: false
cplex_cuts: false
cplex_cuts_wait: 0
cplex_cuts_revpickup: true
cut_reference_bounds: true
fix_intermediate_bounds: false
branching:
method: kfsb
candidates: 3
reduceop: max
sb_coeff_thresh: 0.001
input_split:
enable: false
enhanced_bound_prop_method: alpha-crown
enhanced_branching_method: naive
enhanced_bound_patience: 100000000.0
attack_patience: 100000000.0
adv_check: 0
sort_domain_interval: -1
attack:
enabled: false
beam_candidates: 8
beam_depth: 7
max_dive_fix_ratio: 0.8
min_local_free_ratio: 0.2
mip_start_iteration: 5
mip_timeout: 30.0
adv_pool_threshold: null
refined_mip_attacker: false
refined_batch_size: null
attack:
pgd_order: after
pgd_steps: 100
pgd_restarts: 30
pgd_early_stop: true
pgd_lr_decay: 0.99
pgd_alpha: auto
pgd_loss_mode: null
enable_mip_attack: false
cex_path: ./test_cex.txt
attack_mode: PGD
gama_lambda: 10.0
gama_decay: 0.9
check_clean: false
input_split:
pgd_steps: 100
pgd_restarts: 30
pgd_alpha: auto
input_split_enhanced:
pgd_steps: 200
pgd_restarts: 5000000
pgd_alpha: auto
input_split_check_adv:
pgd_steps: 5
pgd_restarts: 5
pgd_alpha: auto
debug:
lp_test: null
Experiments at Wed Sep 20 01:30:43 2023 on Lizs-Air-3.lan
Sequential(
(0): Flatten()
(1): Linear(in_features=784, out_features=100, bias=True)
(2): ReLU()
(3): Linear(in_features=100, out_features=100, bias=True)
(4): ReLU()
(5): Linear(in_features=100, out_features=100, bias=True)
(6): ReLU()
(7): Linear(in_features=100, out_features=100, bias=True)
(8): ReLU()
(9): Linear(in_features=100, out_features=100, bias=True)
(10): ReLU()
(11): Linear(in_features=100, out_features=10, bias=True)
)
/Users/lizsotomayor/alpha-beta-CROWN-main/complete_verifier/utils.py:623: UserWarning: To copy construct from a tensor, it is recommended to use sourceTensor.clone().detach() or sourceTensor.clone().detach().requires_grad_(True), rather than torch.tensor(sourceTensor).
eps_temp = torch.tensor(eps_temp).reshape(1, -1, 1, 1)
############################
Sampled data loaded. No normalization used!
Shape: torch.Size([1000, 1, 28, 28]) torch.Size([1000]) torch.Size([1000])
X range: tensor(1.) tensor(0.) tensor(0.12226457)
Note runnerup label is empty here!
############################
Internal results will be saved to Verified_ret_[mnist_6_100]_start=0_end=10000_iter=20_b=1024_timeout=300_branching=kfsb-max-3_lra-init=0.1_lra=0.01_lrb=0.05_PGD=after_cplex_cuts=False_multiclass=allclass_domain.npy.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% idx: 0, vnnlib ID: 0 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Traceback (most recent call last):
File "abcrown.py", line 647, in <module>
main()
File "abcrown.py", line 512, in main
model_ori = model_ori.to(device)
File "/Users/lizsotomayor/miniconda3/envs/alpha-beta-crown/lib/python3.7/site-packages/torch/nn/modules/module.py", line 989, in to
return self._apply(convert)
File "/Users/lizsotomayor/miniconda3/envs/alpha-beta-crown/lib/python3.7/site-packages/torch/nn/modules/module.py", line 641, in _apply
module._apply(fn)
File "/Users/lizsotomayor/miniconda3/envs/alpha-beta-crown/lib/python3.7/site-packages/torch/nn/modules/module.py", line 664, in _apply
param_applied = fn(param)
File "/Users/lizsotomayor/miniconda3/envs/alpha-beta-crown/lib/python3.7/site-packages/torch/nn/modules/module.py", line 987, in convert
return t.to(device, dtype if t.is_floating_point() or t.is_complex() else None, non_blocking)
File "/Users/lizsotomayor/miniconda3/envs/alpha-beta-crown/lib/python3.7/site-packages/torch/cuda/__init__.py", line 221, in _lazy_init
raise AssertionError("Torch not compiled with CUDA enabled")
AssertionError: Torch not compiled with CUDA enabled
Hi, I was wondering if it's possible to define integer or binary values in CROWN
Thanks!
Import error at the end of alpha-beta-crown tutorial
A little bit more of basic information explaining the settings would be useful:
Also,
it seems that the setting "save_adv_example" is only saving the last counterexample found by the solver in the file "test_cex.txt". It would be more useful to have the option to save at least one counterexample for each unsafe input instance.
Describe the bug
When I use alpha-beta-crown for evaluation, an cuda error shows, here is the log
"
Traceback (most recent call last):
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/abcrown.py", line 612, in
abcrown.main()
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/abcrown.py", line 591, in main
verified_status = self.complete_verifier(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/abcrown.py", line 416, in complete_verifier
l, nodes, ret = self.bab(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/abcrown.py", line 235, in bab
result = input_bab_parallel(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/input_split/batch_branch_and_bound.py", line 182, in input_bab_parallel
global_lb, ret = net.build(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 455, in build
lb, ub, aux_reference_bounds = self.net.init_alpha(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/optimized_bounds.py", line 766, in init_alpha
l, u = self.compute_bounds(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1206, in compute_bounds
return self._compute_bounds_main(C=C,
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1303, in _compute_bounds_main
self.check_prior_bounds(final)
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
self.check_prior_bounds(n)
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
self.check_prior_bounds(n)
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
self.check_prior_bounds(n)
[Previous line repeated 1 more time]
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 804, in check_prior_bounds
self.compute_intermediate_bounds(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 910, in compute_intermediate_bounds
node.lower, node.upper = self.backward_general(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/backward_bound.py", line 256, in backward_general
A, lower_b, upper_b = l.bound_backward(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/nonlinear.py", line 512, in bound_backward
As, lbias, ubias = super().bound_backward(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/activation_base.py", line 248, in bound_backward
As, lbias, ubias = super().bound_backward(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/activation_base.py", line 66, in bound_backward
self.bound_relax(x, init=True)
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/nonlinear.py", line 231, in bound_relax
self.bound_relax_impl_sigmoid(lb, ub, self.act_func, self.d_act_func)
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/nonlinear.py", line 174, in bound_relax_impl_sigmoid
self.add_linear_relaxation(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/activation_base.py", line 46, in add_linear_relaxation
w_out[..., mask] = (k[..., mask].to(w_out) if isinstance(k, Tensor)
RuntimeError: CUDA error: device-side assert triggered
CUDA kernel errors might be asynchronously reported at some other API call,so the stacktrace below might be incorrect.
For debugging consider passing CUDA_LAUNCH_BLOCKING=1.
"
I have several onnx files for one model (the only difference of them is the weights and bias). But some onnx files meet this problem and some not.
To Reproduce
System configuration:
Thanks in advance for any ideas and suggestions.
Hi everyone,
We are currently trying to get a workflow involving neural network verification for networks that involve convolutional layers to run. Unfortunately, we are having little luck so far, because when skipping PGD-Attack, alpha-beta-crown always returns timeout. The result remained the same for "bab" and for "GCP-CROWN".
We defined a simple test case to allow the reproduction of our problem. Please can you tell us why we get "timeout" every time even for such a simple case? We Attached an example Jupyter notebook for learning and writing an ONNX-file, the resulting the ONNX file, the vnnlib-property file, theyaml-configuration file, and an image of the output we get.
The command we use to run alpha-beta-crown is as follow:
python abcrown.py --config personal_config/onnx_with_one_vnnlib.yaml --timeout 100
Hi,
I would like to kindly ask for help with the following two items:
dropout_rate = 0.2
number_of_neurons = 30
model = nn.Sequential(
nn.Linear(x_train.shape[1], number_of_neurons),
nn.ReLU(),
nn.BatchNorm1d(number_of_neurons),
nn.Dropout(dropout_rate),
nn.Linear(number_of_neurons, number_of_neurons),
nn.ReLU(),
nn.BatchNorm1d(number_of_neurons),
nn.Dropout(dropout_rate),
nn.Linear(number_of_neurons, y_train.shape[1])
).cuda()
Thank you in advance for your help!
Hello, I use your example file at 'exp_configs/cifar_conv_small_sigmoid.yaml' to run abcrown.py, then I got an assertion error:
File "/home/xue/alpha-beta-CROWN/complete_verifier/auto_LiRPA/backward_bound.py", line 760, in get_alpha_crown_start_nodes
assert not sparse_intermediate_bounds or use_sparse_conv is False # Double check our assumption holds. If this fails, then we created wrong shapes for alpha.
AssertionError
I wonder how to handle this?
Thank you.
Hi,
I could not find any Softmax function in the provided demos. I wanted to confirm with you whether Softmax is supported or not.
Thanks!
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.