I am new to this tool. When I am running the example, I notice that the incomplete ver

<a class="user-mention notranslate" data-hovercard-type="user" data-hovercard-url="/us

Can I compute the upper bound using incomplete verifier? about alpha-beta-crown HOT 13 OPEN

emiyacody commented on July 2, 2024

Can I compute the upper bound using incomplete verifier?

from alpha-beta-crown.

Comments (13)

shizhouxing commented on July 2, 2024

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

from alpha-beta-crown.

huanzhang12 commented on July 2, 2024

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.

from alpha-beta-crown.

emiyacody commented on July 2, 2024

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.

from alpha-beta-crown.

shizhouxing commented on July 2, 2024

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 <#53 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACUBARCS4BVNZYZZZHAXKS3YV6FE3AVCNFSM6AAAAABEARX75KVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSNZRHA3TIOBYHE>. You are receiving this because you commented.

from alpha-beta-crown.

emiyacody commented on July 2, 2024

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?

from alpha-beta-crown.

shizhouxing commented on July 2, 2024

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 <#53 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACUBARCNT4CTXATQPJ3DOFDYWTK3RAVCNFSM6AAAAABEARX75KVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSNZXGQYDGNRRG4>. You are receiving this because you commented.

from alpha-beta-crown.

emiyacody commented on July 2, 2024

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?

from alpha-beta-crown.

shizhouxing commented on July 2, 2024

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 <#53 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACUBARF6PS7FHZW34PXPDZTYW577HAVCNFSM6AAAAABEARX75KVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSOBRG44DAOJUG4>. You are receiving this because you commented.

from alpha-beta-crown.

emiyacody commented on July 2, 2024

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.

from alpha-beta-crown.

shizhouxing commented on July 2, 2024

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

from alpha-beta-crown.

emiyacody commented on July 2, 2024

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?

from alpha-beta-crown.

shizhouxing commented on July 2, 2024

@emiyacody Do you have a log for this issue?

from alpha-beta-crown.

emiyacody commented on July 2, 2024

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'

from alpha-beta-crown.

Can I compute the upper bound using incomplete verifier? about alpha-beta-crown HOT 13 OPEN

Comments (13)

Related Issues (20)

Recommend Projects

React

Vue.js

Typescript

TensorFlow

Django

Laravel

D3

Recommend Topics

javascript

web

server

Machine learning

Visualization

Game

Recommend Org

Facebook

Microsoft

Google

Alibaba

D3

Tencent