search

Verified-Intelligence / alpha-beta-CROWN

alpha-beta-CROWN: An Efficient, Scalable and GPU Accelerated Neural Network Verifier (winner of VNN-COMP 2021, 2022, 2023, and 2024)
Other
236 stars 59 forks source link

it is possible to use beta-crown directly without the need for alpha-crown? #79

Open xiaoyuanpigo opened 2 days ago

xiaoyuanpigo commented 2 days ago

I have encountered some questions while working with beta-crown, and I would appreciate your assistance in clarifying them.

I would like to know if it is possible to use beta-crown directly without the need for alpha-crown. If this is possible, could you kindly explain why I am encountering an error when setting "alpha-crown: alpha: false" in the "configuration.yaml"?

The specific error message is as follows: BaB round 1 batch: 1 Traceback (most recent call last):   File "abcrown.py", line 658, in     abcrown.main()   File "abcrown.py", line 632, in main     verified_status = self.complete_verifier(   File "abcrown.py", line 424, in complete_verifier     l, nodes, ret = self.bab(   File "abcrown.py", line 244, in bab     result = general_bab(   File "/data/code/alpha-beta-CROWN/complete_verifier/bab.py", line 345, in general_bab     global_lb = act_split_round(   File "/data/code/alpha-beta-CROWN/complete_verifier/bab.py", line 170, in act_split_round     split_domain(net, domains, d, batch, impl_params=impl_params,   File "/data/code/alpha-beta-CROWN/complete_verifier/bab.py", line 75, in split_domain     branching_heuristic.get_branching_decisions(   File "/root/miniconda3/envs/py38/lib/python3.8/site-packages/torch/autograd/grad_mode.py", line 27, in decorate_context     return func(*args, **kwargs)   File "/data/code//alpha-beta-CROWN/complete_verifier/heuristics/kfsb.py", line 148, in get_branching_decisions     k_ret_lbs = self.net.update_bounds(   File "/data/code/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 309, in updatebounds     lb, , = self.net.compute_bounds(   File "/data/code/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1209, in compute_bounds     return self._compute_bounds_main(C=C,   File "/data/code/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1314, in _compute_bounds_main     ret = self.backward_general(   File "/data/code/alpha-beta-CROWN/complete_verifier/auto_LiRPA/backward_bound.py", line 256, in backward_general     A, lower_b, upper_b = l.bound_backward(   File "/data/code/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/relu.py", line 249, in bound_backward     self._backward_relaxation(last_lA, last_uA, x, start_node, unstable_idx)   File "/data/code/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/relu.py", line 555, in _backward_relaxation     selected_alpha, alpha_lookup_idx = self.select_alpha_by_idx(last_lA, last_uA,   File "/data/code/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/relu.py", line 207, in select_alpha_by_idx     selected_alpha = self.alpha[start_node.name] KeyError: '/50'

shizhouxing commented 2 days ago

That's probably not supported for now, but you may try setting the learning rate for alpha to 0 to effectively disable alpha optimization.

xiaoyuanpigo commented 1 day ago

Thanks!, May I ask why the certified accuracy under the setting: " general:   device: cpu   conv_mode: matrix   root_path: /data/code/   csv_name: mnist_4layer_5.csv   enable_incomplete_verification: False

attack:  pgd_restarts: 50 solver:  batch_size: 4096  beta-crown:    iteration: 20 bab:   timeout: 3600   branching:     method: fsb     reduceop: min     candidates: 1 "

is 64%, while for "

general:   device: cpu   conv_mode: matrix   root_path: ../../   csv_name: mnist_4layer_5.csv attack:  pgd_restarts: 50 solver:  batch_size: 1024  beta-crown:    iteration: 20 bab:  timeout: 180"

is 69%. It seem the front setting is beta-crown and is a complete verifier , while the latter seeting is alpha-beta-crown and is partially incomplete. However, the results for incomplete verifier is more precise than that for complete verifier. The results seem theoretically impossible. Did I make a mistake in the implementation?

shizhouxing commented 1 day ago

The later one is not an incomplete verifier as branch-and-bound is enabled by default. The former one is worse probably because some configs are changed (such as the fsb branching heuristic with 1 candidate, which is worse than the default kfsb)