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
243 stars 60 forks source link

AttributeError: 'BoundReciprocal' object has no attribute 'build_solver' #69

Closed xiaoyuanpigo closed 3 months ago

xiaoyuanpigo commented 3 months ago

I want to use the mip solver to verify a CNN with a sub and a div layer. However, it returns an error as there is no built-solver attribute in BoundReciprocal. How can I fix this error?

The error is shown as below: Traceback (most recent call last): File "abcrown.py", line 653, in abcrown.main() File "abcrown.py", line 606, in main verified_status, ret_mip = mip( File "/data/code/alpha-beta-CROWN/complete_verifier/lp_mip_solver.py", line 76, in mip mip_global_lb, mip_global_ub, mip_status = model.build_the_model_mip( File "/data/code/alpha-beta-CROWN/complete_verifier/lp_mip_solver.py", line 1068, in build_the_model_mip build_solver_model(m, timeout, mip_multi_proc=mip_multi_proc, File "/data/code/alpha-beta-CROWN/complete_verifier/lp_mip_solver.py", line 638, in build_solver_model out_vars = m.net.build_solver_module( File "/data/code/alpha-beta-CROWN/complete_verifier/auto_LiRPA/solver_module.py", line 58, in build_solver_module self._build_solver_general(node=final, C=C, model_type=model_type, solver_pkg=solver_pkg) File "/data/code/alpha-beta-CROWN/complete_verifier/auto_LiRPA/solver_module.py", line 68, in _build_solver_general self._build_solver_general(n, C=C, model_type=model_type) File "/data/code/alpha-beta-CROWN/complete_verifier/auto_LiRPA/solver_module.py", line 68, in _build_solver_general self._build_solver_general(n, C=C, model_type=model_type) File "/data/code/alpha-beta-CROWN/complete_verifier/auto_LiRPA/solver_module.py", line 68, in _build_solver_general self._build_solver_general(n, C=C, model_type=model_type) [Previous line repeated 15 more times] File "/data/code/alpha-beta-CROWN/complete_verifier/auto_LiRPA/solver_module.py", line 79, in _build_solver_general solver_vars = node.build_solver(*inp, model=self.model, C=None, File "/root/miniconda3/envs/py38/lib/python3.8/site-packages/torch/nn/modules/module.py", line 1207, in getattr raise AttributeError("'{}' object has no attribute '{}'".format( AttributeError: 'BoundReciprocal' object has no attribute 'build_solver' Warning: environment still referenced so free is deferred (Continue to use WLS)

shizhouxing commented 3 months ago

Hi @xiaoyuanpigo, MIP is mainly for ReLU models and not supported for your model containing division. Please consider using the default branch-and-bound based solver instead.

A ViT example (which also contains BoundReciprocal): https://github.com/Verified-Intelligence/alpha-beta-CROWN/blob/main/complete_verifier/exp_configs/vnncomp23/vit.yaml

Relevant papers: https://arxiv.org/abs/2405.21063 https://arxiv.org/abs/2002.06622