Can I compute the upper bound using incomplete verifier?

[emiyacody]

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?

[shizhouxing]

@emiyacody You may add a negation to your specification, and the computed lower bound will be an upper bound of your original problem.

[huanzhang12]

There are different definitions of "upper bound", (1) the upper bound of x^*, where x^* is the global optimal solution for min_{x \in S} f(x); or (2) the upper bound of f(x) within {x \in S}. Which upper bound are you looking for?

For (1), adversarial attacks provide an upper bound. For (2), you can just negate the output of your computation, so lower bounds become upper bounds for your original function.

[emiyacody]

I am looking for the pair of upper bound and lower bound of the network output with the given input. I am not sure the upper bound I looking for belongs to which definitions you mentioned. Sorry for the confusing problem.

[shizhouxing]

This should be the case where you can negate the specification and the computed lower bound.

On Feb 29, 2024, at 12:08 PM, emiya cody @.***> wrote:

I am looking for the pair of upper bound and lower bound of the network output with the given input. I am not sure the upper bound I looking for belongs to which definitions you mentioned. Sorry for the confusing problem.

— Reply to this email directly, view it on GitHub https://github.com/Verified-Intelligence/alpha-beta-CROWN/issues/53#issuecomment-1971874889, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACUBARCS4BVNZYZZZHAXKS3YV6FE3AVCNFSM6AAAAABEARX75KVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSNZRHA3TIOBYHE. You are receiving this because you commented.

[emiyacody]

Thank you for the clarification. But I have one concern with negating the specification to compute the upper bound. As far as I know, the computation of the lower bound is approached from below, and the upper bound is approached from above. If I just negate the specification and compute the lower bound, is that the computation of the value approached to the bound still from below, which may not be the over-approximation upper bound of the output?

[shizhouxing]

Suppose f(x) is your original function, and lb is a lower bound computed for the negated problem -f(x):

Lb<=-f(x) => -Lb >= f(x)

So -lb is a sound upper bound for your original function.

On Mar 4, 2024, at 12:31 PM, emiya cody @.***> wrote:

Thank you for the clarification. But I have one concern with negating the specification to compute the upper bound. As far as I know, the computation of the lower bound is approached from below, and the upper bound is approached from above. If I just negate the specification and compute the lower bound, is that the computation of the value approached to the bound still from below, which may not be the over-approximation upper bound of the output?

— Reply to this email directly, view it on GitHub https://github.com/Verified-Intelligence/alpha-beta-CROWN/issues/53#issuecomment-1977403617, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACUBARCNT4CTXATQPJ3DOFDYWTK3RAVCNFSM6AAAAABEARX75KVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSNZXGQYDGNRRG4. You are receiving this because you commented.

[emiyacody]

Thank you for your explanation. I have one more question. You mentioned I can negate the specification to compute the upper bound. But I am kind of confused about the specifications you mentioned. In the cifar resnet example, what is the specification? Is it the difference between the ground true label value and other label values? And, just taking this example, if I want to compute the upper bound, how do I negate the specification?

[shizhouxing]

Yes, for CIFAR, the spec is about lower bounding f{true} - f{other}. To compute an upper bound, you negate the spec into f{other} - f{true} and compute a lower bound.

On Mar 6, 2024, at 1:02 PM, emiya cody @.***> wrote:

Thank you for your explanation. I have one more question. You mentioned I can negate the specification to compute the upper bound. But I am kind of confused about the specifications you mentioned. In the cifar resnet example, what is the specification? Is it the difference between the ground true label value and other label values? And, just taking this example, if I want to compute the upper bound, how do I negate the specification?

— Reply to this email directly, view it on GitHub https://github.com/Verified-Intelligence/alpha-beta-CROWN/issues/53#issuecomment-1981780947, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACUBARF6PS7FHZW34PXPDZTYW577HAVCNFSM6AAAAABEARX75KVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSOBRG44DAOJUG4. You are receiving this because you commented.

[emiyacody]

Is it possible to let the tool keep computing the lower bound even if the (lb-rhs) has been verified to be larger than 0? The tool only use bab method to compute the lower bound when the (lb-rhs) is lower than 0.

[shizhouxing]

@emiyacody For now you can set a very large rhs.

[emiyacody]

Hello, I encountered a question while computing the lower bounds. When there is no domain left, it gives 1e-7 as the lower bound. However, before this round, the lower bound is lb-rhs which would be a large number with a large rhs. In this case, I think the lower bound is incorrect. How should I solve this?

[shizhouxing]

@emiyacody Do you have a log for this issue?

[emiyacody]

That problem has been solved. It is my misunderstanding. However, I encountered another problem when I calculated the bounds. I test it with a small value, and the code can run smoothly and return an expected result. But if the initial CROWN bounds return a large value, the incomplete verifier will raise an exception.

Optimizable variables initialized.
initial CROWN bounds: tensor([[-6078.06298828, -5855.33007812, -4614.85791016, -5779.75878906,
         -4743.13378906, -6629.40625000, -6416.58056641, -5224.37695312,
         -5736.69726562, -3684.95434570]], device='cuda:0') None
Traceback (most recent call last):
  File "/home/cody/alpha-beta-CROWN/complete_verifier/abcrown_test_cifar.py", line 646, in <module>
    abcrown.main()
  File "/home/cody/alpha-beta-CROWN/complete_verifier/abcrown_test_cifar.py", line 586, in main
    verified_status, ret = self.incomplete_verifier(
  File "/home/cody/alpha-beta-CROWN/complete_verifier/abcrown_test_cifar.py", line 124, in incomplete_verifier
    global_lb, ret = model.build(
  File "/home/cody/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 500, in build
    ret = self.net.compute_bounds(
  File "/home/cody/anaconda3/envs/alpha-beta-crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 1193, in compute_bounds
    ret1 = self._get_optimized_bounds(bound_side='lower', **kwargs)
  File "/home/cody/anaconda3/envs/alpha-beta-crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/optimized_bounds.py", line 426, in _get_optimized_bounds
    ret = self.compute_bounds(
  File "/home/cody/anaconda3/envs/alpha-beta-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/cody/anaconda3/envs/alpha-beta-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/cody/anaconda3/envs/alpha-beta-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/cody/anaconda3/envs/alpha-beta-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/cody/anaconda3/envs/alpha-beta-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 14 more times]
  File "/home/cody/anaconda3/envs/alpha-beta-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/cody/anaconda3/envs/alpha-beta-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/cody/anaconda3/envs/alpha-beta-crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/backward_bound.py", line 256, in backward_general
    A, lower_b, upper_b = l.bound_backward(
  File "/home/cody/anaconda3/envs/alpha-beta-crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/operators/relu.py", line 303, in bound_backward
    ub_lower_d = maybe_unfold_patches(ub_lower_d, last_uA, alpha_lookup_idx=alpha_lookup_idx)
  File "/home/cody/anaconda3/envs/alpha-beta-crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/patches.py", line 510, in maybe_unfold_patches
    if last_A.size(0) == d_unfolded_r.size(0):
AttributeError: 'Patches' object has no attribute 'size'

[shizhouxing]

Hi @emiyacody, the issue can be fixed by changing last_A.size(0) into last_A.output_shape[1]. We will push this fix in our next release.